Merged in camilstaps/pygments-main (pull request #564)

Adds a NuSMV (2.6) lexer and example file.

1 files changed, 1124 insertions, 0 deletions

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