example updated

examples/eq.rs

+#![allow(non_snake_case)]
+#![no_main]
+
+extern crate klee;
+use klee::{kassert, ksymbol,kassume};
+
+#[no_mangle]
+fn main() {
+    let mut DATA: [Data; (DISCREPENCY + 2) as usize] =
+        unsafe { core::mem::uninitialized() };
+    ksymbol!(&mut DATA, "DATA");
+
+    let mut STATE_HISTORY: [State; (DISCREPENCY + 2) as usize] =
+        unsafe { core::mem::uninitialized() };
+
+    let mut TIMEOUT_CNTR: u32 = 0;
+    let mut STATE = S8001;
+
+    for i in 0..(DISCREPENCY + 2) as usize {
+        periodic(&mut STATE, &mut TIMEOUT_CNTR, &mut DATA[i as usize]);
+
+        // invariants
+        // S8000 -> a & b
+        // ensures that both inputs are true if we are in the Enable state S8000
+        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
+        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);
+        }
+        // !a & !b -> S8001
+        // ensures that we enter the Init state if both inputs are false
+        if !DATA[i].a & !DATA[i].b & (TIMEOUT_CNTR > 0) {
+            kassert!(STATE == S8001);
+        }
+
+        // DISCREPANCY relatod invariants
+        match STATE {
+            // error states implies TIMEOUT_CNTR to have expired
+            C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
+            // wait states implies that TIMEOUT_CNTR not yet expired
+            S8004 | S8005 | S8014 => {
+                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 ensured
+                    if DATA[i].a & DATA[i].b  & (TIMEOUT_CNTR > 0) {
+                        kassert!(STATE == S8000);
+                    }
+                }
+            }
+        }
+        STATE_HISTORY[i] = STATE;
+    }
+}
+
+#[derive(Debug, Copy, Clone)]
+pub struct Data {
+    a: bool,
+    b: bool,
+}
+
+#[derive(Debug, Copy, Clone, PartialEq)]
+pub enum State {
+    S8000,
+    S8001,
+    S8004,
+    S8014,
+    S8005,
+    C001,
+    C002,
+    C003,
+}
+
+use State::*;
+
+const DISCREPENCY: u32 = 3;
+const T: bool = true;
+const F: bool = false;
+
+fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, DATA: &mut Data) {
+    // we start directly in the init state S80001
+    // static mut STATE: State = State::S8001;
+    // static mut TIMEOUT_CNTR: u32 = 0;
+
+    let data = DATA;
+
+    *STATE = match STATE {
+        S8000 => match (data.a, data.b) {
+            (F, F) => S8001,
+            (F, T) | (T, F) => {
+                *TIMEOUT_CNTR = DISCREPENCY;
+                S8005
+            }
+            (T, T) => S8000,
+        },
+        S8001 => match (data.a, data.b) {
+            (F, F) => S8001,
+            (F, T) => {
+                *TIMEOUT_CNTR = DISCREPENCY;
+                S8014
+            }
+            (T, F) => {
+                *TIMEOUT_CNTR = DISCREPENCY;
+                S8004
+            }
+            (T, T) => S8000,
+        },
+        S8004 => {
+            *TIMEOUT_CNTR -= 1;
+            match *TIMEOUT_CNTR {
+                0 => C001,
+                _ => match (data.a, data.b) {
+                    (F, _) => S8001,
+                    (_, T) => S8000,
+                    _ => S8004,
+                },
+            }
+        }
+        S8014 => {
+            *TIMEOUT_CNTR -= 1;
+            match *TIMEOUT_CNTR {
+                0 => C002,
+                _ => match (data.a, data.b) {
+                    (_, F) => S8001,
+                    (T, _) => S8000,
+                    _ => S8014,
+                },
+            }
+        }
+        S8005 => {
+            *TIMEOUT_CNTR -= 1;
+            match *TIMEOUT_CNTR {
+                0 => C003,
+                _ => match (data.a, data.b) {
+                    (F, F) => S8001,
+                    _ => S8005,
+                },
+            }
+        }
+        C001 | C002 => match (data.a, data.b) {
+            (F, F) => S8001,
+            _ => *STATE,
+        },
+        C003 => match (data.a, data.b) {
+            (F, F) => S8001,
+            _ => C003,
+        },
+    };
+}