%
% ASYNCHRONOUS MID-VALUE SELECT;
%
% - three components sample a common input
% - the values sampled form the three components are read by two separate 
%   voters that use a mid-value select to produce one output.
% - we want to show that the two mid-value select outputs are within some
%   error bounds
%
% - the components are not synchronized.
%

mvs_with_timeouts1: CONTEXT = 

  BEGIN

  TIME: TYPE = REAL;
  
  %
  % Input = a triangular waveform
  %
  plant_period: TIME = 2;
  amplitude: REAL = 1;

  A: REAL = amplitude / (plant_period/2);

  waveform(t: REAL): REAL = 
    IF t < 0 OR t > plant_period THEN 0
    ELSIF t <= plant_period/2 THEN A * t
    ELSE amplitude - A * (t - plant_period/2)
    ENDIF;


  %
  % Source module: at time t, the output is x = waveform(t - k * period) 
  % where period * k <= t < period * (k + 1)
  %
  source: MODULE =
    BEGIN 
      INPUT time: TIME
      LOCAL period_counter: INTEGER
      OUTPUT x: REAL
    DEFINITION
      period_counter IN { n: INTEGER | n * plant_period <= time AND time < (n+1) * plant_period };
      x = waveform(time - period_counter * plant_period);
    END;

  
  %
  % Sampler module: period = fcm_period
  % - reads x at this period.
  %
  fcm_period: TIME = 0.2;

  fcm: MODULE =
    BEGIN
      INPUT
        time: TIME, 
        x: REAL
      OUTPUT 
        timeout: TIME,
        y, pre_y: REAL

      INITIALIZATION
        timeout IN { t: TIME | 0 <= t AND t < fcm_period };
        y = 0;
        pre_y = 0;

      TRANSITION
        [ time = timeout --> 
             timeout' = time + fcm_period;
             y' = x';
             pre_y' = y;
       [] 
          ELSE --> 
        ]
      END;


  %
  % Voter module: period = mvs_period
  % - input = y1, y2, y3 from three samplers
  %    + one validity flag bi for each input
  % - if bi is true then ypi is good
  %   otherwise, ypi is bad and not used in the vote
  %
  mvs_period: TIME = 0.05;

  midval(y1: REAL, y2: REAL, y3: REAL): REAL =
    IF y1 <= y2 THEN
       (IF y2 <= y3 THEN y2 ELSIF y1 <= y3 THEN y3 ELSE y1 ENDIF)
    ELSE
       (IF y1 <= y3 THEN y1 ELSIF y2 <= y3 THEN y3 ELSE y2 ENDIF)
    ENDIF;


  mvs: MODULE = 
    BEGIN
      INPUT
        y1, y2, y3: REAL,
        b1, b2, b3: BOOLEAN,
        time: TIME
      OUTPUT
        timeout: TIME,
        mvs: REAL

      INITIALIZATION
        timeout IN { t: TIME | 0 <= t AND t < mvs_period };
        mvs = 0;

      TRANSITION
        [ time = timeout -->
             timeout' = time + mvs_period;
             mvs' = midval( IF b1' THEN y1' ELSIF b2' AND NOT(b3') THEN y2' ELSIF b3' AND NOT(b2') THEN y3' ELSE mvs ENDIF,
                            IF b2' THEN y2' ELSIF b1' AND NOT(b3') THEN y1' ELSIF b3' AND NOT(b1') THEN y3' ELSE mvs ENDIF,
                            IF b3' THEN y3' ELSIF b1' AND NOT(b2') THEN y1' ELSIF b2' AND NOT(b1') THEN y2' ELSE mvs ENDIF);
       [] 
          ELSE -->
        ]
 
    END;


   %
   % Fault model
   %
   fault_injection : MODULE = 
     BEGIN

     OUTPUT 
	c1_b1,c1_b2,c1_b3 : BOOLEAN,
	c2_b1,c2_b2,c2_b3: BOOLEAN

     DEFINITION

	c1_b1 = true;
	c1_b2 = true;
	c1_b3 = true;
	
	c2_b1 = true;
%	c2_b2 IN { true, false};
%	c2_b3 IN { true, false};
        c2_b2 = true;
        c2_b3 = true;

     END;

   

observer : MODULE =
    
    	BEGIN
	      INPUT
	        fcm_timeout1, fcm_timeout2, fcm_timeout3: TIME,
	        mvs_timeout1, mvs_timeout2: TIME,
	        y1 ,pre_y1 : REAL,
	        y3 , pre_y3 : REAL,
		mvs2, mvs1 : REAL
		
    		OUTPUT z12 : REAL,
    		       z32 : REAL,
    		       z11 : REAL,
    		       z31 : REAL,
    		       lower_bound2 : REAL,
    		       upper_bound2 : REAL,
    		       lower_bound1 : REAL,
       		       upper_bound1 : REAL,
       		       bounded1 : BOOLEAN,
    		       bounded2 : BOOLEAN
   		       
   
   DEFINITION
    		
    		
  		
    		
    		
             z12 = IF fcm_timeout1 - fcm_period <= mvs_timeout2 - mvs_period THEN y1 ELSE pre_y1 ENDIF;
	     z32 = IF fcm_timeout3 - fcm_period <= mvs_timeout2 - mvs_period THEN y3 ELSE pre_y3 ENDIF;

	     z11 = IF fcm_timeout1 - fcm_period <= mvs_timeout1 - mvs_period THEN y1 ELSE pre_y1 ENDIF;
	     z31 = IF fcm_timeout3 - fcm_period <= mvs_timeout1 - mvs_period THEN y3 ELSE pre_y3 ENDIF;

    		upper_bound1 = max(z11,z31);
		lower_bound1 = min(z11,z31);
    		upper_bound2 = max(z12,z32) ;
		lower_bound2 = min(z12,z32);

    		bounded2= mvs2 >= lower_bound2 and mvs2 <= upper_bound2;
    		bounded1= mvs1 >= lower_bound1 and mvs1 <= upper_bound1;

    	

    	
    	
    END;
    


   %
   % Full system: 
   % - synchronous composition of these components
   %
   system: MODULE =
	(RENAME timeout TO fcm_timeout1, y TO y1, pre_y TO pre_y1 IN fcm)
     || (RENAME timeout TO fcm_timeout2, y TO y2, pre_y TO pre_y2 IN fcm)
     || (RENAME timeout TO fcm_timeout3, y TO y3, pre_y TO pre_y3 IN fcm)
     || fault_injection
     || (RENAME b1 TO c1_b1, b2 TO c1_b2, b3 TO c1_b3, timeout TO mvs_timeout1, mvs TO mvs1 IN mvs)
     || (RENAME b1 TO c2_b1, b2 TO c2_b2, b3 TO c2_b3, timeout TO mvs_timeout2, mvs TO mvs2 IN mvs)
     || observer;

  
   %
   % Clock module: advance time to min(fcm_timeout1, fcm_timeout2, fcm_timeout3, mvs_timeout1, mvs_timeout2)
   %
   clock: MODULE =
     BEGIN
      INPUT
        fcm_timeout1, fcm_timeout2, fcm_timeout3: TIME,
        mvs_timeout1, mvs_timeout2: TIME
      OUTPUT
        time: TIME
      INITIALIZATION
        time = 0;
      TRANSITION
       [ time < fcm_timeout1 AND time < fcm_timeout2 AND time < fcm_timeout3 AND time < mvs_timeout1 AND time < mvs_timeout2 -->
               time' IN { t: TIME | t <= fcm_timeout1 AND t <= fcm_timeout2 AND t <= fcm_timeout3
                                    AND t <= mvs_timeout1 AND t <= mvs_timeout2 
                                    AND (t = fcm_timeout1 OR t = fcm_timeout2 OR t = fcm_timeout3 OR t = mvs_timeout1 OR t = mvs_timeout2) }; 
       ]
      END;

   full: MODULE = system [] (clock || source);
    

   %
   % provable: by induction at depth 1 but not used anywhere
   % Still it helps visualize the counterexamples
   %
   time_positive: LEMMA full |- G(time >= 0);


   %
   % All these are also provable by induction at depth 1
   %
   fcm_timeout_bounds1: LEMMA full |- G(time <= fcm_timeout1 AND fcm_timeout1 <= time + fcm_period);

   fcm_timeout_bounds2: LEMMA full |- G(time <= fcm_timeout2 AND fcm_timeout2 <= time + fcm_period);

   fcm_timeout_bounds3: LEMMA full |- G(time <= fcm_timeout3 AND fcm_timeout3 <= time + fcm_period);

   mvs_timeout_bounds1: LEMMA full |- G(time <= mvs_timeout1 AND mvs_timeout1 <= time + mvs_period);

   mvs_timeout_bounds2: LEMMA full |- G(time <= mvs_timeout2 AND mvs_timeout2 <= time + mvs_period);


   %
   % Provable by induction at depth 1
   %
   sampling_error1: LEMMA
     full |- G(x - y1 <= A * (time - (fcm_timeout1 - fcm_period)) AND y1 - x <= A * (time - (fcm_timeout1 - fcm_period)));

   sampling_error2: LEMMA
     full |- G(x - y2 <= A * (time - (fcm_timeout2 - fcm_period)) AND y2 - x <= A * (time - (fcm_timeout2 - fcm_period)));

   sampling_error3: LEMMA
     full |- G(x - y3 <= A * (time - (fcm_timeout3 - fcm_period)) AND y3 - x <= A * (time - (fcm_timeout3 - fcm_period)));



   %
   % Bound on the difference between two successive samples
   % - provable by induction at depth 1, using sampling_error<i> as a lemma
   %
   pre_sampling_delta1: LEMMA 
     full |- G(y1 - pre_y1 <= A * fcm_period AND pre_y1 - y1 <= A * fcm_period);

   pre_sampling_delta2: LEMMA
     full |- G(y2 - pre_y2 <= A * fcm_period AND pre_y2 - y2 <= A * fcm_period);

   pre_sampling_delta3: LEMMA
     full |- G(y3 - pre_y3 <= A * fcm_period AND pre_y3 - y3 <= A * fcm_period);


   %
   % Bound on the difference betweeen two sampling channels
   % - to prove sampling_delta(i,j) use induction at depth 1, with sampling_error<i> and sampling_error<j> as lemmas
   %
   sampling_delta12: LEMMA
     full |- G(fcm_timeout1 >= fcm_timeout2 => y1 - y2 <= A * (fcm_timeout1 - fcm_timeout2) 
                                           AND y2 - y1 <= A * (fcm_timeout1 - fcm_timeout2));

   sampling_delta21: LEMMA
     full |- G(fcm_timeout2 >= fcm_timeout1 => y1 - y2 <= A * (fcm_timeout2 - fcm_timeout1) 
                                           AND y2 - y1 <= A * (fcm_timeout2 - fcm_timeout1));


   sampling_delta13: LEMMA
     full |- G(fcm_timeout1 >= fcm_timeout3 => y1 - y3 <= A * (fcm_timeout1 - fcm_timeout3) 
                                           AND y3 - y1 <= A * (fcm_timeout1 - fcm_timeout3));


   sampling_delta31: LEMMA
     full |- G(fcm_timeout3 >= fcm_timeout1 => y1 - y3 <= A * (fcm_timeout3 - fcm_timeout1) 
                                           AND y3 - y1 <= A * (fcm_timeout3 - fcm_timeout1));


   sampling_delta23: LEMMA
     full |- G(fcm_timeout2 >= fcm_timeout3 => y2 - y3 <= A * (fcm_timeout2 - fcm_timeout3) 
                                           AND y3 - y2 <= A * (fcm_timeout2 - fcm_timeout3));


   sampling_delta32: LEMMA
     full |- G(fcm_timeout3 >= fcm_timeout2 => y2 - y3 <= A * (fcm_timeout3 - fcm_timeout2) 
                                           AND y3 - y2 <= A * (fcm_timeout3 - fcm_timeout2));





   %
   % Equivalent definition of mvs
   % - provable by induction at depth 2 using the lemmas 
   %   fcm_timeout_bounds1, fcm_timeout_bounds2, fcm_timeout_bounds3 and mvs_timeout_bounds<i>
   %
   mvs_invar1: LEMMA full |- G(mvs1 = midval(IF fcm_timeout1 - fcm_period <= mvs_timeout1 - mvs_period THEN y1 ELSE pre_y1 ENDIF,
                                             IF fcm_timeout2 - fcm_period <= mvs_timeout1 - mvs_period THEN y2 ELSE pre_y2 ENDIF,
                                             IF fcm_timeout3 - fcm_period <= mvs_timeout1 - mvs_period THEN y3 ELSE pre_y3 ENDIF));
                                             

   mvs_invar2: LEMMA full |- G(mvs2 = midval(IF fcm_timeout1 - fcm_period <= mvs_timeout2 - mvs_period THEN y1 ELSE pre_y1 ENDIF,
                                             IF fcm_timeout2 - fcm_period <= mvs_timeout2 - mvs_period THEN y2 ELSE pre_y2 ENDIF,
                                             IF fcm_timeout3 - fcm_period <= mvs_timeout2 - mvs_period THEN y3 ELSE pre_y3 ENDIF));



   %
   % agreement can be proved by induction at depth 1
   %
   % lemmas: mvs_invar1 mvs_invar2
   %          sampling_delta12 sampling_delta13 sampling_delta23
   %          sampling_delta21 sampling_delta31 sampling_delta32
   %          pre_sampling_delta1 pre_sampling_delta2 pre_sampling_delta3 
   %

  %error: REAL = A * (fcm_period + mvs_period);
 error: REAL = A * fcm_period;
  
 % error: REAL = 0.9 * A * (fcm_period );

   t: LEMMA full |-G(time < plant_period);
   b1: LEMMA full |- G(bounded1);
   b2: LEMMA full |- G(bounded2);
      	

   
   
   agreement: THEOREM full |- G(mvs1 - mvs2 <= error AND mvs2 - mvs1 <= error);

  END