example updated

examples/eq.rs

@@ -2,7 +2,7 @@
 #![no_main]
 
 extern crate klee;
-use klee::{kassert, ksymbol,kassume};
+use klee::{kassert, kassume, ksymbol};
 
 #[no_mangle]
 fn main() {
@@ -13,7 +13,7 @@ fn main() {
     let mut STATE_HISTORY: [State; (DISCREPENCY + 2) as usize] =
         unsafe { core::mem::uninitialized() };
 
-    let mut TIMEOUT_CNTR: u32 = 0;
+    let mut TIMEOUT_CNTR: u32 = DISCREPENCY;
     let mut STATE = S8001;
 
     for i in 0..(DISCREPENCY + 2) as usize {
@@ -21,31 +21,44 @@ fn main() {
 
         // invariants
         // S8000 -> a & b
-        // ensures that both inputs are true if we are in the Enable state S8000
+        // 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);
         }
+
         // !a | !b -> !S8000
-        // ensures that if any input is true we cannot be in the Enable state
+        // 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, not really sure?
+        // perhaps from the set of passible STATEs as finite, bla, think about it...
+        // not entirely straightforward...
+        // if we come up with a proof of redundancy it can be removed
         if !DATA[i].a | !DATA[i].b {
             kassert!(!(STATE == S8000));
         }
+
         // S8001 -> !a & !b
         // we can only stay or enter the Init state if both inputs are false
         if STATE == S8001 {
-            kassert!(!DATA[i].a | !DATA[i].b);
+            kassert!(TIMEOUT_CNTR == DISCREPENCY && !DATA[i].a | !DATA[i].b);
         }
-        // !a & !b -> S8001
+
+        // !a & !b & !timeout-> S8001
         // ensures that we enter the Init state if both inputs are false
+        // under the condition that a timout has not occured
         if !DATA[i].a & !DATA[i].b & (TIMEOUT_CNTR > 0) {
             kassert!(STATE == S8001);
         }
 
         // DISCREPANCY relatod invariants
         match STATE {
+            // Error -> timeout
             // error states implies TIMEOUT_CNTR to have expired
             C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
+            // Waiting states -> !timeout
             // wait states implies that TIMEOUT_CNTR not yet expired
+            // and that the time remaining is not longer than the discrepency
             S8004 | S8005 | S8014 => {
                 kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPENCY)
             }
@@ -56,11 +69,12 @@ fn main() {
         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 ensured
+                    // liveness from Init and Wait states, Enable is ensured
                     if DATA[i].a & DATA[i].b & (TIMEOUT_CNTR > 0) {
                         kassert!(STATE == S8000);
                     }