wip

examples/eq.rs

@@ -24,25 +24,29 @@ pub enum State {
 
 use State::*;
 
-const DISCREPENCY: u32 = 2;
+//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 T: bool = true;
 const F: bool = false;
 
 #[no_mangle]
 fn main() {
-  let mut DATA: [Data; (DISCREPENCY + 3) as usize] = unsafe { core::mem::uninitialized() };
+  let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
   ksymbol!(&mut DATA, "DATA");
 
-  let mut STATE_HISTORY: [State; (DISCREPENCY + 3) as usize] =
-    unsafe { core::mem::uninitialized() };
+  let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() };
 
-  let mut CNTR_HISTORY: [u32; (DISCREPENCY + 3) as usize] = unsafe { core::mem::uninitialized() };
+  let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
 
   let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
   let mut STATE = S8001;
 
-  for i in 0..(DISCREPENCY + 3) as usize {
-    periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
+  for i in 0..HORIZON {
+    periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i]);
+    STATE_H[i] = STATE;
+    CNTR_H[i] = TIMEOUT_CNTR;
 
     // invariants
     // S8000 -> a & b
@@ -71,13 +75,13 @@ fn main() {
 
     // transition invariants
     if i > 0 {
-      match STATE_HISTORY[i - 1] {
+      match STATE_H[i - 1] {
         C001 | C002 | C003 => {
           // transitions from error
-          kassert!((STATE == S8001) | (STATE == STATE_HISTORY[i - 1]));
+          kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
         }
         S8005 => {
-          kassert!((STATE == S8001) | (STATE == C003) | (STATE == STATE_HISTORY[i - 1]));
+          kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
         }
         _ => (),
       }
@@ -91,20 +95,32 @@ fn main() {
       S8004 | S8005 | S8014 => {
         // remaining in a waiting state decreases the counter
         if i > 0 {
-          if STATE_HISTORY[i - 1] == STATE {
-            kassert!(TIMEOUT_CNTR < CNTR_HISTORY[i - 1]);
+          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 discrepency
-        kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY);
+        // and that the time remaining is not longer than the DISCREPANCY
+        kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
       }
+
       _ => {}
     }
 
+    // // liveness?
+    // if i == HORIZON - 1 {
+    //   let mut ok = false;
+    //   for j in 0..=i {
+    //     if STATE_H[j] == S8001 {
+    //       ok = true;
+    //     }
+    //   }
+    //   kassert!(ok);
+    // }
+
     // if i > 0 {
-    //   match STATE_HISTORY[i - 1] {
+    //   match STATE_H[i - 1] {
     //     C001 | C002 | C003 | S8005 => {
     //       // no (immediate) transition from error / recover to Enable state
     //       kassert!(!(STATE == S8000));
@@ -118,10 +134,7 @@ fn main() {
     //   }
     // }
 
-    STATE_HISTORY[i] = STATE;
-    CNTR_HISTORY[i] = TIMEOUT_CNTR;
-
-    unsafe { core::ptr::read_volatile(&STATE_HISTORY[i]) };
+    unsafe { core::ptr::read_volatile(&STATE_H[i]) };
   }
 }
 
@@ -130,7 +143,7 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
     S8000 => match (data.a, data.b) {
       (F, F) => S8001,
       (F, T) | (T, F) => {
-        *TIMEOUT_CNTR = DISCREPENCY;
+        *TIMEOUT_CNTR = DISCREPANCY;
         S8005
       }
       (T, T) => S8000,
@@ -138,11 +151,11 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
     S8001 => match (data.a, data.b) {
       (F, F) => S8001,
       (F, T) => {
-        *TIMEOUT_CNTR = DISCREPENCY;
+        *TIMEOUT_CNTR = DISCREPANCY;
         S8014
       }
       (T, F) => {
-        *TIMEOUT_CNTR = DISCREPENCY;
+        *TIMEOUT_CNTR = DISCREPANCY;
         S8004
       }
       (T, T) => S8000,