plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/examples/tfpg/cassini/cassini_param_common.smv

#define COMBO_OUT(V1, V2)  case                \
              V1.p_out > V2.p_out : V1.p_out;  \
              V2.p_out > V1.p_out : V2.p_out;  \
              TRUE : V1.p_out;                 \
              esac


------------------------------------------------ HELIUM TANK

MODULE HELIUMTANK (t_#delta)

  VAR
    state            : {ok, empty};
    internal_leakage : {none, leakage};
    p_out            : 0..2;

  DEFINE
    NR_FAILURES := count(internal_leakage=leakage);
    timed := t_#delta > 0;

  ASSIGN

    init(state) := ok;
    next(state) := case
      timed : state;
      state = ok : {ok, empty};
      TRUE : state;
      esac;

    init(p_out) := 2;
    next(p_out) := case
      next(state) = empty : 0;
      internal_leakage = leakage : 1;
      TRUE : 2;
      esac;

   TRANS
     timed -> internal_leakage = next(internal_leakage);

   TRANS
     p_out != next(p_out) -> !timed;


-------------------------------------------- PROPELLANT TANK

MODULE PROPELLANTTANK (p_in, t_#delta)

  VAR
    state            : {ok, empty};
    internal_leakage : {none, leakage};
    p_out            : 0..2;

  DEFINE
    no_helium := p_in = 0 | p_in = 1;
    NR_FAILURES := count(internal_leakage=leakage);
    timed := t_#delta > 0;

  ASSIGN

    init(state) := ok;
    next(state) := case
      timed : state;
      state = ok : {ok, empty};
      TRUE : state;
      esac;

    init(p_out) := case
      no_helium : 1;
      TRUE : 2;
      esac;
    next(p_out) := case
      state = empty : 0;
      no_helium & internal_leakage = leakage : 0;
      no_helium | internal_leakage = leakage : 1;
      TRUE : 2;
      esac;

   TRANS
     timed -> internal_leakage = next(internal_leakage);

   TRANS
     p_out != next(p_out) -> !timed;


----------------------------------------------------- ENGINE

MODULE ENGINE (fuel_p_in, oxidizer_p_in, t_#delta)

  VAR
    thrust : 0..4;

  DEFINE
    will_ignite := fuel_p_in > 0 & oxidizer_p_in > 0;
    will_go_full_thrust := fuel_p_in = 2 & oxidizer_p_in = 2;
    timed := t_#delta > 0;

  ASSIGN

    init(thrust) := 0;
    next(thrust) := case

      timed : thrust;

      !will_ignite & thrust > 0 : thrust - 1;
      !will_ignite & thrust = 0 : 0;

      will_ignite & !will_go_full_thrust & thrust < 2 : thrust + 1;
      will_ignite & !will_go_full_thrust & thrust > 2 : thrust - 1;
      will_ignite & !will_go_full_thrust & thrust = 2 : 2;

      will_go_full_thrust & thrust < 4 : thrust + 1;
      will_go_full_thrust & thrust = 4 : 4;

      TRUE : thrust;

      esac;


---------------------------------------------- ACCELEROMETER 

MODULE ACCELEROMETER (thrust_primary, thrust_backup, t_#delta)

  VAR
    acceleration : {none, low, high};

  DEFINE
    timed := t_#delta > 0;

  ASSIGN

    init(acceleration) := case
      thrust_primary + thrust_backup = 0 : none;
      thrust_primary + thrust_backup < 3 : low;
      TRUE : high;
      esac;
    next(acceleration) := case
      timed : acceleration;
      thrust_primary + thrust_backup = 0 : none;
      thrust_primary + thrust_backup < 3 : low;
      TRUE : high;
      esac;


-------------------------------------------------- PYROVALVE

MODULE PYROVALVE (p_in, t_#delta)

  VAR
    state   : {open, closed};
    ignited : boolean;
    p_out   : 0..2;

  IVAR
    cmdin : {open, close, none};

  DEFINE
    NO_CMD := cmdin = none;
    timed := t_#delta > 0;

  ASSIGN

    -- initial state constraint should be set at a higher level
    next(state) := case
      timed : state;
      ignited : state;
      cmdin = open : open;
      cmdin = close : closed;
      TRUE : state;
      esac;

    init(ignited) := FALSE;
    next(ignited) := case
      timed : ignited;
      ignited : TRUE;
      state = open & cmdin = close : TRUE;
      state = closed & cmdin = open : TRUE;
      TRUE : ignited;
      esac;

    init(p_out) := case
      state = closed : 0;
      TRUE : p_in;
      esac;
    next(p_out) := case
      next(state) = closed : 0;
      TRUE : p_in;
      esac;

  TRANS
    timed -> NO_CMD;

   TRANS
     p_out != next(p_out) -> !timed;

  INVARSPEC next(p_in) <= p_in;


------------------------------------------------------ VALVE

MODULE VALVE (p_in, t_#delta)

  VAR
    state            : {open, closed};
    internal_leakage : {none, leakage};
    is_stuck         : boolean;
    p_out            : 0..2;

  IVAR
    cmdin : {open, close, none};

  DEFINE
    NO_CMD := cmdin = none;
    NR_FAILURES := count(is_stuck, internal_leakage=leakage);
    timed := t_#delta > 0;

  ASSIGN

    -- initial state constraint should be set at a higher level
    next(state) := case
      timed : state;
      is_stuck : state;
      cmdin = open : open;
      cmdin = close : closed;
      TRUE : state;
      esac;

    init(p_out) := case
      state = closed : 0;
      TRUE : p_in;
      esac;
    next(p_out) := case
      next(state) = closed : 0;
      internal_leakage = none : p_in;
      p_in = 2 : 1;
      TRUE : 0;
      esac;

  TRANS
    timed -> internal_leakage = next(internal_leakage);

  TRANS
    timed -> is_stuck = next(is_stuck);

  TRANS
    timed -> NO_CMD;

  TRANS
    p_out != next(p_out) -> !timed;

  INVARSPEC next(p_in) <= p_in;


------------------------------------------------------ VALVE BLOCK

MODULE VALVE_BLOCK (p_in, vb_open, t_#delta)

  VAR v : VALVE (p_in, t_#delta);
  INVAR v.state = open <-> vb_open;
  TRANS v.NO_CMD;

  -- valve can leak
  --INVAR v.internal_leakage = none;

  -- leakage is a permanent failure
  TRANS v.internal_leakage != none -> next(v.internal_leakage != none);

  -- valve cannot get stuck
  INVAR !v.is_stuck;

  VAR pv : PYROVALVE (p_in, t_#delta);
  INVAR pv.state = closed;

  DEFINE p_out := COMBO_OUT(v, pv);


----------------------------------------------------- VALVE CHAINS

MODULE VALVE_CHAIN_2 (p_in, vc_open, t_#delta)
  VAR vb_1 : VALVE_BLOCK(p_in, vc_open, t_#delta);
  VAR pp_12 : PIPE(vb_1.p_out, 1, 2, t_#delta);
  VAR vb_2 : VALVE_BLOCK(pp_12.p_out, vc_open, t_#delta);
  DEFINE p_out := vb_2.p_out;
  DEFINE NR_FAILURES :=
    vb_1.v.NR_FAILURES +
    vb_2.v.NR_FAILURES;

  DEFINE diff_vb_2 := vb_2.p_in != vb_2.p_out;


MODULE VALVE_CHAIN_4 (p_in, vc_open, t_#delta)
  VAR vb_1 : VALVE_BLOCK(p_in, vc_open, t_#delta);
  VAR pp_12 : PIPE(vb_1.p_out, 2, 3, t_#delta);
  VAR vb_2 : VALVE_BLOCK(pp_12.p_out, vc_open, t_#delta);
  VAR pp_23 : PIPE(vb_2.p_out, 1, 2, t_#delta);
  VAR vb_3 : VALVE_BLOCK(pp_23.p_out, vc_open, t_#delta);
  VAR pp_34 : PIPE(vb_3.p_out, 2, 2, t_#delta);
  VAR vb_4 : VALVE_BLOCK(pp_34.p_out, vc_open, t_#delta);
  DEFINE p_out := vb_4.p_out;
  DEFINE NR_FAILURES :=
    vb_1.v.NR_FAILURES +
    vb_2.v.NR_FAILURES +
    vb_3.v.NR_FAILURES +
    vb_4.v.NR_FAILURES;

  DEFINE diff_vb_2 := vb_2.p_in != vb_2.p_out;
  DEFINE diff_vb_3 := vb_3.p_in != vb_3.p_out;
  DEFINE diff_vb_4 := vb_4.p_in != vb_4.p_out;


MODULE VALVE_CHAIN_6 (p_in, vc_open, t_#delta)
  VAR vb_1 : VALVE_BLOCK(p_in, vc_open, t_#delta);
  VAR pp_12 : PIPE(vb_1.p_out, 2, 3, t_#delta);
  VAR vb_2 : VALVE_BLOCK(pp_12.p_out, vc_open, t_#delta);
  VAR pp_23 : PIPE(vb_2.p_out, 1, 2, t_#delta);
  VAR vb_3 : VALVE_BLOCK(pp_23.p_out, vc_open, t_#delta);
  VAR pp_34 : PIPE(vb_3.p_out, 2, 2, t_#delta);
  VAR vb_4 : VALVE_BLOCK(pp_34.p_out, vc_open, t_#delta);
  VAR pp_45 : PIPE(vb_4.p_out, 2, 2, t_#delta);
  VAR vb_5 : VALVE_BLOCK(pp_45.p_out, vc_open, t_#delta);
  VAR pp_56 : PIPE(vb_5.p_out, 3, 4, t_#delta);
  VAR vb_6 : VALVE_BLOCK(pp_56.p_out, vc_open, t_#delta);
  DEFINE p_out := vb_4.p_out;
  DEFINE NR_FAILURES :=
    vb_1.v.NR_FAILURES +
    vb_2.v.NR_FAILURES +
    vb_3.v.NR_FAILURES +
    vb_4.v.NR_FAILURES +
    vb_5.v.NR_FAILURES +
    vb_6.v.NR_FAILURES;

  DEFINE diff_vb_2 := vb_2.p_in != vb_2.p_out;
  DEFINE diff_vb_3 := vb_3.p_in != vb_3.p_out;
  DEFINE diff_vb_4 := vb_4.p_in != vb_4.p_out;
  DEFINE diff_vb_5 := vb_5.p_in != vb_5.p_out;
  DEFINE diff_vb_6 := vb_6.p_in != vb_6.p_out;


MODULE VALVE_CHAIN_8 (p_in, vc_open, t_#delta)
  VAR vb_1 : VALVE_BLOCK(p_in, vc_open, t_#delta);
  VAR pp_12 : PIPE(vb_1.p_out, 2, 3, t_#delta);
  VAR vb_2 : VALVE_BLOCK(pp_12.p_out, vc_open, t_#delta);
  VAR pp_23 : PIPE(vb_2.p_out, 1, 2, t_#delta);
  VAR vb_3 : VALVE_BLOCK(pp_23.p_out, vc_open, t_#delta);
  VAR pp_34 : PIPE(vb_3.p_out, 2, 2, t_#delta);
  VAR vb_4 : VALVE_BLOCK(pp_34.p_out, vc_open, t_#delta);
  VAR pp_45 : PIPE(vb_4.p_out, 2, 2, t_#delta);
  VAR vb_5 : VALVE_BLOCK(pp_45.p_out, vc_open, t_#delta);
  VAR pp_56 : PIPE(vb_5.p_out, 3, 4, t_#delta);
  VAR vb_6 : VALVE_BLOCK(pp_56.p_out, vc_open, t_#delta);
  VAR pp_67 : PIPE(vb_6.p_out, 1, 5, t_#delta);
  VAR vb_7 : VALVE_BLOCK(pp_67.p_out, vc_open, t_#delta);
  VAR pp_78 : PIPE(vb_7.p_out, 2, 4, t_#delta);
  VAR vb_8 : VALVE_BLOCK(pp_78.p_out, vc_open, t_#delta);
  DEFINE p_out := vb_4.p_out;
  DEFINE NR_FAILURES :=
    vb_1.v.NR_FAILURES +
    vb_2.v.NR_FAILURES +
    vb_3.v.NR_FAILURES +
    vb_4.v.NR_FAILURES +
    vb_5.v.NR_FAILURES +
    vb_6.v.NR_FAILURES +
    vb_7.v.NR_FAILURES +
    vb_8.v.NR_FAILURES;

  DEFINE diff_vb_2 := vb_2.p_in != vb_2.p_out;
  DEFINE diff_vb_3 := vb_3.p_in != vb_3.p_out;
  DEFINE diff_vb_4 := vb_4.p_in != vb_4.p_out;
  DEFINE diff_vb_5 := vb_5.p_in != vb_5.p_out;
  DEFINE diff_vb_6 := vb_6.p_in != vb_6.p_out;
  DEFINE diff_vb_7 := vb_7.p_in != vb_7.p_out;
  DEFINE diff_vb_8 := vb_8.p_in != vb_8.p_out;


MODULE VALVE_CHAIN_10 (p_in, vc_open, t_#delta)
  VAR vb_1 : VALVE_BLOCK(p_in, vc_open, t_#delta);
  VAR pp_12 : PIPE(vb_1.p_out, 2, 3, t_#delta);
  VAR vb_2 : VALVE_BLOCK(pp_12.p_out, vc_open, t_#delta);
  VAR pp_23 : PIPE(vb_2.p_out, 1, 2, t_#delta);
  VAR vb_3 : VALVE_BLOCK(pp_23.p_out, vc_open, t_#delta);
  VAR pp_34 : PIPE(vb_3.p_out, 2, 2, t_#delta);
  VAR vb_4 : VALVE_BLOCK(pp_34.p_out, vc_open, t_#delta);
  VAR pp_45 : PIPE(vb_4.p_out, 2, 2, t_#delta);
  VAR vb_5 : VALVE_BLOCK(pp_45.p_out, vc_open, t_#delta);
  VAR pp_56 : PIPE(vb_5.p_out, 3, 4, t_#delta);
  VAR vb_6 : VALVE_BLOCK(pp_56.p_out, vc_open, t_#delta);
  VAR pp_67 : PIPE(vb_6.p_out, 1, 5, t_#delta);
  VAR vb_7 : VALVE_BLOCK(pp_67.p_out, vc_open, t_#delta);
  VAR pp_78 : PIPE(vb_7.p_out, 2, 4, t_#delta);
  VAR vb_8 : VALVE_BLOCK(pp_78.p_out, vc_open, t_#delta);
  VAR pp_89 : PIPE(vb_8.p_out, 3, 4, t_#delta);
  VAR vb_9 : VALVE_BLOCK(pp_89.p_out, vc_open, t_#delta);
  VAR pp_910 : PIPE(vb_9.p_out, 1, 5, t_#delta);
  VAR vb_10 : VALVE_BLOCK(pp_910.p_out, vc_open, t_#delta);
  DEFINE p_out := vb_4.p_out;
  DEFINE NR_FAILURES :=
    vb_1.v.NR_FAILURES +
    vb_2.v.NR_FAILURES +
    vb_3.v.NR_FAILURES +
    vb_4.v.NR_FAILURES +
    vb_5.v.NR_FAILURES +
    vb_6.v.NR_FAILURES +
    vb_7.v.NR_FAILURES +
    vb_8.v.NR_FAILURES +
    vb_9.v.NR_FAILURES + 
    vb_10.v.NR_FAILURES; 

  DEFINE diff_vb_2 := vb_2.p_in != vb_2.p_out;
  DEFINE diff_vb_3 := vb_3.p_in != vb_3.p_out;
  DEFINE diff_vb_4 := vb_4.p_in != vb_4.p_out;
  DEFINE diff_vb_5 := vb_5.p_in != vb_5.p_out;
  DEFINE diff_vb_6 := vb_6.p_in != vb_6.p_out;
  DEFINE diff_vb_7 := vb_7.p_in != vb_7.p_out;
  DEFINE diff_vb_8 := vb_8.p_in != vb_8.p_out;
  DEFINE diff_vb_9 := vb_9.p_in != vb_9.p_out;
  DEFINE diff_vb_10 := vb_10.p_in != vb_10.p_out;


MODULE VALVE_CHAIN_12 (p_in, vc_open, t_#delta)
  VAR vb_1 : VALVE_BLOCK(p_in, vc_open, t_#delta);
  VAR pp_12 : PIPE(vb_1.p_out, 2, 3, t_#delta);
  VAR vb_2 : VALVE_BLOCK(pp_12.p_out, vc_open, t_#delta);
  VAR pp_23 : PIPE(vb_2.p_out, 1, 2, t_#delta);
  VAR vb_3 : VALVE_BLOCK(pp_23.p_out, vc_open, t_#delta);
  VAR pp_34 : PIPE(vb_3.p_out, 2, 2, t_#delta);
  VAR vb_4 : VALVE_BLOCK(pp_34.p_out, vc_open, t_#delta);
  VAR pp_45 : PIPE(vb_4.p_out, 2, 2, t_#delta);
  VAR vb_5 : VALVE_BLOCK(pp_45.p_out, vc_open, t_#delta);
  VAR pp_56 : PIPE(vb_5.p_out, 3, 4, t_#delta);
  VAR vb_6 : VALVE_BLOCK(pp_56.p_out, vc_open, t_#delta);
  VAR pp_67 : PIPE(vb_6.p_out, 1, 5, t_#delta);
  VAR vb_7 : VALVE_BLOCK(pp_67.p_out, vc_open, t_#delta);
  VAR pp_78 : PIPE(vb_7.p_out, 2, 4, t_#delta);
  VAR vb_8 : VALVE_BLOCK(pp_78.p_out, vc_open, t_#delta);
  VAR pp_89 : PIPE(vb_8.p_out, 3, 4, t_#delta);
  VAR vb_9 : VALVE_BLOCK(pp_89.p_out, vc_open, t_#delta);
  VAR pp_910 : PIPE(vb_9.p_out, 1, 5, t_#delta);
  VAR vb_10 : VALVE_BLOCK(pp_910.p_out, vc_open, t_#delta);
  VAR pp_1011 : PIPE(vb_10.p_out, 2, 4, t_#delta);
  VAR vb_11 : VALVE_BLOCK(pp_1011.p_out, vc_open, t_#delta);
  VAR pp_1112 : PIPE(vb_11.p_out, 3, 3, t_#delta);
  VAR vb_12 : VALVE_BLOCK(pp_1112.p_out, vc_open, t_#delta);
  DEFINE p_out := vb_4.p_out;
  DEFINE NR_FAILURES :=
    vb_1.v.NR_FAILURES +
    vb_2.v.NR_FAILURES +
    vb_3.v.NR_FAILURES +
    vb_4.v.NR_FAILURES +
    vb_5.v.NR_FAILURES +
    vb_6.v.NR_FAILURES +
    vb_7.v.NR_FAILURES +
    vb_8.v.NR_FAILURES +
    vb_9.v.NR_FAILURES + 
    vb_10.v.NR_FAILURES +
    vb_11.v.NR_FAILURES +
    vb_12.v.NR_FAILURES;

  DEFINE diff_vb_2 := vb_2.p_in != vb_2.p_out;
  DEFINE diff_vb_3 := vb_3.p_in != vb_3.p_out;
  DEFINE diff_vb_4 := vb_4.p_in != vb_4.p_out;
  DEFINE diff_vb_5 := vb_5.p_in != vb_5.p_out;
  DEFINE diff_vb_6 := vb_6.p_in != vb_6.p_out;
  DEFINE diff_vb_7 := vb_7.p_in != vb_7.p_out;
  DEFINE diff_vb_8 := vb_8.p_in != vb_8.p_out;
  DEFINE diff_vb_9 := vb_9.p_in != vb_9.p_out;
  DEFINE diff_vb_10 := vb_10.p_in != vb_10.p_out;
  DEFINE diff_vb_11 := vb_11.p_in != vb_11.p_out;
  DEFINE diff_vb_12 := vb_12.p_in != vb_12.p_out;


MODULE VALVE_CHAIN_14 (p_in, vc_open, t_#delta)
  VAR vb_1 : VALVE_BLOCK(p_in, vc_open, t_#delta);
  VAR pp_12 : PIPE(vb_1.p_out, 2, 3, t_#delta);
  VAR vb_2 : VALVE_BLOCK(pp_12.p_out, vc_open, t_#delta);
  VAR pp_23 : PIPE(vb_2.p_out, 1, 2, t_#delta);
  VAR vb_3 : VALVE_BLOCK(pp_23.p_out, vc_open, t_#delta);
  VAR pp_34 : PIPE(vb_3.p_out, 2, 2, t_#delta);
  VAR vb_4 : VALVE_BLOCK(pp_34.p_out, vc_open, t_#delta);
  VAR pp_45 : PIPE(vb_4.p_out, 2, 2, t_#delta);
  VAR vb_5 : VALVE_BLOCK(pp_45.p_out, vc_open, t_#delta);
  VAR pp_56 : PIPE(vb_5.p_out, 3, 4, t_#delta);
  VAR vb_6 : VALVE_BLOCK(pp_56.p_out, vc_open, t_#delta);
  VAR pp_67 : PIPE(vb_6.p_out, 1, 5, t_#delta);
  VAR vb_7 : VALVE_BLOCK(pp_67.p_out, vc_open, t_#delta);
  VAR pp_78 : PIPE(vb_7.p_out, 2, 4, t_#delta);
  VAR vb_8 : VALVE_BLOCK(pp_78.p_out, vc_open, t_#delta);
  VAR pp_89 : PIPE(vb_8.p_out, 3, 4, t_#delta);
  VAR vb_9 : VALVE_BLOCK(pp_89.p_out, vc_open, t_#delta);
  VAR pp_910 : PIPE(vb_9.p_out, 1, 5, t_#delta);
  VAR vb_10 : VALVE_BLOCK(pp_910.p_out, vc_open, t_#delta);
  VAR pp_1011 : PIPE(vb_10.p_out, 2, 4, t_#delta);
  VAR vb_11 : VALVE_BLOCK(pp_1011.p_out, vc_open, t_#delta);
  VAR pp_1112 : PIPE(vb_11.p_out, 3, 3, t_#delta);
  VAR vb_12 : VALVE_BLOCK(pp_1112.p_out, vc_open, t_#delta);
  VAR pp_1213 : PIPE(vb_12.p_out, 1, 4, t_#delta);
  VAR vb_13 : VALVE_BLOCK(pp_1213.p_out, vc_open, t_#delta);
  VAR pp_1314 : PIPE(vb_13.p_out, 2, 3, t_#delta);
  VAR vb_14 : VALVE_BLOCK(pp_1314.p_out, vc_open, t_#delta);
  DEFINE p_out := vb_4.p_out;
  DEFINE NR_FAILURES :=
    vb_1.v.NR_FAILURES +
    vb_2.v.NR_FAILURES +
    vb_3.v.NR_FAILURES +
    vb_4.v.NR_FAILURES +
    vb_5.v.NR_FAILURES +
    vb_6.v.NR_FAILURES +
    vb_7.v.NR_FAILURES +
    vb_8.v.NR_FAILURES +
    vb_9.v.NR_FAILURES + 
    vb_10.v.NR_FAILURES +
    vb_11.v.NR_FAILURES +
    vb_12.v.NR_FAILURES +
    vb_13.v.NR_FAILURES + 
    vb_14.v.NR_FAILURES;

  DEFINE diff_vb_2 := vb_2.p_in != vb_2.p_out;
  DEFINE diff_vb_3 := vb_3.p_in != vb_3.p_out;
  DEFINE diff_vb_4 := vb_4.p_in != vb_4.p_out;
  DEFINE diff_vb_5 := vb_5.p_in != vb_5.p_out;
  DEFINE diff_vb_6 := vb_6.p_in != vb_6.p_out;
  DEFINE diff_vb_7 := vb_7.p_in != vb_7.p_out;
  DEFINE diff_vb_8 := vb_8.p_in != vb_8.p_out;
  DEFINE diff_vb_9 := vb_9.p_in != vb_9.p_out;
  DEFINE diff_vb_10 := vb_10.p_in != vb_10.p_out;
  DEFINE diff_vb_11 := vb_11.p_in != vb_11.p_out;
  DEFINE diff_vb_12 := vb_12.p_in != vb_12.p_out;
  DEFINE diff_vb_13 := vb_13.p_in != vb_13.p_out;
  DEFINE diff_vb_14 := vb_14.p_in != vb_14.p_out;


MODULE VALVE_CHAIN_16 (p_in, vc_open, t_#delta)
  VAR vb_1 : VALVE_BLOCK(p_in, vc_open, t_#delta);
  VAR pp_12 : PIPE(vb_1.p_out, 2, 3, t_#delta);
  VAR vb_2 : VALVE_BLOCK(pp_12.p_out, vc_open, t_#delta);
  VAR pp_23 : PIPE(vb_2.p_out, 1, 2, t_#delta);
  VAR vb_3 : VALVE_BLOCK(pp_23.p_out, vc_open, t_#delta);
  VAR pp_34 : PIPE(vb_3.p_out, 2, 2, t_#delta);
  VAR vb_4 : VALVE_BLOCK(pp_34.p_out, vc_open, t_#delta);
  VAR pp_45 : PIPE(vb_4.p_out, 2, 2, t_#delta);
  VAR vb_5 : VALVE_BLOCK(pp_45.p_out, vc_open, t_#delta);
  VAR pp_56 : PIPE(vb_5.p_out, 3, 4, t_#delta);
  VAR vb_6 : VALVE_BLOCK(pp_56.p_out, vc_open, t_#delta);
  VAR pp_67 : PIPE(vb_6.p_out, 1, 5, t_#delta);
  VAR vb_7 : VALVE_BLOCK(pp_67.p_out, vc_open, t_#delta);
  VAR pp_78 : PIPE(vb_7.p_out, 2, 4, t_#delta);
  VAR vb_8 : VALVE_BLOCK(pp_78.p_out, vc_open, t_#delta);
  VAR pp_89 : PIPE(vb_8.p_out, 3, 4, t_#delta);
  VAR vb_9 : VALVE_BLOCK(pp_89.p_out, vc_open, t_#delta);
  VAR pp_910 : PIPE(vb_9.p_out, 1, 5, t_#delta);
  VAR vb_10 : VALVE_BLOCK(pp_910.p_out, vc_open, t_#delta);
  VAR pp_1011 : PIPE(vb_10.p_out, 2, 4, t_#delta);
  VAR vb_11 : VALVE_BLOCK(pp_1011.p_out, vc_open, t_#delta);
  VAR pp_1112 : PIPE(vb_11.p_out, 3, 3, t_#delta);
  VAR vb_12 : VALVE_BLOCK(pp_1112.p_out, vc_open, t_#delta);
  VAR pp_1213 : PIPE(vb_12.p_out, 1, 4, t_#delta);
  VAR vb_13 : VALVE_BLOCK(pp_1213.p_out, vc_open, t_#delta);
  VAR pp_1314 : PIPE(vb_13.p_out, 2, 3, t_#delta);
  VAR vb_14 : VALVE_BLOCK(pp_1314.p_out, vc_open, t_#delta);
  VAR pp_1415 : PIPE(vb_14.p_out, 6, 8, t_#delta);
  VAR vb_15 : VALVE_BLOCK(pp_1415.p_out, vc_open, t_#delta);
  VAR pp_1516 : PIPE(vb_15.p_out, 7, 10, t_#delta);
  VAR vb_16 : VALVE_BLOCK(pp_1516.p_out, vc_open, t_#delta);
  DEFINE p_out := vb_4.p_out;
  DEFINE NR_FAILURES :=
    vb_1.v.NR_FAILURES +
    vb_2.v.NR_FAILURES +
    vb_3.v.NR_FAILURES +
    vb_4.v.NR_FAILURES +
    vb_5.v.NR_FAILURES +
    vb_6.v.NR_FAILURES +
    vb_7.v.NR_FAILURES +
    vb_8.v.NR_FAILURES +
    vb_9.v.NR_FAILURES + 
    vb_10.v.NR_FAILURES +
    vb_11.v.NR_FAILURES +
    vb_12.v.NR_FAILURES +
    vb_13.v.NR_FAILURES + 
    vb_14.v.NR_FAILURES +
    vb_15.v.NR_FAILURES +
    vb_16.v.NR_FAILURES;

  DEFINE diff_vb_2 := vb_2.p_in != vb_2.p_out;
  DEFINE diff_vb_3 := vb_3.p_in != vb_3.p_out;
  DEFINE diff_vb_4 := vb_4.p_in != vb_4.p_out;
  DEFINE diff_vb_5 := vb_5.p_in != vb_5.p_out;
  DEFINE diff_vb_6 := vb_6.p_in != vb_6.p_out;
  DEFINE diff_vb_7 := vb_7.p_in != vb_7.p_out;
  DEFINE diff_vb_8 := vb_8.p_in != vb_8.p_out;
  DEFINE diff_vb_9 := vb_9.p_in != vb_9.p_out;
  DEFINE diff_vb_10 := vb_10.p_in != vb_10.p_out;
  DEFINE diff_vb_11 := vb_11.p_in != vb_11.p_out;
  DEFINE diff_vb_12 := vb_12.p_in != vb_12.p_out;
  DEFINE diff_vb_13 := vb_13.p_in != vb_13.p_out;
  DEFINE diff_vb_14 := vb_14.p_in != vb_14.p_out;
  DEFINE diff_vb_15 := vb_15.p_in != vb_15.p_out;
  DEFINE diff_vb_16 := vb_16.p_in != vb_16.p_out;


------------------------------------------------------ PIPE

MODULE PIPE (p_in, min_pipe_delay, max_pipe_delay, t_#delta)
  -- A pipe implements a delay in the propagation of flow
  -- changes. Here it is assumed that only one such change
  -- can occur at a time, as there is no memory of previous
  -- flow values. This means that before the new value is not
  -- propagated to the output, a second change should not occur.
  --
  -- When a difference in input and output flow is detected,
  -- a timer is started and the output flow is set to the
  -- input flow when the timer reaches the maximum delay.

  VAR p_out : 0..2;
  VAR counter : real;

  DEFINE
    timed := t_#delta > 0;

  ASSIGN init(p_out) := p_in;
  ASSIGN next(p_out) := case
    p_in != p_out & counter < min_pipe_delay : p_out;
    p_in != p_out & counter >= min_pipe_delay & counter < max_pipe_delay : {p_out, p_in};
    TRUE : p_in;
    esac;

  ASSIGN init(counter) := -1;
  ASSIGN next(counter) := case
    next(p_in = p_out) : -1;
    counter = -1 : 0;
    TRUE : counter + t_#delta;
    esac;

  -- Timed transitions need to be interrupted as soon as
  -- the maximum pipe delay is reached.
  TRANS counter + t_#delta <= max_pipe_delay;

  -- No pressure propagation during timed transitions.
  TRANS
    p_out != next(p_out) -> !timed;

  INVARSPEC (timed -> (p_out=next(p_out) & p_in=next(p_in)));
  INVARSPEC counter <= max_pipe_delay;
  INVARSPEC (next(p_in != p_out) & counter = -1) -> (p_in = p_out);
  INVARSPEC (p_in != p_out) -> (p_in >= next(p_in));