Reachability problems: =============================== error_20 reachable via input sequence [B, A, F, A, A] --------------- error_45 reachable via input sequence [B, A, F, F, A] --------------- error_27 reachable via input sequence [B, A, F, C, A] --------------- error_42 reachable via input sequence [B, A, F, D, A] --------------- error_59 reachable via input sequence [B, A, F, B, A] --------------- error_15 reachable via input sequence [E, B, A, A, A] --------------- error_2 reachable via input sequence [E, B, A, F, A] --------------- error_8 reachable via input sequence [E, B, A, C, A] --------------- error_30 reachable via input sequence [E, B, A, D, A] --------------- error_52 reachable via input sequence [E, B, A, B, A] --------------- error_0 reachable via input sequence [B, A, F, E, A, A] --------------- error_54 reachable via input sequence [B, A, F, E, F, A] --------------- error_41 reachable via input sequence [B, A, F, E, C, A] --------------- error_6 reachable via input sequence [B, A, F, E, D, A] --------------- error_57 reachable via input sequence [E, B, A, E, A, A] --------------- error_46 reachable via input sequence [E, B, A, E, C, A] --------------- error_19 reachable via input sequence [E, B, A, E, E, A] --------------- error_47 reachable via input sequence [E, B, A, E, D, A] --------------- error_17 reachable via input sequence [E, B, A, E, B, A] --------------- error_28 reachable via input sequence [B, A, F, E, E, C, A] --------------- error_1 reachable via input sequence [B, A, F, E, B, A, A] --------------- error_51 reachable via input sequence [B, A, F, E, B, C, A] --------------- error_35 reachable via input sequence [B, A, F, E, B, E, A] --------------- error_31 reachable via input sequence [B, A, F, E, B, B, A] --------------- error_43 reachable via input sequence [E, B, A, E, F, C, A] --------------- error_12 reachable via input sequence [E, B, A, E, F, B, A] --------------- error_36 reachable via input sequence [B, A, F, E, B, F, C, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (false R (! iE | (false R ! oU))) "output U does never occur after input E" Formula is satisfied. --------------- Formula: (false R (! (iF & ! iA) | (! iA U (oW & ! iA)))) "output W occurs after input F until input A" Formula is not satisfied! An error path is [iD, oV, iF] ([oY, iF])* --------------- Formula: (! (true U oZ) | (! oW U (iD | oZ))) "input D precedes output W before output Z" Formula is satisfied. --------------- Formula: (! (true U oX) | ((! oW & ! oX) U (oX | ((oW & ! oX) U (oX | ((! oW & ! oX) U (oX | ((oW & ! oX) U (oX | (! oW U oX)))))))))) "output W occurs at most twice before output X" Formula is not satisfied! An error path is [iC, oV, iC, oW, iC, oW, iC, oW, iA, iD, oX] ([iA])* --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: (! oZ WU oU) "output Z does never occur before output U" Formula is not satisfied! An error path is [iC, oV, iD, oZ] ([iA, oV])* --------------- Formula: (! oZ WU iD) "input D precedes output Z" Formula is not satisfied! An error path is [iB, oY, iA, oX, iF, oV, iE, oZ, iB, oX] ([iF, oV, iA, oX])* --------------- Formula: (! oX WU oW) "output W precedes output X" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: (false R (! ((iF & ! iE) & (true U iE)) | (! oW U iE))) "output W does never occur between input F and input E" Formula is satisfied. --------------- Formula: (false R (! oV | (false R ! oZ))) "output Z does never occur after output V" Formula is not satisfied! An error path is [iC, oV, iD, oZ] ([iA, oV])* --------------- Formula: (! (true U oZ) | (! oX U (oW | oZ))) "output W precedes output X before output Z" Formula is not satisfied! An error path is [iF, oX, iF, oX, iD, iD, iD, oZ] ([iA, oV])* --------------- Formula: (! oY WU oX) "output X precedes output Y" Formula is not satisfied! An error path is [iD, oV, iD, oY] ([iC, oX])* --------------- Formula: (! (true U oY) | (! oW U (iB | oY))) "input B precedes output W before output Y" Formula is not satisfied! An error path is [iC, oV, iC, oW, iD, oY] ([iC, oX])* --------------- Formula: (! oU WU oZ) "output U does never occur before output Z" Formula is satisfied. --------------- Formula: (false R (! (iA & ! iC) | (! iC WU (oV & ! iC)))) "output V occurs between input A and input C" Formula is satisfied. --------------- Formula: (! iE WU (oW & ! iE)) "output W occurs before input E" Formula is not satisfied! An error path is [iB, oY, iA, oX, iF, oV, iE, oZ, iE, oX] ([iA])* --------------- Formula: (false R (! (iE & ! oV) | (! oW WU oV))) "output W does never occur after input E until output V" Formula is satisfied. --------------- Formula: (! iA WU (oZ & ! iA)) "output Z occurs before input A" Formula is not satisfied! An error path is [iC, oV, iA, oX] ([iA])* --------------- Formula: (false R (! (iB & ! oV) | (! oV U (oW & ! oV)))) "output W occurs after input B until output V" Formula is not satisfied! An error path is [iB, oY, iA, oX, iF, oV, iE, oZ, iB, oX] ([iF, oV, iA, oX])* --------------- Formula: (! oY WU iA) "output Y does never occur before input A" Formula is not satisfied! An error path is [iD, oV, iD, oY] ([iC, oX])* --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: (false R (! (iD & ! iB) | (! iB U (oU & ! iB)))) "output U occurs after input D until input B" Formula is not satisfied! An error path is [iD, oV] ([iC, oX])* --------------- Formula: (false R (! (oZ & ! iA) | (! iA U (oW & ! iA)))) "output W occurs after output Z until input A" Formula is not satisfied! An error path is [iC, oV, iD, oZ] ([iA, oV])* --------------- Formula: (false R (! (iC & ! oW) | (! oV WU oW))) "output V does never occur after input C until output W" Formula is not satisfied! An error path is [iC, oV] ([iD, oZ, iD])* --------------- Formula: (! (true U oW) | ((! oZ & ! oW) U (oW | ((oZ & ! oW) U (oW | ((! oZ & ! oW) U (oW | ((oZ & ! oW) U (oW | (! oZ U oW)))))))))) "output Z occurs at most twice before output W" Formula is not satisfied! An error path is [iC, oV, iD, oZ, iD, iD, oZ, iD, iD, oZ, iD, iC, oW] ([iC, oW])* --------------- Formula: (false R (! (oV & ! iF) | (! oW WU iF))) "output W does never occur after output V until input F" Formula is not satisfied! An error path is [iC, oV, iC, oW] ([iC, oW])* --------------- Formula: (! oZ WU oW) "output W precedes output Z" Formula is not satisfied! An error path is [iC, oV, iD, oZ] ([iA, oV])* --------------- Formula: (false R (! iA | (true U oX))) "output X responds to input A" Formula is not satisfied! An error path is [iC, oV, iA, oX, iA] ([iA])* --------------- Formula: (false R (! iB | (true U oZ))) "output Z responds to input B" Formula is not satisfied! An error path is [iB, oY, iA, oX, iF, oV, iE, oZ, iB, oX] ([iF, oV, iA, oX])* --------------- Formula: (false R (! oY | (true U oZ))) "output Z responds to output Y" Formula is not satisfied! An error path is [iD, oV, iD, oY] ([iC, oX])* --------------- Formula: (! (true U oY) | ((! oU & ! oY) U (oY | ((oU & ! oY) U (oY | ((! oU & ! oY) U (oY | ((oU & ! oY) U (oY | (! oU U oY)))))))))) "output U occurs at most twice before output Y" Formula is satisfied. --------------- Formula: ((false R ! iF) | (true U (iF & (true U oU)))) "output U occurs after input F" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: (! iB WU (oV & ! iB)) "output V occurs before input B" Formula is not satisfied! An error path is [iB, oY, iA, oX, iF, oV, iE, oZ, iB, oX] ([iF, oV, iA, oX])* --------------- Formula: (false R (! iF | (false R ! oX))) "output X does never occur after input F" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: (! (true U oY) | (! oZ U (iB | oY))) "input B precedes output Z before output Y" Formula is not satisfied! An error path is [iC, oV, iD, oZ, iC, oY] ([iC, oX])* --------------- Formula: (false R (! ((oX & ! oV) & (true U oV)) | (! oW U oV))) "output W does never occur between output X and output V" Formula is not satisfied! An error path is [iF, oX, iD, oW, iD, oX, iF, oX, iD, iA, oV] ([iA, oV])* --------------- Formula: (false R (! (iE & ! oZ) | (! oV WU oZ))) "output V does never occur after input E until output Z" Formula is not satisfied! An error path is [iE, oY, iB, oV, iA, oX, iE, oZ, iF, oV] ([iA, oV])* --------------- Formula: (false R (! (iA & ! oU) | (! oU U (oV & ! oU)))) "output V occurs after input A until output U" Formula is not satisfied! An error path is [iC, oV, iA, oX] ([iA])* --------------- Formula: (! (true U oZ) | (! oX U (iB | oZ))) "input B precedes output X before output Z" Formula is not satisfied! An error path is [iF, oX, iF, oX, iD, iD, iD, oZ] ([iA, oV])* --------------- Formula: ((false R ! iD) | (true U (iD & (true U oV)))) "output V occurs after input D" Formula is not satisfied! An error path is [iC, oV, iD] ([oZ, iD, iD])* --------------- Formula: (false R (! (iF & ! iD) | (! iD WU (oW & ! iD)))) "output W occurs between input F and input D" Formula is not satisfied! An error path is [iF, oX, iD] ([oW, iD, oX, iD])* --------------- Formula: ((false R ! iB) | (true U (iB & (true U oY)))) "output Y occurs after input B" Formula is not satisfied! An error path is [iE, oY, iB, oV, iA, oX, iE, oZ, iF, oV] ([iA, oV])* --------------- Formula: (false R (! (oW & ! iB) | (! iB U (oU & ! iB)))) "output U occurs after output W until input B" Formula is not satisfied! An error path is [iC, oV, iC, oW] ([iC, oW])* --------------- Formula: (! oW WU (oX & ! oW)) "output X occurs before output W" Formula is not satisfied! An error path is [iC, oV, iC, oW] ([iC, oW])* --------------- Formula: (false R (! (oY & ! iF) | (! iF U (oU & ! iF)))) "output U occurs after output Y until input F" Formula is not satisfied! An error path is [iD, oV, iD, oY] ([iC, oX])* --------------- Formula: (false R (! (iB & ! iC) | (! iC U (oX & ! iC)))) "output X occurs after input B until input C" Formula is satisfied. --------------- Formula: (false R (! (oV & ! oY) | (! oY WU (oU & ! oY)))) "output U occurs between output V and output Y" Formula is not satisfied! An error path is [iD, oV, iD, oY] ([iC, oX])* --------------- Formula: (! oY WU (oW & ! oY)) "output W occurs before output Y" Formula is not satisfied! An error path is [iD, oV, iD, oY] ([iC, oX])* --------------- Formula: (false R (! iE | (false R ! oV))) "output V does never occur after input E" Formula is not satisfied! An error path is [iE, oY, iB, oV, iA, oX, iE, oZ, iF, oV] ([iA, oV])* --------------- Formula: (false R (! iB | (false R ! oU))) "output U does never occur after input B" Formula is satisfied. --------------- Formula: (! iC WU (oW & ! iC)) "output W occurs before input C" Formula is not satisfied! An error path is [iC, oV] ([iD, oZ, iD])* --------------- Formula: (false R (! (oW & ! oY) | (! oV WU oY))) "output V does never occur after output W until output Y" Formula is not satisfied! An error path is [iF, oX, iD, oW, iD, oX, iF, oX, iD, iA, oV] ([iA, oV])* --------------- Formula: (! oX WU iB) "input B precedes output X" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: ((false R ! iE) | (true U (iE & (true U oZ)))) "output Z occurs after input E" Formula is satisfied. --------------- Formula: (false R (! iC | (true U oV))) "output V responds to input C" Formula is not satisfied! An error path is [iD, oV, iC] ([oX, iC])* --------------- Formula: (false R (! oW | (true U oY))) "output Y responds to output W" Formula is not satisfied! An error path is [iC, oV, iC, oW] ([iC, oW])* --------------- Formula: (false R (! (iF & ! iB) | (! iB WU (oW & ! iB)))) "output W occurs between input F and input B" Formula is not satisfied! An error path is [iB, oY, iA, oX, iF, oV, iE, oZ, iB, oX] ([iF, oV, iA, oX])* --------------- Formula: (! (true U oX) | ((! oZ & ! oX) U (oX | ((oZ & ! oX) U (oX | ((! oZ & ! oX) U (oX | ((oZ & ! oX) U (oX | (! oZ U oX)))))))))) "output Z occurs at most twice before output X" Formula is not satisfied! An error path is [iC, oV, iD, oZ, iD, iD, oZ, iD, iD, oZ, iF, oX] ([iC, oX])* --------------- Formula: (! oY WU iE) "input E precedes output Y" Formula is not satisfied! An error path is [iD, oV, iD, oY] ([iC, oX])* --------------- Formula: (false R (! ((oZ & ! iF) & (true U iF)) | (! oX U iF))) "output X does never occur between output Z and input F" Formula is not satisfied! An error path is [iC, oV, iD, oZ, iD, iA, oX, iF] ([oX, iF])* --------------- Formula: (false R (! iA | (false R ! oU))) "output U does never occur after input A" Formula is satisfied. --------------- Formula: (! oW WU (oY & ! oW)) "output Y occurs before output W" Formula is not satisfied! An error path is [iC, oV, iC, oW] ([iC, oW])* --------------- Formula: (false R (! iC | (false R ! oZ))) "output Z does never occur after input C" Formula is not satisfied! An error path is [iC, oV, iD, oZ] ([iA, oV])* --------------- Formula: (! oV WU iA) "output V does never occur before input A" Formula is not satisfied! An error path is [iC, oV] ([iD, oZ, iD])* --------------- Formula: ((false R ! iF) | (true U (iF & (true U oZ)))) "output Z occurs after input F" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: (true U oY) "output Y occurs eventually" Formula is not satisfied! An error path is [iC, oV] ([iD, oZ, iD])* --------------- Formula: (false R (! (iC & ! oU) | (! oZ WU oU))) "output Z does never occur after input C until output U" Formula is not satisfied! An error path is [iC, oV, iD, oZ] ([iA, oV])* --------------- Formula: (! iF WU (oV & ! iF)) "output V occurs before input F" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: (! oV WU (oV WU (! oV WU (oV WU (false R ! oV))))) "output V occurs at most twice" Formula is not satisfied! An error path is [iC, oV, iD] ([oZ, iA, oV, iD, iD])* --------------- Formula: (! oY WU (oY WU (! oY WU (oY WU (false R ! oY))))) "output Y occurs at most twice" Formula is not satisfied! An error path is [iD, oV, iD, oY, iC] ([oX, iD, oY, iC])* --------------- Formula: (! oU WU (oU WU (! oU WU (oU WU (false R ! oU))))) "output U occurs at most twice" Formula is satisfied. --------------- Formula: (true U oY) "output Y occurs eventually" Formula is not satisfied! An error path is [iC, oV] ([iD, oZ, iD])* --------------- Formula: (! oY WU (oY WU (! oY WU (oY WU (false R ! oY))))) "output Y occurs at most twice" Formula is not satisfied! An error path is [iD, oV, iD, oY, iC] ([oX, iD, oY, iC])* --------------- Formula: ((false R ! iF) | (true U (iF & (true U oY)))) "output Y occurs after input F" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: (false R (! (oY & ! iC) | (! oV WU iC))) "output V does never occur after output Y until input C" Formula is not satisfied! An error path is [iB, oY, iA, oX, iF, oV, iE, oZ, iB, oX] ([iF, oV, iA, oX])* --------------- Formula: (false R (! ((iA & ! iE) & (true U iE)) | (! oZ U iE))) "output Z does never occur between input A and input E" Formula is satisfied. --------------- Formula: (! (true U iE) | ((! oY & ! iE) U (iE | ((oY & ! iE) U (iE | ((! oY & ! iE) U (iE | ((oY & ! iE) U (iE | (! oY U iE)))))))))) "output Y occurs at most twice before input E" Formula is satisfied. --------------- Formula: (false R (! iC | (false R ! oZ))) "output Z does never occur after input C" Formula is not satisfied! An error path is [iC, oV, iD, oZ] ([iA, oV])* --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iD, oV] ([iC, oX])* --------------- Formula: ((false R ! oU) | (true U (oU & (true U oW)))) "output W occurs after output U" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iF) | (! iF U (oZ & ! iF)))) "output Z occurs after input B until input F" Formula is not satisfied! An error path is [iB, oY, iA, oX, iF, oV, iE, oZ, iB, oX] ([iF, oV, iA, oX])* --------------- Formula: (false R (! (iD & ! oU) | (! oV WU oU))) "output V does never occur after input D until output U" Formula is not satisfied! An error path is [iD, oV] ([iC, oX])* --------------- Formula: (false R (! ((oU & ! oW) & (true U oW)) | (! oZ U oW))) "output Z does never occur between output U and output W" Formula is satisfied. --------------- Formula: (! (true U oW) | ((! oU & ! oW) U (oW | ((oU & ! oW) U (oW | ((! oU & ! oW) U (oW | ((oU & ! oW) U (oW | (! oU U oW)))))))))) "output U occurs at most twice before output W" Formula is satisfied. --------------- Formula: (false R (! ((iC & ! oV) & (true U oV)) | (! oZ U oV))) "output Z does never occur between input C and output V" Formula is satisfied. --------------- Formula: (false R (! oV | (true U oX))) "output X responds to output V" Formula is not satisfied! An error path is [iC, oV] ([iD, oZ, iD])* --------------- Formula: (false R (! (oY & ! oU) | (! oX WU oU))) "output X does never occur after output Y until output U" Formula is not satisfied! An error path is [iD, oV, iD, oY, iC, oX] ([iC, oX])* --------------- Formula: (! (true U oV) | (! oZ U (oY | oV))) "output Y precedes output Z before output V" Formula is not satisfied! An error path is [iF, oX, iF, oX, iD, iD, iD, oZ, iA, oV] ([iA, oV])* --------------- Formula: (! oZ WU iB) "output Z does never occur before input B" Formula is not satisfied! An error path is [iC, oV, iD, oZ] ([iA, oV])* --------------- Formula: (! oW WU oX) "output W does never occur before output X" Formula is not satisfied! An error path is [iC, oV, iC, oW] ([iC, oW])* --------------- Formula: (! oZ WU oY) "output Z does never occur before output Y" Formula is not satisfied! An error path is [iC, oV, iD, oZ] ([iA, oV])* --------------- Formula: (! (true U iE) | ((! oW & ! iE) U (iE | ((oW & ! iE) U (iE | ((! oW & ! iE) U (iE | ((oW & ! iE) U (iE | (! oW U iE)))))))))) "output W occurs at most twice before input E" Formula is satisfied. --------------- Formula: (! oX WU iC) "output X does never occur before input C" Formula is not satisfied! An error path is [iF, oX] ([iD, oW, iD, oX])* --------------- Formula: (! oV WU (oV WU (! oV WU (oV WU (false R ! oV))))) "output V occurs at most twice" Formula is not satisfied! An error path is [iC, oV, iD] ([oZ, iA, oV, iD, iD])* --------------- Formula: (false R (! iB | (false R ! oW))) "output W does never occur after input B" Formula is satisfied. --------------- Formula: (! oU WU oY) "output U does never occur before output Y" Formula is satisfied. --------------- Formula: (false R (! (iD & ! iC) | (! oU WU iC))) "output U does never occur after input D until input C" Formula is satisfied. --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iC, oV] ([iD, oZ, iD])* --------------- Formula: (false R (! (iE & ! oX) | (! oU WU oX))) "output U does never occur after input E until output X" Formula is satisfied. --------------- Formula: (false R (! (oU & ! iD) | (! iD WU (oX & ! iD)))) "output X occurs between output U and input D" Formula is satisfied. --------------- 24 constraints satisfied, 76 unsatisfied.