Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (2.44 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X and pre Sofar;
5
tel
6
node edge(X: bool) returns(Y: bool);
7
let
8
    Y = X -> X and not pre(X);
9
tel
10
node after(A: bool) returns(afterA: bool);
11
let
12
    afterA = false -> pre(A and afterA);
13
tel
14
node always_since(B, A: bool) returns(alwaysBsinceA: bool);
15
let
16
    alwaysBsinceA = if A then B else if after(A) then
17
                           B and pre(alwaysBsinceA) else true;
18
tel
19
node once_since(C, A: bool) returns(onceCsinceA: bool);
20
let
21
    onceCsinceA = if A then C else if after(A) then
22
                          C or pre(onceCsinceA) else true;
23
tel
24
node implies(A, B: bool) returns(AimpliesB: bool);
25
let
26
    AimpliesB = not A or B;
27
tel
28
node always_from_to(B, A, C: bool) returns(X: bool);
29
let
30
    X = implies(after(A), always_since(B, A) or once_since(C, A));
31
tel
32
node UMS(on_A, on_B, on_C, ack_AB, ack_BC: bool)
33
returns(grant_access, grant_exit, do_AB, do_BC: bool);
34
var
35
   empty_section, only_on_B: bool;
36
let
37
   grant_access = empty_section and ack_AB;
38
   grant_exit = only_on_B and ack_BC;
39
   do_AB = not ack_AB and empty_section;
40
   do_BC = not ack_BC and only_on_B;
41
   empty_section = not(on_A or on_B or on_C);
42
   only_on_B = on_B and not(on_A or on_C);
43
tel
44
node top(on_A, on_B, on_C, ack_AB, ack_BC: bool)
45
returns(OK: bool);
46
var
47
   grant_access, grant_exit: bool;
48
   do_AB, do_BC: bool;
49
   no_collision, exclusive_req: bool;
50
   no_derail_AB, no_derail_BC: bool;
51
   empty_section, only_on_B: bool;
52
   env : bool;
53
let
54
   empty_section = not(on_A or on_B or on_C);
55
   only_on_B = on_B and not(on_A or on_C);
56
   (grant_access, grant_exit, do_AB, do_BC) =
57
       UMS(on_A, on_B, on_C, ack_AB, ack_BC);
58
   env = Sofar( not(ack_AB and ack_BC) and
59
               always_from_to(ack_AB, ack_AB, do_BC) and
60
               always_from_to(ack_BC, ack_BC, do_AB) and
61
               (empty_section -> true) and
62
               (true -> implies(edge(not empty_section), pre grant_access)) and
63
               (true -> implies(edge(on_C), pre grant_exit)) and
64
               implies(edge(not on_A), on_B) and
65
               implies(edge(not on_B), on_A or on_C) );
66
   no_collision = implies(grant_access, empty_section);
67
   exclusive_req = not(do_AB and do_BC);
68
   no_derail_AB = always_from_to(ack_AB, grant_access, only_on_B);
69
   no_derail_BC = always_from_to(ack_BC, grant_exit, empty_section);
70
   OK = env => no_collision and exclusive_req and
71
                     no_derail_AB and no_derail_BC;
72
  --%MAIN;
73
  --%PROPERTY  OK=true;
74
tel