paper version

examples/eq.rs

@@ -24,10 +24,8 @@ pub enum State {
 
 use State::*;
 
-//const DISCREPANCY: u32 = 2;
 const DISCREPANCY: u32 = 1;
-//const HORIZON: usize = (DISCREPANCY + 4 - 1) as usize;
-const HORIZON: usize = (DISCREPANCY + 4 + 1) as usize;
+const HORIZON: usize = (DISCREPANCY + 4) as usize;
 const T: bool = true;
 const F: bool = false;
 
@@ -87,24 +85,24 @@ fn main() {
       }
     }
 
-    // DISCREPANCY related invariants
+    // // DISCREPANCY related invariants
     match STATE {
       // Error -> timeout
       C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
 
       S8004 | S8005 | S8014 => {
-        // remaining in a waiting state decreases the counter
+        // // remaining in a waiting state decreases the counter
         if i > 0 {
           if STATE_H[i - 1] == STATE_H[i] {
             kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
           }
         }
-        // Waiting states -> !timeout
-        // Waiting states implies that TIMEOUT_CNTR has not yet expired
-        // and that the time remaining is not longer than the DISCREPANCY
-        kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
+        // // Waiting states -> !timeout
+        // // Waiting states implies that TIMEOUT_CNTR has not yet expired
+        // // and that the time remaining is not longer than the DISCREPANCY
+        //   kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
+        // kassert!(TIMEOUT_CNTR <= DISCREPANCY);
       }
-
       _ => {}
     }
 
@@ -160,38 +158,38 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
       }
       (T, T) => S8000,
     },
-    S8004 => {
-      *TIMEOUT_CNTR -= 1;
-      match *TIMEOUT_CNTR {
+    S8004 => match *TIMEOUT_CNTR {
       0 => C001,
-        _ => match (data.a, data.b) {
+      _ => {
+        *TIMEOUT_CNTR -= 1;
+        match (data.a, data.b) {
           (F, _) => S8001,
           (_, T) => S8000,
           _ => S8004,
-        },
         }
       }
-    S8014 => {
-      *TIMEOUT_CNTR -= 1;
-      match *TIMEOUT_CNTR {
+    },
+    S8014 => match *TIMEOUT_CNTR {
       0 => C002,
-        _ => match (data.a, data.b) {
+      _ => {
+        *TIMEOUT_CNTR -= 1;
+        match (data.a, data.b) {
           (_, F) => S8001,
           (T, _) => S8000,
           _ => S8014,
-        },
         }
       }
-    S8005 => {
-      *TIMEOUT_CNTR -= 1;
-      match *TIMEOUT_CNTR {
+    },
+    S8005 => match *TIMEOUT_CNTR {
       0 => C003,
-        _ => match (data.a, data.b) {
+      _ => {
+        *TIMEOUT_CNTR -= 1;
+        match (data.a, data.b) {
           (F, F) => S8001,
           _ => S8005,
-        },
         }
       }
+    },
     C001 | C002 => match (data.a, data.b) {
       (F, F) => S8001,
       _ => *STATE,