Problem1-Full.smv 19.8 KB
Newer Older
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
MODULE main
VAR
    state  : {s0, s1, s10, s11, s12, s2, s3, s4, s5, s6, s7, s8, s9};
    input  : {iA, iB, iC, iD, iE, null};
    output : {oInv, oS, oT, oU, oV, oW, oX, oY, oZ, null};
ASSIGN
    init(state)  := s0;
    init(output) := null;
    next(state)  := case
        state = s0 & input = iA : s0;
        state = s0 & input = iB : s3;
        state = s0 & input = iC : s0;
        state = s0 & input = iD : s1;
        state = s0 & input = iE : s0;
        state = s1 & input = iA : s2;
        state = s1 & input = iB : s1;
        state = s1 & input = iC : s1;
        state = s1 & input = iD : s1;
        state = s1 & input = iE : s1;
        state = s10 & input = iA : s10;
        state = s10 & input = iB : s10;
        state = s10 & input = iC : s10;
        state = s10 & input = iD : s11;
        state = s10 & input = iE : s10;
        state = s11 & input = iA : s11;
        state = s11 & input = iB : s11;
        state = s11 & input = iC : s12;
        state = s11 & input = iD : s12;
        state = s11 & input = iE : s11;
        state = s12 & input = iA : s12;
        state = s12 & input = iB : s12;
        state = s12 & input = iC : s12;
        state = s12 & input = iD : s12;
        state = s12 & input = iE : s3;
        state = s2 & input = iA : s2;
        state = s2 & input = iB : s2;
        state = s2 & input = iC : s5;
        state = s2 & input = iD : s2;
        state = s2 & input = iE : s2;
        state = s3 & input = iA : s3;
        state = s3 & input = iB : s3;
        state = s3 & input = iC : s4;
        state = s3 & input = iD : s3;
        state = s3 & input = iE : s3;
        state = s4 & input = iA : s4;
        state = s4 & input = iB : s4;
        state = s4 & input = iC : s9;
        state = s4 & input = iD : s4;
        state = s4 & input = iE : s4;
        state = s5 & input = iA : s5;
        state = s5 & input = iB : s5;
        state = s5 & input = iC : s7;
        state = s5 & input = iD : s6;
        state = s5 & input = iE : s5;
        state = s6 & input = iA : s6;
        state = s6 & input = iB : s6;
        state = s6 & input = iC : s2;
        state = s6 & input = iD : s2;
        state = s6 & input = iE : s2;
        state = s7 & input = iA : s7;
        state = s7 & input = iB : s7;
        state = s7 & input = iC : s7;
        state = s7 & input = iD : s8;
        state = s7 & input = iE : s7;
        state = s8 & input = iA : s6;
        state = s8 & input = iB : s8;
        state = s8 & input = iC : s8;
        state = s8 & input = iD : s6;
        state = s8 & input = iE : s8;
        state = s9 & input = iA : s10;
        state = s9 & input = iB : s9;
        state = s9 & input = iC : s9;
        state = s9 & input = iD : s9;
        state = s9 & input = iE : s9;
        input = null : state;
    esac;
    next(output) := case
        state = s0 & input = iA : oInv;
        state = s0 & input = iB : oY;
        state = s0 & input = iC : oInv;
        state = s0 & input = iD : oS;
        state = s0 & input = iE : oInv;
        state = s1 & input = iA : oY;
        state = s1 & input = iB : oInv;
        state = s1 & input = iC : oInv;
        state = s1 & input = iD : oInv;
        state = s1 & input = iE : oInv;
        state = s10 & input = iA : oInv;
        state = s10 & input = iB : oInv;
        state = s10 & input = iC : oInv;
        state = s10 & input = iD : oY;
        state = s10 & input = iE : oInv;
        state = s11 & input = iA : oInv;
        state = s11 & input = iB : oInv;
        state = s11 & input = iC : oW;
        state = s11 & input = iD : oW;
        state = s11 & input = iE : oInv;
        state = s12 & input = iA : oInv;
        state = s12 & input = iB : oInv;
        state = s12 & input = iC : oInv;
        state = s12 & input = iD : oInv;
        state = s12 & input = iE : oY;
        state = s2 & input = iA : oInv;
        state = s2 & input = iB : oInv;
        state = s2 & input = iC : oZ;
        state = s2 & input = iD : oInv;
        state = s2 & input = iE : oInv;
        state = s3 & input = iA : oInv;
        state = s3 & input = iB : oInv;
        state = s3 & input = iC : oZ;
        state = s3 & input = iD : oInv;
        state = s3 & input = iE : oInv;
        state = s4 & input = iA : oInv;
        state = s4 & input = iB : oInv;
        state = s4 & input = iC : oW;
        state = s4 & input = iD : oInv;
        state = s4 & input = iE : oInv;
        state = s5 & input = iA : oInv;
        state = s5 & input = iB : oInv;
        state = s5 & input = iC : oX;
        state = s5 & input = iD : oW;
        state = s5 & input = iE : oInv;
        state = s6 & input = iA : oInv;
        state = s6 & input = iB : oInv;
        state = s6 & input = iC : oY;
        state = s6 & input = iD : oY;
        state = s6 & input = iE : oY;
        state = s7 & input = iA : oInv;
        state = s7 & input = iB : oInv;
        state = s7 & input = iC : oInv;
        state = s7 & input = iD : oU;
        state = s7 & input = iE : oInv;
        state = s8 & input = iA : oW;
        state = s8 & input = iB : oInv;
        state = s8 & input = iC : oInv;
        state = s8 & input = iD : oW;
        state = s8 & input = iE : oInv;
        state = s9 & input = iA : oY;
        state = s9 & input = iB : oInv;
        state = s9 & input = iC : oInv;
        state = s9 & input = iD : oInv;
        state = s9 & input = iE : oInv;
        input = null : null;
    esac;
INVAR !(input = null & output = null)
    & !(input != null & output != null)
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
LTLSPEC (FALSE V (! input = iC | (TRUE U ((output = oU & ! output = oW) & X (! output = oW U output = oV)))))
LTLSPEC (FALSE V (! input = iD | ((! ((output = oS & ! input = iC) & X (! input = iC U (output = oY & ! input = iC))) U (input = iC | output = oU)) | (FALSE V ! (output = oS & X (TRUE U output = oY))))))
LTLSPEC (FALSE V (! (output = oS & (TRUE U input = iB)) | (! output = oV U (input = iB | ((output = oW & ! output = oV) & X (! output = oV U output = oX))))))
LTLSPEC (! (TRUE U output = oT) | ((input = iB & (! X (! output = oT U input = iD) | X (! output = oT U (input = iD & (TRUE U output = oZ))))) U output = oT))
LTLSPEC (FALSE V (! output = oU | (FALSE V (! input = iC | (output = oW & X (TRUE U output = oV))))))
LTLSPEC (FALSE V (! (output = oW & (TRUE U output = oU)) | ((input = iA & (! X (! output = oU U input = iC) | X (! output = oU U (input = iC & (TRUE U output = oY))))) U output = oU)))
LTLSPEC (! (TRUE U output = oX) | (! output = oY U (input = iB | output = oX)))
LTLSPEC (FALSE V (! (output = oW & (TRUE U output = oU)) | (! ((output = oY & ! output = oU) & X (! output = oU U (output = oZ & ! output = oU))) U (output = oU | output = oX))))
LTLSPEC (FALSE V (! (output = oS & (TRUE U output = oX)) | ((! input = iD | (! output = oX U ((output = oT & ! output = oX) & X (! output = oX U output = oW)))) U output = oX)))
LTLSPEC (FALSE V (! input = iC | ((! input = iA | (! output = oY U (((output = oS & ! output = oY) & ! output = oX) & X ((! output = oY & ! output = oX) U output = oT)))) U (output = oY | (FALSE V (! input = iA | ((output = oS & ! output = oX) & X (! output = oX U output = oT))))))))
LTLSPEC (FALSE V (! ((input = iD & ! output = oZ) & (TRUE U output = oZ)) | (! output = oW U (output = oU | output = oZ))))
LTLSPEC (FALSE V (output = oT & (! ! input = iA | ((output = oV | input = iA) V (! output = oW | (output = oV | input = iA))))))
LTLSPEC (FALSE V (! (output = oV & (TRUE U input = iA)) | ((! input = iD | (! input = iA U (((output = oZ & ! input = iA) & ! output = oW) & X ((! input = iA & ! output = oW) U output = oT)))) U input = iA)))
LTLSPEC (FALSE V (! input = iB | (FALSE V (! input = iE | (output = oT & X (TRUE U output = oX))))))
LTLSPEC (! (TRUE U output = oS) | ((! input = iE | (! output = oS U (output = oU & ! output = oS))) U output = oS))
LTLSPEC (FALSE V (! output = oX | ((! input = iE | (! input = iB U ((output = oZ & ! input = iB) & X (! input = iB U output = oS)))) U (input = iB | (FALSE V (! input = iE | (output = oZ & X (TRUE U output = oS))))))))
LTLSPEC (FALSE V (! output = oW | ((! input = iC | (! input = iA U ((output = oU & ! input = iA) & X (! input = iA U output = oY)))) U (input = iA | (FALSE V (! input = iC | (output = oU & X (TRUE U output = oY))))))))
LTLSPEC (FALSE V (! input = iE | ((! input = iC | (! output = oX U ((output = oS & ! output = oX) & X (! output = oX U output = oT)))) U (output = oX | (FALSE V (! input = iC | (output = oS & X (TRUE U output = oT))))))))
LTLSPEC (! (TRUE U output = oY) | ((! input = iC | (! output = oY U (output = oT & ! output = oY))) U output = oY))
LTLSPEC ((FALSE V ! output = oS) | (TRUE U (output = oS & (input = iC V (! output = oV | input = iC)))))
LTLSPEC (! (TRUE U output = oV) | (! output = oZ U (output = oX | output = oV)))
LTLSPEC (! (TRUE U input = iE) | ((input = iB & (! X (! input = iE U input = iD) | X (! input = iE U (input = iD & (TRUE U output = oZ))))) U input = iE))
LTLSPEC (! (TRUE U output = oZ) | ((input = iD & (! X (! output = oZ U input = iC) | X (! output = oZ U (input = iC & (TRUE U output = oW))))) U output = oZ))
LTLSPEC (FALSE V (! input = iD | (TRUE U (output = oZ & X (TRUE U output = oV)))))
LTLSPEC (FALSE V (! input = iB | (TRUE U (output = oU & X (TRUE U output = oX)))))
LTLSPEC (FALSE V (! input = iE | (FALSE V (! input = iB | (TRUE U output = oX)))))
LTLSPEC (FALSE V (! ((input = iA & ! output = oY) & (TRUE U output = oY)) | (! output = oZ U (output = oW | output = oY))))
LTLSPEC (FALSE V (! output = oT | (FALSE V (! input = iD | ((output = oV & ! output = oX) & X (! output = oX U output = oZ))))))
LTLSPEC (FALSE V (! input = iA | (TRUE U ((output = oY & ! output = oS) & X (! output = oS U output = oW)))))
LTLSPEC (input = iB V (! output = oV | input = iB))
LTLSPEC (! (TRUE U output = oW) | (! output = oS U (input = iE | output = oW)))
LTLSPEC ((FALSE V ! output = oS) | (! output = oS U (output = oS & (! (TRUE U output = oX) | (! output = oX U ((input = iC & ! output = oX) & X (! output = oX U output = oV)))))))
LTLSPEC (FALSE V (! input = iB | (TRUE U output = oW)))
LTLSPEC (FALSE V (! input = iA | (TRUE U output = oS)))
LTLSPEC (FALSE V (! input = iB | ((! input = iE | (! output = oS U (((output = oV & ! output = oS) & ! output = oZ) & X ((! output = oS & ! output = oZ) U output = oY)))) U (output = oS | (FALSE V (! input = iE | ((output = oV & ! output = oZ) & X (! output = oZ U output = oY))))))))
LTLSPEC (FALSE V (! output = oZ | ((! input = iD | (! output = oW U (((output = oY & ! output = oW) & ! output = oS) & X ((! output = oW & ! output = oS) U output = oT)))) U (output = oW | (FALSE V (! input = iD | ((output = oY & ! output = oS) & X (! output = oS U output = oT))))))))
LTLSPEC (FALSE V (! input = iE | ((! ((output = oT & ! output = oV) & X (! output = oV U (output = oW & ! output = oV))) U (output = oV | input = iA)) | (FALSE V ! (output = oT & X (TRUE U output = oW))))))
LTLSPEC (FALSE V (! input = iC | (TRUE U (output = oV & X (TRUE U output = oU)))))
LTLSPEC (! (TRUE U output = oX) | ((input = iA & (! X (! output = oX U input = iB) | X (! output = oX U (input = iB & (TRUE U output = oV))))) U output = oX))
LTLSPEC (FALSE V (input = iB & (! ! input = iA | ((output = oZ | input = iA) V (! output = oU | (output = oZ | input = iA))))))
LTLSPEC (FALSE V (! ((input = iB & ! output = oZ) & (TRUE U output = oZ)) | ((! input = iA | (! output = oZ U (output = oY & ! output = oZ))) U output = oZ)))
LTLSPEC (FALSE V (! input = iE | (FALSE V (input = iD & (! X (TRUE U input = iB) | X (! input = iB U (input = iB & (TRUE U output = oY))))))))
LTLSPEC (! (TRUE U output = oZ) | ((! input = iD | (! output = oZ U (output = oS & ! output = oZ))) U output = oZ))
LTLSPEC (FALSE V (! output = oX | (FALSE V (! input = iA | (output = oW & X (TRUE U output = oZ))))))
LTLSPEC (FALSE V (! ((output = oV & ! input = iA) & (TRUE U input = iA)) | ((! input = iB | (! input = iA U (output = oX & ! input = iA))) U input = iA)))
LTLSPEC (FALSE V (! output = oU | ((! ((output = oY & ! input = iC) & X (! input = iC U (output = oS & ! input = iC))) U (input = iC | output = oZ)) | (FALSE V ! (output = oY & X (TRUE U output = oS))))))
LTLSPEC (FALSE V (! input = iD | ((input = iC & (! X (! output = oY U input = iB) | X (! output = oY U (input = iB & (TRUE U output = oT))))) U (output = oY | (FALSE V (input = iC & (! X (! output = oY U input = iB) | X (! output = oY U (input = iB & (TRUE U output = oT))))))))))
LTLSPEC (! (TRUE U input = iC) | (! output = oX U (output = oW | input = iC)))
LTLSPEC (FALSE V (! input = iE | ((input = iC & (! X (! input = iA U input = iD) | X (! input = iA U (input = iD & (TRUE U output = oW))))) U (input = iA | (FALSE V (input = iC & (! X (! input = iA U input = iD) | X (! input = iA U (input = iD & (TRUE U output = oW))))))))))
LTLSPEC (FALSE V (! input = iE | (TRUE U (output = oX & X (TRUE U output = oV)))))
LTLSPEC ((FALSE V ! output = oS) | (! output = oS U (output = oS & (! (TRUE U (output = oW & X (TRUE U output = oY))) | (! output = oW U input = iE)))))
LTLSPEC ((FALSE V ! input = iA) | (! input = iA U (input = iA & (! (TRUE U (output = oX & X (TRUE U output = oY))) | (! output = oX U output = oS)))))
LTLSPEC (! (TRUE U (output = oV & X (TRUE U output = oU))) | (! output = oV U output = oY))
LTLSPEC (! (TRUE U input = iC) | ((input = iD & (! X (! input = iC U input = iA) | X (! input = iC U (input = iA & (TRUE U output = oT))))) U input = iC))
LTLSPEC (FALSE V (! output = oV | ((! ((output = oY & ! output = oU) & X (! output = oU U (output = oZ & ! output = oU))) U (output = oU | input = iB)) | (FALSE V ! (output = oY & X (TRUE U output = oZ))))))
LTLSPEC (FALSE V (input = iD & (! ! output = oY | ((input = iE | output = oY) V (! output = oX | (input = iE | output = oY))))))
LTLSPEC (! (TRUE U output = oS) | (! ((output = oT & ! output = oS) & X (! output = oS U (output = oV & ! output = oS))) U (output = oS | output = oZ)))
LTLSPEC (! (TRUE U input = iD) | (! output = oY U (input = iD | ((output = oT & ! output = oY) & X (! output = oY U output = oW)))))
LTLSPEC (FALSE V (! output = oY | (FALSE V (! input = iD | (output = oV & X (TRUE U output = oZ))))))
LTLSPEC (! (TRUE U output = oV) | (! ((output = oX & ! output = oV) & X (! output = oV U (output = oS & ! output = oV))) U (output = oV | input = iB)))
LTLSPEC (FALSE V (! (output = oV & (TRUE U output = oT)) | (! ((output = oX & ! output = oT) & X (! output = oT U (output = oW & ! output = oT))) U (output = oT | input = iE))))
LTLSPEC (! (TRUE U input = iD) | (! output = oU U (input = iD | ((output = oZ & ! output = oU) & X (! output = oU U input = iC)))))
LTLSPEC (FALSE V (! ((input = iB & ! output = oT) & (TRUE U output = oT)) | ((! input = iA | (! output = oT U (output = oX & ! output = oT))) U output = oT)))
LTLSPEC (FALSE V (! (output = oZ & (TRUE U output = oX)) | ((input = iA & (! X (! output = oX U input = iC) | X (! output = oX U (input = iC & (TRUE U output = oY))))) U output = oX)))
LTLSPEC (! (TRUE U input = iE) | ((! input = iD | (! input = iE U ((output = oX & ! input = iE) & X (! input = iE U output = oZ)))) U input = iE))
LTLSPEC (FALSE V (! ((input = iC & ! output = oV) & (TRUE U output = oV)) | (! output = oT U (input = iD | output = oV))))
LTLSPEC (! (TRUE U output = oV) | ((! input = iD | (! output = oV U (((output = oX & ! output = oV) & ! output = oW) & X ((! output = oV & ! output = oW) U output = oS)))) U output = oV))
LTLSPEC (FALSE V (! output = oV | ((input = iD & (! X (! output = oX U input = iA) | X (! output = oX U (input = iA & (TRUE U output = oU))))) U (output = oX | (FALSE V (input = iD & (! X (! output = oX U input = iA) | X (! output = oX U (input = iA & (TRUE U output = oU))))))))))
LTLSPEC (FALSE V (! (output = oW & (TRUE U output = oV)) | ((! input = iC | (! output = oV U ((output = oX & ! output = oV) & X (! output = oV U output = oZ)))) U output = oV)))
LTLSPEC (! (TRUE U output = oT) | ((input = iD & (! X (! output = oT U input = iC) | X (! output = oT U (input = iC & (TRUE U output = oV))))) U output = oT))
LTLSPEC (FALSE V (output = oT & (! ! output = oY | (output = oY V ((! input = iA | (! output = oY U (output = oX & ! output = oY))) | output = oY)))))
LTLSPEC (FALSE V (! input = iC | (FALSE V (! input = iD | (output = oX & X (TRUE U output = oZ))))))
LTLSPEC (FALSE V (! (output = oY & (TRUE U output = oT)) | ((! input = iB | (! output = oT U ((output = oX & ! output = oT) & X (! output = oT U output = oV)))) U output = oT)))
LTLSPEC (FALSE V (! ((input = iB & ! input = iD) & (TRUE U input = iD)) | ((! input = iA | (! input = iD U (output = oX & ! input = iD))) U input = iD)))
LTLSPEC (! (TRUE U input = iB) | ((input = iA & (! X (! input = iB U input = iD) | X (! input = iB U (input = iD & (TRUE U output = oX))))) U input = iB))
LTLSPEC (! (TRUE U output = oT) | ((input = iB & (! X (! output = oT U input = iA) | X (! output = oT U (input = iA & (TRUE U output = oY))))) U output = oT))
LTLSPEC (FALSE V (! input = iE | (TRUE U ((output = oZ & ! output = oU) & X (! output = oU U output = oS)))))
LTLSPEC (FALSE V (! output = oV | ((! input = iB | (! input = iE U (((output = oY & ! input = iE) & ! output = oX) & X ((! input = iE & ! output = oX) U output = oU)))) U (input = iE | (FALSE V (! input = iB | ((output = oY & ! output = oX) & X (! output = oX U output = oU))))))))
LTLSPEC (! (TRUE U input = iC) | (! output = oU U (output = oX | input = iC)))
LTLSPEC (FALSE V (! input = iB | (FALSE V (! input = iA | (TRUE U output = oY)))))
LTLSPEC (FALSE V (! ((input = iD & ! input = iC) & (TRUE U input = iC)) | ((! input = iB | (! input = iC U (output = oW & ! input = iC))) U input = iC)))
LTLSPEC (FALSE V (! ((output = oW & ! output = oV) & (TRUE U output = oV)) | (! output = oY U (input = iB | output = oV))))
LTLSPEC (FALSE V (! (input = iB & (TRUE U output = oV)) | ((input = iE & (! X (! output = oV U input = iA) | X (! output = oV U (input = iA & (TRUE U output = oT))))) U output = oV)))
LTLSPEC (! (TRUE U output = oX) | ((! input = iE | (! output = oX U ((output = oS & ! output = oX) & X (! output = oX U output = oV)))) U output = oX))
LTLSPEC (! (TRUE U input = iB) | (! ((output = oW & ! input = iB) & X (! input = iB U (output = oZ & ! input = iB))) U (input = iB | input = iD)))
LTLSPEC (FALSE V (! input = iC | (TRUE U output = oV)))
LTLSPEC (FALSE V (input = iA & (! ! output = oW | (output = oW V ((! input = iD | (! output = oW U (output = oT & ! output = oW))) | output = oW)))))
LTLSPEC (! (TRUE U output = oS) | ((! input = iA | (! output = oS U ((output = oT & ! output = oS) & X (! output = oS U output = oX)))) U output = oS))
LTLSPEC (FALSE V (! ((output = oW & ! input = iB) & (TRUE U input = iB)) | ((! input = iC | (! input = iB U (output = oY & ! input = iB))) U input = iB)))
LTLSPEC (FALSE V (input = iE & (! ! output = oY | (output = oY V ((! input = iA | (! output = oY U (output = oV & ! output = oY))) | output = oY)))))
LTLSPEC (FALSE V (! input = iC | (TRUE U output = oS)))
LTLSPEC (! (TRUE U output = oX) | (! output = oX U ((output = oV & ! output = oX) & X (! output = oX U input = iC))))
LTLSPEC (FALSE V (! output = oU | (FALSE V (! input = iB | (TRUE U output = oY)))))
LTLSPEC (! (TRUE U output = oX) | ((! input = iD | (! output = oX U ((output = oU & ! output = oX) & X (! output = oX U output = oY)))) U output = oX))
LTLSPEC (FALSE V (! input = iE | ((input = iD & (! X (! output = oS U input = iB) | X (! output = oS U (input = iB & (TRUE U output = oY))))) U (output = oS | (FALSE V (input = iD & (! X (! output = oS U input = iB) | X (! output = oS U (input = iB & (TRUE U output = oY))))))))))
LTLSPEC (FALSE V (! input = iE | (TRUE U (output = oV & X (TRUE U output = oU)))))
LTLSPEC (FALSE V (! input = iE | (TRUE U ((output = oX & ! output = oU) & X (! output = oU U output = oV)))))
LTLSPEC ((FALSE V ! output = oW) | (TRUE U (output = oW & (output = oU V (! output = oV | output = oU)))))
LTLSPEC (FALSE V (! ((input = iA & ! input = iD) & (TRUE U input = iD)) | (! output = oU U (input = iE | input = iD))))
LTLSPEC (FALSE V (! output = oY | ((! ((output = oV & ! input = iA) & X (! input = iA U (output = oU & ! input = iA))) U (input = iA | input = iD)) | (FALSE V ! (output = oV & X (TRUE U output = oU))))))