Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

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

History | View | Annotate | Download (3.57 KB)

1

    
2
node Sofar( X : bool ) returns ( Sofar : bool );
3
let
4
    Sofar = X -> X and pre Sofar;
5
tel
6

    
7
node excludes9( X1, X2, X3, X4, X5, X6, X7, X8, X9 : bool ) returns ( excludes : bool );
8
let
9
    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
10
                  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
11
              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
12
              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
13
              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
14
              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
15
              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
16
              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
17
              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
18
              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;
19
tel
20

    
21
node ticket3i(e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
22
init_a1, init_a2, init_a3, init_t : int) returns (
23
p1, p2, p3, t, s, a1, a2, a3 : int; erreur_ticket3i : bool);
24
var
25
   g1, g2, g3, g4, g5, g6, g7, g8, g9 : bool;
26
let
27

    
28
   erreur_ticket3i = if((p1>=3) or (p2>=3) or (p3>=3)) then true else false;
29

    
30
   g1 = pre p1 = 0;
31
   g2 = pre p1 = 1 and pre s >= a1;
32
   g3 = pre p1 = 2;
33
   g4 = pre p2 = 0;
34
   g5 = pre p2 = 1 and pre s >= a2;
35
   g6 = pre p2 = 2;
36
   g7 = pre p3 = 0;
37
   g8 = pre p3 = 1 and pre s >= a3;
38
   g9 = pre p3 = 2;
39

    
40
   p1 = 0 -> 
41
   if(e1) then if(g1) then 1 else pre p1 else 
42
   if(e2) then if(g2) then 2 else pre p1 else 
43
   if(e3) then if(g3) then 0 else pre p1 else 
44
   pre p1;
45

    
46
   p2 = 0 -> 
47
   if(e4) then if(g4) then 1 else pre p2 else 
48
   if(e5) then if(g5) then 2 else pre p2 else 
49
   if(e6) then if(g6) then 0 else pre p2 else 
50
   pre p2;
51

    
52
   p3 = 0 -> 
53
   if(e7) then if(g7) then 1 else pre p3 else 
54
   if(e8) then if(g8) then 2 else pre p3 else 
55
   if(e9) then if(g9) then 0 else pre p3 else 
56
   pre p3;
57

    
58
   t = init_t -> 
59
   if(e1) then if(g1) then pre t+1 else pre t else 
60
   if(e4) then if(g4) then pre t+1 else pre t else 
61
   if(e7) then if(g7) then pre t+1 else pre t else 
62
   pre t;
63

    
64
   s = t -> 
65
   if(e3) then if(g3) then pre s+1 else pre s else 
66
   if(e6) then if(g6) then pre s+1 else pre s else 
67
   if(e9) then if(g9) then pre s+1 else pre s else 
68
   pre s;
69

    
70
   a1 = init_a1 -> 
71
   if(e1) then if(g1) then pre t else pre a1 else 
72
   pre a1;
73

    
74
   a2 = init_a2 -> 
75
   if(e4) then if(g4) then pre t else pre a2 else 
76
   pre a2;
77

    
78
   a3 = init_a3 -> 
79
   if(e7) then if(g7) then pre t else pre a3 else 
80
   pre a3;
81

    
82
tel
83

    
84
-- Not provable in luke-bitvec
85
node top( e1, e2, e3, e4, e5, e6, e7, e8, e9 : bool;
86
         init_a1, init_a2, init_a3, init_t : int )
87
returns ( OK : bool );
88
    var p1, p2, p3, t, s, a1, a2, a3 : int;
89
        erreur_ticket3i : bool;
90
        env : bool;
91
let
92
    ( p1, p2, p3, t, s, a1, a2, a3 , erreur_ticket3i ) =
93
        ticket3i( e1, e2, e3, e4, e5, e6, e7, e8, e9,
94
                  init_a1, init_a2, init_a3, init_t );
95
    env = Sofar( excludes9( e1, e2, e3, e4, e5, e6, e7, e8, e9 ) and
96
                 init_a1 >= 0 and
97
                 init_a2 >= 0 and
98
                 init_a3 >= 0 and
99
                 init_t >= 0);
100
    OK = env => s >= 0;
101
    --%PROPERTY OK=true;
102
    --%MAIN;
103
tel