repositories
/
mc1516.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
bda0e95
)
update phils
author
Mart Lubbers
<mart@martlubbers.net>
Tue, 1 Mar 2016 20:17:09 +0000
(21:17 +0100)
committer
Mart Lubbers
<mart@martlubbers.net>
Tue, 1 Mar 2016 20:17:09 +0000
(21:17 +0100)
e42.smv
patch
|
blob
|
history
diff --git
a/e42.smv
b/e42.smv
index
a142f73
..
91f16e7
100644
(file)
--- a/
e42.smv
+++ b/
e42.smv
@@
-26,40
+26,40
@@
VAR
ph5: phil(f[4], f[6]);
ph6: phil(f[5], f[0]);
ASSIGN
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
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
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
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
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
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
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
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(
TRUE: free;
esac;
LTLSPEC F(