#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; | |