up

[mc1516.git] / e42.smv

diff --git a/e42.smv b/e42.smv
index a142f73..c227d2a 100644 (file)
--- a/e42.smv
+++ b/e42.smv
@@ -6,14 +6,17 @@ ASSIGN
        next(state) := case
                state=none: case
                        leftfork=inuse: none;
-                       TRUE: left;
+                       TRUE: {none, left};
                esac;
                state=left: case
-                       rightfork=inuse: left;
-                       TRUE: both;
+--                     rightfork=inuse: left;
+                       rightfork=inuse: {none, left};
+--                     TRUE: {left, both};
+                       TRUE: {none, left, both};
                esac;
                TRUE: none;
        esac;
+JUSTICE state=both
 
 MODULE main
 VAR
@@ -26,51 +29,58 @@ VAR
        ph5: phil(f[4], f[6]);
        ph6: phil(f[5], f[0]);
 ASSIGN
-       init(f[0]):=free;
-       init(f[1]):=free;
-       init(f[2]):=free;
-       init(f[3]):=free;
-       init(f[4]):=free;
-       init(f[5]):=free;
-       init(f[6]):=free;
+       init(f[0]) := free;
+       init(f[1]) := free;
+       init(f[2]) := free;
+       init(f[3]) := free;
+       init(f[4]) := free;
+       init(f[5]) := free;
+       init(f[6]) := free;
 
        next(f[0]) := case
-               ph6.state=both | ph1.state=left | ph0.state=both: inuse;
+               next(ph6.state)=both | next(ph1.state)=left | next(ph0.state)=both: inuse;
                TRUE: free;
        esac;
        next(f[1]) := case
-               ph0.state=both | ph2.state=left | ph2.state=both: inuse;
+               next(ph0.state)=both | next(ph2.state)=left | next(ph2.state)=both: inuse;
                TRUE: free;
        esac;
        next(f[2]) := case
-               ph1.state=both | ph3.state=left | ph3.state=both: inuse;
+               next(ph1.state)=both | next(ph3.state)=left | next(ph3.state)=both: inuse;
                TRUE: free;
        esac;
        next(f[3]) := case
-               ph2.state=both | ph4.state=left | ph4.state=both: inuse;
+               next(ph2.state)=both | next(ph4.state)=left | next(ph4.state)=both: inuse;
                TRUE: free;
        esac;
        next(f[4]) := case
-               ph3.state=both | ph5.state=left | ph5.state=both: inuse;
+               next(ph3.state)=both | next(ph5.state)=left | next(ph5.state)=both: inuse;
                TRUE: free;
        esac;
        next(f[5]) := case
-               ph4.state=both | ph6.state=left | ph6.state=both: inuse;
+               next(ph4.state)=both | next(ph6.state)=left | next(ph6.state)=both: inuse;
                TRUE: free;
        esac;
        next(f[6]) := case
-               ph5.state=both | ph0.state=left | ph0.state=both: inuse;
+               next(ph5.state)=both | next(ph0.state)=left | next(ph0.state)=both: inuse;
                TRUE: free;
        esac;
+--This finds a deadlock
 LTLSPEC F(
-       G(ph0.state=left) | 
-       G(ph1.state=left) | 
-       G(ph2.state=left) | 
-       G(ph3.state=left) | 
-       G(ph4.state=left) | 
-       G(ph5.state=left) | 
-       G(ph6.state=left))
---LTLSPEC G(
---     (F (ph0.state=both)) & (F (ph1.state=both)) & (F (ph2.state=both)) &
---     (F (ph3.state=both)) & (F (ph4.state=both)) & (F (ph5.state=both)) &
---     (F (ph6.state=both)))
+       ph0.state=left &
+       ph1.state=left &
+       ph2.state=left &
+       ph3.state=left &
+       ph4.state=left &
+       ph5.state=left &
+       ph6.state=left)
+
+--Checks starvation
+CTLSPEC AG(
+       (EF (ph0.state=both)) &
+       (EF (ph1.state=both)) &
+       (EF (ph2.state=both)) &
+       (EF (ph3.state=both)) &
+       (EF (ph4.state=both)) &
+       (EF (ph5.state=both)) &
+       (EF (ph6.state=both)))