From c0a8adae6ff29ce556bc40d410ef5232c2aeb7a7 Mon Sep 17 00:00:00 2001 From: Per <Per Lindgren> Date: Thu, 7 Feb 2019 16:30:49 +0100 Subject: [PATCH] example wip --- examples/eq.rs | 123 +++++++++++++++++++++++-------------------------- 1 file changed, 58 insertions(+), 65 deletions(-) diff --git a/examples/eq.rs b/examples/eq.rs index b4e36a8..ae2a410 100644 --- a/examples/eq.rs +++ b/examples/eq.rs @@ -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, }, }; -- GitLab