Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

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