lustrec / test / src / kind_fmcad08 / simulation / production_cell.lus @ 22fe1c93
History | View | Annotate | Download (1.41 KB)
1 |
-- From |
---|---|
2 |
-- Production Cell in Lustre: A Case Study, by Leszek Holenderski |
3 |
-- Published in Formal Development of Reactive Systems, Claus Lewerentz and |
4 |
-- Thomas Lindner (eds.), Springer-Verlag, LNCS 891, 1995. |
5 |
|
6 |
|
7 |
node redge (signal: bool) returns (r: bool); |
8 |
let |
9 |
r = signal -> (signal and pre(not signal)); |
10 |
tel |
11 |
|
12 |
|
13 |
node fedge (signal: bool) returns (f: bool); |
14 |
let |
15 |
f = redge(not signal); |
16 |
tel |
17 |
|
18 |
|
19 |
node sustain (on, off: bool) returns (s: bool); |
20 |
let |
21 |
s = on -> if on then true else if off then false else pre(s); |
22 |
tel |
23 |
|
24 |
|
25 |
node top (MaySafelyMove, TryToMove1, TryToMove2: bool) |
26 |
returns (OK: bool); |
27 |
var |
28 |
MayMove1, MayMove2: bool; |
29 |
start1, start2, stop, moving: bool; |
30 |
let |
31 |
MayMove1 = TryToMove1 and MaySafelyMove; |
32 |
MayMove2 = TryToMove2 and MaySafelyMove; |
33 |
moving = sustain(start1 or start2, stop); |
34 |
start1 = redge(MayMove1 and (true -> pre(not TryToMove2))); |
35 |
start2 = redge(MayMove2 and (true -> pre(not TryToMove1))); |
36 |
stop = fedge(MayMove1) or fedge(MayMove2); |
37 |
OK = true -> if (not redge(TryToMove1) or not redge(TryToMove2)) then ( |
38 |
((not start1 and not start2) or (not start2 and not stop) |
39 |
or (not start1 and not stop)) |
40 |
and not (start1 and start2 and stop) |
41 |
and if moving then MaySafelyMove else true) |
42 |
else true; |
43 |
--%MAIN; |
44 |
--%PROPERTY OK=true; |
45 |
|
46 |
-- assert #(redge(TryToMove1), redge(TryToMove2)); |
47 |
-- OK = #(start1, start2, stop) and |
48 |
-- if moving then MaySafelyMove else true; |
49 |
tel |