Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_unitdelay_test / unitdelay_test.smt2 @ 6c3ea955

History | View | Annotate | Download (11.3 KB)

1
; unitdelay_test
2
(declare-var unitdelay_test.In1_1_1 Real)
3
(declare-var unitdelay_test.In2_1_1 Real)
4
(declare-var unitdelay_test.In3_1_1 Bool)
5
(declare-var unitdelay_test.In4_1_1 Int)
6
(declare-var unitdelay_test.In5_1_1 Int)
7
(declare-var unitdelay_test.In6_1_1 Int)
8
(declare-var unitdelay_test.In7_1_1 Bool)
9
(declare-var unitdelay_test.In8_1_1 Bool)
10
(declare-var unitdelay_test.In9_1_1 Bool)
11
(declare-var unitdelay_test.Out1_1_1 Real)
12
(declare-var unitdelay_test.Out2_2_1 Real)
13
(declare-var unitdelay_test.Out3_3_1 Bool)
14
(declare-var unitdelay_test.Out4_4_1 Int)
15
(declare-var unitdelay_test.Out5_5_1 Int)
16
(declare-var unitdelay_test.Out6_6_1 Int)
17
(declare-var unitdelay_test.Out7_7_1 Bool)
18
(declare-var unitdelay_test.Out8_8_1 Bool)
19
(declare-var unitdelay_test.Out9_9_1 Bool)
20
(declare-var unitdelay_test.__unitdelay_test_10_c Real)
21
(declare-var unitdelay_test.__unitdelay_test_2_c Bool)
22
(declare-var unitdelay_test.__unitdelay_test_3_c Bool)
23
(declare-var unitdelay_test.__unitdelay_test_4_c Bool)
24
(declare-var unitdelay_test.__unitdelay_test_5_c Int)
25
(declare-var unitdelay_test.__unitdelay_test_6_c Int)
26
(declare-var unitdelay_test.__unitdelay_test_7_c Int)
27
(declare-var unitdelay_test.__unitdelay_test_8_c Bool)
28
(declare-var unitdelay_test.__unitdelay_test_9_c Real)
29
(declare-var unitdelay_test.ni_0._arrow._first_c Bool)
30
(declare-var unitdelay_test.__unitdelay_test_10_m Real)
31
(declare-var unitdelay_test.__unitdelay_test_2_m Bool)
32
(declare-var unitdelay_test.__unitdelay_test_3_m Bool)
33
(declare-var unitdelay_test.__unitdelay_test_4_m Bool)
34
(declare-var unitdelay_test.__unitdelay_test_5_m Int)
35
(declare-var unitdelay_test.__unitdelay_test_6_m Int)
36
(declare-var unitdelay_test.__unitdelay_test_7_m Int)
37
(declare-var unitdelay_test.__unitdelay_test_8_m Bool)
38
(declare-var unitdelay_test.__unitdelay_test_9_m Real)
39
(declare-var unitdelay_test.ni_0._arrow._first_m Bool)
40
(declare-var unitdelay_test.__unitdelay_test_10_x Real)
41
(declare-var unitdelay_test.__unitdelay_test_2_x Bool)
42
(declare-var unitdelay_test.__unitdelay_test_3_x Bool)
43
(declare-var unitdelay_test.__unitdelay_test_4_x Bool)
44
(declare-var unitdelay_test.__unitdelay_test_5_x Int)
45
(declare-var unitdelay_test.__unitdelay_test_6_x Int)
46
(declare-var unitdelay_test.__unitdelay_test_7_x Int)
47
(declare-var unitdelay_test.__unitdelay_test_8_x Bool)
48
(declare-var unitdelay_test.__unitdelay_test_9_x Real)
49
(declare-var unitdelay_test.ni_0._arrow._first_x Bool)
50
(declare-var unitdelay_test.UnitDelay1_1_1 Real)
51
(declare-var unitdelay_test.UnitDelay2_1_1 Bool)
52
(declare-var unitdelay_test.UnitDelay3_1_1 Int)
53
(declare-var unitdelay_test.UnitDelay4_1_1 Int)
54
(declare-var unitdelay_test.UnitDelay5_1_1 Int)
55
(declare-var unitdelay_test.UnitDelay6_1_1 Bool)
56
(declare-var unitdelay_test.UnitDelay7_1_1 Bool)
57
(declare-var unitdelay_test.UnitDelay8_1_1 Bool)
58
(declare-var unitdelay_test.UnitDelay_1_1 Real)
59
(declare-var unitdelay_test.__unitdelay_test_1 Bool)
60
(declare-var unitdelay_test.i_virtual_local Real)
61
(declare-rel unitdelay_test_reset (Real Bool Bool Bool Int Int Int Bool Real Bool Real Bool Bool Bool Int Int Int Bool Real Bool))
62
(declare-rel unitdelay_test_step (Real Real Bool Int Int Int Bool Bool Bool Real Real Bool Int Int Int Bool Bool Bool Real Bool Bool Bool Int Int Int Bool Real Bool Real Bool Bool Bool Int Int Int Bool Real Bool))
63

    
64
(rule (=> 
65
  (and 
66
       (= unitdelay_test.__unitdelay_test_10_m unitdelay_test.__unitdelay_test_10_c)
67
       (= unitdelay_test.__unitdelay_test_2_m unitdelay_test.__unitdelay_test_2_c)
68
       (= unitdelay_test.__unitdelay_test_3_m unitdelay_test.__unitdelay_test_3_c)
69
       (= unitdelay_test.__unitdelay_test_4_m unitdelay_test.__unitdelay_test_4_c)
70
       (= unitdelay_test.__unitdelay_test_5_m unitdelay_test.__unitdelay_test_5_c)
71
       (= unitdelay_test.__unitdelay_test_6_m unitdelay_test.__unitdelay_test_6_c)
72
       (= unitdelay_test.__unitdelay_test_7_m unitdelay_test.__unitdelay_test_7_c)
73
       (= unitdelay_test.__unitdelay_test_8_m unitdelay_test.__unitdelay_test_8_c)
74
       (= unitdelay_test.__unitdelay_test_9_m unitdelay_test.__unitdelay_test_9_c)
75
       (= unitdelay_test.ni_0._arrow._first_m true)
76
  )
77
  (unitdelay_test_reset unitdelay_test.__unitdelay_test_10_c
78
                        unitdelay_test.__unitdelay_test_2_c
79
                        unitdelay_test.__unitdelay_test_3_c
80
                        unitdelay_test.__unitdelay_test_4_c
81
                        unitdelay_test.__unitdelay_test_5_c
82
                        unitdelay_test.__unitdelay_test_6_c
83
                        unitdelay_test.__unitdelay_test_7_c
84
                        unitdelay_test.__unitdelay_test_8_c
85
                        unitdelay_test.__unitdelay_test_9_c
86
                        unitdelay_test.ni_0._arrow._first_c
87
                        unitdelay_test.__unitdelay_test_10_m
88
                        unitdelay_test.__unitdelay_test_2_m
89
                        unitdelay_test.__unitdelay_test_3_m
90
                        unitdelay_test.__unitdelay_test_4_m
91
                        unitdelay_test.__unitdelay_test_5_m
92
                        unitdelay_test.__unitdelay_test_6_m
93
                        unitdelay_test.__unitdelay_test_7_m
94
                        unitdelay_test.__unitdelay_test_8_m
95
                        unitdelay_test.__unitdelay_test_9_m
96
                        unitdelay_test.ni_0._arrow._first_m)
97
))
98

    
99
(rule (=> 
100
  (and (= unitdelay_test.ni_0._arrow._first_m unitdelay_test.ni_0._arrow._first_c)
101
       (and (= unitdelay_test.__unitdelay_test_1 (ite unitdelay_test.ni_0._arrow._first_m true false))
102
            (= unitdelay_test.ni_0._arrow._first_x false))
103
       (and (or (not (= unitdelay_test.__unitdelay_test_1 false))
104
               (and (= unitdelay_test.i_virtual_local 1.0)
105
                    (= unitdelay_test.UnitDelay1_1_1 unitdelay_test.__unitdelay_test_9_c)
106
                    ))
107
            (or (not (= unitdelay_test.__unitdelay_test_1 true))
108
               (and (= unitdelay_test.i_virtual_local 0.0)
109
                    (= unitdelay_test.UnitDelay1_1_1 0.00000000)
110
                    ))
111
       )
112
       (= unitdelay_test.__unitdelay_test_9_x unitdelay_test.In2_1_1)
113
       (and (or (not (= unitdelay_test.__unitdelay_test_1 true))
114
               (= unitdelay_test.UnitDelay2_1_1 true))
115
            (or (not (= unitdelay_test.__unitdelay_test_1 false))
116
               (= unitdelay_test.UnitDelay2_1_1 unitdelay_test.__unitdelay_test_8_c))
117
       )
118
       (= unitdelay_test.__unitdelay_test_8_x unitdelay_test.In3_1_1)
119
       (and (or (not (= unitdelay_test.__unitdelay_test_1 true))
120
               (= unitdelay_test.UnitDelay3_1_1 0))
121
            (or (not (= unitdelay_test.__unitdelay_test_1 false))
122
               (= unitdelay_test.UnitDelay3_1_1 unitdelay_test.__unitdelay_test_7_c))
123
       )
124
       (= unitdelay_test.__unitdelay_test_7_x unitdelay_test.In4_1_1)
125
       (and (or (not (= unitdelay_test.__unitdelay_test_1 true))
126
               (= unitdelay_test.UnitDelay4_1_1 0))
127
            (or (not (= unitdelay_test.__unitdelay_test_1 false))
128
               (= unitdelay_test.UnitDelay4_1_1 unitdelay_test.__unitdelay_test_6_c))
129
       )
130
       (= unitdelay_test.__unitdelay_test_6_x unitdelay_test.In5_1_1)
131
       (and (or (not (= unitdelay_test.__unitdelay_test_1 true))
132
               (= unitdelay_test.UnitDelay5_1_1 1))
133
            (or (not (= unitdelay_test.__unitdelay_test_1 false))
134
               (= unitdelay_test.UnitDelay5_1_1 unitdelay_test.__unitdelay_test_5_c))
135
       )
136
       (= unitdelay_test.__unitdelay_test_5_x unitdelay_test.In6_1_1)
137
       (and (or (not (= unitdelay_test.__unitdelay_test_1 true))
138
               (= unitdelay_test.UnitDelay6_1_1 false))
139
            (or (not (= unitdelay_test.__unitdelay_test_1 false))
140
               (= unitdelay_test.UnitDelay6_1_1 unitdelay_test.__unitdelay_test_4_c))
141
       )
142
       (= unitdelay_test.__unitdelay_test_4_x unitdelay_test.In7_1_1)
143
       (and (or (not (= unitdelay_test.__unitdelay_test_1 true))
144
               (= unitdelay_test.UnitDelay7_1_1 false))
145
            (or (not (= unitdelay_test.__unitdelay_test_1 false))
146
               (= unitdelay_test.UnitDelay7_1_1 unitdelay_test.__unitdelay_test_3_c))
147
       )
148
       (= unitdelay_test.__unitdelay_test_3_x unitdelay_test.In8_1_1)
149
       (and (or (not (= unitdelay_test.__unitdelay_test_1 true))
150
               (= unitdelay_test.UnitDelay8_1_1 true))
151
            (or (not (= unitdelay_test.__unitdelay_test_1 false))
152
               (= unitdelay_test.UnitDelay8_1_1 unitdelay_test.__unitdelay_test_2_c))
153
       )
154
       (= unitdelay_test.__unitdelay_test_2_x unitdelay_test.In9_1_1)
155
       (and (or (not (= unitdelay_test.__unitdelay_test_1 true))
156
               (= unitdelay_test.UnitDelay_1_1 0.00000000))
157
            (or (not (= unitdelay_test.__unitdelay_test_1 false))
158
               (= unitdelay_test.UnitDelay_1_1 unitdelay_test.__unitdelay_test_10_c))
159
       )
160
       (= unitdelay_test.__unitdelay_test_10_x unitdelay_test.In1_1_1)
161
       (= unitdelay_test.Out9_9_1 unitdelay_test.UnitDelay8_1_1)
162
       (= unitdelay_test.Out8_8_1 unitdelay_test.UnitDelay7_1_1)
163
       (= unitdelay_test.Out7_7_1 unitdelay_test.UnitDelay6_1_1)
164
       (= unitdelay_test.Out6_6_1 unitdelay_test.UnitDelay5_1_1)
165
       (= unitdelay_test.Out5_5_1 unitdelay_test.UnitDelay4_1_1)
166
       (= unitdelay_test.Out4_4_1 unitdelay_test.UnitDelay3_1_1)
167
       (= unitdelay_test.Out3_3_1 unitdelay_test.UnitDelay2_1_1)
168
       (= unitdelay_test.Out2_2_1 unitdelay_test.UnitDelay1_1_1)
169
       (= unitdelay_test.Out1_1_1 unitdelay_test.UnitDelay_1_1)
170
       )
171
  (unitdelay_test_step unitdelay_test.In1_1_1
172
                       unitdelay_test.In2_1_1
173
                       unitdelay_test.In3_1_1
174
                       unitdelay_test.In4_1_1
175
                       unitdelay_test.In5_1_1
176
                       unitdelay_test.In6_1_1
177
                       unitdelay_test.In7_1_1
178
                       unitdelay_test.In8_1_1
179
                       unitdelay_test.In9_1_1
180
                       unitdelay_test.Out1_1_1
181
                       unitdelay_test.Out2_2_1
182
                       unitdelay_test.Out3_3_1
183
                       unitdelay_test.Out4_4_1
184
                       unitdelay_test.Out5_5_1
185
                       unitdelay_test.Out6_6_1
186
                       unitdelay_test.Out7_7_1
187
                       unitdelay_test.Out8_8_1
188
                       unitdelay_test.Out9_9_1
189
                       unitdelay_test.__unitdelay_test_10_c
190
                       unitdelay_test.__unitdelay_test_2_c
191
                       unitdelay_test.__unitdelay_test_3_c
192
                       unitdelay_test.__unitdelay_test_4_c
193
                       unitdelay_test.__unitdelay_test_5_c
194
                       unitdelay_test.__unitdelay_test_6_c
195
                       unitdelay_test.__unitdelay_test_7_c
196
                       unitdelay_test.__unitdelay_test_8_c
197
                       unitdelay_test.__unitdelay_test_9_c
198
                       unitdelay_test.ni_0._arrow._first_c
199
                       unitdelay_test.__unitdelay_test_10_x
200
                       unitdelay_test.__unitdelay_test_2_x
201
                       unitdelay_test.__unitdelay_test_3_x
202
                       unitdelay_test.__unitdelay_test_4_x
203
                       unitdelay_test.__unitdelay_test_5_x
204
                       unitdelay_test.__unitdelay_test_6_x
205
                       unitdelay_test.__unitdelay_test_7_x
206
                       unitdelay_test.__unitdelay_test_8_x
207
                       unitdelay_test.__unitdelay_test_9_x
208
                       unitdelay_test.ni_0._arrow._first_x)
209
))
210