diff options
Diffstat (limited to 'tests/examplefiles/guidance.smv')
| -rw-r--r-- | tests/examplefiles/guidance.smv | 1124 |
1 files changed, 1124 insertions, 0 deletions
diff --git a/tests/examplefiles/guidance.smv b/tests/examplefiles/guidance.smv new file mode 100644 index 00000000..671d1e1c --- /dev/null +++ b/tests/examplefiles/guidance.smv @@ -0,0 +1,1124 @@ +-- +-- Shuttle Digital Autopilot +-- by Sergey Berezin (berez@cs.cmu.edu) +-- +MODULE cont_3eo_mode_select(start,smode5,vel,q_bar,apogee_alt_LT_alt_ref, + h_dot_LT_hdot_reg2,alpha_n_GRT_alpha_reg2, + delta_r_GRT_del_r_usp,v_horiz_dnrng_LT_0, + high_rate_sep,meco_confirmed) + +VAR cont_3EO_start: boolean; + RTLS_abort_declared: boolean; + region_selected : boolean; + m_mode: {mm102, mm103, mm601}; + r: {reg-1, reg0, reg1, reg2, reg3, reg102}; + step : {1,2,3,4,5,6,7,8,9,10, exit, undef}; + +ASSIGN + init(cont_3EO_start) := FALSE; + init(m_mode) := {mm102, mm103}; + init(region_selected) := FALSE; + init(RTLS_abort_declared) := FALSE; + init(r) := reg-1; + init(step) := undef; + + next(step) := + case + step = 1 & m_mode = mm102 : exit; + step = 1 : 2; + step = 2 & smode5 : 5; + step = 2 & vel = GRT_vi_3eo_max: exit; + step = 2 : 3; + step = 3 & vel = LEQ_vi_3eo_min : 6; + step = 3 : 4; + step = 4 & apogee_alt_LT_alt_ref: exit; + step = 4 : 6; + step = 5 : 6; + step = 6 & r = reg0 : exit; + step = 6 : 7; + step = 7 : 8; + step = 8 & q_bar = GRT_qbar_reg3 & !high_rate_sep : 10; + step = 8 : 9; + step = 9 : 10; + step = 10: exit; + next(start): 1; + step = exit : undef; + TRUE: step; + esac; + + next(cont_3EO_start) := + case + step = 1 & m_mode = mm102 : TRUE; + step = 10 & meco_confirmed : TRUE; + TRUE : cont_3EO_start; + esac; + + next(r) := + case + step = 1 & m_mode = mm102 : reg102; + step = 2 & !smode5 & vel = GRT_vi_3eo_max: reg0; + step = 4 & apogee_alt_LT_alt_ref: reg0; + step = 5 & v_horiz_dnrng_LT_0 & delta_r_GRT_del_r_usp : reg0; + step = 8 & q_bar = GRT_qbar_reg3 & !high_rate_sep : reg3; + step = 9: case + (h_dot_LT_hdot_reg2 & alpha_n_GRT_alpha_reg2 & + q_bar = GRT_qbar_reg1) | high_rate_sep : reg2; + TRUE : reg1; + esac; + next(step) = 1 : reg-1; + TRUE: r; + esac; + + next(RTLS_abort_declared) := + case + step = 10 & meco_confirmed & m_mode = mm103 : TRUE; + TRUE: RTLS_abort_declared; + esac; + + next(m_mode) := + case + step = 10 & meco_confirmed & m_mode = mm103 : mm601; + TRUE: m_mode; + esac; + + next(region_selected) := + case + next(step) = 1 : FALSE; + next(step) = exit : TRUE; + TRUE : region_selected; + esac; + +MODULE cont_3eo_guide(start,cont_3EO_start, mode_select_completed, et_sep_cmd, + h_dot_LT_0, q_bar_a_GRT_qbar_max_sep, m_mode, r0, + cont_minus_z_compl, t_nav-t_et_sep_GRT_dt_min_z_102, + ABS_q_orb_GRT_q_minus_z_max, ABS_r_orb_GRT_r_minus_z_max, + excess_OMS_propellant, q_bar_a_LT_qbar_oms_dump, + entry_mnvr_couter_LE_0, rcs_all_jet_inhibit, + alt_GRT_alt_min_102_dump, t_nav-t_gmtlo_LT_t_dmp_last, + pre_sep, cond_18, q_orb_LT_0, ABS_alf_err_LT_alf_sep_err, + cond_20b, cond_21, ABS_beta_n_GRT_beta_max, cond_24, cond_26, + cond_27, cond_29, mm602_OK) +VAR + step: {1,a1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20, + b20, c20, d20, 21,22,23,24,25,26,27,28,29,exit, undef}; + call_RTLS_abort_task : boolean; + first3: boolean; -- indicates if it is the first pass + first8: boolean; + first27: boolean; + s_unconv : boolean; + mode_2_indicator : boolean; + et_sep_man_initiate : boolean; + emerg_sep : boolean; + cont_3eo_pr_delay : {minus_z_reg1, minus_z_reg2, + minus_z_reg3, minus_z_reg4, minus_z_reg102, 0, 5}; + etsep_y_drift : {undef, minus_z_reg1, minus_z_reg2, + minus_z_reg3, minus_z_reg4, minus_z_reg102, 0}; + fwd_rcs_dump_enable : boolean; + fcs_accept_icnct : boolean; + oms_rcs_i_c_inh_ena_cmd : boolean; + orbiter_dump_ena : boolean; + frz_3eo : boolean; + high_rate_sep: boolean; + entry_gains : boolean; + cont_sep_cplt : boolean; + pch_cmd_reg4 : boolean; + alpha_ok : boolean; + r : {reg-1, reg0, reg1, reg2, reg3, reg4, reg102}; + early_sep : boolean; +-------------------------------------------- +----- Additional Variables ----------------- +-------------------------------------------- + rtls_lo_f_d_delay : {undef, 0}; + wcb2 : {undef, reg1_0, reg2_neg4, wcb2_3eo, reg4_0, + reg102_undef, post_sep_0}; + q_gcb_i : {undef, quat_reg1, quat_reg2, quat_reg3, quat_reg4, + quat_reg102_undef, quat_entry_M50_to_cmdbody}; + oms_nz_lim : {undef, oms_nz_lim_3eo, oms_nz_lim_iload, oms_nz_lim_std}; + contingency_nz_lim : {undef, contingency_nz_lim_3eo, + contingency_nz_lim_iload, contingency_nz_lim_std}; + + + +ASSIGN + init(entry_gains) := FALSE; + init(frz_3eo) := FALSE; + init(cont_3eo_pr_delay) := 5; + init(etsep_y_drift) := undef; + init(r) := reg-1; + init(step) := undef; + init(call_RTLS_abort_task) := FALSE; + init(first3) := TRUE; + init(first8) := TRUE; + init(first27) := TRUE; + init(cont_sep_cplt) := FALSE; + init(et_sep_man_initiate) := FALSE; + init(alpha_ok) := FALSE; + init(pch_cmd_reg4) := FALSE; + +-- Assumed initializations: + + init(rtls_lo_f_d_delay) := undef; + init(wcb2) := undef; + init(q_gcb_i) := undef; + init(oms_nz_lim) := undef; + init(contingency_nz_lim) := undef; + init(oms_rcs_i_c_inh_ena_cmd) := FALSE; + init(orbiter_dump_ena) := FALSE; +-- init(early_sep) := FALSE; + +------------- + + next(step) := nextstep; + + next(r) := + case + step = a1 & (cont_3EO_start | mode_select_completed) : r0; + step = 21 & cond_21 : reg4; + step = 23 & ABS_beta_n_GRT_beta_max & !high_rate_sep : reg1; + TRUE : r; + esac; + + next(first3) := + case + step = 3 & cont_3EO_start : FALSE; + TRUE : first3; + esac; + + next(first8) := + case + step = 8 & excess_OMS_propellant & cont_3EO_start : FALSE; + TRUE : first8; + esac; + + next(first27) := + case + step = 27 : FALSE; + TRUE: first27; + esac; + + next(s_unconv) := + case + step = 3 : FALSE; + TRUE : s_unconv; + esac; + + next(call_RTLS_abort_task) := + case + step = 3 : TRUE; + TRUE : call_RTLS_abort_task; + esac; + + next(mode_2_indicator) := + case + step = 4 : TRUE; + TRUE : mode_2_indicator; + esac; + + next(et_sep_man_initiate) := + case + step = 5 & h_dot_LT_0 & q_bar_a_GRT_qbar_max_sep & m_mode != mm102 : TRUE; + step = 14 & pre_sep : TRUE; + step = 19 & q_orb_LT_0 : TRUE; + step = d20 : TRUE; + step = 26 & cond_26 : TRUE; + step = 29 & cond_29 : TRUE; + TRUE : et_sep_man_initiate; + esac; + + next(emerg_sep) := + case + next(step) = 1 : FALSE; + step = 5 & h_dot_LT_0 & q_bar_a_GRT_qbar_max_sep & m_mode != mm102: TRUE; + TRUE : emerg_sep; + esac; + + next(cont_3eo_pr_delay) := + case + next(step) = 1 : 5; + step = 5 & h_dot_LT_0 & q_bar_a_GRT_qbar_max_sep & m_mode != mm102 : + minus_z_reg3; + step = 7 & !cont_minus_z_compl & r = reg102 & + t_nav-t_et_sep_GRT_dt_min_z_102 & + (ABS_q_orb_GRT_q_minus_z_max | ABS_r_orb_GRT_r_minus_z_max) : 0; + step = 14 & pre_sep : minus_z_reg102; + step = 19 & q_orb_LT_0 : minus_z_reg4; + step = d20 : minus_z_reg3; + step = 26 & cond_26 : minus_z_reg2; + step = 27 & first27 : minus_z_reg1; + TRUE : cont_3eo_pr_delay; + esac; + + next(etsep_y_drift) := + case + step = 5 & h_dot_LT_0 & q_bar_a_GRT_qbar_max_sep & m_mode != mm102 : + minus_z_reg3; + step = 7 & !cont_minus_z_compl & r = reg102 & + t_nav-t_et_sep_GRT_dt_min_z_102 & + (ABS_q_orb_GRT_q_minus_z_max | ABS_r_orb_GRT_r_minus_z_max) : 0; + step = 14 & pre_sep : minus_z_reg102; + step = 19 & q_orb_LT_0 : minus_z_reg4; + step = d20 : minus_z_reg3; + step = 26 & cond_26 : minus_z_reg2; + step = 27 & first27 : minus_z_reg1; + TRUE : etsep_y_drift; + esac; + + next(fwd_rcs_dump_enable) := + case + step = 8 & excess_OMS_propellant & first8 : FALSE; + TRUE : fwd_rcs_dump_enable; + esac; + + next(fcs_accept_icnct) := + case + step = 9 & q_bar_a_LT_qbar_oms_dump & r != reg102 : TRUE; + TRUE : fcs_accept_icnct; + esac; + + next(oms_rcs_i_c_inh_ena_cmd) := + case +-- next(step) = 1 & oms_rcs_i_c_inh_ena_cmd : {0,1}; + next(step) = 1 & oms_rcs_i_c_inh_ena_cmd : FALSE; -- Assumed initialization + step = 9 & q_bar_a_LT_qbar_oms_dump & r != reg102 : TRUE; + TRUE : oms_rcs_i_c_inh_ena_cmd; + esac; + + next(orbiter_dump_ena) := + case + next(start) = TRUE : FALSE; -- Assumed initialization + step = 9 & q_bar_a_LT_qbar_oms_dump & r != reg102 : TRUE; + step = 13 & alt_GRT_alt_min_102_dump & t_nav-t_gmtlo_LT_t_dmp_last : TRUE; + TRUE : orbiter_dump_ena; + esac; + + next(frz_3eo) := + case + next(step) = 1 : FALSE; + step = 10 & entry_mnvr_couter_LE_0 & !rcs_all_jet_inhibit : FALSE; + step = 28 & !et_sep_man_initiate : TRUE; + TRUE : frz_3eo; + esac; + + next(high_rate_sep) := + case + step = 10 & entry_mnvr_couter_LE_0 & !rcs_all_jet_inhibit : FALSE; + step = 25 : TRUE; + TRUE : high_rate_sep; + esac; + + next(entry_gains) := + case + next(step) = 1 : FALSE; + step = 10 & entry_mnvr_couter_LE_0 & !rcs_all_jet_inhibit : TRUE; + TRUE : entry_gains; + esac; + + next(cont_sep_cplt) := + case + next(step) = 1 : FALSE; + step = 12 & mm602_OK : TRUE; + TRUE : cont_sep_cplt; + esac; + + next(pch_cmd_reg4) := + case + next(step) = 1 : FALSE; + step = 18 & !pch_cmd_reg4 & cond_18 : TRUE; + TRUE : pch_cmd_reg4; + esac; + + next(alpha_ok) := + case + next(step) = 1 : FALSE; + step = 20 & ABS_alf_err_LT_alf_sep_err : TRUE; + TRUE : alpha_ok; + esac; + + next(early_sep) := + case + step = 27 & first27 : + case + cond_27 : TRUE; + TRUE : FALSE; + esac; + TRUE : early_sep; + esac; + +-------------------------------------------- +----- Additional Variables ----------------- +-------------------------------------------- + + next(rtls_lo_f_d_delay) := + case + next(start) = TRUE : undef; -- Assumed initialization + step = 8 & first8 & excess_OMS_propellant : 0; + TRUE : rtls_lo_f_d_delay; + esac; + + next(wcb2) := + case + next(start) = TRUE : undef; -- Assumed initialization + step = 10 & entry_mnvr_couter_LE_0 : post_sep_0; + step = 12 : case + r = reg4 : reg4_0; + TRUE : wcb2_3eo; + esac; + step = 14 & pre_sep : reg102_undef; + step = 15 : case + r = reg4 : reg4_0; + TRUE : wcb2_3eo; + esac; + step = 25 : reg2_neg4; + TRUE : wcb2; + esac; + + next(q_gcb_i) := + case + next(start) = TRUE : undef; -- Assumed initialization + step = 11 : quat_entry_M50_to_cmdbody; + step = 14 & pre_sep : quat_reg102_undef; + step = 16 : case + r = reg4 : quat_reg4; + TRUE : quat_reg3; + esac; + step = 22 : quat_reg2; + +-- Without this step the value "quat_reg2" would remain in "reg1": +-- step = 23 & ABS_beta_n_GRT_beta_max & !high_rate_sep : undef; + + TRUE : q_gcb_i; + esac; + + next(oms_nz_lim) := + case + next(start) = TRUE : undef; -- Assumed initialization + step = 9 & q_bar_a_LT_qbar_oms_dump & r != reg102 : oms_nz_lim_3eo; + step = 12 & mm602_OK : oms_nz_lim_std; + TRUE : oms_nz_lim; + esac; + + next(contingency_nz_lim) := + case + next(start) = TRUE : undef; -- Assumed initialization + step = 9 & q_bar_a_LT_qbar_oms_dump & r != reg102 : + contingency_nz_lim_3eo; + step = 12 & mm602_OK : contingency_nz_lim_std; + TRUE : contingency_nz_lim; + esac; + +DEFINE + finished := step = exit; + idle := step = undef; + + start_cont_3eo_mode_select := + case + step = 1 & !cont_3EO_start : TRUE; + TRUE : FALSE; + esac; + + nextstep := + case + step = 1 : a1; + step = a1 : case + (cont_3EO_start | mode_select_completed) : 2; + TRUE : step; + esac; + step = 2 : case + !cont_3EO_start : exit; + first3 : 3; + TRUE: 4; + esac; + step = 3 : 4; + step = 4 : case + et_sep_cmd : 7; + TRUE : 5; + esac; + step = 5 : case + h_dot_LT_0 & q_bar_a_GRT_qbar_max_sep & + m_mode != mm102 : exit; + TRUE : 6; + esac; + step = 6 : + case + r = reg102 : 13; + r in {reg3, reg4} : 15; + r = reg2 : 22; + r = reg1 : 27; + TRUE : exit; + esac; + step = 7 : case + cont_minus_z_compl : 8; + TRUE : exit; + esac; + step = 8 : case + excess_OMS_propellant & first8 : 9; + TRUE : 10; + esac; + step = 9 : exit; + step = 10 : case + !entry_mnvr_couter_LE_0 | rcs_all_jet_inhibit : exit; + TRUE : 11; + esac; + step = 11 : 12; + step = 12 : exit; + step = 13 : 14; + step = 14 : exit; + step = 15 : 16; + step = 16 : 17; + step = 17 : case + r = reg4 : 18; + TRUE : 20; + esac; + step = 18 : case + pch_cmd_reg4 | cond_18 : 19; + TRUE : exit; + esac; + step = 19 : exit; + step = 20 : case + ABS_alf_err_LT_alf_sep_err : b20; + TRUE : c20; + esac; + step = b20 : case + cond_20b : d20; + TRUE : exit; + esac; + step = c20 : case + alpha_ok : d20; + TRUE : 21; + esac; + step = d20 : exit; + TRUE : nextstep21; + esac; + + nextstep21 := + case + step = 21 : case + cond_21 : 15; + TRUE : exit; + esac; + step = 22 : 23; + step = 23 : case + ABS_beta_n_GRT_beta_max & !high_rate_sep : 27; + TRUE : 24; + esac; + step = 24 : case + cond_24 | high_rate_sep : 25; + TRUE : exit; + esac; + step = 25 : 26; + step = 26 : exit; + step = 27 : 28; + step = 28 : case + !et_sep_man_initiate : 29; + TRUE : exit; + esac; + step = 29 : exit; + start : 1; + step = exit : undef; + TRUE : step; + esac; + + post_sep_mode := step in {7,8,9,10,11,12}; + +------------------------------------------------------------------ +------------------------------------------------------------------ + +MODULE main +VAR + smode5: boolean; + vel : {GRT_vi_3eo_max, GRT_vi_3eo_min, LEQ_vi_3eo_min}; + q_bar: {GRT_qbar_reg3, GRT_qbar_reg1, LEQ_qbar_reg1}; + q_bar_a_GRT_qbar_max_sep : boolean; + q_bar_a_LT_qbar_oms_dump : boolean; + apogee_alt_LT_alt_ref : boolean; + h_dot_LT_hdot_reg2 : boolean; + h_dot_LT_0 : boolean; + alpha_n_GRT_alpha_reg2 : boolean; + delta_r_GRT_del_r_usp : boolean; + v_horiz_dnrng_LT_0: boolean; + meco_confirmed: boolean; + et_sep_cmd : boolean; + cont_minus_z_compl : boolean; + t_nav-t_et_sep_GRT_dt_min_z_102 : boolean; + ABS_q_orb_GRT_q_minus_z_max : boolean; + ABS_r_orb_GRT_r_minus_z_max : boolean; + excess_OMS_propellant : boolean; + entry_mnvr_couter_LE_0 : boolean; + rcs_all_jet_inhibit : boolean; + alt_GRT_alt_min_102_dump : boolean; + t_nav-t_gmtlo_LT_t_dmp_last : boolean; + pre_sep : boolean; + cond_18 : boolean; + q_orb_LT_0 : boolean; + ABS_alf_err_LT_alf_sep_err : boolean; + cond_20b : boolean; + cond_21 : boolean; + ABS_beta_n_GRT_beta_max : boolean; + cond_24 : boolean; + cond_26 : boolean; + cond_27 : boolean; + cond_29 : boolean; + mm602_OK : boolean; + start_guide : boolean; + mated_coast_mnvr : boolean; + + cs: cont_3eo_mode_select(cg.start_cont_3eo_mode_select, + smode5,vel,q_bar,apogee_alt_LT_alt_ref, + h_dot_LT_hdot_reg2,alpha_n_GRT_alpha_reg2, + delta_r_GRT_del_r_usp,v_horiz_dnrng_LT_0, + cg.high_rate_sep,meco_confirmed); + + cg: cont_3eo_guide(start_guide, + cs.cont_3EO_start, cs.region_selected, et_sep_cmd, + h_dot_LT_0, q_bar_a_GRT_qbar_max_sep, cs.m_mode, cs.r, + cont_minus_z_compl, t_nav-t_et_sep_GRT_dt_min_z_102, + ABS_q_orb_GRT_q_minus_z_max, ABS_r_orb_GRT_r_minus_z_max, + excess_OMS_propellant, q_bar_a_LT_qbar_oms_dump, + entry_mnvr_couter_LE_0, rcs_all_jet_inhibit, + alt_GRT_alt_min_102_dump, t_nav-t_gmtlo_LT_t_dmp_last, + pre_sep, cond_18, q_orb_LT_0, ABS_alf_err_LT_alf_sep_err, + cond_20b, cond_21, ABS_beta_n_GRT_beta_max, cond_24, cond_26, + cond_27, cond_29, mm602_OK); + +ASSIGN + init(start_guide) := FALSE; + init(mated_coast_mnvr) := FALSE; + + next(entry_mnvr_couter_LE_0) := + case + !entry_mnvr_couter_LE_0 : {FALSE, TRUE}; + TRUE : TRUE; + esac; + +--------------------------------------------------------------------- +--------------------------------------------------------------------- + next(start_guide) := + case + start_guide : FALSE; + !cg.idle : FALSE; + TRUE : {FALSE, TRUE}; + esac; + + next(smode5) := + case + fixed_values : smode5; + cg.idle : { FALSE, TRUE }; + TRUE : smode5; + esac; + + next(vel) := + case + fixed_values : vel; + cg.idle : {GRT_vi_3eo_max, GRT_vi_3eo_min, LEQ_vi_3eo_min}; + TRUE : vel; + esac; + + next(q_bar) := + case + fixed_values : q_bar; + cg.idle : {GRT_qbar_reg3, GRT_qbar_reg1, LEQ_qbar_reg1}; + TRUE : q_bar; + esac; + + next(q_bar_a_GRT_qbar_max_sep) := + case + fixed_values : q_bar_a_GRT_qbar_max_sep; + cg.idle : { FALSE, TRUE }; + TRUE : q_bar_a_GRT_qbar_max_sep; + esac; + + next(apogee_alt_LT_alt_ref) := + case + fixed_values : apogee_alt_LT_alt_ref; + cg.idle : { FALSE, TRUE }; + TRUE : apogee_alt_LT_alt_ref; + esac; + + next(h_dot_LT_hdot_reg2) := + case + fixed_values : h_dot_LT_hdot_reg2; + cg.idle : { FALSE, TRUE }; + TRUE : h_dot_LT_hdot_reg2; + esac; + + next(h_dot_LT_0) := + case + fixed_values : h_dot_LT_0; + cg.idle : { FALSE, TRUE }; + TRUE : h_dot_LT_0; + esac; + + next(alpha_n_GRT_alpha_reg2) := + case + fixed_values : alpha_n_GRT_alpha_reg2; + cg.idle : { FALSE, TRUE }; + TRUE : alpha_n_GRT_alpha_reg2; + esac; + + next(delta_r_GRT_del_r_usp) := + case + fixed_values : delta_r_GRT_del_r_usp; + cg.idle : { FALSE, TRUE }; + TRUE : delta_r_GRT_del_r_usp; + esac; + + next(v_horiz_dnrng_LT_0) := + case + fixed_values : v_horiz_dnrng_LT_0; + cg.idle : { FALSE, TRUE }; + TRUE : v_horiz_dnrng_LT_0; + esac; + + next(meco_confirmed) := + case + fixed_values : meco_confirmed; + meco_confirmed : TRUE; + cg.idle : { FALSE, TRUE }; + TRUE : meco_confirmed; + esac; + + next(et_sep_cmd) := + case + fixed_values : et_sep_cmd; + et_sep_cmd : TRUE; + cg.idle : { FALSE, TRUE }; + TRUE : et_sep_cmd; + esac; + + next(cont_minus_z_compl) := + case + fixed_values : cont_minus_z_compl; + cg.idle : { FALSE, TRUE }; + TRUE : cont_minus_z_compl; + esac; + + next(t_nav-t_et_sep_GRT_dt_min_z_102) := + case + fixed_values : t_nav-t_et_sep_GRT_dt_min_z_102; + cg.idle : { FALSE, TRUE }; + TRUE : t_nav-t_et_sep_GRT_dt_min_z_102; + esac; + + next(ABS_q_orb_GRT_q_minus_z_max) := + case + fixed_values : ABS_q_orb_GRT_q_minus_z_max; + cg.idle : { FALSE, TRUE }; + TRUE : ABS_q_orb_GRT_q_minus_z_max; + esac; + + next(ABS_r_orb_GRT_r_minus_z_max) := + case + fixed_values : ABS_r_orb_GRT_r_minus_z_max; + cg.idle : { FALSE, TRUE }; + TRUE : ABS_r_orb_GRT_r_minus_z_max; + esac; + + next(excess_OMS_propellant) := + case + fixed_values : excess_OMS_propellant; + cg.idle & excess_OMS_propellant : { FALSE, TRUE }; + TRUE : excess_OMS_propellant; + esac; + + next(q_bar_a_LT_qbar_oms_dump) := + case + fixed_values : q_bar_a_LT_qbar_oms_dump; + cg.idle : { FALSE, TRUE }; + TRUE : q_bar_a_LT_qbar_oms_dump; + esac; + + next(rcs_all_jet_inhibit) := + case + fixed_values : rcs_all_jet_inhibit; + cg.idle : { FALSE, TRUE }; + TRUE : rcs_all_jet_inhibit; + esac; + + next(alt_GRT_alt_min_102_dump) := + case + fixed_values : alt_GRT_alt_min_102_dump; + cg.idle : { FALSE, TRUE }; + TRUE : alt_GRT_alt_min_102_dump; + esac; + + next(t_nav-t_gmtlo_LT_t_dmp_last) := + case + fixed_values : t_nav-t_gmtlo_LT_t_dmp_last; + cg.idle : { FALSE, TRUE }; + TRUE : t_nav-t_gmtlo_LT_t_dmp_last; + esac; + + next(pre_sep) := + case + fixed_values : pre_sep; + cg.idle : { FALSE, TRUE }; + TRUE : pre_sep; + esac; + + next(cond_18) := + case + fixed_values : cond_18; + cg.idle : { FALSE, TRUE }; + TRUE : cond_18; + esac; + + next(q_orb_LT_0) := + case + fixed_values : q_orb_LT_0; + cg.idle : { FALSE, TRUE }; + TRUE : q_orb_LT_0; + esac; + + next(ABS_alf_err_LT_alf_sep_err) := + case + fixed_values : ABS_alf_err_LT_alf_sep_err; + cg.idle : { FALSE, TRUE }; + TRUE : ABS_alf_err_LT_alf_sep_err; + esac; + + next(cond_20b) := + case + fixed_values : cond_20b; + cg.idle : { FALSE, TRUE }; + TRUE : cond_20b; + esac; + + next(cond_21) := + case + fixed_values : cond_21; + cg.idle : { FALSE, TRUE }; + TRUE : cond_21; + esac; + + next(ABS_beta_n_GRT_beta_max) := + case + fixed_values : ABS_beta_n_GRT_beta_max; + cg.idle : { FALSE, TRUE }; + TRUE : ABS_beta_n_GRT_beta_max; + esac; + + next(cond_24) := + case + fixed_values : cond_24; + cg.idle : { FALSE, TRUE }; + TRUE : cond_24; + esac; + + next(cond_26) := + case + fixed_values : cond_26; + cg.idle : { FALSE, TRUE }; + TRUE : cond_26; + esac; + + next(cond_27) := + case + fixed_values : cond_27; + cg.idle : { FALSE, TRUE }; + TRUE : cond_27; + esac; + + next(cond_29) := + case + fixed_values : cond_29; + cg.idle : { FALSE, TRUE }; + TRUE : cond_29; + esac; + + next(mm602_OK) := + case + fixed_values : mm602_OK; + cg.idle : { FALSE, TRUE }; + TRUE : mm602_OK; + esac; + + next(mated_coast_mnvr) := + case + next(cg.step) = 1 : FALSE; + cg.step = 6 & cg.r in {reg1, reg2, reg3, reg4, reg102} : TRUE; + TRUE : mated_coast_mnvr; + esac; + +--------------------------------------------------------------------- +--------------------------------------------------------------------- +DEFINE + fixed_values := FALSE; + + output_ok := + case + cg.q_gcb_i = undef | cg.wcb2 = undef | + cg.cont_3eo_pr_delay = 5 | + cg.etsep_y_drift = undef : + case + !mated_coast_mnvr: 1; + TRUE : undef; + esac; + !mated_coast_mnvr: toint(cg.q_gcb_i = quat_entry_M50_to_cmdbody & + cg.wcb2 = post_sep_0); +-- reg1 never happens? +-- cg.r = reg1 : (cg.q_gcb_i = quat_reg1 & cg.wcb2 = reg1_0 & +-- cg.cont_3eo_pr_delay = minus_z_reg1 & +-- cg.etsep_y_drift = minus_z_reg1) | cg.emerg_sep; + cg.r = reg2 : toint((cg.q_gcb_i = quat_reg2 & cg.wcb2 = reg2_neg4 & + cg.cont_3eo_pr_delay = minus_z_reg2 & + cg.etsep_y_drift = minus_z_reg2) | cg.emerg_sep); + + cg.r = reg3 : toint((cg.q_gcb_i = quat_reg3 & cg.wcb2 = wcb2_3eo & + cg.cont_3eo_pr_delay = minus_z_reg3 & + cg.etsep_y_drift = minus_z_reg3) | cg.emerg_sep); + cg.r = reg4 : toint((cg.q_gcb_i = quat_reg4 & cg.wcb2 = reg4_0 & + cg.cont_3eo_pr_delay = minus_z_reg4 & + cg.etsep_y_drift = minus_z_reg4) | cg.emerg_sep); + cg.r = reg102 : toint((cg.q_gcb_i = quat_reg102_undef & + cg.wcb2 = reg102_undef & + cg.cont_3eo_pr_delay = minus_z_reg102 & + cg.etsep_y_drift = minus_z_reg102) | cg.emerg_sep); + TRUE : 0; + esac; + +--------------------------------------------------------------------- +-------- Specifications --------------------------------------------- +--------------------------------------------------------------------- + +-- Contingency Guide terminates + +SPEC AG(!cg.idle -> AF(cg.finished)) + +-- Contingency guide can be executed infinitely often + +SPEC AG( (cg.idle | cg.finished) -> + EF(!(cg.idle | cg.finished) & EF(cg.finished))) + +-- Contingency mode select task works fine + +SPEC AG(cs.cont_3EO_start & cs.region_selected -> + ((cs.m_mode = mm102 | meco_confirmed) & + cs.r != reg-1 & cs.r != reg0)) + +-- Bad (initial) value never happens again once region is computed +-- unless we restart the task + +--SPEC AG(cs.r != reg-1 -> !E[!cg.start_cont_3eo_mode_select U +-- cs.r = reg-1 & !cg.start_cont_3eo_mode_select]) + +-- Comment out each of the regions and see if this is still true +-- (Check, if ALL of the regions can happen) + +--SPEC AG(cs.r in {reg-1 +-- ,reg0 +-- ,reg1 +-- ,reg2 +-- ,reg3 +-- ,reg102 +-- }) + +-- Comment out each of the regions and see if this is still true +-- (Check, if ALL of the regions can happen) + +--SPEC AG(cg.r in {reg-1 +-- ,reg0 +-- ,reg1 +-- ,reg2 +-- ,reg3 +-- ,reg4 +-- ,reg102 +-- }) + +-- Mode_select starts at the next step after its "start" bit is set: + +--SPEC AG(!cg.start_cont_3eo_mode_select -> +-- AX(cg.start_cont_3eo_mode_select & cs.step in {exit, undef} -> +-- AX(cs.step = 1 & !cs.region_selected))) + +-- During major mode 103, the inertial velocity is monitored. +-- Below an I-loaded velocity, a MECO would constitute a contingency +-- abort. (Must NOT be in SMODE=5 (??)) + +SPEC AG(cg.start_cont_3eo_mode_select & cs.m_mode = mm103 & + vel = LEQ_vi_3eo_min & meco_confirmed & !smode5 -> + A[!cs.region_selected U cs.region_selected & cs.cont_3EO_start]) + +-- Above a certain inertial velocity (in mode 103), the 3E/O field +-- is blanked, indicating that a MECO at this point would not require +-- an OPS 6 contingency abort. + +SPEC AG(cs.region_selected -> + (cs.m_mode = mm103 & vel = GRT_vi_3eo_max -> !cs.cont_3EO_start)) + +-- Between the two velocities, an apogee altitude - velocity curve is +-- constructed based on the current inertial velocity. If the apogee +-- altitude is above this curve, a contingency abort capability is +-- still required and a 3E/O region index will be calculated. +-- Otherwise, the 3E/O field is blanked out and no further contingency +-- abort calculations will be performed. (Must NOT be in SMODE=5 (??)) + +SPEC AG(cg.start_cont_3eo_mode_select & cs.m_mode = mm103 & + vel = GRT_vi_3eo_min & meco_confirmed & !smode5 -> + A[!cs.region_selected U cs.region_selected & + apogee_alt_LT_alt_ref = !cs.cont_3EO_start]) + +-- For an RTLS trajectory (SMODE=5), a check is made on the downrange +-- velocity to see if the vehicle is heading away from the landing site. +-- If this is the case, a 3E/O region index is calculated. If the vehicle +-- is heading back to the landing site, and the current range to the MECO +-- R-V line is greater than an I-loaded value, a 3E/O region index is +-- calculated. Otherwise, an intact abort is possible and the 3E/O field +-- is blanked. + +SPEC AG(cg.start_cont_3eo_mode_select & smode5 & meco_confirmed & + (!v_horiz_dnrng_LT_0 | !delta_r_GRT_del_r_usp) -> + A[!cs.region_selected U cs.region_selected & cs.cont_3EO_start]) + +-- If this task is called prior to SRB separation [mm102], the 3E/O region +-- index is set to 102 and the 3E/O contingency flag is set. + +SPEC AG(cs.m_mode = mm102 & cg.start_cont_3eo_mode_select -> + AX (A [ !cs.region_selected U cs.region_selected & + cs.r = reg102 & cs.cont_3EO_start])) + +-- After SRB separation, on every pass that the 3E/O region index is +-- calculated, a check is made to see if MECO confirmed has occured. If +-- so, a check is made to see if the major mode is 103. If so, an RTLS is +-- automatically invoked to transition to major mode 601. + +SPEC AG(!cs.region_selected & cs.m_mode = mm103 & meco_confirmed -> + A[!cs.region_selected U cs.region_selected & cs.r != reg0 -> + cs.m_mode = mm601 & cs.RTLS_abort_declared]) + +-- Once the 3E/O contingency flag has been set, this task is no longer +-- executed. + +SPEC AG(cs.cont_3EO_start -> AG(!cg.start_cont_3eo_mode_select)) + +-- If MECO confirmed occurs in MM103 and an OPS 6 contingency abort +-- procedure is still required, contingency 3E/O guidance sets the +-- CONT_3EO_START flag ON. Contingency 3E/O guidance then switches +-- from its display support function into an actual auto guidance +-- steering process. [...] Contingency 3E/O guidance sets the RTLS abort +-- declared flag and the MSC performs the transition from from major mode +-- 103 to 601. + +SPEC AG(!cg.idle & !cg.finished & !cs.region_selected & cs.m_mode = mm103 -> + A[ !cg.finished U cg.finished & cs.region_selected & + (cs.cont_3EO_start -> cs.m_mode = mm601 & cs.RTLS_abort_declared) ]) + +-- If MECO confirmed occurs in a major mode 601 and a contingency abort +-- procedure is still required, contingency 3E/O guidance sets the +-- CONT_3EO_START flag ON. [...] Contingency 3E/O guidance then commands +-- 3E/O auto maneuvers in major mode 601. [What are these maneuvers??] + +SPEC AG(cg.finished & cs.m_mode = mm601 & !et_sep_cmd & + meco_confirmed & cs.cont_3EO_start -> + cg.q_gcb_i in {quat_reg1, quat_reg2, quat_reg3, quat_reg4, undef} + | cg.emerg_sep) + +-- If MECO confirmed occurs in a first stage (MM102) [...], contingency +-- 3E/O guidance will command a fast ET separation during SRB tailoff in +-- major mode 102. CONT 3E/O GUID will then command maneuver post-sep in +-- MM601 (???). [ I'm not sure what indicates fast ET sep.: emerg_sep or +-- early_sep, or what? ] + +SPEC AG(cg.finished & cs.m_mode = mm102 & meco_confirmed & pre_sep -> + cg.emerg_sep | et_sep_cmd + | cg.et_sep_man_initiate + | cg.early_sep + ) + +--------------------------------------------- +-- Invariants from Murphi code -------------- +--------------------------------------------- + +--SPEC AG(cg.finished -> (output_ok != 0 | (output_ok = undef & +-- (cg.emerg_sep | !cg.cont_sep_cplt)))) + +--SPEC AG(!cg.finished & !cg.idle -> !mated_coast_mnvr | !et_sep_cmd) + +-- Stronger version !!! + +SPEC AG(cg.finished -> output_ok != 0) + +-- Contingency Guidance shall command an ET separation +-- [under certain conditions :-]. + +SPEC AG(cs.cont_3EO_start & cg.finished & + (cg.r = reg1 -> cond_29) & + (cg.r = reg2 -> cond_24 & cond_26) & + (cg.r = reg3 -> cg.alpha_ok & + (ABS_alf_err_LT_alf_sep_err -> cond_20b)) & + (cg.r = reg4 -> cond_18 & q_orb_LT_0) & + (cg.r = reg102 -> pre_sep) -> + et_sep_cmd | cg.et_sep_man_initiate + | cg.early_sep + | cg.emerg_sep + ) + +-- Contingency Guidance shall command at most one interconnected OMS dump. + +SPEC AG(cg.finished & cg.oms_rcs_i_c_inh_ena_cmd -> + AG(!cg.oms_rcs_i_c_inh_ena_cmd -> AG(!cg.oms_rcs_i_c_inh_ena_cmd))) + +-- Contingency Guidance shall command a transition to glide RTLS +-- (flight mode 602) + +SPEC AG(cg.finished & cs.m_mode = mm601 -> + --cg.cont_sep_cplt | cg.emerg_sep | + cg.call_RTLS_abort_task) + +-- Paper, p. 28, unstated assumption 2: at step 6 the region is +-- among 102, 1-4. + +SPEC AG(cg.step = 6 -> cg.r in {reg102, reg1, reg2, reg3, reg4}) + +-- The transition to mode 602 shall not occur until the entry maneuver +-- has been calculated + +SPEC !E[cg.q_gcb_i = undef U cg.cont_sep_cplt & cg.q_gcb_i = undef] + +-- The entry maneuver calculations shall not commence until the OMS/RCS +-- interconnect, if any, is complete (??? What does it exactly mean???) +-- !!! +--SPEC AG(cg.oms_rcs_i_c_inh_ena_cmd -> +-- !E[cg.oms_rcs_i_c_inh_ena_cmd U +-- cg.q_gcb_i != undef & cg.oms_rcs_i_c_inh_ena_cmd]) + +SPEC AG(cg.oms_rcs_i_c_inh_ena_cmd -> + !E[rcs_all_jet_inhibit U + cg.q_gcb_i != undef & rcs_all_jet_inhibit]) + +-- The OMS dump shall not be considered until the -Z translation is complete. + +SPEC !E[!cont_minus_z_compl & cg.r != reg102 U cg.orbiter_dump_ena] + +-- Completion of -Z translation shall not be checked until ET separation +-- has been commanded + +SPEC !E[!et_sep_cmd U cg.step = 7] + +-- ET separation shall be commanded if and only if an abort maneuver +-- region is assigned [and again there are *certain conditions*]. + +SPEC AG(cg.finished & cs.cont_3EO_start & + (cg.r = reg1 -> cond_29) & + (cg.r = reg2 -> cond_24 & cond_26) & + (cg.r = reg3 -> cg.alpha_ok & + (ABS_alf_err_LT_alf_sep_err -> cond_20b)) & + (cg.r = reg4 -> cond_18 & q_orb_LT_0) & + (cg.r = reg102 -> pre_sep) -> + (cg.et_sep_man_initiate | et_sep_cmd + <-> cg.r in {reg1, reg2, reg3, reg4, reg102})) + +-- The assigned region can not change arbitrarily. + +-- Regions 1 and 2 may interchange, but will not switch to any other region: + +SPEC AG(cg.finished & cs.cont_3EO_start & cg.r in {reg1,reg2} -> + AG(cg.finished -> cg.r in {reg1,reg2})) + +-- Regions 3 and 4 may interchange, but will not switch to any other region: + +SPEC AG(cg.finished & cs.cont_3EO_start & cg.r in {reg3,reg4} -> + AG(cg.finished -> cg.r in {reg3,reg4})) + +-- Region 102 never changes: + +SPEC AG(cg.finished & cg.r = reg102 -> AG(cg.finished -> cg.r = reg102)) |