From 2135bc5d53450c6d82c521356246eab5b70beb74 Mon Sep 17 00:00:00 2001
From: Nils Fitinghoff <nils.fitinghoff@grepit.se>
Date: Fri, 29 Mar 2019 19:51:27 +0100
Subject: [PATCH] remove assertion that the paper does not explain
---
examples/eq_paper.rs | 6 ------
1 file changed, 6 deletions(-)
diff --git a/examples/eq_paper.rs b/examples/eq_paper.rs
index 1781e1e..ce9c963 100644
--- a/examples/eq_paper.rs
+++ b/examples/eq_paper.rs
@@ -71,12 +71,6 @@ fn main() {
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 {
- kassert!(!DATA[i].a | !DATA[i].b);
- }
-
// transition invariants
if i > 0 {
match STATE_H[i - 1] {
--
GitLab