Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / simulation / production_cell_e7_21.lus @ 65f71d05

History | View | Annotate | Download (1.08 KB)

1

    
2
node redge (signal: bool) returns (r: bool);
3
let
4
  r = signal -> (signal or 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
--@ ensures OK;
15
node top (MaySafelyMove, TryToMove1, TryToMove2: bool)
16
returns (OK: bool);
17
var
18
  MayMove1, MayMove2: bool;
19
  start1, start2, stop, moving: bool;
20
let
21
  MayMove1 = TryToMove1 and MaySafelyMove;
22
  MayMove2 = TryToMove2 and MaySafelyMove;
23
  moving = sustain(start1 or start2, stop);
24
  start1 = redge(MayMove1 and (true -> pre(not TryToMove2)));
25
  start2 = redge(MayMove2 and (true -> pre(not TryToMove1)));
26
  stop = fedge(MayMove1) or fedge(MayMove2);
27
  OK = true -> if (not redge(TryToMove1) or not redge(TryToMove2)) then (
28
         ((not start1 and not start2) or (not start2 and not stop) 
29
            or (not start1 and not stop))
30
         and not (start1 and start2 and stop) 
31
         and if moving then MaySafelyMove else true)
32
         else true;
33
  --%MAIN;
34
  --%PROPERTY  OK=true;
35
tel