Reachability problems: =============================== error_20 reachable via input sequence [A, C, D, A, E] --------------- error_22 reachable via input sequence [A, C, C, A, D] --------------- error_23 reachable via input sequence [A, C, C, E, D] --------------- error_28 reachable via input sequence [C, D, D, E, B] --------------- error_29 reachable via input sequence [A, C, D, A, D] --------------- error_44 reachable via input sequence [A, C, C, E, B] --------------- error_51 reachable via input sequence [C, D, D, E, D] --------------- error_62 reachable via input sequence [C, D, D, E, E] --------------- error_75 reachable via input sequence [A, C, C, A, B] --------------- error_79 reachable via input sequence [A, C, D, A, B] --------------- error_81 reachable via input sequence [A, C, C, E, C] --------------- error_82 reachable via input sequence [A, C, C, E, E] --------------- All other errors unreachable LTL problems: =============================== Formula: (! (true U oV) | (! oV U ((oY & ! oV) & X (! oV U oX)))) "output Y, output X always precedes output V" Formula is not satisfied! An error path is [iC, oT, iA, oV] ([iD, oW, iA, oV, iD, oV])* --------------- Formula: (! (true U oZ) | (! oT U (oW | oZ))) "output W precedes output T before output Z" Formula is satisfied. --------------- Formula: (! (true U (oV & X (true U oS))) | (! oV U oT)) "output T always precedes output V, output S" Formula is not satisfied! An error path is [iA, oX, iC, oX, iD, oV, iA, oS] ([iA, oW, iA, oS])* --------------- Formula: (false R (! (iB & (true U iE)) | ((! iD | (! iE U ((oZ & ! iE) & X (! iE U oT)))) U iE))) "output Z, output T responds to input D between input B and input E" Formula is satisfied. --------------- Formula: (! (true U oY) | ((iE & (! X (! oY U iC) | X (! oY U (iC & (true U oV))))) U oY)) "output V responds to input E, input C before output Y" Formula is satisfied. --------------- Formula: (! (true U iC) | ((! iA | (! iC U (oX & ! iC))) U iC)) "output X responds to input A before input C" Formula is satisfied. --------------- Formula: (! (true U (oV & X (true U oX))) | (! oV U oY)) "output Y always precedes output V, output X" Formula is not satisfied! An error path is [iC, oT, iA, oV, iC, oX, iE, oT] ([iC, oT])* --------------- Formula: (false R (! ((oW & ! iE) & (true U iE)) | ((! iD | (! iE U (oZ & ! iE))) U iE))) "output Z responds to input D between output W and input E" Formula is not satisfied! An error path is [iC, oT, iA, oV, iD, oW, iA, oV, iD, oV, iC, oX, iE, oT] ([iC, oT])* --------------- Formula: ((false R ! iB) | (! iB U (iB & (! (true U oV) | (! oV U ((oX & ! oV) & X (! oV U iA))))))) "output X, input A precedes output V after input B" Formula is satisfied. --------------- Formula: (! (true U oW) | ((! iE | (! oW U (((oT & ! oW) & ! oS) & X ((! oW & ! oS) U oX)))) U oW)) "output T, output X without output S responds to input E before output W" Formula is not satisfied! An error path is [iC, oT, iD, oS, iD, oV, iE, oT, iA, oW] ([iC, oT])* --------------- Formula: (false R (! (oZ & (true U oT)) | ((! iD | (! oT U ((oV & ! oT) & X (! oT U oW)))) U oT))) "output V, output W responds to input D between output Z and output T" Formula is satisfied. --------------- Formula: (! (true U iB) | (! ((oY & ! iB) & X (! iB U (oT & ! iB))) U (iB | oS))) "output S precedes output Y, output T before input B" Formula is satisfied. --------------- Formula: (false R (oZ & (! ! oV | (! oW WU (iA | oV))))) "input A precedes output W after output Z until output V" Formula is not satisfied! An error path is [iA, oX] ([iC, oX, iC, oW, iA, oS, iA, oW])* --------------- Formula: (false R (! ((oV & ! oZ) & (true U oZ)) | ((! iA | (! oZ U (oY & ! oZ))) U oZ))) "output Y responds to input A between output V and output Z" Formula is satisfied. --------------- Formula: (false R (oV & (! ! iB | (! oT WU (iD | iB))))) "input D precedes output T after output V until input B" Formula is not satisfied! An error path is [iA, oX] ([iC, oX, iC, oW, iA, oS, iA, oW])* --------------- Formula: (false R (! iE | (false R (! iB | ((oT & ! oY) & X (! oY U oW)))))) "output T, output W without output Y responds to input B after input E" Formula is satisfied. --------------- Formula: (false R (! ((iA & ! oZ) & (true U oZ)) | ((! iC | (! oZ U (oU & ! oZ))) U oZ))) "output U responds to input C between input A and output Z" Formula is satisfied. --------------- Formula: (false R (! iB | (false R (! iC | ((oV & ! oW) & X (! oW U oS)))))) "output V, output S without output W responds to input C after input B" Formula is satisfied. --------------- Formula: (false R (! iA | (false R (! iE | (oZ & X (true U oT)))))) "output Z, output T responds to input E after input A" Formula is not satisfied! An error path is [iA, oX, iC, oX, iC, oW, iE] ([oV, iA, oV, iC, oX, iC, oW, iE])* --------------- Formula: (false R (! (iC & (true U iB)) | ((! iA | (! iB U (((oZ & ! iB) & ! oU) & X ((! iB & ! oU) U oV)))) U iB))) "output Z, output V without output U responds to input A betwen input C and input B" Formula is satisfied. --------------- Formula: (! (true U iD) | (! oS U (oU | iD))) "output U precedes output S before input D" Formula is not satisfied! An error path is [iA, oX, iC, oX, iC, oW, iA, oS, iA, oW, iC, oX, iD] ([oV, iA, oS, iC, oV, iD])* --------------- Formula: (false R (! ((iA & ! iB) & (true U iB)) | ((! iC | (! iB U (oZ & ! iB))) U iB))) "output Z responds to input C between input A and input B" Formula is satisfied. --------------- Formula: (! (true U oS) | ((! iC | (! oS U (oT & ! oS))) U oS)) "output T responds to input C before output S" Formula is not satisfied! An error path is [iA, oX, iC, oX, iC, oW, iA, oS] ([iA, oW, iC, oX, iC, oW, iA, oS])* --------------- Formula: ((false R ! oS) | (! oS U (oS & (! (true U (oW & X (true U oV))) | (! oW U oZ))))) "output Z precedes output W, output V after output S" Formula is not satisfied! An error path is [iA, oX, iC, oX, iC, oW, iA, oS, iA, oW] ([iC, oX, iD, oV, iA, oS, iC, oV, iC, oW, iA, oS, iA, oW])* --------------- Formula: (! (true U oS) | ((! iB | (! oS U (((oX & ! oS) & ! oV) & X ((! oS & ! oV) U oY)))) U oS)) "output X, output Y without output V responds to input B before output S" Formula is satisfied. --------------- Formula: (false R (! iC | (true U oY))) "output Y always responds to input C" Formula is not satisfied! An error path is [iA, oX, iC] ([oX, iC, oW, iA, oS, iA, oW, iC])* --------------- Formula: (false R (! iC | (true U ((oW & ! oS) & X (! oS U oT))))) "output W, output T without output S always responds to input C" Formula is not satisfied! An error path is [iA, oX, iC] ([oX, iC, oW, iA, oS, iA, oW, iC])* --------------- Formula: (false R (! oV | (false R (! iC | ((oX & ! oY) & X (! oY U oT)))))) "output X, output T without output Y responds to input C after output V" Formula is not satisfied! An error path is [iC, oT, iA, oV, iD, oW, iC] ([oV, iD, oV, iD, oW, iC])* --------------- Formula: (false R (! iB | (true U ((oU & ! oY) & X (! oY U oZ))))) "output U, output Z without output Y always responds to input B" Formula is satisfied. --------------- Formula: (! (true U oV) | ((! iA | (! oV U ((oX & ! oV) & X (! oV U oT)))) U oV)) "output X, output T responds to input A before output V" Formula is not satisfied! An error path is [iC, oT, iA, oV] ([iD, oW, iA, oV, iD, oV])* --------------- Formula: (false R (! ((oY & ! oT) & (true U oT)) | (! oX U (oV | oT)))) "output V precedes output X between output Y and output T" Formula is satisfied. --------------- Formula: (false R (! oY | (false R (iA & (! X (true U iC) | X (! iC U (iC & (true U oX)))))))) "output X responds to input A, input C after output Y" Formula is satisfied. --------------- Formula: (false R (! (iC & (true U oZ)) | (! oW U (oZ | ((iE & ! oW) & X (! oW U iD)))))) "input E, input D precedes output W between input C and output Z" Formula is satisfied. --------------- Formula: (! (true U oW) | (! oW U ((oU & ! oW) & X (! oW U oS)))) "output U, output S always precedes output W" Formula is not satisfied! An error path is [iA, oX, iC, oX, iC, oW] ([iA, oS, iA, oW, iC, oX, iC, oW])* --------------- Formula: ((false R ! iA) | (! iA U (iA & (! (true U oU) | (! oU U ((iC & ! oU) & X (! oU U oX))))))) "input C, output X precedes output U after input A" Formula is satisfied. --------------- Formula: (false R (! iA | (true U oZ))) "output Z always responds to input A" Formula is not satisfied! An error path is [iA, oX] ([iC, oX, iC, oW, iA, oS, iA, oW])* --------------- Formula: (! (true U oS) | (! oS U ((iE & ! oS) & X (! oS U iD)))) "input E, input D always precedes output S" Formula is not satisfied! An error path is [iC, oT, iD, oS, iD, oV] ([iC, oV, iC, oW])* --------------- Formula: ((false R ! oV) | (true U (oV & (! oU WU iC)))) "input C precedes output U after output V" Formula is satisfied. --------------- Formula: ((false R ! oT) | (true U (oT & (! oX WU iE)))) "input E precedes output X after output T" Formula is satisfied. --------------- Formula: (false R (! oX | (! (true U oV) | (! oV U (iB | ((oT & ! oV) & X (! oV U oU))))))) "output T, output U precedes output V after output X until input B" Formula is not satisfied! An error path is [iA, oX, iC, oX, iD, oV] ([iA, oS, iA, oW])* --------------- Formula: (false R (! ((oU & ! iD) & (true U iD)) | (! oT U (iA | iD)))) "input A precedes output T between output U and input D" Formula is satisfied. --------------- Formula: (! (true U iA) | (! ((oY & ! iA) & X (! iA U (oU & ! iA))) U (iA | oW))) "output W precedes output Y, output U before input A" Formula is satisfied. --------------- Formula: (false R (! ((iC & ! iE) & (true U iE)) | (! oV U (oU | iE)))) "output U precedes output V between input C and input E" Formula is not satisfied! An error path is [iC, oT, iA, oV, iC, oX, iE, oT] ([iC, oT])* --------------- Formula: (! (true U oX) | ((! iA | (! oX U (oU & ! oX))) U oX)) "output U responds to input A before output X" Formula is not satisfied! An error path is [iA, oX] ([iC, oX, iC, oW, iA, oS, iA, oW])* --------------- Formula: (! oZ WU oU) "output U always precedes output Z" Formula is satisfied. --------------- Formula: (false R (! oX | ((iE & (! X (! iB U iA) | X (! iB U (iA & (true U oV))))) U (iB | (false R (iE & (! X (! iB U iA) | X (! iB U (iA & (true U oV)))))))))) "output V responds to input E, input A after output X until input B" Formula is not satisfied! An error path is [iA, oX] ([iC, oX, iC, oW, iA, oS, iA, oW])* --------------- Formula: (! (true U iD) | (! ((oV & ! iD) & X (! iD U (oZ & ! iD))) U (iD | oY))) "output Y precedes output V, output Z before input D" Formula is satisfied. --------------- Formula: (! (true U oX) | (! oZ U (oX | ((oY & ! oZ) & X (! oZ U oV))))) "output Y, output V precedes output Z before output X" Formula is satisfied. --------------- Formula: (! (true U oT) | ((iE & (! X (! oT U iB) | X (! oT U (iB & (true U oS))))) U oT)) "output S responds to input E, input B before output T" Formula is not satisfied! An error path is [iC, oT, iA, oV] ([iD, oW, iA, oV, iD, oV])* --------------- Formula: (! (true U oV) | (! ((oY & ! oV) & X (! oV U (oZ & ! oV))) U (oV | iA))) "input A precedes output Y, output Z before output V" Formula is satisfied. --------------- Formula: (false R (! (oT & (true U oW)) | (! ((oY & ! oW) & X (! oW U (oZ & ! oW))) U (oW | oV)))) "output V precedes output Y, output Z between output T and output W" Formula is satisfied. --------------- Formula: (false R (! (iD & (true U iA)) | ((! iC | (! iA U ((oV & ! iA) & X (! iA U oX)))) U iA))) "output V, output X responds to input C between input D and input A" Formula is not satisfied! An error path is [iC, oT, iA, oV, iD, oW, iC, oV, iD, oV, iD, oW, iA] ([oV, iD, oV, iD, oW, iA])* --------------- Formula: (false R (! oY | (false R (iB & (! X (true U iA) | X (! iA U (iA & (true U oX)))))))) "output X responds to input B, input A after output Y" Formula is satisfied. --------------- Formula: (false R (! (oZ & (true U oU)) | ((! iA | (! oU U ((oS & ! oU) & X (! oU U oT)))) U oU))) "output S, output T responds to input A between output Z and output U" Formula is satisfied. --------------- Formula: (false R (! ((oS & ! oV) & (true U oV)) | ((! iD | (! oV U (oX & ! oV))) U oV))) "output X responds to input D between output S and output V" Formula is not satisfied! An error path is [iC, oT, iD, oS, iD, oV] ([iC, oV, iC, oW])* --------------- Formula: (! (true U oV) | (! oX U (iA | oV))) "input A precedes output X before output V" Formula is satisfied. --------------- Formula: (false R (! (oY & (true U iA)) | (! oZ U (iA | ((oU & ! oZ) & X (! oZ U oW)))))) "output U, output W precedes output Z between output Y and input A" Formula is satisfied. --------------- Formula: (! (true U oS) | (! oU U (oW | oS))) "output W precedes output U before output S" Formula is satisfied. --------------- Formula: (false R (! iA | (true U oX))) "output X always responds to input A" Formula is not satisfied! An error path is [iC, oT, iA, oV] ([iD, oW, iA, oV, iD, oV])* --------------- Formula: (false R (! iA | (true U ((oW & ! oX) & X (! oX U oS))))) "output W, output S without output X always responds to input A" Formula is not satisfied! An error path is [iA, oX] ([iC, oX, iC, oW, iE, oV, iA, oV])* --------------- Formula: (! (true U (oU & X (true U oT))) | (! oU U iA)) "input A always precedes output U, output T" Formula is satisfied. --------------- Formula: (! (true U oS) | ((iB & (! X (! oS U iC) | X (! oS U (iC & (true U oZ))))) U oS)) "output Z responds to input B, input C before output S" Formula is not satisfied! An error path is [iC, oT, iD, oS, iD, oV] ([iC, oV, iC, oW])* --------------- Formula: (! (true U oX) | ((! iB | (! oX U ((oV & ! oX) & X (! oX U oU)))) U oX)) "output V, output U responds to input B before output X" Formula is satisfied. --------------- Formula: (! (true U iB) | (! oU U (oV | iB))) "output V precedes output U before input B" Formula is satisfied. --------------- Formula: (false R (! oS | (false R (! iC | ((oX & ! oT) & X (! oT U oU)))))) "output X, output U without output T responds to input C after output S" Formula is not satisfied! An error path is [iC, oT, iD, oS, iD, oV, iC] ([oV, iC, oW, iC])* --------------- Formula: (! (true U iC) | ((iB & (! X (! iC U iA) | X (! iC U (iA & (true U oX))))) U iC)) "output X responds to input B, input A before input C" Formula is not satisfied! An error path is [iA, oX, iC] ([oX, iC, oW, iA, oS, iA, oW, iC])* --------------- Formula: (! (true U iA) | ((iB & (! X (! iA U iC) | X (! iA U (iC & (true U oV))))) U iA)) "output V responds to input B, input C before input A" Formula is not satisfied! An error path is [iC, oT, iA, oV] ([iD, oW, iA, oV, iD, oV])* --------------- Formula: (! (true U oU) | (! oT U (iD | oU))) "input D precedes output T before output U" Formula is satisfied. --------------- Formula: (false R (! iC | (false R (! iA | ((oU & ! oY) & X (! oY U oV)))))) "output U, output V without output Y responds to input A after input C" Formula is not satisfied! An error path is [iC, oT, iA, oV] ([iD, oW, iA, oV, iD, oV])* --------------- Formula: (! (true U oX) | ((! iB | (! oX U ((oW & ! oX) & X (! oX U oZ)))) U oX)) "output W, output Z responds to input B before output X" Formula is satisfied. --------------- Formula: (false R (! iD | (false R (! iE | ((oV & ! oX) & X (! oX U oW)))))) "output V, output W without output X responds to input E after input D" Formula is not satisfied! An error path is [iC, oT, iD, oS, iD, oV, iE, oT, iA, oW] ([iC, oT])* --------------- Formula: (false R (! oV | ((! ((oS & ! oU) & X (! oU U (oX & ! oU))) U (oU | oZ)) | (false R ! (oS & X (true U oX)))))) "output Z precedes output S, output X after output V until output U" Formula is not satisfied! An error path is [iA, oX, iC, oX, iD, oV, iA, oS, iC, oV, iC, oW, iA, oS, iC, oX] ([iA, oW, iC, oX, iC, oW, iA, oS])* --------------- Formula: (! (true U oU) | (! oU U ((oW & ! oU) & X (! oU U oV)))) "output W, output V always precedes output U" Formula is satisfied. --------------- Formula: (! (true U oS) | ((! iD | (! oS U ((oZ & ! oS) & X (! oS U oW)))) U oS)) "output Z, output W responds to input D before output S" Formula is not satisfied! An error path is [iC, oT, iD, oS, iD, oV] ([iC, oV, iC, oW])* --------------- Formula: (false R (! iE | (true U (oS & X (true U oU))))) "output S, output U always responds to input E" Formula is not satisfied! An error path is [iA, oX, iC, oX, iC, oW, iE] ([oV, iA, oV, iC, oX, iC, oW, iE])* --------------- Formula: (false R (! (oU & (true U oX)) | ((! iE | (! oX U ((oY & ! oX) & X (! oX U oZ)))) U oX))) "output Y, output Z responds to input E between output U and output X" Formula is satisfied. --------------- Formula: (false R (! ((iB & ! iD) & (true U iD)) | ((! iE | (! iD U (oS & ! iD))) U iD))) "output S responds to input E between input B and input D" Formula is satisfied. --------------- Formula: (! (true U iE) | ((iC & (! X (! iE U iB) | X (! iE U (iB & (true U oT))))) U iE)) "output T responds to input C, input B before input E" Formula is not satisfied! An error path is [iA, oX, iC, oX, iC, oW, iE] ([oV, iA, oV, iC, oX, iC, oW, iE])* --------------- Formula: (false R (! ((iA & ! oY) & (true U oY)) | ((! iB | (! oY U (oZ & ! oY))) U oY))) "output Z responds to input B between input A and output Y" Formula is satisfied. --------------- Formula: (! oX WU iD) "input D always precedes output X" Formula is not satisfied! An error path is [iA, oX] ([iC, oX, iC, oW, iA, oS, iA, oW])* --------------- Formula: (false R (! (iC & (true U oU)) | ((! iE | (! oU U (((oT & ! oU) & ! oZ) & X ((! oU & ! oZ) U oW)))) U oU))) "output T, output W without output Z responds to input E betwen input C and output U" Formula is satisfied. --------------- Formula: (! (true U oV) | ((! iD | (! oV U ((oZ & ! oV) & X (! oV U oT)))) U oV)) "output Z, output T responds to input D before output V" Formula is not satisfied! An error path is [iA, oX, iC, oX, iD, oV] ([iA, oS, iA, oW])* --------------- Formula: (false R (! oU | (false R (iB & (! X (true U iE) | X (! iE U (iE & (true U oZ)))))))) "output Z responds to input B, input E after output U" Formula is satisfied. --------------- Formula: (! (true U iE) | (! ((oV & ! iE) & X (! iE U (oZ & ! iE))) U (iE | oW))) "output W precedes output V, output Z before input E" Formula is satisfied. --------------- Formula: (! (true U iB) | (! ((oS & ! iB) & X (! iB U (oV & ! iB))) U (iB | iD))) "input D precedes output S, output V before input B" Formula is satisfied. --------------- Formula: (false R (! ((oX & ! oT) & (true U oT)) | ((! iB | (! oT U (oV & ! oT))) U oT))) "output V responds to input B between output X and output T" Formula is satisfied. --------------- Formula: (! (true U oW) | (! oW U ((oV & ! oW) & X (! oW U oY)))) "output V, output Y always precedes output W" Formula is not satisfied! An error path is [iA, oX, iC, oX, iC, oW] ([iA, oS, iA, oW, iC, oX, iC, oW])* --------------- Formula: ((false R ! oV) | (! oV U (oV & (! (true U oS) | (! oS U ((iC & ! oS) & X (! oS U oT))))))) "input C, output T precedes output S after output V" Formula is not satisfied! An error path is [iA, oX, iC, oX, iD, oV, iA, oS] ([iA, oW, iA, oS])* --------------- Formula: (! (true U (oZ & X (true U oY))) | (! oZ U oU)) "output U always precedes output Z, output Y" Formula is satisfied. --------------- Formula: (false R (iC & (! X (true U iD) | X (true U (iD & (true U oW)))))) "output W always responds to input C, input D" Formula is not satisfied! An error path is [iA, oX] ([iC, oX, iC, oW, iA, oS, iA, oW])* --------------- Formula: ((false R ! iA) | (! iA U (iA & (! (true U (oX & X (true U oS))) | (! oX U oT))))) "output T precedes output X, output S after input A" Formula is not satisfied! An error path is [iA, oX, iC, oX] ([iC, oW, iA, oS, iA, oW, iC, oX])* --------------- Formula: (false R (! oS | ((! ((oU & ! oV) & X (! oV U (oW & ! oV))) U (oV | oY)) | (false R ! (oU & X (true U oW)))))) "output Y precedes output U, output W after output S until output V" Formula is satisfied. --------------- Formula: (false R (! (oW & (true U oY)) | (! oZ U (oY | ((oT & ! oZ) & X (! oZ U oV)))))) "output T, output V precedes output Z between output W and output Y" Formula is satisfied. --------------- Formula: (! (true U (oT & X (true U oV))) | (! oT U oU)) "output U always precedes output T, output V" Formula is not satisfied! An error path is [iC, oT, iA, oV] ([iD, oW, iA, oV, iD, oV])* --------------- Formula: (false R (! oT | ((iC & (! X (! oS U iA) | X (! oS U (iA & (true U oU))))) U (oS | (false R (iC & (! X (! oS U iA) | X (! oS U (iA & (true U oU)))))))))) "output U responds to input C, input A after output T until output S" Formula is not satisfied! An error path is [iC, oT, iA, oV] ([iD, oW, iA, oV, iD, oV])* --------------- Formula: (! (true U iD) | (! oX U (oS | iD))) "output S precedes output X before input D" Formula is not satisfied! An error path is [iA, oX, iC, oX, iD] ([oV, iA, oS, iC, oV, iD])* --------------- Formula: (! (true U oT) | (! oY U (iB | oT))) "input B precedes output Y before output T" Formula is satisfied. --------------- Formula: (false R (iC & (! ! oT | (! oV WU (oU | oT))))) "output U precedes output V after input C until output T" Formula is not satisfied! An error path is [iA, oX] ([iC, oX, iC, oW, iA, oS, iA, oW])* --------------- Formula: (false R (! iA | ((! iC | (! oV U ((oY & ! oV) & X (! oV U oX)))) U (oV | (false R (! iC | (oY & X (true U oX)))))))) "output Y, output X responds to input C after input A until output V" Formula is not satisfied! An error path is [iA, oX, iC] ([oX, iC, oW, iA, oS, iA, oW, iC])* --------------- Formula: (false R (! (oW & (true U iE)) | ((! iA | (! iE U (((oT & ! iE) & ! oS) & X ((! iE & ! oS) U oZ)))) U iE))) "output T, output Z without output S responds to input A betwen output W and input E" Formula is not satisfied! An error path is [iA, oX, iC, oX, iC, oW, iA, oS, iE, oV] ([iC, oT])* --------------- 51 constraints satisfied, 49 unsatisfied.