-- -- 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))