Project

General

Profile

Statistics
| Branch: | Tag: | Revision:

lustrec-tests / regression_tests / lustre_files / success / Simulink / src_muxdemux_test / muxdemux_test.smt2 @ 6c3ea955

History | View | Annotate | Download (8.05 KB)

1
; muxdemux_test
2
(declare-var muxdemux_test.In2_1_1 Real)
3
(declare-var muxdemux_test.In2_1_2 Real)
4
(declare-var muxdemux_test.In2_1_3 Real)
5
(declare-var muxdemux_test.Out2_1_1 Real)
6
(declare-var muxdemux_test.Out2_1_2 Real)
7
(declare-var muxdemux_test.Out2_1_3 Real)
8
(declare-var muxdemux_test.Out1_2_1 Real)
9
(declare-var muxdemux_test.Out1_2_2 Real)
10
(declare-var muxdemux_test.Out1_2_3 Real)
11
(declare-var muxdemux_test.Out1_2_4 Real)
12
(declare-var muxdemux_test.Out1_2_5 Real)
13
(declare-var muxdemux_test.Out1_2_6 Real)
14
(declare-var muxdemux_test.Out3_3_1 Real)
15
(declare-var muxdemux_test.Out3_3_2 Real)
16
(declare-var muxdemux_test.Out3_3_3 Real)
17
(declare-var muxdemux_test.ni_0._arrow._first_c Bool)
18
(declare-var muxdemux_test.ni_0._arrow._first_m Bool)
19
(declare-var muxdemux_test.ni_0._arrow._first_x Bool)
20
(declare-var muxdemux_test.Constant1_1_1 Real)
21
(declare-var muxdemux_test.Constant1_1_2 Real)
22
(declare-var muxdemux_test.Constant1_1_3 Real)
23
(declare-var muxdemux_test.Constant_1_1 Real)
24
(declare-var muxdemux_test.Constant_1_2 Real)
25
(declare-var muxdemux_test.Constant_1_3 Real)
26
(declare-var muxdemux_test.Constant_1_4 Real)
27
(declare-var muxdemux_test.Constant_1_5 Real)
28
(declare-var muxdemux_test.Constant_1_6 Real)
29
(declare-var muxdemux_test.Demux1_1_1 Real)
30
(declare-var muxdemux_test.Demux1_2_1 Real)
31
(declare-var muxdemux_test.Demux2_1_1 Real)
32
(declare-var muxdemux_test.Demux2_2_1 Real)
33
(declare-var muxdemux_test.Demux3_1_1 Real)
34
(declare-var muxdemux_test.Demux3_2_1 Real)
35
(declare-var muxdemux_test.Demux_1_1 Real)
36
(declare-var muxdemux_test.Demux_2_1 Real)
37
(declare-var muxdemux_test.Demux_3_1 Real)
38
(declare-var muxdemux_test.Mux1_1_1 Real)
39
(declare-var muxdemux_test.Mux1_1_2 Real)
40
(declare-var muxdemux_test.Mux2_1_1 Real)
41
(declare-var muxdemux_test.Mux2_1_2 Real)
42
(declare-var muxdemux_test.Mux3_1_1 Real)
43
(declare-var muxdemux_test.Mux3_1_2 Real)
44
(declare-var muxdemux_test.Mux_1_1 Real)
45
(declare-var muxdemux_test.Mux_1_2 Real)
46
(declare-var muxdemux_test.Mux_1_3 Real)
47
(declare-var muxdemux_test.Selector1_1_1 Real)
48
(declare-var muxdemux_test.Selector1_1_2 Real)
49
(declare-var muxdemux_test.Selector2_1_1 Real)
50
(declare-var muxdemux_test.Selector2_1_2 Real)
51
(declare-var muxdemux_test.Selector4_1_1 Real)
52
(declare-var muxdemux_test.Selector5_1_1 Real)
53
(declare-var muxdemux_test.Selector6_1_1 Real)
54
(declare-var muxdemux_test.Selector_1_1 Real)
55
(declare-var muxdemux_test.Selector_1_2 Real)
56
(declare-var muxdemux_test.VectorConcatenate2_1_1 Real)
57
(declare-var muxdemux_test.VectorConcatenate2_1_2 Real)
58
(declare-var muxdemux_test.VectorConcatenate2_1_3 Real)
59
(declare-var muxdemux_test.VectorConcatenate_1_1 Real)
60
(declare-var muxdemux_test.VectorConcatenate_1_2 Real)
61
(declare-var muxdemux_test.VectorConcatenate_1_3 Real)
62
(declare-var muxdemux_test.VectorConcatenate_1_4 Real)
63
(declare-var muxdemux_test.VectorConcatenate_1_5 Real)
64
(declare-var muxdemux_test.VectorConcatenate_1_6 Real)
65
(declare-var muxdemux_test.__muxdemux_test_1 Bool)
66
(declare-var muxdemux_test.i_virtual_local Real)
67
(declare-rel muxdemux_test_reset (Bool Bool))
68
(declare-rel muxdemux_test_step (Real Real Real Real Real Real Real Real Real Real Real Real Real Real Real Bool Bool))
69

    
70
(rule (=> 
71
  (and 
72
       
73
       (= muxdemux_test.ni_0._arrow._first_m true)
74
  )
75
  (muxdemux_test_reset muxdemux_test.ni_0._arrow._first_c
76
                       muxdemux_test.ni_0._arrow._first_m)
77
))
78

    
79
(rule (=> 
80
  (and (= muxdemux_test.ni_0._arrow._first_m muxdemux_test.ni_0._arrow._first_c)
81
       (and (= muxdemux_test.__muxdemux_test_1 (ite muxdemux_test.ni_0._arrow._first_m true false))
82
            (= muxdemux_test.ni_0._arrow._first_x false))
83
       (and (or (not (= muxdemux_test.__muxdemux_test_1 true))
84
               (= muxdemux_test.i_virtual_local 0.0))
85
            (or (not (= muxdemux_test.__muxdemux_test_1 false))
86
               (= muxdemux_test.i_virtual_local 1.0))
87
       )
88
       (= muxdemux_test.Constant_1_6 9.00000000)
89
       (= muxdemux_test.Selector2_1_2 muxdemux_test.Constant_1_6)
90
       (= muxdemux_test.Demux3_2_1 muxdemux_test.Selector2_1_2)
91
       (= muxdemux_test.Mux3_1_2 muxdemux_test.Demux3_2_1)
92
       (= muxdemux_test.VectorConcatenate_1_6 muxdemux_test.Mux3_1_2)
93
       (= muxdemux_test.Constant_1_5 6.00000000)
94
       (= muxdemux_test.Selector1_1_2 muxdemux_test.Constant_1_5)
95
       (= muxdemux_test.Demux2_2_1 muxdemux_test.Selector1_1_2)
96
       (= muxdemux_test.Mux2_1_2 muxdemux_test.Demux2_2_1)
97
       (= muxdemux_test.VectorConcatenate_1_5 muxdemux_test.Mux2_1_2)
98
       (= muxdemux_test.Constant_1_4 8.00000000)
99
       (= muxdemux_test.Selector_1_2 muxdemux_test.Constant_1_4)
100
       (= muxdemux_test.Demux1_2_1 muxdemux_test.Selector_1_2)
101
       (= muxdemux_test.Mux1_1_2 muxdemux_test.Demux1_2_1)
102
       (= muxdemux_test.VectorConcatenate_1_4 muxdemux_test.Mux1_1_2)
103
       (= muxdemux_test.Constant_1_3 5.00000000)
104
       (= muxdemux_test.Selector2_1_1 muxdemux_test.Constant_1_3)
105
       (= muxdemux_test.Demux3_1_1 muxdemux_test.Selector2_1_1)
106
       (= muxdemux_test.Mux3_1_1 muxdemux_test.Demux3_1_1)
107
       (= muxdemux_test.VectorConcatenate_1_3 muxdemux_test.Mux3_1_1)
108
       (= muxdemux_test.Constant_1_2 3.00000000)
109
       (= muxdemux_test.Selector1_1_1 muxdemux_test.Constant_1_2)
110
       (= muxdemux_test.Demux2_1_1 muxdemux_test.Selector1_1_1)
111
       (= muxdemux_test.Mux2_1_1 muxdemux_test.Demux2_1_1)
112
       (= muxdemux_test.VectorConcatenate_1_2 muxdemux_test.Mux2_1_1)
113
       (= muxdemux_test.Constant_1_1 2.00000000)
114
       (= muxdemux_test.Selector_1_1 muxdemux_test.Constant_1_1)
115
       (= muxdemux_test.Demux1_1_1 muxdemux_test.Selector_1_1)
116
       (= muxdemux_test.Mux1_1_1 muxdemux_test.Demux1_1_1)
117
       (= muxdemux_test.VectorConcatenate_1_1 muxdemux_test.Mux1_1_1)
118
       (= muxdemux_test.Constant1_1_3 5.00000000)
119
       (= muxdemux_test.Selector6_1_1 muxdemux_test.Constant1_1_3)
120
       (= muxdemux_test.VectorConcatenate2_1_3 muxdemux_test.Selector6_1_1)
121
       (= muxdemux_test.Constant1_1_2 3.00000000)
122
       (= muxdemux_test.Selector5_1_1 muxdemux_test.Constant1_1_2)
123
       (= muxdemux_test.VectorConcatenate2_1_2 muxdemux_test.Selector5_1_1)
124
       (= muxdemux_test.Constant1_1_1 2.00000000)
125
       (= muxdemux_test.Selector4_1_1 muxdemux_test.Constant1_1_1)
126
       (= muxdemux_test.VectorConcatenate2_1_1 muxdemux_test.Selector4_1_1)
127
       (= muxdemux_test.Out3_3_3 muxdemux_test.VectorConcatenate2_1_3)
128
       (= muxdemux_test.Out3_3_2 muxdemux_test.VectorConcatenate2_1_2)
129
       (= muxdemux_test.Out3_3_1 muxdemux_test.VectorConcatenate2_1_1)
130
       (= muxdemux_test.Demux_3_1 muxdemux_test.In2_1_3)
131
       (= muxdemux_test.Mux_1_3 muxdemux_test.Demux_3_1)
132
       (= muxdemux_test.Out2_1_3 muxdemux_test.Mux_1_3)
133
       (= muxdemux_test.Demux_2_1 muxdemux_test.In2_1_2)
134
       (= muxdemux_test.Mux_1_2 muxdemux_test.Demux_2_1)
135
       (= muxdemux_test.Out2_1_2 muxdemux_test.Mux_1_2)
136
       (= muxdemux_test.Demux_1_1 muxdemux_test.In2_1_1)
137
       (= muxdemux_test.Mux_1_1 muxdemux_test.Demux_1_1)
138
       (= muxdemux_test.Out2_1_1 muxdemux_test.Mux_1_1)
139
       (= muxdemux_test.Out1_2_6 muxdemux_test.VectorConcatenate_1_6)
140
       (= muxdemux_test.Out1_2_5 muxdemux_test.VectorConcatenate_1_5)
141
       (= muxdemux_test.Out1_2_4 muxdemux_test.VectorConcatenate_1_4)
142
       (= muxdemux_test.Out1_2_3 muxdemux_test.VectorConcatenate_1_3)
143
       (= muxdemux_test.Out1_2_2 muxdemux_test.VectorConcatenate_1_2)
144
       (= muxdemux_test.Out1_2_1 muxdemux_test.VectorConcatenate_1_1)
145
       )
146
  (muxdemux_test_step muxdemux_test.In2_1_1
147
                      muxdemux_test.In2_1_2
148
                      muxdemux_test.In2_1_3
149
                      muxdemux_test.Out2_1_1
150
                      muxdemux_test.Out2_1_2
151
                      muxdemux_test.Out2_1_3
152
                      muxdemux_test.Out1_2_1
153
                      muxdemux_test.Out1_2_2
154
                      muxdemux_test.Out1_2_3
155
                      muxdemux_test.Out1_2_4
156
                      muxdemux_test.Out1_2_5
157
                      muxdemux_test.Out1_2_6
158
                      muxdemux_test.Out3_3_1
159
                      muxdemux_test.Out3_3_2
160
                      muxdemux_test.Out3_3_3
161
                      muxdemux_test.ni_0._arrow._first_c
162
                      muxdemux_test.ni_0._arrow._first_x)
163
))
164