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