Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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