reorder to match paper

examples/eq_paper.rs

@@ -52,15 +52,7 @@ fn main() {
     STATE_H[i] = STATE;
     CNTR_H[i] = TIMEOUT_CNTR;
 
-    // invariants
-    // (1) S8000 -> a & b
-    // ensures that Enable implies that both a and b are true
-    // this is the main safety condition
-    if STATE == S8000 {
-      kassert!(DATA[i].a & DATA[i].b);
-    }
-
-    // (2) !a | !b -> !S8000
+    // (1) !a | !b -> !S8000
     // ensures that if any input is false we cannot enter the Enable state
     // this can also be seen as a safty condition
     // (can it be derived from the first condition, but we keep is as
@@ -71,6 +63,14 @@ fn main() {
       kassert!(!(STATE == S8000));
     }
 
+    // invariants
+    // (2) S8000 -> a & b
+    // ensures that Enable implies that both a and b are true
+    // this is the main safety condition
+    if STATE == S8000 {
+      kassert!(DATA[i].a & DATA[i].b);
+    }
+
     // S8001 -> !a & !b
     // we can only stay or enter the Init state unless either (or both) inputs are false
     if STATE == S8001 {