updated
authorMart Lubbers <mart@martlubbers.net>
Tue, 1 Mar 2016 20:11:40 +0000 (21:11 +0100)
committerMart Lubbers <mart@martlubbers.net>
Tue, 1 Mar 2016 20:11:40 +0000 (21:11 +0100)
e41.smv

diff --git a/e41.smv b/e41.smv
index 3cbf9c1..67031b2 100644 (file)
--- a/e41.smv
+++ b/e41.smv
@@ -4,15 +4,16 @@ VAR
 ASSIGN
        init(line):=l2;
        next(line):=case
-               line=l2: l3;
-               line=l3: l4;
+               line=l2: {l2,l3};
+               line=l3: {l3,l4};
                line=l4: case
                        !(yother=0 | s!=i) : l4;
-                       TRUE: l7;
+                       TRUE: {l4,l7};
                esac;
-               line=l7: l8;
-               line=l8: l2;
+               line=l7: {l7,l8};
+               line=l8: {l8,l2};
        esac;
+JUSTICE line=l7
 
 MODULE main
 VAR