path: root/tests/examplefiles/guidance.smv

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