Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / production_cell_e8_6_e7_651.lus @ 22fe1c93

 1 ```node redge (signal: bool) returns (r: bool); ``` ```let ``` ``` r = signal -> (signal or pre(not signal)); ``` ```tel ``` ```node fedge (signal: bool) returns (f: bool); ``` ```let ``` ``` f = redge(not signal); ``` ```tel ``` ```node sustain (on, off: bool) returns (s: bool); ``` ```let ``` ``` s = on -> if on then true else if off then false else pre(s); ``` ```tel ``` ```node top (MaySafelyMove, TryToMove1, TryToMove2: bool) ``` ```returns (OK: bool); ``` ```var ``` ``` MayMove1, MayMove2: bool; ``` ``` start1, start2, stop, moving: bool; ``` ```let ``` ``` MayMove1 = TryToMove1 and MaySafelyMove; ``` ``` MayMove2 = TryToMove2 and MaySafelyMove; ``` ``` moving = sustain(start1 and start2, stop); ``` ``` start1 = redge(MayMove1 and (true -> pre(not TryToMove2))); ``` ``` start2 = redge(MayMove2 and (true -> pre(not TryToMove1))); ``` ``` stop = fedge(MayMove1) or fedge(MayMove2); ``` ``` OK = true -> if (not redge(TryToMove1) or not redge(TryToMove2)) then ( ``` ``` ((not start1 and not start2) or (not start2 and not stop) ``` ``` or (not start1 and not stop)) ``` ``` and not (start1 and start2 and stop) ``` ``` and if moving then MaySafelyMove else true) ``` ``` else true; ``` ``` --%MAIN; ``` ``` --%PROPERTY OK=true; ``` ```tel ```