Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.58 KB)

1
--
2
-- Source: Magnus Ljung
3
-- This is the source to the UMS example. It is taken from HLR92.
4
--
5

    
6
node Sofar( X : bool ) returns ( Sofar : bool );
7
let
8
    Sofar = X -> X and pre Sofar;
9
tel
10

    
11
node edge(X: bool) returns(Y: bool);
12
let
13
    Y = X -> X and not pre(X);
14
tel
15

    
16
node after(A: bool) returns(afterA: bool);
17
let
18
    afterA = false -> pre(A or afterA);
19
tel
20

    
21
node always_since(B, A: bool) returns(alwaysBsinceA: bool);
22
let
23
    alwaysBsinceA = if A then B else if after(A) then
24
                           B and pre(alwaysBsinceA) else true;
25
tel
26

    
27
node once_since(C, A: bool) returns(onceCsinceA: bool);
28
let
29
    onceCsinceA = if A then C else if after(A) then
30
                          C or pre(onceCsinceA) else true;
31
tel
32

    
33
node implies(A, B: bool) returns(AimpliesB: bool);
34
let
35
    AimpliesB = not A or B;
36
tel
37

    
38
node always_from_to(B, A, C: bool) returns(X: bool);
39
let
40
    X = implies(after(A), always_since(B, A) or once_since(C, A));
41
tel
42

    
43
node UMS(on_A, on_B, on_C, ack_AB, ack_BC: bool)
44
returns(grant_access, grant_exit, do_AB, do_BC: bool);
45
var
46
   empty_section, only_on_B: bool;
47
let
48
   grant_access = empty_section and ack_AB;
49
   grant_exit = only_on_B and ack_BC;
50
   do_AB = not ack_AB and empty_section;
51
   do_BC = not ack_BC and only_on_B;
52
   empty_section = not(on_A or on_B or on_C);
53
   only_on_B = on_B and not(on_A or on_C);
54
tel
55

    
56
node top(on_A, on_B, on_C, ack_AB, ack_BC: bool)
57
returns(OK: bool);
58
var
59
   grant_access, grant_exit: bool;
60
   do_AB, do_BC: bool;
61
   no_collision, exclusive_req: bool;
62
   no_derail_AB, no_derail_BC: bool;
63
   empty_section, only_on_B: bool;
64
   env : bool;
65
let
66
   empty_section = not(on_A or on_B or on_C);
67
   only_on_B = on_B and not(on_A or on_C);
68

    
69
   -- UMS CALL
70
   (grant_access, grant_exit, do_AB, do_BC) =
71
       UMS(on_A, on_B, on_C, ack_AB, ack_BC);
72

    
73
   env = Sofar( not(ack_AB and ack_BC) and
74
               always_from_to(ack_AB, ack_AB, do_BC) and
75
               always_from_to(ack_BC, ack_BC, do_AB) and
76
               (empty_section -> true) and
77
               (true -> implies(edge(not empty_section), pre grant_access)) and
78
               (true -> implies(edge(on_C), pre grant_exit)) and
79
               implies(edge(not on_A), on_B) and
80
               implies(edge(not on_B), on_A or on_C) );
81

    
82
   -- PROPERTIES
83
   no_collision = implies(grant_access, empty_section);
84
   exclusive_req = not(do_AB and do_BC);
85
   no_derail_AB = always_from_to(ack_AB, grant_access, only_on_B);
86
   no_derail_BC = always_from_to(ack_BC, grant_exit, empty_section);
87

    
88
   OK = env => no_collision and exclusive_req and
89
                     no_derail_AB and no_derail_BC;
90
   --%PROPERTY OK=true;
91
   --%MAIN;
92
tel