CristalCaveGem » LustreC

node REDGE(S:bool) returns(REDGE:bool); 

let 

  REDGE= S -> S and not(pre(S)); 

tel

node sum(a_0,a_1,a_2,a_3:int) returns(sum:int); 

let 

  sum = a_0 +1- a_1 + a_2 + a_3; 

tel

node AND(a_0,a_1,a_2,a_3:bool) returns(AND:bool); 

let 

  AND = a_0 and a_1 and a_2 and a_3;

tel

node OR(a_0,a_1,a_2,a_3:bool) returns(OR:bool); 

let 

  OR = a_0 or a_1 or a_2 or a_3;

tel

node NOT(a_0,a_1,a_2,a_3:bool) returns(NOT_0,NOT_1,NOT_2,NOT_3:bool); 

let 

  NOT_0 = not a_0;

  NOT_1 = not a_1;

  NOT_2 = not a_2;

  NOT_3 = not a_3;

tel

node FEDGE1(S:bool) returns(FEDGE1:bool); 

let 

  FEDGE1= not(S) -> not(S) and pre(S); 

tel

node FEDGE2(S:bool) returns(FEDGE2:bool); 

let 

  FEDGE2= REDGE(not(S)); 

tel

node Verification(S1,S2:bool) returns(property_ok:bool); 

var property1,property2:bool; 

let 

  property1=FEDGE1(S1)=FEDGE2(S1); 

  property2=FEDGE1(S1)=REDGE(S2);

  property_ok=if (S2=not(S1)) then

(property1 and property2)

else true;

tel

node Operator(stop:bool) returns (stop_request:bool); 

var nb_stops:int; 

let 

  nb_stops = (if stop then 1 else 0) -> 

    if stop then pre(nb_stops)+1 else 0; 

  stop_request = (nb_stops>=3); 

tel

node Defect(statein:int; fail_cond,ack_chan,repair_chan:bool) 

  returns(stateout:int); 

let 

  stateout = if (statein=0) then 

    if fail_cond then 1 else 0 

    else 

      if (statein=1) then 

        if ack_chan then 2 else 1 

      else 

        if repair_chan then 0 else 2; 

tel

node level_failure_detect(level:int) returns(level_failure_detect:bool); 

let 

  level_failure_detect = ((level < 0) or (level > 1000)); 

tel

node steam_failure_detect(steam:int) returns(steam_failure_detect:bool); 

let 

  steam_failure_detect = ((steam < 0) or (steam > 25)); 

tel

node LevelDefect(level_failure_acknowledgement,level_repaired:bool; 

  level:int) 

  returns( LevelDefect:int); 

let 

  LevelDefect = 0 -> 

    Defect(pre(LevelDefect), level_failure_detect(level), level_failure_acknowledgement, level_repaired); 

tel

node SteamDefect(steam_failure_acknowledgement,steam_repaired:bool; 

  steam:int) 

  returns( SteamDefect:int); 

let 

  SteamDefect = 0 -> 

    Defect(pre(SteamDefect), steam_failure_detect(steam), steam_failure_acknowledgement, steam_repaired); 

tel

node pump_failure_detect(pump_status,pump_state:int; 

  pump_control_state:bool) 

  returns(pump_failure_detect,pump_control_failure_detect,flow:bool); 

let 

  pump_failure_detect = ((pump_status=0) and pump_state=1) 

    or (((pump_status=1) or (pump_status=2))and pump_state=0); 

  pump_control_failure_detect = (((pump_status=0) or 

    (pump_status=2)) and pump_state=0 and pump_control_state) 

    or ((pump_status=1) and pump_state=1 and not(pump_control_state)) 

    or ((pump_status=2) and pump_state=1 and pump_control_state); 

  flow = ((pump_status=0) and pump_state=1 and pump_control_state) 

    or ((pump_status=1) and pump_state=0 and pump_control_state) 

    or ((pump_status=1) and pump_state=1); 

tel

node PumpDefect( 

  pump_failure_acknowledgement,pump_repaired, 

  pump_control_failure_acknowledgement,pump_control_repaired:bool; 

  pump_status,pump_state:int; 

  pump_control_state:bool) 

  returns(PumpDefect,PumpControlDefect:int;Flow:bool); 

var 

  pump_failure_d, pump_control_failure_d:bool; 

let 

  (pump_failure_d, pump_control_failure_d, Flow) = pump_failure_detect(pump_status, pump_state, pump_control_state); 

  PumpDefect = 0 -> 

    Defect(pre(PumpDefect), pump_failure_d, pump_failure_acknowledgement, pump_repaired); 

  PumpControlDefect = 0 -> 

    Defect(pre(PumpControlDefect), pump_control_failure_d, pump_control_failure_acknowledgement, pump_control_repaired); 

tel

node level_failure(level_defect:int) returns(level_failure:bool); 

let 

  level_failure = (level_defect<>0); 

tel

node steam_failure(steam_defect:int) returns(steam_failure:bool); 

let 

  steam_failure = (steam_defect<>0); 

tel

node pump_failure(pump_defect:int) returns(pump_failure:bool); 

let 

  pump_failure = (pump_defect<>0); 

tel

node pump_control_failure(pump_defect:int) returns(pump_failure:bool); 

let 

  pump_failure = (pump_defect<>0); 

tel

node Dynamics(valve_state,level,steam,level_defect,steam_defect:int; 

  flow_0,flow_1,flow_2,flow_3:bool) 

  returns (q,v:int; p_0,p_1,p_2,p_3:int); 

let 

  q = level-> 

    if level_failure(level_defect) then 

      pre(q) - steam*5 + sum(p_0,p_1,p_2,p_3)*5 - (if valve_state=1 then 10*5 else 0) 

    else 

      level; 

  v = steam-> 

    if steam_failure(steam_defect) then 

      (pre(q) -q) div 5 + sum(p_0,p_1,p_2,p_3)*5 

    else 

      steam; 

  p_0 = 0-> 

    if (not(flow_0)) then 

      0 

    else 

      15; 

  p_1 = 0-> 

    if (not(flow_1)) then 

      0 

    else 

      15; 

  p_2 = 0-> 

    if (not(flow_2)) then 

      0 

    else 

      15; 

  p_3 = 0-> 

    if (not(flow_3)) then 

      0 

    else 

      15; 

tel

node PumpsDecision(q,v:int) returns (n_pumps:int); 

let 

  n_pumps = if q>600 then 

      (v div 15) 

    else 

      if q<400 then 

        (v div 15) +1 

      else 

        pre(n_pumps) ; 

tel

node operate_pumps(n, n_pumps_to_open:int; 

  pump_status_0,pump_status_1,pump_status_2,pump_status_3,

  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 

  flow_0,flow_1,flow_2,flow_3:bool) 

  returns(operate_pumps_0,operate_pumps_1,operate_pumps_2,operate_pumps_3:int); 

let 

  operate_pumps_0 =  

      if ((n_pumps_to_open>0) and 

        not(flow_0) and 

        not(pump_failure(pump_defect_0)) and 

        (pump_status_0=0)) then 

        2 

      else 

        if ((n_pumps_to_open<0) and 

          flow_0 and 

          not(pump_failure(pump_defect_0)) and 

          (pump_status_0=1)) then 

          0 

        else 

          if (pump_status_0=2) then 

            1 

          else 

            if (pre(pump_defect_0)=2 and 

              pump_defect_0=0) then 

              if pump_status_0=1 then 

                0 

              else 

                1 

            else 

              pump_status_0; 

  operate_pumps_1 =  

      if ((n_pumps_to_open>0) and 

        not(flow_1) and 

        not(pump_failure(pump_defect_1)) and 

        (pump_status_1=0)) then 

        2 

      else 

        if ((n_pumps_to_open<0) and 

          flow_1 and 

          not(pump_failure(pump_defect_1)) and 

          (pump_status_1=1)) then 

          0 

        else 

          if (pump_status_1=2) then 

            1 

          else 

            if (pre(pump_defect_1)=2 and 

              pump_defect_1=0) then 

              if pump_status_1=1 then 

                0 

              else 

                1 

            else 

              pump_status_1; 

  operate_pumps_2 =  

      if ((n_pumps_to_open>0) and 

        not(flow_2) and 

        not(pump_failure(pump_defect_2)) and 

        (pump_status_2=0)) then 

        2 

      else 

        if ((n_pumps_to_open<0) and 

          flow_2 and 

          not(pump_failure(pump_defect_2)) and 

          (pump_status_2=1)) then 

          0 

        else 

          if (pump_status_2=2) then 

            1 

          else 

            if (pre(pump_defect_2)=2 and 

              pump_defect_2=0) then 

              if pump_status_2=1 then 

                0 

              else 

                1 

            else 

              pump_status_2; 

  operate_pumps_3 =  

      if ((n_pumps_to_open>0) and 

        not(flow_3) and 

        not(pump_failure(pump_defect_3)) and 

        (pump_status_3=0)) then 

        2 

      else 

        if ((n_pumps_to_open<0) and 

          flow_3 and 

          not(pump_failure(pump_defect_3)) and 

          (pump_status_3=1)) then 

          0 

        else 

          if (pump_status_3=2) then 

            1 

          else 

            if (pre(pump_defect_3)=2 and 

              pump_defect_3=0) then 

              if pump_status_3=1 then 

                0 

              else 

                1 

            else 

              pump_status_3; 

tel

node PumpsStatus( 

  n_pumps:int; 

  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 

  flow_0,flow_1,flow_2,flow_3:bool) 

  returns(pump_status_0,pump_status_1,pump_status_2,pump_status_3:int); 

var 

  n_pumps_flow,n_pumps_to_open:int; 

  t0,t1,t2,t3:int;

let 

  n_pumps_flow = (if flow_0 then 1 else 0) + (if flow_1 then 1 else 0) + 

    (if flow_2 then 1 else 0) + (if flow_3 then 1 else 0); 

  n_pumps_to_open = n_pumps-n_pumps_flow; 

  pump_status_0 = 0 ->t0;

  pump_status_1 = 0 ->t1;

  pump_status_2 = 0 ->t2;

  pump_status_3 = 0 ->t3;

  (t0,t1,t2,t3) =

    operate_pumps(4, n_pumps_to_open, 

      pre(pump_status_0),pre(pump_status_1),pre(pump_status_2),pre(pump_status_3), 

      pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, 

      flow_0,flow_1,flow_2,flow_3); 

tel

node transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 

  returns(transmission_failure:bool); 

let 

  transmission_failure = pump_state_0=3 or pump_state_1=3 or pump_state_2=3 or pump_state_3=3; 

tel

node dangerous_level(q:int) returns(dangerous_level:bool); 

let 

  dangerous_level = (q <= 150) or (q >= 850); 

tel

node steam_failure_startup(steam:int) returns(steam_failure_startup:bool); 

let 

  steam_failure_startup=(steam<>0); 

tel

node critical_failure( 

  op_mode,steam,level_defect,steam_defect:int; 

  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3:int; 

  q:int; 

  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 

  returns(critical_failure:bool); 

let 

  critical_failure = transmission_failure(pump_state_0,pump_state_1,pump_state_2,pump_state_3) or 

    (op_mode=1 and steam_failure_startup(steam)) or 

    (op_mode=2 and (level_failure(level_defect) or steam_failure(steam_defect))) or 

    (op_mode=3 and dangerous_level(q)) or 

    (op_mode=4 and dangerous_level(q)) or 

    (op_mode=5 and (dangerous_level(q) or steam_failure(steam_defect) or AND(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)))); 

tel

node failure( 

  level_defect,steam_defect:int; 

  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int) 

  returns(failure:bool); 

let 

  failure = level_failure(level_defect) or 

    steam_failure(steam_defect) or 

    OR(pump_failure(pump_defect_0),pump_failure(pump_defect_1),pump_failure(pump_defect_2),pump_failure(pump_defect_3)) or 

    OR(pump_control_failure(pump_control_defect_0),pump_control_failure(pump_control_defect_1),pump_control_failure(pump_control_defect_2),pump_control_failure(pump_control_defect_3)); 

tel

node ControlMode( 

  steam_boiler_waiting,physical_units_ready,stop_request:bool; 

  steam,level_defect,steam_defect:int; 

  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int; 

  q:int; 

  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 

  returns(op_mode :int); 

let 

  op_mode= 1-> 

    if (critical_failure(pre(op_mode), 

      steam, level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, q, pump_state_0,pump_state_1,pump_state_2,pump_state_3) or 

      stop_request or pre(op_mode)=6) then 

      6 

    else 

      if (pre(op_mode)=1) then 

        if steam_boiler_waiting then 2 else 1 

      else 

        if (pre(op_mode)=2 and not physical_units_ready) then 

          2 

        else 

          if level_failure(level_defect) then 

            5 

          else 

            if failure(level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3) then 

              4 

            else 

              3; 

tel

node Valve(op_mode:int;q:int) returns (valve:bool;valve_state:int); 

let 

  valve_state=0-> 

    if (op_mode=2) then 

      if (q>600) then 

        1 

      else 

        if (q<=600) then 0 else pre(valve_state) 

    else 

      pre(valve_state); 

  valve =false-> 

    (valve_state<>pre(valve_state)); 

tel

node initialization_complete(op_mode,level:int;valve:bool) 

  returns(initialization_complete:bool); 

let 

  initialization_complete =(op_mode=2) and 

    ((400<=level) and (level<=600))and 

    not(valve); 

tel

node ControlOutput(op_mode,level:int;valve:bool) 

  returns(program_ready:bool;mode:int); 

let 

  program_ready=initialization_complete(op_mode,level,valve); 

  mode =op_mode; 

tel

node LevelOutput(op_mode,level_defect:int; level_repaired:bool) 

  returns (level_outcome_failure_detection, 

level_outcome_repaired_acknowledgement : bool); 

let 

  level_outcome_failure_detection= 

    not ((op_mode=6) or (op_mode=1)) and 

    (level_defect=1); 

  level_outcome_repaired_acknowledgement = 

    not ((op_mode=6) or (op_mode=1)) and 

    level_repaired; 

tel

node SteamOutput(op_mode,steam_defect:int; steam_repaired:bool) 

  returns (steam_outcome_failure_detection, 

steam_outcome_repaired_acknowledgement : bool); 

let 

  steam_outcome_failure_detection= 

    not ((op_mode=6) or (op_mode=1)) and 

    (steam_defect=1); 

  steam_outcome_repaired_acknowledgement = 

    not ((op_mode=6) or (op_mode=1)) and 

    steam_repaired; 

tel

node PumpsOutput(op_mode:int; 

  pump_status_0,pump_status_1,pump_status_2,pump_status_3,

  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,

  pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int; 

  pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3,

  pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3:bool) 

  returns (open_pump_0,open_pump_1,open_pump_2,open_pump_3,

  close_pump_0,close_pump_1,close_pump_2,close_pump_3,

  pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3, 

  pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3,

  pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3, 

  pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool); 

let 

  open_pump_0 = 

     op_mode<>6 and op_mode<>1 and pump_status_0=2;

  open_pump_1 = 

     op_mode<>6 and op_mode<>1 and pump_status_1=2;

  open_pump_2 = 

     op_mode<>6 and op_mode<>1 and pump_status_2=2;

  open_pump_3 = 

     op_mode<>6 and op_mode<>1 and pump_status_3=2; 

  close_pump_0 = 

     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_0)<>0 and pump_defect_0=0 and pre(pump_defect_0)=0;

  close_pump_1 = 

     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_1)<>0 and pump_defect_0=0 and pre(pump_defect_1)=0;

  close_pump_2 = 

     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_2)<>0 and pump_defect_0=0 and pre(pump_defect_2)=0;

  close_pump_3 = 

     op_mode<>6 and op_mode<>1 and pump_status_0=0 and pre(pump_status_3)<>0 and pump_defect_0=0 and pre(pump_defect_3)=0;

  pump_failure_detection_0 = 

    op_mode<>6 and op_mode<>1 and pump_defect_0=1;

  pump_failure_detection_1 = 

     op_mode<>6 and op_mode<>1 and pump_defect_1=1;

  pump_failure_detection_2 = 

     op_mode<>6 and op_mode<>1 and pump_defect_2=1;

  pump_failure_detection_3 = 

     op_mode<>6 and op_mode<>1 and pump_defect_3=1;

  pump_repaired_acknowledgement_0 = 

    op_mode<>6 and op_mode<>1 and pump_repaired_0;

  pump_repaired_acknowledgement_1 = 

     op_mode<>6 and op_mode<>1 and pump_repaired_1;

  pump_repaired_acknowledgement_2 = 

     op_mode<>6 and op_mode<>1 and pump_repaired_2;

  pump_repaired_acknowledgement_3 = 

     op_mode<>6 and op_mode<>1 and pump_repaired_3;

  pump_control_failure_detection_0 = 

    op_mode<>6 and op_mode<>1 and pump_control_defect_0=1;

  pump_control_failure_detection_1 = 

    op_mode<>6 and op_mode<>1 and pump_control_defect_1=1;

  pump_control_failure_detection_2 = 

    op_mode<>6 and op_mode<>1 and pump_control_defect_2=1;

  pump_control_failure_detection_3 = 

    op_mode<>6 and op_mode<>1 and pump_control_defect_3=1;

  pump_control_repaired_acknowledgement_0 = 

    op_mode<>6 and op_mode<>1 and pump_control_repaired_0;

  pump_control_repaired_acknowledgement_1 = 

    op_mode<>6 and op_mode<>1 and pump_control_repaired_1;

  pump_control_repaired_acknowledgement_2 = 

    op_mode<>6 and op_mode<>1 and pump_control_repaired_2;

  pump_control_repaired_acknowledgement_3 = 

    op_mode<>6 and op_mode<>1 and pump_control_repaired_3;

tel

node BoilerController( 

  stop, 

  steam_boiler_waiting, 

  physical_units_ready : bool; 

  level : int; 

  steam : int; 

  pump_state_0,pump_state_1,pump_state_2,pump_state_3 : int; 

  pump_control_state_0,pump_control_state_1,pump_control_state_2,pump_control_state_3 : bool; 

  pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3 : bool; 

  pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3 : bool; 

  level_repaired : bool; 

  steam_repaired : bool; 

  pump_failure_acknowledgement_0,pump_failure_acknowledgement_1,pump_failure_acknowledgement_2,pump_failure_acknowledgement_3 : bool; 

  pump_control_failure_acknowledgement_0,pump_control_failure_acknowledgement_1,pump_control_failure_acknowledgement_2,pump_control_failure_acknowledgement_3 : bool; 

  level_failure_acknowledgement : bool; 

  steam_failure_acknowledgement : bool) 

  returns(

  program_ready : bool; 

  mode : int; 

  valve : bool; 

  open_pump_0,open_pump_1,open_pump_2,open_pump_3 : bool; 

  close_pump_0,close_pump_1,close_pump_2,close_pump_3 : bool; 

  pump_failure_detection_0,pump_failure_detection_1,pump_failure_detection_2,pump_failure_detection_3 : bool; 

  pump_control_failure_detection_0,pump_control_failure_detection_1,pump_control_failure_detection_2,pump_control_failure_detection_3 : bool; 

  level_failure_detection : bool; 

  steam_outcome_failure_detection : bool; 

  pump_repaired_acknowledgement_0,pump_repaired_acknowledgement_1,pump_repaired_acknowledgement_2,pump_repaired_acknowledgement_3 : bool; 

  pump_control_repaired_acknowledgement_0,pump_control_repaired_acknowledgement_1,pump_control_repaired_acknowledgement_2,pump_control_repaired_acknowledgement_3 : bool; 

  level_repaired_acknowledgement : bool; 

  steam_outcome_repaired_acknowledgement: bool); 

var 

  stop_request : bool; 

  op_mode : int; 

  q : int; 

  v : int; 

  p_0,p_1,p_2,p_3 : int; 

  valve_state : int; 

  n_pumps : int; 

  pump_status_0,pump_status_1,pump_status_2,pump_status_3 : int; 

  level_defect : int; 

  steam_defect : int; 

  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3 : int; 

  pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3 : int; 

  flow_0,flow_1,flow_2,flow_3 : bool; 

  t00,t01,t10,t20,t30,t11,t21,t31:int;

  t02,t12,t22,t32,u4,u6:bool;

  t4,t5,t6,t7,t8,t9,u0,u1,u2,u3,u5,u7:int;

  a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24:bool;

  b0,b1,b2,b3:bool;

let 

  stop_request = Operator(stop); 

  level_defect = 0-> 

    LevelDefect(level_failure_acknowledgement, level_repaired, level); 

  steam_defect = 0-> 

    SteamDefect(steam_failure_acknowledgement, steam_repaired, steam); 

  pump_defect_0 = 0 -> t00;

  pump_control_defect_0 = 0 -> t01;

  flow_0 = false -> t02;

  (t00,t01,t02) =

       PumpDefect(pump_failure_acknowledgement_0, pump_repaired_0, 

         pump_control_failure_acknowledgement_0, pump_control_repaired_0,

         pre(pump_status_0), pump_state_0, pump_control_state_0); 

  pump_defect_1 = 0 -> t10;

  pump_control_defect_1 = 0 -> t11;

  flow_1 = false -> t12;

  (t10,t11,t12) =

       PumpDefect(pump_failure_acknowledgement_1, pump_repaired_1, 

         pump_control_failure_acknowledgement_1, pump_control_repaired_1,

         pre(pump_status_1), pump_state_1, pump_control_state_1); 

  pump_defect_2 = 0 -> t20;

  pump_control_defect_2 = 0 -> t21;

  flow_2 = false -> t22;

  (t20,t21,t22) =

       PumpDefect(pump_failure_acknowledgement_2, pump_repaired_2, 

         pump_control_failure_acknowledgement_2, pump_control_repaired_2,

         pre(pump_status_2), pump_state_2, pump_control_state_2); 

  pump_defect_3 = 0 -> t30;

  pump_control_defect_3 = 0 -> t31;

  flow_3 = false -> t32;

  (t30,t31,t32) =

       PumpDefect(pump_failure_acknowledgement_3, pump_repaired_3, 

         pump_control_failure_acknowledgement_3, pump_control_repaired_3,

         pre(pump_status_3), pump_state_3, pump_control_state_3); 

  q = level -> t4;

  v = steam -> t5;

  p_0 = 0 -> t6;

  p_1 = 0 -> t7;

  p_2 = 0 -> t8;

  p_3 = 0 -> t9;

  (t4,t5,t6,t7,t8,t9) =

    Dynamics(pre(valve_state), level, steam, level_defect, steam_defect, flow_0,flow_1,flow_2,flow_3); 

  n_pumps = 0-> PumpsDecision(q,v); 

  pump_status_0 = 0 -> u0;

  pump_status_1 = 0 -> u1;

  pump_status_2 = 0 -> u2;

  pump_status_3 = 0 -> u3;

  (u0,u1,u2,u3) =

    PumpsStatus(n_pumps, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,

      flow_0,flow_1,flow_2,flow_3); 

  op_mode = 1-> 

    ControlMode( steam_boiler_waiting, physical_units_ready, stop_request, steam, level_defect, steam_defect, pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3, pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3, q, pump_state_0,pump_state_1,pump_state_2,pump_state_3); 

  valve = false -> u4;

  valve_state = 0 -> u5;

  (u4,u5) =

    Valve(op_mode,q); 

  program_ready = false -> u6;

  mode = 1-> u7;

  (u6,u7) =

    ControlOutput(op_mode,level,valve); 

  open_pump_0=a1;

  open_pump_1=a2;

  open_pump_2=a3;

  open_pump_3=a4;

  close_pump_0=a5;

  close_pump_1=a6;

  close_pump_2=a7;

  close_pump_3=a8;

  pump_failure_detection_0=a9;

  pump_failure_detection_1=a10;

  pump_failure_detection_2=a11;

  pump_failure_detection_3=a12;

  pump_repaired_acknowledgement_0=a13;

  pump_repaired_acknowledgement_1=a14;

  pump_repaired_acknowledgement_2=a15;

  pump_repaired_acknowledgement_3=a16;

  pump_control_failure_detection_0=a17;

  pump_control_failure_detection_1=a18;

  pump_control_failure_detection_2=a19;

  pump_control_failure_detection_3=a20;

  pump_control_repaired_acknowledgement_0=a21;

  pump_control_repaired_acknowledgement_1=a22;

  pump_control_repaired_acknowledgement_2=a23;

  pump_control_repaired_acknowledgement_3=a24;

   (a1,a2,a3,a4,a5,a6,a7,a8,a9,a10,a11,a12,a13,a14,a15,a16,a17,a18,a19,a20,a21,a22,a23,a24)=

      PumpsOutput(op_mode, pump_status_0,pump_status_1,pump_status_2,pump_status_3,

        pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,

        pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3,

        pump_repaired_0,pump_repaired_1,pump_repaired_2,pump_repaired_3,

        pump_control_repaired_0,pump_control_repaired_1,pump_control_repaired_2,pump_control_repaired_3); 

  level_failure_detection = false -> b0;

  level_repaired_acknowledgement = false -> b1;

  (b0,b1)=

    LevelOutput(op_mode,level_defect,level_repaired); 

  steam_outcome_failure_detection = false -> b2;

  steam_outcome_repaired_acknowledgement = false -> b3;

  (b2,b3)=

    SteamOutput(op_mode,steam_defect,steam_repaired); 

tel

--@ ensures OK;

node top(

  steam_boiler_waiting,physical_units_ready,stop_request:bool; 

  steam,level_defect,steam_defect:int; 

  pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3:int; 

  q:int; 

  pump_state_0,pump_state_1,pump_state_2,pump_state_3:int) 

  returns(OK:bool); 

var 

  op_mode :int; 

  mode_normal_then_water_level_ok, 

  mode_normal_then_no_stop_request:bool; 

let 

  op_mode= 

    ControlMode(

      steam_boiler_waiting,physical_units_ready,stop_request,

      steam,level_defect,steam_defect,

      pump_defect_0,pump_defect_1,pump_defect_2,pump_defect_3,pump_control_defect_0,pump_control_defect_1,pump_control_defect_2,pump_control_defect_3,

      q, pump_state_0,pump_state_1,pump_state_2,pump_state_3); 

  OK = 

    mode_normal_then_water_level_ok and 

    mode_normal_then_no_stop_request; 

  mode_normal_then_no_stop_request = 

    (op_mode=3 => not(stop_request)); 

  mode_normal_then_water_level_ok = 

    true ->

    (op_mode=3 and pre(op_mode)=3 =>

    not(dangerous_level(q))); 

  --%MAIN;

--!k:2;

--!PROPERTY:  OK=true;

tel