Problem9-LTL.smv 16.1 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 ((FALSE V ! (input = iO)) | (TRUE U ((input = iO) & ((input = iF) V (! (output = oU) | (input = iF))))))
LTLSPEC (! (TRUE U ((output = oZ) & X (TRUE U (output = oV)))) | (! (output = oZ) U (input = iD)))
LTLSPEC (! (TRUE U (input = iK)) | (! (output = oZ) U ((input = iS) | (input = iK))))
LTLSPEC (FALSE V (! ((input = iK) & (TRUE U (input = iC))) | ((! (input = iO) | (! (input = iC) U ((((output = oZ) & ! (input = iC)) & ! (output = oY)) & X ((! (input = iC) & ! (output = oY)) U (output = oV))))) U (input = iC))))
LTLSPEC (FALSE V (! ((input = iH) & (TRUE U (input = iJ))) | ((! (input = iK) | (! (input = iJ) U ((((output = oZ) & ! (input = iJ)) & ! (output = oV)) & X ((! (input = iJ) & ! (output = oV)) U (output = oU))))) U (input = iJ))))
LTLSPEC (FALSE V (! (input = iT) | ((! (((output = oV) & ! (input = iL)) & X (! (input = iL) U ((output = oZ) & ! (input = iL)))) U ((input = iL) | (input = iO))) | (FALSE V ! ((output = oV) & X (TRUE U (output = oZ)))))))
LTLSPEC (FALSE V (! (input = iR) | (FALSE V (! (input = iN) | (((output = oW) & ! (output = oY)) & X (! (output = oY) U (output = oZ)))))))
LTLSPEC (! (TRUE U (output = oZ)) | (! (output = oZ) U (((output = oU) & ! (output = oZ)) & X (! (output = oZ) U (input = iT)))))
LTLSPEC (FALSE V (! (input = iD) | ((! (((output = oZ) & ! (input = iJ)) & X (! (input = iJ) U ((output = oX) & ! (input = iJ)))) U ((input = iJ) | (input = iO))) | (FALSE V ! ((output = oZ) & X (TRUE U (output = oX)))))))
LTLSPEC (FALSE V (! ((input = iN) & (TRUE U (output = oU))) | ((! (input = iP) | (! (output = oU) U (((output = oZ) & ! (output = oU)) & X (! (output = oU) U (output = oW))))) U (output = oU))))
LTLSPEC (FALSE V ((output = oW) & (! ! (input = iK) | ((input = iK) V ((! (input = iE) | (! (input = iK) U ((output = oV) & ! (input = iK)))) | (input = iK))))))
LTLSPEC (! (TRUE U (input = iR)) | (((input = iG) & (! X (! (input = iR) U (input = iS)) | X (! (input = iR) U ((input = iS) & (TRUE U (output = oW)))))) U (input = iR)))
LTLSPEC (FALSE V (! ((input = iR) & (TRUE U (input = iN))) | (! (((output = oZ) & ! (input = iN)) & X (! (input = iN) U ((output = oY) & ! (input = iN)))) U ((input = iN) | (output = oX)))))
LTLSPEC (FALSE V (! (input = iR) | ((! (input = iB) | (! (input = iD) U (((output = oV) & ! (input = iD)) & X (! (input = iD) U (output = oZ))))) U ((input = iD) | (FALSE V (! (input = iB) | ((output = oV) & X (TRUE U (output = oZ)))))))))
LTLSPEC (FALSE V (! ((output = oX) & (TRUE U (input = iG))) | ((! (input = iR) | (! (input = iG) U (((output = oU) & ! (input = iG)) & X (! (input = iG) U (output = oY))))) U (input = iG))))
LTLSPEC (FALSE V (! (input = iL) | (FALSE V (! (input = iJ) | (((output = oZ) & ! (output = oV)) & X (! (output = oV) U (output = oY)))))))
LTLSPEC (FALSE V (! (input = iO) | (TRUE U (output = oW))))
LTLSPEC (FALSE V (! (input = iK) | ((! (input = iR) | (! (input = iI) U (((output = oV) & ! (input = iI)) & X (! (input = iI) U (output = oZ))))) U ((input = iI) | (FALSE V (! (input = iR) | ((output = oV) & X (TRUE U (output = oZ)))))))))
LTLSPEC (FALSE V (! ((input = iP) & (TRUE U (input = iI))) | ((! (input = iD) | (! (input = iI) U ((((output = oY) & ! (input = iI)) & ! (output = oZ)) & X ((! (input = iI) & ! (output = oZ)) U (output = oX))))) U (input = iI))))
LTLSPEC (FALSE V (! ((input = iM) & (TRUE U (output = oV))) | (! (output = oZ) U ((output = oV) | (((input = iA) & ! (output = oZ)) & X (! (output = oZ) U (input = iB)))))))
LTLSPEC ((FALSE V ! (input = iG)) | (! (input = iG) U ((input = iG) & (! (TRUE U ((output = oW) & X (TRUE U (output = oZ)))) | (! (output = oW) U (output = oX))))))
LTLSPEC (FALSE V (! ((input = iR) & (TRUE U (input = iS))) | ((! (input = iI) | (! (input = iS) U ((((output = oX) & ! (input = iS)) & ! (output = oW)) & X ((! (input = iS) & ! (output = oW)) U (output = oZ))))) U (input = iS))))
LTLSPEC (FALSE V (! (input = iQ) | (FALSE V ((input = iR) & (! X (TRUE U (input = iA)) | X (! (input = iA) U ((input = iA) & (TRUE U (output = oU)))))))))
LTLSPEC (FALSE V (! (output = oW) | (((input = iL) & (! X (! (input = iC) U (input = iM)) | X (! (input = iC) U ((input = iM) & (TRUE U (output = oY)))))) U ((input = iC) | (FALSE V ((input = iL) & (! X (! (input = iC) U (input = iM)) | X (! (input = iC) U ((input = iM) & (TRUE U (output = oY)))))))))))
LTLSPEC (FALSE V (! (((input = iF) & ! (input = iA)) & (TRUE U (input = iA))) | ((! (input = iB) | (! (input = iA) U ((output = oW) & ! (input = iA)))) U (input = iA))))
LTLSPEC ((FALSE V ! (input = iP)) | (! (input = iP) U ((input = iP) & (! (TRUE U (output = oV)) | (! (output = oV) U (((input = iH) & ! (output = oV)) & X (! (output = oV) U (input = iT))))))))
LTLSPEC (! (TRUE U (output = oX)) | (! (output = oX) U (((output = oY) & ! (output = oX)) & X (! (output = oX) U (output = oZ)))))
LTLSPEC (! (TRUE U (input = iE)) | (((input = iD) & (! X (! (input = iE) U (input = iF)) | X (! (input = iE) U ((input = iF) & (TRUE U (output = oX)))))) U (input = iE)))
LTLSPEC (FALSE V (! (((input = iR) & ! (input = iI)) & (TRUE U (input = iI))) | ((! (input = iO) | (! (input = iI) U ((output = oV) & ! (input = iI)))) U (input = iI))))
LTLSPEC (FALSE V (! (input = iT) | (FALSE V ((input = iB) & (! X (TRUE U (input = iL)) | X (! (input = iL) U ((input = iL) & (TRUE U (output = oX)))))))))
LTLSPEC (! (TRUE U (output = oU)) | (! (output = oU) U (((input = iC) & ! (output = oU)) & X (! (output = oU) U (input = iG)))))
LTLSPEC ((FALSE V ! (output = oW)) | (TRUE U ((output = oW) & ((input = iB) V (! (output = oY) | (input = iB))))))
LTLSPEC (FALSE V (! (((output = oU) & ! (input = iP)) & (TRUE U (input = iP))) | (! (output = oZ) U ((input = iG) | (input = iP)))))
LTLSPEC (FALSE V (! (((input = iG) & ! (input = iA)) & (TRUE U (input = iA))) | ((! (input = iS) | (! (input = iA) U ((output = oU) & ! (input = iA)))) U (input = iA))))
LTLSPEC (FALSE V (! (input = iK) | (TRUE U (((output = oU) & ! (output = oY)) & X (! (output = oY) U (output = oZ))))))
LTLSPEC (! (TRUE U (output = oX)) | (! (output = oW) U ((output = oX) | (((input = iN) & ! (output = oW)) & X (! (output = oW) U (input = iL))))))
LTLSPEC (FALSE V (! (((output = oY) & ! (input = iF)) & (TRUE U (input = iF))) | ((! (input = iR) | (! (input = iF) U ((output = oU) & ! (input = iF)))) U (input = iF))))
LTLSPEC (! (TRUE U ((output = oU) & X (TRUE U (output = oX)))) | (! (output = oU) U (input = iO)))
LTLSPEC (FALSE V (! (((input = iP) & ! (input = iF)) & (TRUE U (input = iF))) | ((! (input = iL) | (! (input = iF) U ((output = oY) & ! (input = iF)))) U (input = iF))))
LTLSPEC (FALSE V ((input = iF) & (! ! (output = oY) | (((output = oU) | (output = oY)) V (! (output = oX) | ((output = oU) | (output = oY)))))))
LTLSPEC (! (TRUE U (input = iR)) | (! (output = oY) U ((output = oZ) | (input = iR))))
LTLSPEC (FALSE V (! (input = iA) | ((! (input = iG) | (! (input = iO) U ((((output = oW) & ! (input = iO)) & ! (output = oY)) & X ((! (input = iO) & ! (output = oY)) U (output = oV))))) U ((input = iO) | (FALSE V (! (input = iG) | (((output = oW) & ! (output = oY)) & X (! (output = oY) U (output = oV)))))))))
LTLSPEC (FALSE V (! (input = iD) | (FALSE V (! (input = iR) | ((output = oX) & X (TRUE U (output = oW)))))))
LTLSPEC (FALSE V (! ((input = iD) & (TRUE U (output = oY))) | (((input = iM) & (! X (! (output = oY) U (input = iO)) | X (! (output = oY) U ((input = iO) & (TRUE U (output = oW)))))) U (output = oY))))
LTLSPEC (FALSE V (! (input = iL) | (TRUE U ((output = oY) & X (TRUE U (output = oU))))))
LTLSPEC (! (TRUE U (input = iI)) | ((! (input = iF) | (! (input = iI) U ((output = oY) & ! (input = iI)))) U (input = iI)))
LTLSPEC (FALSE V (! (input = iD) | (TRUE U (output = oX))))
LTLSPEC (FALSE V (! ((input = iD) & (TRUE U (input = iO))) | ((! (input = iQ) | (! (input = iO) U ((((output = oU) & ! (input = iO)) & ! (output = oY)) & X ((! (input = iO) & ! (output = oY)) U (output = oZ))))) U (input = iO))))
LTLSPEC (FALSE V (! (input = iD) | (FALSE V (! (input = iG) | (((output = oW) & ! (output = oU)) & X (! (output = oU) U (output = oY)))))))
LTLSPEC (FALSE V (! (input = iR) | ((! (input = iQ) | (! (input = iH) U (((output = oY) & ! (input = iH)) & X (! (input = iH) U (output = oX))))) U ((input = iH) | (FALSE V (! (input = iQ) | ((output = oY) & X (TRUE U (output = oX)))))))))
LTLSPEC (FALSE V (! (input = iR) | (TRUE U (((output = oU) & ! (output = oY)) & X (! (output = oY) U (output = oV))))))
LTLSPEC (FALSE V (! (((input = iG) & ! (input = iA)) & (TRUE U (input = iA))) | (! (output = oU) U ((input = iR) | (input = iA)))))
LTLSPEC ((FALSE V ! (input = iQ)) | (TRUE U ((input = iQ) & ((input = iM) V (! (output = oW) | (input = iM))))))
LTLSPEC (! (TRUE U ((output = oW) & X (TRUE U (output = oV)))) | (! (output = oW) U (output = oX)))
LTLSPEC (FALSE V (! ((output = oU) & (TRUE U (input = iL))) | ((! (input = iR) | (! (input = iL) U (((output = oY) & ! (input = iL)) & X (! (input = iL) U (output = oX))))) U (input = iL))))
LTLSPEC (FALSE V (! (input = iD) | (FALSE V (! (input = iT) | (((output = oV) & ! (output = oW)) & X (! (output = oW) U (output = oZ)))))))
LTLSPEC (FALSE V (! (input = iA) | (((input = iF) & (! X (! (input = iS) U (input = iB)) | X (! (input = iS) U ((input = iB) & (TRUE U (output = oV)))))) U ((input = iS) | (FALSE V ((input = iF) & (! X (! (input = iS) U (input = iB)) | X (! (input = iS) U ((input = iB) & (TRUE U (output = oV)))))))))))
LTLSPEC (FALSE V (! ((output = oX) & (TRUE U (input = iB))) | (! (((output = oV) & ! (input = iB)) & X (! (input = iB) U ((output = oW) & ! (input = iB)))) U ((input = iB) | (input = iJ)))))
LTLSPEC (! (TRUE U (input = iA)) | ((! (input = iS) | (! (input = iA) U ((((output = oZ) & ! (input = iA)) & ! (output = oY)) & X ((! (input = iA) & ! (output = oY)) U (output = oW))))) U (input = iA)))
LTLSPEC (! (TRUE U (input = iS)) | ((! (input = iT) | (! (input = iS) U (((output = oX) & ! (input = iS)) & X (! (input = iS) U (output = oV))))) U (input = iS)))
LTLSPEC (FALSE V (! (input = iE) | (! (TRUE U (output = oV)) | (! (output = oV) U ((input = iF) | (((input = iB) & ! (output = oV)) & X (! (output = oV) U (input = iL))))))))
LTLSPEC (! (TRUE U (input = iF)) | ((! (input = iR) | (! (input = iF) U (((output = oW) & ! (input = iF)) & X (! (input = iF) U (output = oU))))) U (input = iF)))
LTLSPEC (FALSE V (! (input = iR) | (TRUE U (((output = oV) & ! (output = oY)) & X (! (output = oY) U (output = oZ))))))
LTLSPEC (FALSE V (! (input = iR) | (TRUE U (((output = oV) & ! (output = oY)) & X (! (output = oY) U (output = oX))))))
LTLSPEC (! (TRUE U (input = iC)) | (((input = iM) & (! X (! (input = iC) U (input = iI)) | X (! (input = iC) U ((input = iI) & (TRUE U (output = oW)))))) U (input = iC)))
LTLSPEC (FALSE V (! ((input = iE) & (TRUE U (input = iR))) | ((! (input = iN) | (! (input = iR) U (((output = oV) & ! (input = iR)) & X (! (input = iR) U (output = oU))))) U (input = iR))))
LTLSPEC (FALSE V (! ((input = iB) & (TRUE U (input = iC))) | (! (output = oV) U ((input = iC) | (((input = iD) & ! (output = oV)) & X (! (output = oV) U (input = iL)))))))
LTLSPEC (! (TRUE U (input = iE)) | ((! (input = iR) | (! (input = iE) U ((output = oW) & ! (input = iE)))) U (input = iE)))
LTLSPEC (FALSE V (! (input = iA) | (FALSE V (! (input = iS) | (TRUE U (output = oY))))))
LTLSPEC (! (TRUE U (input = iR)) | ((! (input = iJ) | (! (input = iR) U (((output = oU) & ! (input = iR)) & X (! (input = iR) U (output = oY))))) U (input = iR)))
LTLSPEC (FALSE V (! (input = iA) | (FALSE V (! (input = iP) | (((output = oV) & ! (output = oX)) & X (! (output = oX) U (output = oU)))))))
LTLSPEC (FALSE V (! (input = iF) | ((! (input = iJ) | (! (input = iK) U ((((output = oW) & ! (input = iK)) & ! (output = oZ)) & X ((! (input = iK) & ! (output = oZ)) U (output = oY))))) U ((input = iK) | (FALSE V (! (input = iJ) | (((output = oW) & ! (output = oZ)) & X (! (output = oZ) U (output = oY)))))))))
LTLSPEC (FALSE V (! (output = oZ) | ((! (((output = oU) & ! (input = iL)) & X (! (input = iL) U ((output = oY) & ! (input = iL)))) U ((input = iL) | (input = iD))) | (FALSE V ! ((output = oU) & X (TRUE U (output = oY)))))))
LTLSPEC (FALSE V (! (((output = oU) & ! (input = iP)) & (TRUE U (input = iP))) | (! (output = oX) U ((input = iB) | (input = iP)))))
LTLSPEC (FALSE V (! (input = iP) | ((! (input = iI) | (! (output = oX) U ((((output = oW) & ! (output = oX)) & ! (output = oV)) & X ((! (output = oX) & ! (output = oV)) U (output = oU))))) U ((output = oX) | (FALSE V (! (input = iI) | (((output = oW) & ! (output = oV)) & X (! (output = oV) U (output = oU)))))))))
LTLSPEC (FALSE V (! (input = iB) | (FALSE V (! (input = iG) | (((output = oW) & ! (output = oX)) & X (! (output = oX) U (output = oZ)))))))
LTLSPEC (FALSE V (! (input = iG) | (FALSE V (! (input = iI) | ((output = oX) & X (TRUE U (output = oU)))))))
LTLSPEC (FALSE V (! (input = iM) | (TRUE U (((output = oW) & ! (output = oZ)) & X (! (output = oZ) U (output = oU))))))
LTLSPEC (! (TRUE U ((output = oZ) & X (TRUE U (output = oW)))) | (! (output = oZ) U (input = iN)))
LTLSPEC (FALSE V (! (input = iK) | (((input = iP) & (! X (! (output = oX) U (input = iC)) | X (! (output = oX) U ((input = iC) & (TRUE U (output = oY)))))) U ((output = oX) | (FALSE V ((input = iP) & (! X (! (output = oX) U (input = iC)) | X (! (output = oX) U ((input = iC) & (TRUE U (output = oY)))))))))))
LTLSPEC (FALSE V (! (input = iI) | ((! (((output = oX) & ! (output = oU)) & X (! (output = oU) U ((output = oV) & ! (output = oU)))) U ((output = oU) | (input = iJ))) | (FALSE V ! ((output = oX) & X (TRUE U (output = oV)))))))
LTLSPEC (! (TRUE U (output = oY)) | (! (output = oY) U (((input = iL) & ! (output = oY)) & X (! (output = oY) U (input = iS)))))
LTLSPEC (FALSE V (! (input = iA) | (FALSE V (! (input = iM) | ((output = oU) & X (TRUE U (output = oX)))))))
LTLSPEC (FALSE V (! (input = iA) | (FALSE V (! (input = iP) | (TRUE U (output = oV))))))
LTLSPEC ((FALSE V ! (input = iM)) | (! (input = iM) U ((input = iM) & (! (TRUE U ((output = oW) & X (TRUE U (output = oU)))) | (! (output = oW) U (input = iA))))))
LTLSPEC (FALSE V (! (output = oX) | ((! (((output = oY) & ! (input = iQ)) & X (! (input = iQ) U ((output = oU) & ! (input = iQ)))) U ((input = iQ) | (input = iB))) | (FALSE V ! ((output = oY) & X (TRUE U (output = oU)))))))
LTLSPEC ((FALSE V ! (output = oZ)) | (TRUE U ((output = oZ) & ((input = iO) V (! (output = oX) | (input = iO))))))
LTLSPEC (FALSE V (! (input = iR) | (FALSE V ((input = iK) & (! X (TRUE U (input = iM)) | X (! (input = iM) U ((input = iM) & (TRUE U (output = oU)))))))))
LTLSPEC (FALSE V (! (input = iI) | (TRUE U (output = oZ))))
LTLSPEC (FALSE V (! (input = iK) | ((! (((output = oW) & ! (output = oX)) & X (! (output = oX) U ((output = oV) & ! (output = oX)))) U ((output = oX) | (input = iR))) | (FALSE V ! ((output = oW) & X (TRUE U (output = oV)))))))
LTLSPEC (FALSE V (! (((input = iA) & ! (input = iL)) & (TRUE U (input = iL))) | ((! (input = iG) | (! (input = iL) U ((output = oW) & ! (input = iL)))) U (input = iL))))
LTLSPEC (! (TRUE U (output = oV)) | (! (((output = oX) & ! (output = oV)) & X (! (output = oV) U ((output = oU) & ! (output = oV)))) U ((output = oV) | (input = iC))))
LTLSPEC (FALSE V (! ((input = iJ) & (TRUE U (input = iA))) | ((! (input = iS) | (! (input = iA) U (((output = oY) & ! (input = iA)) & X (! (input = iA) U (output = oW))))) U (input = iA))))
LTLSPEC (! (TRUE U ((output = oV) & X (TRUE U (output = oY)))) | (! (output = oV) U (input = iP)))
LTLSPEC (! (TRUE U (input = iA)) | (((input = iG) & (! X (! (input = iA) U (input = iT)) | X (! (input = iA) U ((input = iT) & (TRUE U (output = oU)))))) U (input = iA)))
LTLSPEC (FALSE V (! ((input = iM) & (TRUE U (input = iA))) | ((! (input = iP) | (! (input = iA) U (((output = oU) & ! (input = iA)) & X (! (input = iA) U (output = oY))))) U (input = iA))))
LTLSPEC (FALSE V (! (input = iI) | (TRUE U (output = oW))))
LTLSPEC (FALSE V (! (input = iP) | (TRUE U (((output = oW) & ! (output = oZ)) & X (! (output = oZ) U (output = oY))))))
LTLSPEC (FALSE V (! ((input = iB) & (TRUE U (input = iF))) | (! (((output = oY) & ! (input = iF)) & X (! (input = iF) U ((output = oW) & ! (input = iF)))) U ((input = iF) | (output = oV)))))
LTLSPEC (FALSE V (! (input = iH) | ((! (input = iT) | (! (input = iP) U (((output = oU) & ! (input = iP)) & X (! (input = iP) U (output = oY))))) U ((input = iP) | (FALSE V (! (input = iT) | ((output = oU) & X (TRUE U (output = oY)))))))))