
#include "cassini_param_common.smv"

MODULE main

  -- time

  IVAR t_#delta : real;
  TRANS t_#delta >= 0;
  DEFINE timed := t_#delta > 0;

  -- No two consecutive timed transitions.
  VAR done_delta : boolean;
  INIT !done_delta
  TRANS timed -> !done_delta & next(done_delta);
  TRANS !timed -> !next(done_delta);

  -- configuration modes

  FROZENVAR config_helium_segment : {standard, backup};
  FROZENVAR config_fuel_segment : {standard, backup};

  -- tanks, valves, and pipes;

  VAR HT  : HELIUMTANK (t_#delta);

  VAR V1  : VALVE (HT.p_out, t_#delta);
  VAR V2  : VALVE (HT.p_out, t_#delta);
  VAR PV1 : PYROVALVE (V1.p_out, t_#delta);
  VAR PV2 : PYROVALVE (V2.p_out, t_#delta);

  INVAR V1.state = open <-> config_helium_segment = backup;
  INVAR V2.state = open <-> config_helium_segment = standard;
  INVAR PV1.state = open <-> config_helium_segment = backup;
  INVAR PV2.state = open <-> config_helium_segment = standard;

  DEFINE pv1_pv2_p_out := COMBO_OUT(PV1, PV2);

  VAR PP1 : PIPE(pv1_pv2_p_out, 5, 7, t_#delta);

  VAR V3  : VALVE (PP1.p_out, t_#delta);
  VAR V4  : VALVE (PP1.p_out, t_#delta);
  VAR PV3 : PYROVALVE (PP1.p_out, t_#delta);
  VAR PV4 : PYROVALVE (PP1.p_out, t_#delta);

  INVAR V3.state = open <-> config_helium_segment = standard;
  INVAR V4.state = open <-> config_helium_segment = standard;
  INVAR PV3.state = open <-> config_helium_segment = backup;
  INVAR PV4.state = open <-> config_helium_segment = backup;

  DEFINE v3_pv3_p_out := COMBO_OUT(V3, PV3);
  DEFINE v4_pv4_p_out := COMBO_OUT(V4, PV4);

  VAR FT : PROPELLANTTANK (v3_pv3_p_out, t_#delta);
  VAR OT : PROPELLANTTANK (v4_pv4_p_out, t_#delta);

  VAR PV5 : PYROVALVE (FT.p_out, t_#delta);
  VAR PV6 : PYROVALVE (OT.p_out, t_#delta);
  VAR PV7 : PYROVALVE (FT.p_out, t_#delta);
  VAR PV8 : PYROVALVE (OT.p_out, t_#delta);

  INVAR PV5.state = open <-> config_fuel_segment = standard;
  INVAR PV6.state = open <-> config_fuel_segment = standard;
  INVAR PV7.state = open <-> config_fuel_segment = backup;
  INVAR PV8.state = open <-> config_fuel_segment = backup;

  VAR V9_SEGMENT : VALVE_CHAIN_2 (PV5.p_out, config_fuel_segment=standard, t_#delta);
  VAR V10_SEGMENT : VALVE_CHAIN_2 (PV6.p_out, config_fuel_segment=standard, t_#delta);
  VAR V11_SEGMENT : VALVE_CHAIN_2 (PV7.p_out, config_fuel_segment=backup, t_#delta);
  VAR V12_SEGMENT : VALVE_CHAIN_2 (PV8.p_out, config_fuel_segment=backup, t_#delta);

  VAR V13 : VALVE (V9_SEGMENT.p_out, t_#delta);
  VAR V14 : VALVE (V10_SEGMENT.p_out, t_#delta);
  VAR V15 : VALVE (V11_SEGMENT.p_out, t_#delta);
  VAR V16 : VALVE (V12_SEGMENT.p_out, t_#delta);

  INVAR V13.state = open <-> config_fuel_segment = standard;
  INVAR V14.state = open <-> config_fuel_segment = standard;
  INVAR V15.state = open <-> config_fuel_segment = backup;
  INVAR V16.state = open <-> config_fuel_segment = backup;

  VAR PRIMARY_ENGINE : ENGINE (V13.p_out, V14.p_out, t_#delta);
  VAR BACKUP_ENGINE  : ENGINE (V15.p_out, V16.p_out, t_#delta);

  VAR ACC : ACCELEROMETER (PRIMARY_ENGINE.thrust, BACKUP_ENGINE.thrust, t_#delta);

  DEFINE NR_FAILURES := HT.NR_FAILURES +
                        OT.NR_FAILURES +
                        FT.NR_FAILURES +
                        V1.NR_FAILURES +
                        V2.NR_FAILURES +
                        V3.NR_FAILURES +
                        V4.NR_FAILURES +
                        V13.NR_FAILURES +
                        V14.NR_FAILURES +
                        V15.NR_FAILURES +
                        V16.NR_FAILURES +
                        V9_SEGMENT.NR_FAILURES +
                        V10_SEGMENT.NR_FAILURES +
                        V11_SEGMENT.NR_FAILURES +
                        V12_SEGMENT.NR_FAILURES
                        ;

  ---------------------------------------------------------- OPERATIONAL CONTEXT

  -- CONTEXT RESTRICTIONS

  DEFINE TANKS_ARE_FULL := HT.state=ok & FT.state=ok & OT.state=ok;
  DEFINE TANKS_ARE_FULL_AND_PRESSURIZED := TANKS_ARE_FULL & !FT.no_helium & !OT.no_helium;

  INVAR TANKS_ARE_FULL;
  --INVAR TANKS_ARE_FULL_AND_PRESSURIZED;

  -- at most one failure
  INVAR NR_FAILURES < 2;


  ------------------------------------------------------- FAULT DYNAMICS (TANKS)

  --INVAR HT.internal_leakage = none;
  INIT HT.internal_leakage = none;
  TRANS HT.internal_leakage = leakage -> next(HT.internal_leakage = leakage);

  --INVAR FT.internal_leakage = none;
  INIT FT.internal_leakage = none;
  TRANS FT.internal_leakage = leakage -> next(FT.internal_leakage = leakage);

  --INVAR OT.internal_leakage = none;
  INIT OT.internal_leakage = none;
  TRANS OT.internal_leakage = leakage -> next(OT.internal_leakage = leakage);


  ------------------------------------------------------ FAULT DYNAMICS (VALVES)

  INVAR V1.internal_leakage = none;
  INIT V1.internal_leakage = none;
  TRANS V1.internal_leakage = leakage -> next(V1.internal_leakage = leakage);
  INVAR !V1.is_stuck;

  --INVAR V2.internal_leakage = none;
  INIT V2.internal_leakage = none;
  TRANS V2.internal_leakage = leakage -> next(V2.internal_leakage = leakage);
  INVAR !V2.is_stuck;

  --INVAR V3.internal_leakage = none;
  INIT V3.internal_leakage = none;
  TRANS V3.internal_leakage = leakage -> next(V3.internal_leakage = leakage);
  INVAR !V3.is_stuck;

  --INVAR V4.internal_leakage = none;
  INIT V4.internal_leakage = none;
  TRANS V4.internal_leakage = leakage -> next(V4.internal_leakage = leakage);
  INVAR !V4.is_stuck;

  INVAR V13.internal_leakage = none;
  INIT V13.internal_leakage = none;
  TRANS V13.internal_leakage = leakage -> next(V13.internal_leakage = leakage);
  INVAR !V13.is_stuck;

  INVAR V14.internal_leakage = none;
  INIT V14.internal_leakage = none;
  TRANS V14.internal_leakage = leakage -> next(V14.internal_leakage = leakage);
  INVAR !V14.is_stuck;

  INVAR V15.internal_leakage = none;
  INIT V15.internal_leakage = none;
  TRANS V15.internal_leakage = leakage -> next(V15.internal_leakage = leakage);
  INVAR !V15.is_stuck;

  INVAR V16.internal_leakage = none;
  INIT V16.internal_leakage = none;
  TRANS V16.internal_leakage = leakage -> next(V16.internal_leakage = leakage);
  INVAR !V16.is_stuck;