wip

examples/eq.rs

@@ -36,6 +36,8 @@ fn main() {
   let mut STATE_HISTORY: [State; (DISCREPENCY + 3) as usize] =
     unsafe { core::mem::uninitialized() };
 
+  let mut CNTR_HISTORY: [u32; (DISCREPENCY + 3) as usize] = unsafe { core::mem::uninitialized() };
+
   let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
   let mut STATE = S8001;
 
@@ -67,38 +69,58 @@ fn main() {
       kassert!(!DATA[i].a | !DATA[i].b);
     }
 
-        
+    // transition invariants
+    if i > 0 {
+      match STATE_HISTORY[i - 1] {
+        C001 | C002 | C003 => {
+          // transitions from error
+          kassert!((STATE == S8001) | (STATE == STATE_HISTORY[i - 1]));
+        }
+        S8005 => {
+          kassert!((STATE == S8001) | (STATE == C003) | (STATE == STATE_HISTORY[i - 1]));
+        }
+        _ => (),
+      }
+    }
 
     // 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
+        if i > 0 {
+          if STATE_HISTORY[i - 1] == STATE {
+            kassert!(TIMEOUT_CNTR < CNTR_HISTORY[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
-            S8004 | S8005 | S8014 => {
-                kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY)
+        kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY);
       }
       _ => {}
     }
 
-        // transition invariants
-        if i > 0 {
-            match STATE_HISTORY[i - 1] {
-                C001 | C002 | C003 | S8005 => {
-                    // no (immediate) transition from error / recover to Enable state
-                    kassert!(!(STATE == S8000));
-                }
-                _ => {
-                    // liveness from Init and Wait states, Enable is ensured
-                    if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
-                        kassert!(STATE == S8000);
-                    }
-                }
-            }
-        }
+    // if i > 0 {
+    //   match STATE_HISTORY[i - 1] {
+    //     C001 | C002 | C003 | S8005 => {
+    //       // no (immediate) transition from error / recover to Enable state
+    //       kassert!(!(STATE == S8000));
+    //     }
+    //     _ => {
+    //       // liveness from Init and Wait states, Enable is ensured
+    //       if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
+    //         kassert!(STATE == S8000);
+    //       }
+    //     }
+    //   }
+    // }
+
     STATE_HISTORY[i] = STATE;
+    CNTR_HISTORY[i] = TIMEOUT_CNTR;
+
     unsafe { core::ptr::read_volatile(&STATE_HISTORY[i]) };
   }
 }

src/main.rs

@@ -5,8 +5,7 @@ use klee::{kassert, ksymbol};
 
 #[no_mangle]
 fn main() {
-    let mut DATA: [Data; (DISCREPENCY + 1) as usize] =
-        unsafe { core::mem::uninitialized() };
+    let mut DATA: [Data; (DISCREPENCY + 1) as usize] = unsafe { core::mem::uninitialized() };
     ksymbol!(&mut DATA, "DATA");
 
     let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };