From: Mart Lubbers Date: Tue, 1 Mar 2016 20:17:09 +0000 (+0100) Subject: update phils X-Git-Url: https://git.martlubbers.net/?a=commitdiff_plain;h=f36a4faf3ca545644d3c859f8bc6592325fc33e9;p=mc1516.git update phils --- diff --git a/e42.smv b/e42.smv index a142f73..91f16e7 100644 --- a/e42.smv +++ b/e42.smv @@ -26,40 +26,40 @@ 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; LTLSPEC F(