Problem4-LTL.smv 15.3 KB
Newer Older
Joshua Moerman's avatar
Joshua Moerman committed
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 (! (TRUE U (output = oZ)) | (! (output = oV) U ((output = oZ) | (((input = iD) & ! (output = oV)) & X (! (output = oV) U (output = oO))))))
LTLSPEC (FALSE V (! (input = iA) | (TRUE U ((output = oV) & X (TRUE U (output = oX))))))
LTLSPEC (FALSE V (! (input = iH) | (TRUE U (output = oY))))
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 (! (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 (FALSE V (! ((output = oS) & (TRUE U (output = oW))) | ((! (input = iG) | (! (output = oW) U ((((output = oR) & ! (output = oW)) & ! (output = oT)) & X ((! (output = oW) & ! (output = oT)) U (output = oP))))) U (output = oW))))
LTLSPEC (FALSE V (! (output = oP) | (FALSE V ((input = iH) & (! X (TRUE U (input = iB)) | X (! (input = iB) U ((input = iB) & (TRUE U (output = oS)))))))))
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 (FALSE V (! (input = iH) | (TRUE U ((output = oR) & X (TRUE U (output = oQ))))))
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 (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 = iD) | (TRUE U (output = oR))))
LTLSPEC (FALSE V (! (((input = iA) & ! (output = oR)) & (TRUE U (output = oR))) | (! (output = oS) U ((input = iD) | (output = oR)))))
LTLSPEC (! (TRUE U (output = oX)) | (! (output = oX) U (((output = oO) & ! (output = oX)) & X (! (output = oX) U (input = iA)))))
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 (input = iJ)) | (! (((output = oO) & ! (input = iJ)) & X (! (input = iJ) U ((output = oV) & ! (input = iJ)))) U ((input = iJ) | (output = oY))))
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 (output = oS)) | ((! (input = iF) | (! (output = oS) U (((output = oT) & ! (output = oS)) & X (! (output = oS) U (output = oP))))) U (output = oS)))
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 = oV) V (! (output = oR) | (output = oV)))
LTLSPEC (! (TRUE U (input = iI)) | (! (output = oZ) U ((output = oQ) | (input = iI))))
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 = iA)) | ((! (input = iJ) | (! (input = iA) U (((output = oR) & ! (input = iA)) & X (! (input = iA) U (output = oZ))))) U (input = iA)))
LTLSPEC (FALSE V (! (input = iH) | ((! (input = iF) | (! (output = oY) U (((output = oS) & ! (output = oY)) & X (! (output = oY) U (output = oX))))) U ((output = oY) | (FALSE V (! (input = iF) | ((output = oS) & X (TRUE U (output = oX)))))))))
LTLSPEC ((FALSE V ! (output = oX)) | (TRUE U ((output = oX) & ((output = oW) V (! (output = oO) | (output = oW))))))
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 (! (TRUE U (output = oS)) | (! (output = oS) U (((output = oT) & ! (output = oS)) & X (! (output = oS) U (input = iE)))))
LTLSPEC (! (TRUE U (input = iH)) | (! (((output = oW) & ! (input = iH)) & X (! (input = iH) U ((output = oQ) & ! (input = iH)))) U ((input = iH) | (output = oX))))
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 (! (input = iG) | (TRUE U (output = oR))))
LTLSPEC (! (TRUE U (output = oR)) | (! (output = oU) U ((output = oR) | (((output = oO) & ! (output = oU)) & X (! (output = oU) U (input = iF))))))
LTLSPEC (FALSE V (! ((output = oT) & (TRUE U (input = iF))) | (! (output = oY) U ((input = iF) | (((output = oP) & ! (output = oY)) & X (! (output = oY) U (input = iG)))))))
LTLSPEC (! (TRUE U (input = iG)) | ((! (input = iC) | (! (input = iG) U ((output = oW) & ! (input = iG)))) U (input = iG)))
LTLSPEC (FALSE V ((input = iJ) & (! ! (input = iH) | (((input = iI) | (input = iH)) V (! (output = oP) | ((input = iI) | (input = iH)))))))
LTLSPEC (! (TRUE U (output = oZ)) | ((! (input = iE) | (! (output = oZ) U ((output = oU) & ! (output = oZ)))) U (output = oZ)))
LTLSPEC (FALSE V (! (input = iF) | (TRUE U (((output = oQ) & ! (output = oU)) & X (! (output = oU) U (output = oR))))))
LTLSPEC (! (TRUE U (input = iA)) | (! (((output = oY) & ! (input = iA)) & X (! (input = iA) U ((output = oS) & ! (input = iA)))) U ((input = iA) | (output = oQ))))
LTLSPEC (! (TRUE U (output = oZ)) | (! (output = oQ) U ((input = iA) | (output = oZ))))
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 (! (output = oZ) | (FALSE V (! (input = iB) | (((output = oT) & ! (output = oU)) & X (! (output = oU) U (output = oQ)))))))
LTLSPEC (FALSE V (! (((input = iE) & ! (output = oR)) & (TRUE U (output = oR))) | (! (output = oY) U ((output = oO) | (output = oR)))))
LTLSPEC (! (TRUE U (input = iC)) | (! (output = oQ) U ((input = iC) | (((output = oS) & ! (output = oQ)) & X (! (output = oQ) U (output = oY))))))
LTLSPEC (FALSE V ((input = iA) & (! ! (input = iJ) | (((output = oZ) | (input = iJ)) V (! (output = oP) | ((output = oZ) | (input = iJ)))))))
LTLSPEC (! (TRUE U (output = oZ)) | (! (output = oY) U ((output = oZ) | (((output = oT) & ! (output = oY)) & X (! (output = oY) U (input = iF))))))
LTLSPEC (FALSE V (! ((input = iB) & (TRUE U (input = iD))) | ((! (input = iA) | (! (input = iD) U (((output = oP) & ! (input = iD)) & X (! (input = iD) U (output = oZ))))) U (input = iD))))
LTLSPEC (FALSE V (! (output = oV) | ((! (((output = oX) & ! (output = oW)) & X (! (output = oW) U ((output = oS) & ! (output = oW)))) U ((output = oW) | (output = oR))) | (FALSE V ! ((output = oX) & X (TRUE U (output = oS)))))))
LTLSPEC (FALSE V ((input = iD) & (! ! (output = oU) | (((input = iB) | (output = oU)) V (! (output = oR) | ((input = iB) | (output = oU)))))))
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 (input = iI)) | (! (output = oY) U ((input = iI) | (((output = oU) & ! (output = oY)) & X (! (output = oY) U (input = iJ))))))
LTLSPEC (FALSE V (! (input = iB) | (TRUE U ((output = oQ) & X (TRUE U (output = oY))))))
LTLSPEC (! (TRUE U (output = oU)) | (! (output = oU) U (((output = oW) & ! (output = oU)) & X (! (output = oU) U (input = iJ)))))
LTLSPEC (FALSE V (! (input = iI) | (TRUE U ((output = oU) & X (TRUE U (output = oV))))))
LTLSPEC (FALSE V ((output = oR) & (! ! (output = oU) | ((output = oU) V ((! (input = iJ) | (! (output = oU) U ((output = oT) & ! (output = oU)))) | (output = oU))))))
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 (! (TRUE U (input = iJ)) | (! (((output = oO) & ! (input = iJ)) & X (! (input = iJ) U ((output = oY) & ! (input = iJ)))) U ((input = iJ) | (output = oV))))
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 (FALSE V (! (((output = oS) & ! (output = oY)) & (TRUE U (output = oY))) | (! (output = oX) U ((input = iI) | (output = oY)))))
LTLSPEC (! (TRUE U (output = oZ)) | (! (output = oU) U ((input = iD) | (output = oZ))))
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 ((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 (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 (! (output = oV) | (FALSE V ((input = iA) & (! X (TRUE U (input = iG)) | X (! (input = iG) U ((input = iG) & (TRUE U (output = oX)))))))))
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 (! (TRUE U (input = iD)) | ((! (input = iE) | (! (input = iD) U ((output = oR) & ! (input = iD)))) U (input = iD)))
LTLSPEC ((output = oZ) V (! (output = oO) | (output = oZ)))
LTLSPEC (! (TRUE U (output = oO)) | (! (output = oR) U ((input = iC) | (output = oO))))
LTLSPEC (FALSE V ((input = iB) & (! ! (output = oX) | ((output = oX) V ((! (input = iA) | (! (output = oX) U ((output = oQ) & ! (output = oX)))) | (output = oX))))))
LTLSPEC ((output = oX) V (! (output = oV) | (output = oX)))
LTLSPEC ((input = iG) V (! (output = oZ) | (input = iG)))
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 (! (TRUE U (input = iA)) | ((! (input = iG) | (! (input = iA) U ((((output = oX) & ! (input = iA)) & ! (output = oS)) & X ((! (input = iA) & ! (output = oS)) U (output = oP))))) U (input = iA)))
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 (! (TRUE U (output = oO)) | ((! (input = iF) | (! (output = oO) U ((output = oW) & ! (output = oO)))) U (output = oO)))
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 (! (input = iB) | (TRUE U (((output = oY) & ! (output = oW)) & X (! (output = oW) U (output = oZ))))))
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 (! (TRUE U (output = oO)) | ((! (input = iH) | (! (output = oO) U (((output = oW) & ! (output = oO)) & X (! (output = oO) U (output = oZ))))) U (output = oO)))
LTLSPEC (! (TRUE U (output = oQ)) | ((! (input = iD) | (! (output = oQ) U ((output = oS) & ! (output = oQ)))) U (output = oQ)))
LTLSPEC (! (TRUE U (input = iH)) | ((! (input = iE) | (! (input = iH) U ((output = oS) & ! (input = iH)))) U (input = iH)))
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 (FALSE V (! ((input = iG) & (TRUE U (output = oS))) | ((! (input = iA) | (! (output = oS) U ((((output = oW) & ! (output = oS)) & ! (output = oT)) & X ((! (output = oS) & ! (output = oT)) U (output = oQ))))) U (output = oS))))
LTLSPEC (FALSE V (! (output = oU) | (! (TRUE U (output = oT)) | (! (output = oT) U ((input = iA) | (((input = iJ) & ! (output = oT)) & X (! (output = oT) U (input = iB))))))))
LTLSPEC (! (TRUE U (output = oR)) | (! (((output = oX) & ! (output = oR)) & X (! (output = oR) U ((output = oZ) & ! (output = oR)))) U ((output = oR) | (input = iB))))
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 (FALSE V (! (input = iD) | (FALSE V (! (input = iH) | (TRUE U (output = oX))))))
LTLSPEC (! (TRUE U (output = oO)) | (! (output = oO) U (((output = oZ) & ! (output = oO)) & X (! (output = oO) U (output = oP)))))
LTLSPEC (FALSE V (! ((input = iI) & (TRUE U (output = oO))) | (! (output = oT) U ((output = oO) | (((output = oQ) & ! (output = oT)) & X (! (output = oT) U (output = oZ)))))))
LTLSPEC (FALSE V (! (input = iH) | (FALSE V (! (input = iB) | ((output = oQ) & X (TRUE U (output = oS)))))))
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 (! (TRUE U (input = iH)) | (! (output = oW) U ((input = iH) | (((input = iJ) & ! (output = oW)) & X (! (output = oW) U (output = oZ))))))
LTLSPEC ((FALSE V ! (input = iE)) | (TRUE U ((input = iE) & ((input = iI) V (! (output = oQ) | (input = iI))))))
LTLSPEC (FALSE V (! (output = oR) | (FALSE V (! (input = iJ) | (((output = oZ) & ! (output = oV)) & X (! (output = oV) U (output = oX)))))))
LTLSPEC (FALSE V (! (input = iE) | (TRUE U ((output = oX) & X (TRUE U (output = oY))))))
LTLSPEC (! (TRUE U (input = iG)) | (! (output = oR) U ((input = iB) | (input = iG))))
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 (output = oO)) | ((! (input = iE) | (! (output = oO) U (((output = oR) & ! (output = oO)) & X (! (output = oO) U (output = oT))))) U (output = oO)))
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)) | (((input = iH) & (! X (! (input = iG) U (input = iJ)) | X (! (input = iG) U ((input = iJ) & (TRUE U (output = oQ)))))) U (input = iG)))
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)))))))