Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_goto_from_test / goto_from_test.smt2 @ 6c3ea955

History | View | Annotate | Download (10.3 KB)

1
; goto_from_test
2
(declare-var goto_from_test.In1_1_1 Real)
3
(declare-var goto_from_test.In2_1_1 Int)
4
(declare-var goto_from_test.In2_1_2 Int)
5
(declare-var goto_from_test.In3_1_1 Bool)
6
(declare-var goto_from_test.In3_1_2 Bool)
7
(declare-var goto_from_test.In3_1_3 Bool)
8
(declare-var goto_from_test.In3_1_4 Bool)
9
(declare-var goto_from_test.In3_1_5 Bool)
10
(declare-var goto_from_test.In3_1_6 Bool)
11
(declare-var goto_from_test.Out1_1_1 Real)
12
(declare-var goto_from_test.Out2_2_1 Int)
13
(declare-var goto_from_test.Out2_2_2 Int)
14
(declare-var goto_from_test.Out3_3_1 Int)
15
(declare-var goto_from_test.Out3_3_2 Int)
16
(declare-var goto_from_test.Out3_3_3 Int)
17
(declare-var goto_from_test.Out3_3_4 Int)
18
(declare-var goto_from_test.Out3_3_5 Int)
19
(declare-var goto_from_test.Out3_3_6 Int)
20
(declare-var goto_from_test.ni_0._arrow._first_c Bool)
21
(declare-var goto_from_test.ni_0._arrow._first_m Bool)
22
(declare-var goto_from_test.ni_0._arrow._first_x Bool)
23
(declare-var goto_from_test.Goto_A_1 Real)
24
(declare-var goto_from_test.Goto_B_1 Int)
25
(declare-var goto_from_test.Goto_B_2 Int)
26
(declare-var goto_from_test.Goto_C_1 Bool)
27
(declare-var goto_from_test.Goto_C_2 Bool)
28
(declare-var goto_from_test.Goto_C_3 Bool)
29
(declare-var goto_from_test.Goto_C_4 Bool)
30
(declare-var goto_from_test.Goto_C_5 Bool)
31
(declare-var goto_from_test.Goto_C_6 Bool)
32
(declare-var goto_from_test.Subsystem1_Add_1_1 Int)
33
(declare-var goto_from_test.Subsystem1_Add_1_2 Int)
34
(declare-var goto_from_test.Subsystem1_From_1_1 Int)
35
(declare-var goto_from_test.Subsystem1_From_1_2 Int)
36
(declare-var goto_from_test.Subsystem2_Add_1_1 Int)
37
(declare-var goto_from_test.Subsystem2_Add_1_2 Int)
38
(declare-var goto_from_test.Subsystem2_Add_1_3 Int)
39
(declare-var goto_from_test.Subsystem2_Add_1_4 Int)
40
(declare-var goto_from_test.Subsystem2_Add_1_5 Int)
41
(declare-var goto_from_test.Subsystem2_Add_1_6 Int)
42
(declare-var goto_from_test.Subsystem2_From_1_1 Bool)
43
(declare-var goto_from_test.Subsystem2_From_1_2 Bool)
44
(declare-var goto_from_test.Subsystem2_From_1_3 Bool)
45
(declare-var goto_from_test.Subsystem2_From_1_4 Bool)
46
(declare-var goto_from_test.Subsystem2_From_1_5 Bool)
47
(declare-var goto_from_test.Subsystem2_From_1_6 Bool)
48
(declare-var goto_from_test.Subsystem_Add_1_1 Real)
49
(declare-var goto_from_test.Subsystem_From_1_1 Real)
50
(declare-var goto_from_test.__goto_from_test_1 Bool)
51
(declare-var goto_from_test.__goto_from_test_10 Int)
52
(declare-var goto_from_test.__goto_from_test_11 Int)
53
(declare-var goto_from_test.__goto_from_test_12 Int)
54
(declare-var goto_from_test.__goto_from_test_13 Int)
55
(declare-var goto_from_test.__goto_from_test_2 Int)
56
(declare-var goto_from_test.__goto_from_test_3 Int)
57
(declare-var goto_from_test.__goto_from_test_4 Int)
58
(declare-var goto_from_test.__goto_from_test_5 Int)
59
(declare-var goto_from_test.__goto_from_test_6 Int)
60
(declare-var goto_from_test.__goto_from_test_7 Int)
61
(declare-var goto_from_test.__goto_from_test_8 Int)
62
(declare-var goto_from_test.__goto_from_test_9 Int)
63
(declare-var goto_from_test.i_virtual_local Real)
64
(declare-rel goto_from_test_reset (Bool Bool))
65
(declare-rel goto_from_test_step (Real Int Int Bool Bool Bool Bool Bool Bool Real Int Int Int Int Int Int Int Int Bool Bool))
66

    
67
(rule (=> 
68
  (and 
69
       
70
       (= goto_from_test.ni_0._arrow._first_m true)
71
  )
72
  (goto_from_test_reset goto_from_test.ni_0._arrow._first_c
73
                        goto_from_test.ni_0._arrow._first_m)
74
))
75

    
76
(rule (=> 
77
  (and (= goto_from_test.ni_0._arrow._first_m goto_from_test.ni_0._arrow._first_c)
78
       (and (= goto_from_test.__goto_from_test_1 (ite goto_from_test.ni_0._arrow._first_m true false))
79
            (= goto_from_test.ni_0._arrow._first_x false))
80
       (and (or (not (= goto_from_test.__goto_from_test_1 true))
81
               (= goto_from_test.i_virtual_local 0.0))
82
            (or (not (= goto_from_test.__goto_from_test_1 false))
83
               (= goto_from_test.i_virtual_local 1.0))
84
       )
85
       (and (or (not (= goto_from_test.In3_1_3 true))
86
               (= goto_from_test.__goto_from_test_9 1))
87
            (or (not (= goto_from_test.In3_1_3 false))
88
               (= goto_from_test.__goto_from_test_9 0))
89
       )
90
       (= goto_from_test.Goto_C_3 goto_from_test.In3_1_3)
91
       (= goto_from_test.Subsystem2_From_1_3 goto_from_test.Goto_C_3)
92
       (and (or (not (= goto_from_test.Subsystem2_From_1_3 true))
93
               (= goto_from_test.__goto_from_test_8 1))
94
            (or (not (= goto_from_test.Subsystem2_From_1_3 false))
95
               (= goto_from_test.__goto_from_test_8 0))
96
       )
97
       (and (or (not (= goto_from_test.In3_1_4 true))
98
               (= goto_from_test.__goto_from_test_7 1))
99
            (or (not (= goto_from_test.In3_1_4 false))
100
               (= goto_from_test.__goto_from_test_7 0))
101
       )
102
       (= goto_from_test.Goto_C_4 goto_from_test.In3_1_4)
103
       (= goto_from_test.Subsystem2_From_1_4 goto_from_test.Goto_C_4)
104
       (and (or (not (= goto_from_test.Subsystem2_From_1_4 true))
105
               (= goto_from_test.__goto_from_test_6 1))
106
            (or (not (= goto_from_test.Subsystem2_From_1_4 false))
107
               (= goto_from_test.__goto_from_test_6 0))
108
       )
109
       (and (or (not (= goto_from_test.In3_1_5 true))
110
               (= goto_from_test.__goto_from_test_5 1))
111
            (or (not (= goto_from_test.In3_1_5 false))
112
               (= goto_from_test.__goto_from_test_5 0))
113
       )
114
       (= goto_from_test.Goto_C_5 goto_from_test.In3_1_5)
115
       (= goto_from_test.Subsystem2_From_1_5 goto_from_test.Goto_C_5)
116
       (and (or (not (= goto_from_test.Subsystem2_From_1_5 true))
117
               (= goto_from_test.__goto_from_test_4 1))
118
            (or (not (= goto_from_test.Subsystem2_From_1_5 false))
119
               (= goto_from_test.__goto_from_test_4 0))
120
       )
121
       (and (or (not (= goto_from_test.In3_1_6 true))
122
               (= goto_from_test.__goto_from_test_3 1))
123
            (or (not (= goto_from_test.In3_1_6 false))
124
               (= goto_from_test.__goto_from_test_3 0))
125
       )
126
       (= goto_from_test.Goto_C_6 goto_from_test.In3_1_6)
127
       (= goto_from_test.Subsystem2_From_1_6 goto_from_test.Goto_C_6)
128
       (and (or (not (= goto_from_test.Subsystem2_From_1_6 true))
129
               (= goto_from_test.__goto_from_test_2 1))
130
            (or (not (= goto_from_test.Subsystem2_From_1_6 false))
131
               (= goto_from_test.__goto_from_test_2 0))
132
       )
133
       (and (or (not (= goto_from_test.In3_1_1 true))
134
               (= goto_from_test.__goto_from_test_13 1))
135
            (or (not (= goto_from_test.In3_1_1 false))
136
               (= goto_from_test.__goto_from_test_13 0))
137
       )
138
       (= goto_from_test.Goto_C_1 goto_from_test.In3_1_1)
139
       (= goto_from_test.Subsystem2_From_1_1 goto_from_test.Goto_C_1)
140
       (and (or (not (= goto_from_test.Subsystem2_From_1_1 true))
141
               (= goto_from_test.__goto_from_test_12 1))
142
            (or (not (= goto_from_test.Subsystem2_From_1_1 false))
143
               (= goto_from_test.__goto_from_test_12 0))
144
       )
145
       (and (or (not (= goto_from_test.In3_1_2 true))
146
               (= goto_from_test.__goto_from_test_11 1))
147
            (or (not (= goto_from_test.In3_1_2 false))
148
               (= goto_from_test.__goto_from_test_11 0))
149
       )
150
       (= goto_from_test.Goto_C_2 goto_from_test.In3_1_2)
151
       (= goto_from_test.Subsystem2_From_1_2 goto_from_test.Goto_C_2)
152
       (and (or (not (= goto_from_test.Subsystem2_From_1_2 true))
153
               (= goto_from_test.__goto_from_test_10 1))
154
            (or (not (= goto_from_test.Subsystem2_From_1_2 false))
155
               (= goto_from_test.__goto_from_test_10 0))
156
       )
157
       (= goto_from_test.Goto_A_1 goto_from_test.In1_1_1)
158
       (= goto_from_test.Subsystem_From_1_1 goto_from_test.Goto_A_1)
159
       (= goto_from_test.Subsystem_Add_1_1 (+ goto_from_test.In1_1_1 goto_from_test.Subsystem_From_1_1))
160
       (= goto_from_test.Subsystem2_Add_1_6 (+ goto_from_test.__goto_from_test_3 goto_from_test.__goto_from_test_2))
161
       (= goto_from_test.Subsystem2_Add_1_5 (+ goto_from_test.__goto_from_test_5 goto_from_test.__goto_from_test_4))
162
       (= goto_from_test.Subsystem2_Add_1_4 (+ goto_from_test.__goto_from_test_7 goto_from_test.__goto_from_test_6))
163
       (= goto_from_test.Subsystem2_Add_1_3 (+ goto_from_test.__goto_from_test_9 goto_from_test.__goto_from_test_8))
164
       (= goto_from_test.Subsystem2_Add_1_2 (+ goto_from_test.__goto_from_test_11 goto_from_test.__goto_from_test_10))
165
       (= goto_from_test.Subsystem2_Add_1_1 (+ goto_from_test.__goto_from_test_13 goto_from_test.__goto_from_test_12))
166
       (= goto_from_test.Goto_B_2 goto_from_test.In2_1_2)
167
       (= goto_from_test.Subsystem1_From_1_2 goto_from_test.Goto_B_2)
168
       (= goto_from_test.Goto_B_1 goto_from_test.In2_1_1)
169
       (= goto_from_test.Subsystem1_From_1_1 goto_from_test.Goto_B_1)
170
       (= goto_from_test.Subsystem1_Add_1_2 (+ goto_from_test.In2_1_2 goto_from_test.Subsystem1_From_1_2))
171
       (= goto_from_test.Subsystem1_Add_1_1 (+ goto_from_test.In2_1_1 goto_from_test.Subsystem1_From_1_1))
172
       (= goto_from_test.Out3_3_6 goto_from_test.Subsystem2_Add_1_6)
173
       (= goto_from_test.Out3_3_5 goto_from_test.Subsystem2_Add_1_5)
174
       (= goto_from_test.Out3_3_4 goto_from_test.Subsystem2_Add_1_4)
175
       (= goto_from_test.Out3_3_3 goto_from_test.Subsystem2_Add_1_3)
176
       (= goto_from_test.Out3_3_2 goto_from_test.Subsystem2_Add_1_2)
177
       (= goto_from_test.Out3_3_1 goto_from_test.Subsystem2_Add_1_1)
178
       (= goto_from_test.Out2_2_2 goto_from_test.Subsystem1_Add_1_2)
179
       (= goto_from_test.Out2_2_1 goto_from_test.Subsystem1_Add_1_1)
180
       (= goto_from_test.Out1_1_1 goto_from_test.Subsystem_Add_1_1)
181
       )
182
  (goto_from_test_step goto_from_test.In1_1_1
183
                       goto_from_test.In2_1_1
184
                       goto_from_test.In2_1_2
185
                       goto_from_test.In3_1_1
186
                       goto_from_test.In3_1_2
187
                       goto_from_test.In3_1_3
188
                       goto_from_test.In3_1_4
189
                       goto_from_test.In3_1_5
190
                       goto_from_test.In3_1_6
191
                       goto_from_test.Out1_1_1
192
                       goto_from_test.Out2_2_1
193
                       goto_from_test.Out2_2_2
194
                       goto_from_test.Out3_3_1
195
                       goto_from_test.Out3_3_2
196
                       goto_from_test.Out3_3_3
197
                       goto_from_test.Out3_3_4
198
                       goto_from_test.Out3_3_5
199
                       goto_from_test.Out3_3_6
200
                       goto_from_test.ni_0._arrow._first_c
201
                       goto_from_test.ni_0._arrow._first_x)
202
))
203