Problem5-LTL.smv 13.9 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
LTLSPEC (FALSE V (! input = iE | ((! input = iI | (! input = iC U ((output = oP & ! input = iC) & X (! input = iC U output = oW)))) U (input = iC | (FALSE V (! input = iI | (output = oP & X (TRUE U output = oW))))))))
LTLSPEC (! (TRUE U output = oZ) | (! output = oQ U (input = iA | output = oZ)))
LTLSPEC (! (TRUE U input = iA) | (! ((output = oY & ! input = iA) & X (! input = iA U (output = oS & ! input = iA))) U (input = iA | output = oQ)))
LTLSPEC ((FALSE V ! output = oZ) | (! output = oZ U (output = oZ & (! (TRUE U (output = oV & X (TRUE U output = oX))) | (! output = oV U input = iH)))))
LTLSPEC ((FALSE V ! input = iE) | (TRUE U (input = iE & (input = iI V (! output = oQ | input = iI)))))
LTLSPEC (! (TRUE U output = oO) | ((! input = iF | (! output = oO U (output = oW & ! output = oO))) U output = oO))
LTLSPEC (FALSE V (! output = oR | ((! input = iB | (! output = oS U (((output = oY & ! output = oS) & ! output = oP) & X ((! output = oS & ! output = oP) U output = oX)))) U (output = oS | (FALSE V (! input = iB | ((output = oY & ! output = oP) & X (! output = oP U output = oX))))))))
LTLSPEC (FALSE V (! ((output = oS & ! output = oY) & (TRUE U output = oY)) | (! output = oX U (input = iI | output = oY))))
LTLSPEC (FALSE V (output = oW & (! ! output = oP | ((output = oX | output = oP) V (! output = oY | (output = oX | output = oP))))))
LTLSPEC (FALSE V (! (input = iD & (TRUE U output = oW)) | ((input = iC & (! X (! output = oW U input = iE) | X (! output = oW U (input = iE & (TRUE U output = oZ))))) U output = oW)))
LTLSPEC (FALSE V (output = oR & (! ! output = oU | (output = oU V ((! input = iJ | (! output = oU U (output = oT & ! output = oU))) | output = oU)))))
LTLSPEC (FALSE V (! input = iI | (TRUE U (output = oU & X (TRUE U output = oV)))))
LTLSPEC (FALSE V (! input = iJ | (TRUE U ((output = oO & ! output = oX) & X (! output = oX U output = oU)))))
LTLSPEC (FALSE V (! (input = iJ & (TRUE U output = oR)) | ((! input = iC | (! output = oR U (((output = oT & ! output = oR) & ! output = oS) & X ((! output = oR & ! output = oS) U output = oW)))) U output = oR)))
LTLSPEC (FALSE V (! output = oY | ((input = iD & (! X (! output = oQ U input = iG) | X (! output = oQ U (input = iG & (TRUE U output = oX))))) U (output = oQ | (FALSE V (input = iD & (! X (! output = oQ U input = iG) | X (! output = oQ U (input = iG & (TRUE U output = oX))))))))))
LTLSPEC (FALSE V (! input = iB | ((! input = iA | (! input = iD U (((output = oV & ! input = iD) & ! output = oQ) & X ((! input = iD & ! output = oQ) U output = oP)))) U (input = iD | (FALSE V (! input = iA | ((output = oV & ! output = oQ) & X (! output = oQ U output = oP))))))))
LTLSPEC (FALSE V (! input = iB | (TRUE U ((output = oY & ! output = oW) & X (! output = oW U output = oZ)))))
LTLSPEC (output = oV V (! output = oR | output = oV))
LTLSPEC (! (TRUE U output = oZ) | ((! input = iI | (! output = oZ U (((output = oO & ! output = oZ) & ! output = oP) & X ((! output = oZ & ! output = oP) U output = oW)))) U output = oZ))
LTLSPEC (! (TRUE U input = iJ) | (! ((output = oO & ! input = iJ) & X (! input = iJ U (output = oV & ! input = iJ))) U (input = iJ | output = oY)))
LTLSPEC (! (TRUE U output = oR) | (! ((output = oX & ! output = oR) & X (! output = oR U (output = oZ & ! output = oR))) U (output = oR | input = iB)))
LTLSPEC (! (TRUE U output = oO) | ((! input = iH | (! output = oO U ((output = oW & ! output = oO) & X (! output = oO U output = oZ)))) U output = oO))
LTLSPEC ((FALSE V ! output = oV) | (TRUE U (output = oV & (output = oO V (! output = oU | output = oO)))))
LTLSPEC (output = oX V (! output = oV | output = oX))
LTLSPEC (! (TRUE U input = iG) | ((! input = iC | (! input = iG U (output = oW & ! input = iG))) U input = iG))
LTLSPEC (! (TRUE U output = oP) | ((! input = iC | (! output = oP U ((output = oR & ! output = oP) & X (! output = oP U output = oU)))) U output = oP))
LTLSPEC (! (TRUE U output = oS) | (! output = oS U ((output = oT & ! output = oS) & X (! output = oS U input = iE))))
LTLSPEC (FALSE V (! output = oT | (FALSE V (input = iB & (! X (TRUE U input = iH) | X (! input = iH U (input = iH & (TRUE U output = oZ))))))))
LTLSPEC (FALSE V (! output = oY | (FALSE V (input = iC & (! X (TRUE U input = iD) | X (! input = iD U (input = iD & (TRUE U output = oR))))))))
LTLSPEC (FALSE V (! input = iE | (TRUE U (output = oX & X (TRUE U output = oY)))))
LTLSPEC (FALSE V (! (output = oT & (TRUE U output = oX)) | ((! input = iH | (! output = oX U ((output = oU & ! output = oX) & X (! output = oX U output = oY)))) U output = oX)))
LTLSPEC (! (TRUE U output = oO) | (! output = oR U (input = iC | output = oO)))
LTLSPEC (! (TRUE U output = oO) | ((! input = iC | (! output = oO U ((output = oW & ! output = oO) & X (! output = oO U output = oT)))) U output = oO))
LTLSPEC ((FALSE V ! input = iE) | (! input = iE U (input = iE & (! (TRUE U output = oZ) | (! output = oZ U ((output = oQ & ! output = oZ) & X (! output = oZ U output = oT)))))))
LTLSPEC (input = iF V (! output = oU | input = iF))
LTLSPEC (! (TRUE U output = oS) | (! output = oS U ((input = iD & ! output = oS) & X (! output = oS U input = iA))))
LTLSPEC (FALSE V (! ((input = iE & ! output = oR) & (TRUE U output = oR)) | (! output = oY U (output = oO | output = oR))))
LTLSPEC (FALSE V (! output = oY | (! (TRUE U output = oP) | (! output = oP U (output = oT | ((input = iD & ! output = oP) & X (! output = oP U output = oX)))))))
LTLSPEC (FALSE V (input = iE & (! ! input = iD | ((output = oT | input = iD) V (! output = oZ | (output = oT | input = iD))))))
LTLSPEC (FALSE V (! input = iJ | ((input = iD & (! X (! output = oQ U input = iA) | X (! output = oQ U (input = iA & (TRUE U output = oS))))) U (output = oQ | (FALSE V (input = iD & (! X (! output = oQ U input = iA) | X (! output = oQ U (input = iA & (TRUE U output = oS))))))))))
LTLSPEC (! (TRUE U input = iD) | (! output = oP U (input = iD | ((input = iC & ! output = oP) & X (! output = oP U output = oU)))))
LTLSPEC ((FALSE V ! output = oX) | (! output = oX U (output = oX & (! (TRUE U output = oW) | (! output = oW U ((output = oS & ! output = oW) & X (! output = oW U input = iF)))))))
LTLSPEC ((FALSE V ! output = oQ) | (! output = oQ U (output = oQ & (! (TRUE U output = oS) | (! output = oS U ((output = oR & ! output = oS) & X (! output = oS U input = iG)))))))
LTLSPEC (! (TRUE U input = iG) | (! ((output = oY & ! input = iG) & X (! input = iG U (output = oX & ! input = iG))) U (input = iG | input = iH)))
LTLSPEC (FALSE V (input = iB & (! ! output = oX | (output = oX V ((! input = iA | (! output = oX U (output = oQ & ! output = oX))) | output = oX)))))
LTLSPEC (FALSE V (! ((output = oQ & ! input = iC) & (TRUE U input = iC)) | ((! input = iG | (! input = iC U (output = oP & ! input = iC))) U input = iC)))
LTLSPEC (FALSE V (! output = oQ | (FALSE V (input = iJ & (! X (TRUE U input = iA) | X (! input = iA U (input = iA & (TRUE U output = oP))))))))
LTLSPEC (FALSE V (! (input = iI & (TRUE U output = oO)) | (! ((output = oS & ! output = oO) & X (! output = oO U (output = oY & ! output = oO))) U (output = oO | input = iB))))
LTLSPEC (! (TRUE U output = oU) | (! ((output = oY & ! output = oU) & X (! output = oU U (output = oV & ! output = oU))) U (output = oU | input = iC)))
LTLSPEC (! (TRUE U output = oZ) | (! output = oZ U ((input = iA & ! output = oZ) & X (! output = oZ U output = oY))))
LTLSPEC (FALSE V (! output = oQ | ((! ((output = oR & ! input = iB) & X (! input = iB U (output = oX & ! input = iB))) U (input = iB | output = oW)) | (FALSE V ! (output = oR & X (TRUE U output = oX))))))
LTLSPEC ((FALSE V ! input = iA) | (TRUE U (input = iA & (input = iC V (! output = oT | input = iC)))))
LTLSPEC (FALSE V (! output = oY | (! (TRUE U output = oS) | (! output = oS U (output = oX | ((output = oW & ! output = oS) & X (! output = oS U output = oO)))))))
LTLSPEC (FALSE V (! input = iI | ((! input = iA | (! input = iE U (((output = oR & ! input = iE) & ! output = oU) & X ((! input = iE & ! output = oU) U output = oT)))) U (input = iE | (FALSE V (! input = iA | ((output = oR & ! output = oU) & X (! output = oU U output = oT))))))))
LTLSPEC (FALSE V (! (output = oZ & (TRUE U input = iH)) | ((! input = iB | (! input = iH U ((output = oQ & ! input = iH) & X (! input = iH U output = oS)))) U input = iH)))
LTLSPEC (FALSE V (! input = iA | (TRUE U (output = oV & X (TRUE U output = oX)))))
LTLSPEC (input = iG V (! output = oZ | input = iG))
LTLSPEC (! (TRUE U input = iH) | ((! input = iE | (! input = iH U (output = oS & ! input = iH))) U input = iH))
LTLSPEC (FALSE V (! (output = oT & (TRUE U output = oX)) | ((! input = iC | (! output = oX U ((output = oU & ! output = oX) & X (! output = oX U output = oR)))) U output = oX)))
LTLSPEC (! (TRUE U output = oO) | ((! input = iE | (! output = oO U ((output = oR & ! output = oO) & X (! output = oO U output = oT)))) U output = oO))
LTLSPEC (! (TRUE U input = iJ) | (! ((output = oO & ! input = iJ) & X (! input = iJ U (output = oY & ! input = iJ))) U (input = iJ | output = oV)))
LTLSPEC (! (TRUE U (output = oR & X (TRUE U output = oV))) | (! output = oR U output = oS))
LTLSPEC (FALSE V (! ((input = iH & ! output = oS) & (TRUE U output = oS)) | ((! input = iD | (! output = oS U (output = oT & ! output = oS))) U output = oS)))
LTLSPEC (output = oZ V (! output = oO | output = oZ))
LTLSPEC (FALSE V (! ((input = iC & ! output = oP) & (TRUE U output = oP)) | ((! input = iI | (! output = oP U (output = oS & ! output = oP))) U output = oP)))
LTLSPEC (! (TRUE U input = iH) | (! ((output = oW & ! input = iH) & X (! input = iH U (output = oQ & ! input = iH))) U (input = iH | output = oX)))
LTLSPEC (! (TRUE U output = oS) | ((! input = iF | (! output = oS U ((output = oT & ! output = oS) & X (! output = oS U output = oP)))) U output = oS))
LTLSPEC (! (TRUE U input = iG) | ((input = iH & (! X (! input = iG U input = iJ) | X (! input = iG U (input = iJ & (TRUE U output = oQ))))) U input = iG))
LTLSPEC (! (TRUE U output = oQ) | ((! input = iD | (! output = oQ U (output = oS & ! output = oQ))) U output = oQ))
LTLSPEC (FALSE V (! input = iG | (TRUE U output = oR)))
LTLSPEC (! (TRUE U output = oU) | (! output = oU U ((output = oW & ! output = oU) & X (! output = oU U input = iJ))))
LTLSPEC ((FALSE V ! output = oX) | (! output = oX U (output = oX & (! (TRUE U (output = oO & X (TRUE U output = oV))) | (! output = oO U output = oT)))))
LTLSPEC (! (TRUE U input = iD) | ((! input = iE | (! input = iD U (output = oR & ! input = iD))) U input = iD))
LTLSPEC (! (TRUE U output = oO) | (! output = oO U ((output = oT & ! output = oO) & X (! output = oO U output = oW))))
LTLSPEC (! (TRUE U input = iA) | ((! input = iJ | (! input = iA U ((output = oR & ! input = iA) & X (! input = iA U output = oZ)))) U input = iA))
LTLSPEC (FALSE V (! input = iH | (FALSE V (! input = iB | (output = oQ & X (TRUE U output = oS))))))
LTLSPEC (FALSE V (! input = iH | (! (TRUE U output = oY) | (! output = oY U (output = oV | ((output = oS & ! output = oY) & X (! output = oY U output = oR)))))))
LTLSPEC (! (TRUE U output = oZ) | (! output = oY U (output = oZ | ((output = oT & ! output = oY) & X (! output = oY U input = iF)))))
LTLSPEC (FALSE V (! output = oR | (FALSE V (! input = iJ | ((output = oZ & ! output = oV) & X (! output = oV U output = oX))))))
LTLSPEC (FALSE V (! input = iE | (FALSE V (input = iF & (! X (TRUE U input = iG) | X (! input = iG U (input = iG & (TRUE U output = oV))))))))
LTLSPEC (! (TRUE U input = iI) | ((! input = iD | (! input = iI U (output = oQ & ! input = iI))) U input = iI))
LTLSPEC (FALSE V (! input = iC | (TRUE U output = oT)))
LTLSPEC (! (TRUE U output = oV) | ((! input = iG | (! output = oV U ((output = oX & ! output = oV) & X (! output = oV U output = oT)))) U output = oV))
LTLSPEC (FALSE V (! output = oU | ((! input = iD | (! input = iI U (((output = oO & ! input = iI) & ! output = oW) & X ((! input = iI & ! output = oW) U output = oR)))) U (input = iI | (FALSE V (! input = iD | ((output = oO & ! output = oW) & X (! output = oW U output = oR))))))))
LTLSPEC (! (TRUE U output = oZ) | (! output = oV U (output = oZ | ((input = iD & ! output = oV) & X (! output = oV U output = oO)))))
LTLSPEC (FALSE V (! (output = oO & (TRUE U output = oY)) | ((input = iJ & (! X (! output = oY U input = iE) | X (! output = oY U (input = iE & (TRUE U output = oS))))) U output = oY)))
LTLSPEC (FALSE V (! input = iF | ((! ((output = oW & ! input = iJ) & X (! input = iJ U (output = oZ & ! input = iJ))) U (input = iJ | output = oT)) | (FALSE V ! (output = oW & X (TRUE U output = oZ))))))
LTLSPEC (! (TRUE U output = oZ) | ((! input = iE | (! output = oZ U (output = oU & ! output = oZ))) U output = oZ))
LTLSPEC (! (TRUE U output = oO) | (! ((output = oX & ! output = oO) & X (! output = oO U (output = oR & ! output = oO))) U (output = oO | output = oP)))
LTLSPEC (! (TRUE U output = oO) | (! output = oO U ((output = oZ & ! output = oO) & X (! output = oO U output = oP))))
LTLSPEC (FALSE V (! output = oO | ((input = iG & (! X (! input = iJ U input = iI) | X (! input = iJ U (input = iI & (TRUE U output = oV))))) U (input = iJ | (FALSE V (input = iG & (! X (! input = iJ U input = iI) | X (! input = iJ U (input = iI & (TRUE U output = oV))))))))))
LTLSPEC (! (TRUE U input = iG) | (! output = oR U (input = iB | input = iG)))
LTLSPEC (FALSE V (! output = oV | (FALSE V (input = iA & (! X (TRUE U input = iG) | X (! input = iG U (input = iG & (TRUE U output = oX))))))))
LTLSPEC (! (TRUE U input = iI) | (! output = oY U (input = iI | ((output = oU & ! output = oY) & X (! output = oY U input = iJ)))))
LTLSPEC (FALSE V (input = iJ & (! ! input = iH | ((input = iI | input = iH) V (! output = oP | (input = iI | input = iH))))))
LTLSPEC (! (TRUE U input = iI) | (! output = oZ U (output = oQ | input = iI)))
LTLSPEC (! (TRUE U output = oZ) | (! output = oU U (input = iD | output = oZ)))
LTLSPEC (! (TRUE U output = oZ) | (! output = oZ U ((input = iJ & ! output = oZ) & X (! output = oZ U output = oP))))
LTLSPEC (FALSE V (! input = iG | (FALSE V (! input = iJ | (output = oT & X (TRUE U output = oX))))))
LTLSPEC (FALSE V (! output = oP | (FALSE V (input = iH & (! X (TRUE U input = iB) | X (! input = iB U (input = iB & (TRUE U output = oS))))))))