% Mid Value Select 
MVS: CONTEXT =
BEGIN

 faulty: BOOLEAN = FALSE ;
 reallyfaulty: BOOLEAN = FALSE ;
 dt: REAL = 0.2 ;
 % e: REAL = 0.1 ;
 e: REAL = 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;
 
 % The plant generates a continuous signal
 % But in our model, it will generate a set !
 plant: MODULE =
 BEGIN
  OUTPUT yub, ylb: REAL
  LOCAL inc: BOOLEAN
  INITIALIZATION
   yub = 0;
   ylb = 0;
   inc = TRUE ;
  TRANSITION
  [
   yub >= -0.8 AND  yub <= 0.8 AND inc -->
	yub' = yub + dt * 1 ;
	ylb' = yub + (dt - e) * 1;
   []
   yub >= -0.8 AND  yub <= 0.8 AND NOT(inc) -->
	yub' = yub + dt * (-1) ;
	ylb' = yub + (dt - e) * (-1);
   []
   ((yub <= -0.8 AND yub >= -1) OR yub >= 0.8) AND NOT(inc) -->
	yub' = yub + dt * (-0.1) ;
	ylb' = yub + (dt - e) * (-0.1);
 	inc' = IF yub' <= -1 THEN TRUE ELSE FALSE ENDIF ;
   []
   ((yub >= 0.8 AND yub <= 1) OR yub <= -0.8) AND inc -->
	yub' = yub + dt * (0.1) ;
	ylb' = yub + (dt - e) * (0.1) ;
 	inc' = IF yub' >= 1 THEN FALSE ELSE TRUE ENDIF ;
  ]
 END;

 % 3 inputs, 3 valid bits, output 1 value
 mvs: MODULE =
 BEGIN
  INPUT x1, x2, x3: REAL
  INPUT b1, b2, b3: BOOLEAN
  OUTPUT x: REAL
  INITIALIZATION x = 0
  TRANSITION
  [
   TRUE -->
    x' = midval( 
	IF b1' THEN x1' ELSE x ENDIF,
	IF b2' THEN x2' ELSE x ENDIF,
	IF b3' THEN x3' ELSE x ENDIF)
  ]
 END;

 asynchronousBus: MODULE =
 BEGIN
  INPUT ylb, yub: REAL
  OUTPUT x1, x2, x3: REAL
  OUTPUT b1, b2, b3: BOOLEAN
  INITIALIZATION 
   x1 IN {z: REAL | (ylb <= z AND z <= yub) OR (ylb >= z AND z >= yub) };
   x2 IN {z: REAL | (ylb <= z AND z <= yub) OR (ylb >= z AND z >= yub) };
   x3 IN {z: REAL | (ylb <= z AND z <= yub) OR (ylb >= z AND z >= yub) };
   b1 = TRUE; b2 = NOT(reallyfaulty); b3 = NOT(faulty)
  TRANSITION
  [
  TRUE --> % faulty or not choose x1,x2,x3 correctly
   	x1' IN {z:REAL| (ylb' <= z AND z <= yub') OR (ylb' >= z AND z >= yub')};
   	x2' IN {z:REAL| (ylb' <= z AND z <= yub') OR (ylb' >= z AND z >= yub')};
   	x3' IN {z:REAL| (ylb' <= z AND z <= yub') OR (ylb' >= z AND z >= yub')};
  ]
 END;

 system: MODULE = 
  asynchronousBus || plant || mvs ;

 deadzoneMonitor: MODULE =
 BEGIN
  INPUT yub: REAL
  INPUT x: REAL
  OUTPUT flag: BOOLEAN
  INITIALIZATION flag = FALSE
  TRANSITION
  [
   NOT (yub = yub') --> flag' = (x = x')
   []
   ELSE -->
  ]
 END;

 systemmonitor: MODULE = system || deadzoneMonitor ;

 p0: THEOREM
  systemmonitor |- G ( (x >= yub AND x - yub <= 0.05) OR (x <= yub AND yub - x <= 0.05) ) ;

 l1: THEOREM
  systemmonitor |- G ( b1 AND b2 AND b3 );

 l2: THEOREM
  systemmonitor |- G ( b1 AND b2 AND NOT(b3) );

 l3: THEOREM
  systemmonitor |- G ( -1.02 <= yub AND yub <= 1.02 );

 p1: THEOREM
  systemmonitor |- G ( flag = FALSE ) ;

 p2: THEOREM
  systemmonitor |- G ( inc ) ;

END