Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec / optim / wpdir / typed / Axiomatic.ergo @ 6a93d814

History | View | Annotate | Download (2.51 KB)

1
(* ---------------------------------------------------------- *)
2
(* --- Global Definitions                                 --- *)
3
(* ---------------------------------------------------------- *)
4

    
5
predicate P_trans_totoA() = true
6

    
7
predicate P_clock_d() = true
8

    
9
predicate P_trans_d
10
    (x:int,
11
    d:int) =
12
    ((0 = d) and (x <= 0)) or ((1 = d) and (0 < x))
13

    
14
predicate P_trans_totoB
15
    (x:int,
16
    d:int) =
17
    P_trans_totoA and (P_clock_d -> P_trans_d(x, d))
18

    
19
predicate P_clock_toto_2(d:int) = 1 = d
20

    
21
predicate P_trans_toto_2(x:int, toto_2_0:int) = (0 = x) <-> (0 <> toto_2_0)
22

    
23
predicate P_trans_totoC
24
    (x:int,
25
    d:int,
26
    toto_2_0:int) =
27
    P_trans_totoB(x, d) and
28
    (P_clock_toto_2(d) -> P_trans_toto_2(x, toto_2_0))
29

    
30
predicate P_clock_c(d:int) = 1 = d
31

    
32
predicate P_trans_c
33
    (toto_2_0:int,
34
    c:int) =
35
    ((0 = c) and (0 <> toto_2_0)) or ((0 = toto_2_0) and (1 = c))
36

    
37
predicate P_trans_totoD
38
    (x:int,
39
    d:int,
40
    c:int) =
41
    exists i : int. is_uint32(i) and P_trans_totoC(x, d, i) and
42
    (P_clock_c(d) -> P_trans_c(i, c))
43

    
44
predicate P_clock_b2(d:int, c:int) = (0 = c) and P_clock_c(d)
45

    
46
predicate P_trans_b2(b2_0:int) = 2 = b2_0
47

    
48
predicate P_trans_totoE
49
    (x:int,
50
    d:int,
51
    c:int,
52
    b2_0:int) =
53
    P_trans_totoD(x, d, c) and (P_clock_b2(d, c) -> P_trans_b2(b2_0))
54

    
55
predicate P_clock_b1(d:int, c:int) = (1 = c) and P_clock_c(d)
56

    
57
predicate P_trans_b1(b1_0:int) = 1 = b1_0
58

    
59
predicate P_trans_totoF
60
    (x:int,
61
    d:int,
62
    c:int,
63
    b2_0:int,
64
    b1_0:int) =
65
    P_trans_totoE(x, d, c, b2_0) and (P_clock_b1(d, c) -> P_trans_b1(b1_0))
66

    
67
predicate P_clock_z(d:int) = P_clock_c(d)
68

    
69
predicate P_trans_z
70
    (c:int,
71
    b1_0:int,
72
    b2_0:int,
73
    z:int) =
74
    ((1 = c) -> (b1_0 = z)) and ((0 = c) -> (b2_0 = z))
75

    
76
predicate P_trans_totoG
77
    (x:int,
78
    d:int,
79
    z:int) =
80
    exists i_2,i_1,i : int. is_sint32(i) and is_sint32(i_1) and
81
    is_uint32(i_2) and P_trans_totoF(x, d, i_2, i_1, i) and
82
    (P_clock_z(d) -> P_trans_z(i_2, i, i_1, z))
83

    
84
predicate P_clock_b3(d:int) = 0 = d
85

    
86
predicate P_trans_b3(b3_0:int) = 3 = b3_0
87

    
88
predicate P_trans_totoH
89
    (x:int,
90
    d:int,
91
    z:int,
92
    b3_0:int) =
93
    P_trans_totoG(x, d, z) and (P_clock_b3(d) -> P_trans_b3(b3_0))
94

    
95
predicate P_clock_y() = P_clock_d
96

    
97
predicate P_trans_y
98
    (d:int,
99
    b3_0:int,
100
    z:int,
101
    y:int) =
102
    ((0 = d) -> (b3_0 = y)) and ((1 = d) -> (y = z))
103

    
104
predicate P_trans_totoI
105
    (x:int,
106
    y:int) =
107
    exists i_2,i_1,i : int. is_sint32(i_1) and is_sint32(i_2) and
108
    is_uint32(i) and P_trans_totoH(x, i, i_2, i_1) and
109
    (P_clock_y -> P_trans_y(i, i_1, i_2, y))
110