Problem1-LTL.smv 15.8 KB
 Joshua Moerman committed Aug 31, 2016 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 = 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)))))))``````