From a510b93e7ef355e534ffe0af9ad13460d08e4d6d Mon Sep 17 00:00:00 2001
From: Per <Per Lindgren>
Date: Tue, 5 Feb 2019 14:14:10 +0100
Subject: [PATCH] example updated
---
examples/eq.rs | 167 +++++++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 167 insertions(+)
create mode 100644 examples/eq.rs
diff --git a/examples/eq.rs b/examples/eq.rs
new file mode 100644
index 0000000..bb3d139
--- /dev/null
+++ b/examples/eq.rs
@@ -0,0 +1,167 @@
+#![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,
+ },
+ };
+}
--
GitLab