Skip to content
Snippets Groups Projects
Commit c0a8adae authored by Per's avatar Per
Browse files

example wip

parent dc75f851
No related branches found
No related tags found
No related merge requests found
Show whitespace changes
Inline Side-by-side
Showing
with 58 additions and 65 deletions
examples/eq.rs
+ 58
− 65
View file @ c0a8adae
......@@ -30,13 +30,14 @@ const F: bool = false;
#[no_mangle]
fn main() {
let mut DATA: [Data; (DISCREPENCY + 2) as usize] = unsafe { core::mem::uninitialized() };
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 = DISCREPENCY;
let mut TIMEOUT_CNTR: u32 = unsafe { core::mem::uninitialized() };
let mut STATE = S8001;
for i in 0..(DISCREPENCY + 2) as usize {
......@@ -62,66 +63,73 @@ fn main() {
}
// S8001 -> !a & !b
// we can only stay or enter the Init state if both inputs are false
// we can only stay or enter the Init state if either input are false
if STATE == S8001 {
kassert!(TIMEOUT_CNTR == DISCREPENCY);
// kassert!(TIMEOUT_CNTR == DISCREPENCY);
kassert!(!DATA[i].a | !DATA[i].b);
}
// !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 related 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),
_ => {}
}
// 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);
}
}
}
}
// // !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 {
// kassert!(STATE == S8001);
// }
// // DISCREPANCY related 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)
// }
// _ => {}
// }
// // 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);
// }
// }
// }
// }
STATE_HISTORY[i] = STATE;
}
}
fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
*STATE = match STATE {
S8000 => match (data.a, data.b) {
(F, F) => {
(F, F) => S8001,
(F, T) | (T, F) => {
*TIMEOUT_CNTR = DISCREPENCY;
S8001
S8005
}
(F, T) | (T, F) => S8005,
(T, T) => S8000,
},
S8001 => match (data.a, data.b) {
(F, F) => S8001,
(F, T) => S8014,
(T, F) => S8004,
(F, T) => {
*TIMEOUT_CNTR = DISCREPENCY;
S8014
}
(T, F) => {
*TIMEOUT_CNTR = DISCREPENCY;
S8004
}
(T, T) => S8000,
},
S8004 => {
......@@ -129,10 +137,7 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
match *TIMEOUT_CNTR {
0 => C001,
_ => match (data.a, data.b) {
(F, _) => {
*TIMEOUT_CNTR = DISCREPENCY;
S8001
}
(F, _) => S8001,
(_, T) => S8000,
_ => S8004,
},
......@@ -143,10 +148,7 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
match *TIMEOUT_CNTR {
0 => C002,
_ => match (data.a, data.b) {
(_, F) => {
*TIMEOUT_CNTR = DISCREPENCY;
S8001
}
(_, F) => S8001,
(T, _) => S8000,
_ => S8014,
},
......@@ -157,26 +159,17 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
match *TIMEOUT_CNTR {
0 => C003,
_ => match (data.a, data.b) {
(F, F) => {
*TIMEOUT_CNTR = DISCREPENCY;
S8001
}
(F, F) => S8001,
_ => S8005,
},
}
}
C001 | C002 => match (data.a, data.b) {
(F, F) => {
*TIMEOUT_CNTR = DISCREPENCY;
S8001
}
(F, F) => S8001,
_ => *STATE,
},
C003 => match (data.a, data.b) {
(F, F) => {
*TIMEOUT_CNTR = DISCREPENCY;
S8001
}
(F, F) => S8001,
_ => C003,
},
};
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment