Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / test / src / kind_fmcad08 / misc / ticket3i_7_e8_2126_e7_78.lus @ 22fe1c93

History | View | Annotate | Download (3.66 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X or pre Sofar;
5
tel
6
node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool );
7
let
8
    excludes = not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
9
                  X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
10
              not X1 and     X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
11
              not X1 and not X2 and     X3 and not X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
12
              not X1 and not X2 and not X3 and     X4 and not X5 and not X6 and not X7 and not X8 and not X9 or
13
              not X1 and not X2 and not X3 and not X4 and     X5 and not X6 and not X7 and not X8 and not X9 or
14
              not X1 and not X2 and not X3 and not X4 and not X5 and     X6 and not X7 and not X8 and not X9 or
15
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and     X7 and not X8 and not X9 or
16
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and     X8 and not X9 or
17
              not X1 and not X2 and not X3 and not X4 and not X5 and not X6 and not X7 and not X8 and     X9;
18
tel
19
node ticket3i(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
20
init_a1, init_a2, init_a3, init_t : int) returns (
21
p1, p2, p3, t, s, a1, a2, a3 : int; erreur_ticket3i : bool);
22
var
23
   g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool;
24
let
25
   erreur_ticket3i = if((p1>=3) and (p2>=3) or (p3>=3)) then true else false;
26
   g1 = pre p1 = 0;
27
   g2 = pre p1 = 1 and pre s >= a1;
28
   g3 = pre p1 = 2;
29
   g4 = pre p2 = 0;
30
   g5 = pre p2 = 1 and pre s >= a2;
31
   g6 = pre p2 = 2;
32
   g7 = pre p3 = 0;
33
   g8 = pre p3 = 1 and pre s >= a3;
34
   g9 = pre p3 = 2;
35
   p1 = 0 -> 
36
   if(e1) then if(g1) then 1 else pre p1 else 
37
   if(e2) then if(g2) then 2 else pre p1 else 
38
   if(e3) then if(g3) then 0 else pre p1 else 
39
   pre p1;
40
   p2 = 0 -> 
41
   if(e4) then if(g4) then 1 else pre p2 else 
42
   if(e5) then if(g5) then 2 else pre p2 else 
43
   if(e6) then if(g6) then 0 else pre p2 else 
44
   pre p2;
45
   p3 = 0 -> 
46
   if(e7) then if(g7) then 1 else pre p3 else 
47
   if(e8) then if(g8) then 2 else pre p3 else 
48
   if(e9) then if(g9) then 0 else pre p3 else 
49
   pre p3;
50
   t = init_t -> 
51
   if(e1) then if(g1) then pre t+1 else pre t else 
52
   if(e4) then if(g4) then pre t+1 else pre t else 
53
   if(e7) then if(g7) then pre t+1 else pre t else 
54
   pre t;
55
   s = t -> 
56
   if(e3) then if(g3) then pre s+1 else pre s else 
57
   if(e6) then if(g6) then pre s+1 else pre s else 
58
   if(e9) then if(g9) then pre s+1 else pre s else 
59
   pre s;
60
   a1 = init_a1 -> 
61
   if(e1) then if(g1) then pre t else pre a1 else 
62
   pre a1;
63
   a2 = init_a2 -> 
64
   if(e4) then if(g4) then pre t else pre a2 else 
65
   pre a2;
66
   a3 = init_a3 -> 
67
   if(e7) then if(g7) then pre t else pre a3 else 
68
   pre a3;
69
tel
70
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
71
         init_a1, init_a2, init_a3, init_t : int )
72
returns ( OK : bool );
73
    var p1, p2, p3, t, s, a1, a2, a3 : int;
74
        erreur_ticket3i : bool;
75
        env : bool;
76
let
77
    ( p1, p2, p3, t, s, a1, a2, a3 , erreur_ticket3i ) =
78
        ticket3i( e1, e2, e3, e4, e5, e6, e7, e8, e9,
79
                  init_a1, init_a2, init_a3, init_t );
80
    env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and
81
                 init_a1 >= 0 and
82
                 init_a2 >= 0 and
83
                 init_a3 >= 0 and
84
                 init_t >= 0 );
85
    OK = env => 0 <= p1 and p1 <= 3 and
86
                     0 <= p2 and p2 <= 3 and
87
                     0 <= p3 and p3 <= 3 and
88
                     p1 + p2 + p3 <= 9;
89
  --%MAIN;
90
  --%PROPERTY  OK=true;
91
tel