From 3362a9e54bee399df0fcc6973bfd099fea905572 Mon Sep 17 00:00:00 2001
From: Nils Fitinghoff <nils.fitinghoff@grepit.se>
Date: Fri, 29 Mar 2019 17:27:12 +0100
Subject: [PATCH] reorder to match paper
---
examples/eq_paper.rs | 18 +++++++++---------
1 file changed, 9 insertions(+), 9 deletions(-)
diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs
index 7797817..1781e1e 100644
--- a/examples/eq_paper.rs
+++ b/examples/eq_paper.rs
@@ -52,15 +52,7 @@ fn main() {
STATE_H[i] = STATE;
CNTR_H[i] = TIMEOUT_CNTR;
- // invariants
- // (1) S8000 -> a & b
- // ensures that Enable implies that both a and b are true
- // this is the main safety condition
- if STATE == S8000 {
- kassert!(DATA[i].a & DATA[i].b);
- }
-
- // (2) !a | !b -> !S8000
+ // (1) !a | !b -> !S8000
// ensures that if any input is false we cannot enter the Enable state
// this can also be seen as a safty condition
// (can it be derived from the first condition, but we keep is as
@@ -71,6 +63,14 @@ fn main() {
kassert!(!(STATE == S8000));
}
+ // invariants
+ // (2) S8000 -> a & b
+ // ensures that Enable implies that both a and b are true
+ // this is the main safety condition
+ if STATE == S8000 {
+ kassert!(DATA[i].a & DATA[i].b);
+ }
+
// S8001 -> !a & !b
// we can only stay or enter the Init state unless either (or both) inputs are false
if STATE == S8001 {
--
GitLab