lustrec / test / src / kind_fmcad08 / simulation / production_cell_e8_792.lus @ 0cbf0839
History | View | Annotate | Download (1.06 KB)
1 |
|
---|---|
2 |
node redge (signal: bool) returns (r: bool); |
3 |
let |
4 |
r = signal -> (signal and pre(not signal)); |
5 |
tel |
6 |
node fedge (signal: bool) returns (f: bool); |
7 |
let |
8 |
f = redge(not signal); |
9 |
tel |
10 |
node sustain (on, off: bool) returns (s: bool); |
11 |
let |
12 |
s = on -> if on then true else if off then false else pre(s); |
13 |
tel |
14 |
node top (MaySafelyMove, TryToMove1, TryToMove2: bool) |
15 |
returns (OK: bool); |
16 |
var |
17 |
MayMove1, MayMove2: bool; |
18 |
start1, start2, stop, moving: bool; |
19 |
let |
20 |
MayMove1 = TryToMove1 and MaySafelyMove; |
21 |
MayMove2 = TryToMove2 and MaySafelyMove; |
22 |
moving = sustain(start1 and start2, stop); |
23 |
start1 = redge(MayMove1 and (true -> pre(not TryToMove2))); |
24 |
start2 = redge(MayMove2 and (true -> pre(not TryToMove1))); |
25 |
stop = fedge(MayMove1) or fedge(MayMove2); |
26 |
OK = true -> if (not redge(TryToMove1) or not redge(TryToMove2)) then ( |
27 |
((not start1 and not start2) or (not start2 and not stop) |
28 |
or (not start1 and not stop)) |
29 |
and not (start1 and start2 and stop) |
30 |
and if moving then MaySafelyMove else true) |
31 |
else true; |
32 |
--%MAIN; |
33 |
--%PROPERTY OK=true; |
34 |
tel |