1124 lines
33 KiB
Text
1124 lines
33 KiB
Text
--
|
|
-- 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))
|