From 6a08958ae5c81880ec693337b15a2b1ec13b88a6 Mon Sep 17 00:00:00 2001
From: Per Lindgren <per.lindgren@ltu.se>
Date: Sun, 10 Feb 2019 22:26:19 +0100
Subject: [PATCH] paper version
---
examples/eq.rs | 60 ++++++++++++++++++++++++--------------------------
1 file changed, 29 insertions(+), 31 deletions(-)
diff --git a/examples/eq.rs b/examples/eq.rs
index 79e61ec..a881738 100644
--- a/examples/eq.rs
+++ b/examples/eq.rs
@@ -24,10 +24,8 @@ pub enum State {
use State::*;
-//const DISCREPANCY: u32 = 2;
const DISCREPANCY: u32 = 1;
-//const HORIZON: usize = (DISCREPANCY + 4 - 1) as usize;
-const HORIZON: usize = (DISCREPANCY + 4 + 1) as usize;
+const HORIZON: usize = (DISCREPANCY + 4) as usize;
const T: bool = true;
const F: bool = false;
@@ -87,24 +85,24 @@ fn main() {
}
}
- // DISCREPANCY related invariants
+ // // DISCREPANCY related invariants
match STATE {
// Error -> timeout
C001 | C002 | C003 => kassert!(TIMEOUT_CNTR == 0),
S8004 | S8005 | S8014 => {
- // remaining in a waiting state decreases the counter
+ // // remaining in a waiting state decreases the counter
if i > 0 {
if STATE_H[i - 1] == STATE_H[i] {
kassert!(TIMEOUT_CNTR < CNTR_H[i - 1]);
}
}
- // Waiting states -> !timeout
- // Waiting states implies that TIMEOUT_CNTR has not yet expired
- // and that the time remaining is not longer than the DISCREPANCY
- kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
+ // // Waiting states -> !timeout
+ // // Waiting states implies that TIMEOUT_CNTR has not yet expired
+ // // and that the time remaining is not longer than the DISCREPANCY
+ // kassert!(0 < TIMEOUT_CNTR && TIMEOUT_CNTR <= DISCREPANCY);
+ // kassert!(TIMEOUT_CNTR <= DISCREPANCY);
}
-
_ => {}
}
@@ -160,38 +158,38 @@ fn periodic(STATE: &mut State, TIMEOUT_CNTR: &mut u32, data: &Data) {
}
(T, T) => S8000,
},
- S8004 => {
- *TIMEOUT_CNTR -= 1;
- match *TIMEOUT_CNTR {
- 0 => C001,
- _ => match (data.a, data.b) {
+ S8004 => match *TIMEOUT_CNTR {
+ 0 => C001,
+ _ => {
+ *TIMEOUT_CNTR -= 1;
+ match (data.a, data.b) {
(F, _) => S8001,
(_, T) => S8000,
_ => S8004,
- },
+ }
}
- }
- S8014 => {
- *TIMEOUT_CNTR -= 1;
- match *TIMEOUT_CNTR {
- 0 => C002,
- _ => match (data.a, data.b) {
+ },
+ S8014 => match *TIMEOUT_CNTR {
+ 0 => C002,
+ _ => {
+ *TIMEOUT_CNTR -= 1;
+ match (data.a, data.b) {
(_, F) => S8001,
(T, _) => S8000,
_ => S8014,
- },
+ }
}
- }
- S8005 => {
- *TIMEOUT_CNTR -= 1;
- match *TIMEOUT_CNTR {
- 0 => C003,
- _ => match (data.a, data.b) {
+ },
+ S8005 => match *TIMEOUT_CNTR {
+ 0 => C003,
+ _ => {
+ *TIMEOUT_CNTR -= 1;
+ match (data.a, data.b) {
(F, F) => S8001,
_ => S8005,
- },
+ }
}
- }
+ },
C001 | C002 => match (data.a, data.b) {
(F, F) => S8001,
_ => *STATE,
--
GitLab