dfs working paper

examples/eq_dfs.rs

@@ -2,8 +2,8 @@
 #![no_main]
 #![no_std]
 
-extern crate panic_abort;
 extern crate klee;
+extern crate panic_abort;
 use klee::{kassert, kassume, ksymbol};
 
 #[derive(Debug, Copy, Clone)]
@@ -28,19 +28,19 @@ use State::*;
 
 const DISCREPANCY: u32 = 2;
 // const HORIZON: usize = (2 * DISCREPANCY + 5) as usize;
-const HORIZON: usize = 100 as usize;
+const HORIZON: usize = (DISCREPANCY * 3 + 4) as usize;
 
 const T: bool = true;
 const F: bool = false;
 
 #[no_mangle]
 fn main() {
-    let mut DATA: [Data; HORIZON] = unsafe { core::mem::uninitialized() };
+  let mut DATA: [Data; HORIZON + 1] = unsafe { core::mem::uninitialized() };
   ksymbol!(&mut DATA, "DATA");
 
-    let mut STATE_H: [State; HORIZON] = unsafe { core::mem::uninitialized() };
+  let mut STATE_H: [State; HORIZON + 1] = unsafe { core::mem::uninitialized() };
 
-    let mut CNTR_H: [u32; HORIZON] = unsafe { core::mem::uninitialized() };
+  let mut CNTR_H: [u32; HORIZON + 1] = unsafe { core::mem::uninitialized() };
 
   let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
   // initial state, Init
@@ -89,11 +89,7 @@ fn main() {
           kassert!((STATE_H[i] == S8001) | (STATE == STATE_H[i - 1]));
         }
         S8005 => {
-                    kassert!(
-                        (STATE_H[i] == S8001)
-                            | (STATE == C003)
-                            | (STATE == STATE_H[i - 1])
-                    );
+          kassert!((STATE_H[i] == S8001) | (STATE == C003) | (STATE == STATE_H[i - 1]));
         }
         _ => (),
       }
@@ -146,11 +142,16 @@ fn main() {
     //   }
     // }
 
-        unsafe { core::ptr::read_volatile(&STATE_H[i]) };
 
     let mut is_visited = false;
     match STATE {
-            S8004 | S8005 | S8014 => {}
+      S8004 | S8005 | S8014 => {
+          for j in 0..i {
+          if (STATE_H[i] == STATE_H[j] && CNTR_H[i] == CNTR_H[j]) {
+            is_visited = true;
+          }
+        }
+      }
       _ => {
         for j in 0..i {
           if (STATE_H[i] == STATE_H[j]) {
@@ -163,14 +164,20 @@ fn main() {
     if is_visited {
       break;
     }
-        i += 1;
+
     if i == HORIZON {
       kassert!(false);
     }
+
+    i += 1;
   }
 }
 
-fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
+fn eq(
+  STATE: &mut State,
+  TIMEOUT_CNTR: &mut u32,
+  data: &Data,
+) {
   *STATE = match STATE {
     S8000 => match (data.a, data.b) {
       (F, F) => S8001,
@@ -197,8 +204,12 @@ fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
       _ => {
         *TIMEOUT_CNTR -= 1;
         match (data.a, data.b) {
-                    (F, _) => S8001,
-                    (_, T) => S8000,
+          (F, F) => S8001,
+          (F, T) => {
+            *TIMEOUT_CNTR = DISCREPANCY;
+            S8014
+          }
+          (T, T) => S8000,
           _ => S8004,
         }
       }
@@ -208,8 +219,12 @@ fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
       _ => {
         *TIMEOUT_CNTR -= 1;
         match (data.a, data.b) {
-                    (_, F) => S8001,
-                    (T, _) => S8000,
+          (F, F) => S8001,
+          (T, F) => {
+            *TIMEOUT_CNTR = DISCREPANCY;
+            S8004
+          }
+          (T, T) => S8000,
           _ => S8014,
         }
       }
@@ -224,9 +239,13 @@ fn eq(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
         }
       }
     },
-        C001 | C002 | C003 => match (data.a, data.b) {
+    C001 | C002 => match (data.a, data.b) {
       (F, F) => S8001,
       _ => *STATE,
     },
+    C003 => match (data.a, data.b) {
+      (F, F) => S8001,
+      _ => C003,
+    },
   };
 }