Skip to content
Snippets Groups Projects
Commit 2135bc5d authored by Nils Fitinghoff's avatar Nils Fitinghoff
Browse files

remove assertion that the paper does not explain

parent 3362a9e5
No related branches found
No related tags found
No related merge requests found
......@@ -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] {
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment