started with 4

[mc1516.git] / e42.smv

diff --git a/e42.smv b/e42.smv
new file mode 100644 (file)
index 0000000..a142f73
--- /dev/null
+++ b/e42.smv
@@ -0,0 +1,76 @@
+MODULE phil(leftfork, rightfork)
+VAR
+       state: {none, left, both};
+ASSIGN
+       init(state) := none;
+       next(state) := case
+               state=none: case
+                       leftfork=inuse: none;
+                       TRUE: left;
+               esac;
+               state=left: case
+                       rightfork=inuse: left;
+                       TRUE: both;
+               esac;
+               TRUE: none;
+       esac;
+
+MODULE main
+VAR
+       f: array 0..6 of {free, inuse};
+       ph0: phil(f[6], f[1]);
+       ph1: phil(f[0], f[2]);
+       ph2: phil(f[1], f[3]);
+       ph3: phil(f[2], f[4]);
+       ph4: phil(f[3], f[5]);
+       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;
+
+       next(f[0]) := case
+               ph6.state=both | ph1.state=left | ph0.state=both: inuse;
+               TRUE: free;
+       esac;
+       next(f[1]) := case
+               ph0.state=both | ph2.state=left | ph2.state=both: inuse;
+               TRUE: free;
+       esac;
+       next(f[2]) := case
+               ph1.state=both | ph3.state=left | ph3.state=both: inuse;
+               TRUE: free;
+       esac;
+       next(f[3]) := case
+               ph2.state=both | ph4.state=left | ph4.state=both: inuse;
+               TRUE: free;
+       esac;
+       next(f[4]) := case
+               ph3.state=both | ph5.state=left | ph5.state=both: inuse;
+               TRUE: free;
+       esac;
+       next(f[5]) := case
+               ph4.state=both | ph6.state=left | ph6.state=both: inuse;
+               TRUE: free;
+       esac;
+       next(f[6]) := case
+               ph5.state=both | ph0.state=left | ph0.state=both: inuse;
+               TRUE: free;
+       esac;
+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)))