Reachability problems: =============================== error_0 reachable via input sequence [D, E, F, A] --------------- error_1 reachable via input sequence [D, D, F, A] --------------- error_2 reachable via input sequence [D, B, F, A] --------------- error_3 reachable via input sequence [D, C, F, A] --------------- error_4 reachable via input sequence [C, E, F, A] --------------- error_5 reachable via input sequence [C, D, E, A] --------------- error_6 reachable via input sequence [C, D, F, A] --------------- error_7 reachable via input sequence [C, B, F, A] --------------- error_8 reachable via input sequence [C, C, C, A] --------------- error_9 reachable via input sequence [C, C, F, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (! oV WU iA) "input A precedes output V" Formula is satisfied. --------------- Formula: (false R (! (iE & ! iF) | (! iF WU (oY & ! iF)))) "output Y occurs between input E and input F" Formula is satisfied. --------------- Formula: (false R (! (oV & ! oW) | (! oW U (oU & ! oW)))) "output U occurs after output V until output W" Formula is satisfied. --------------- Formula: (false R (! iF | (false R ! oV))) "output V does never occur after input F" Formula is satisfied. --------------- Formula: (! (true U iF) | ((! oX & ! iF) U (iF | ((oX & ! iF) U (iF | ((! oX & ! iF) U (iF | ((oX & ! iF) U (iF | (! oX U iF)))))))))) "output X occurs at most twice before input F" Formula is satisfied. --------------- Formula: (! (true U oV) | ((! oX & ! oV) U (oV | ((oX & ! oV) U (oV | ((! oX & ! oV) U (oV | ((oX & ! oV) U (oV | (! oX U oV)))))))))) "output X occurs at most twice before output V" Formula is satisfied. --------------- Formula: (! oY WU (oV & ! oY)) "output V occurs before output Y" Formula is not satisfied! An error path is [iA, oW, iC, oY] ([iA, oW, iC, oY])* --------------- Formula: (false R (! (iD & ! iA) | (! iA WU (oX & ! iA)))) "output X occurs between input D and input A" Formula is not satisfied! An error path is [iA, oW, iD, oZ, iA] ([oZ, iA])* --------------- Formula: (! oV WU (oY & ! oV)) "output Y occurs before output V" Formula is satisfied. --------------- Formula: (false R (! ((oU & ! iF) & (true U iF)) | (! oZ U iF))) "output Z does never occur between output U and input F" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iD) | (! iD U (oY & ! iD)))) "output Y occurs after input B until input D" Formula is not satisfied! An error path is [iA, oW, iB] ([oU, iA, oW, iB])* --------------- Formula: (! (true U oW) | (! oZ U (iF | oW))) "input F precedes output Z before output W" Formula is not satisfied! An error path is [iD, oZ, iE, oX, iD, oW] ([iA, iB, iC, oZ])* --------------- Formula: (false R (! oU | (true U oZ))) "output Z responds to output U" Formula is not satisfied! An error path is [iC, oU] ([iD, oU, iC, iB])* --------------- Formula: (! oU WU oW) "output U does never occur before output W" Formula is not satisfied! An error path is [iC, oU] ([iA, oZ, iB])* --------------- Formula: (false R ! oV) "output V does never occur" Formula is satisfied. --------------- Formula: (false R (! (iD & ! oW) | (! oW WU (oZ & ! oW)))) "output Z occurs between input D and output W" Formula is not satisfied! An error path is [iA, oW, iE, oX, iD, oW] ([iA, oZ, iB])* --------------- Formula: ((false R ! oZ) | (true U (oZ & (true U oX)))) "output X occurs after output Z" Formula is not satisfied! An error path is [iD, oZ] ([iB, oU, iA, oZ])* --------------- Formula: (! oX WU (oY & ! oX)) "output Y occurs before output X" Formula is not satisfied! An error path is [iA, oW, iE, oX] ([iC, iC, oW, iE, oX])* --------------- Formula: (false R (! (oX & ! iC) | (! oV WU iC))) "output V does never occur after output X until input C" Formula is satisfied. --------------- Formula: (false R (! oV | (true U oX))) "output X responds to output V" Formula is satisfied. --------------- Formula: (false R (! iB | (false R ! oZ))) "output Z does never occur after input B" Formula is not satisfied! An error path is [iD, oZ, iB, oU, iB, oZ] ([iB, oU, iA, oZ])* --------------- Formula: (! (true U iB) | (! oU U (iE | iB))) "input E precedes output U before input B" Formula is not satisfied! An error path is [iC, oU, iB] ([oY, iA, iC, oZ, iE, oX, iB, oZ, iB, iB])* --------------- Formula: (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) "output X occurs at most twice" Formula is not satisfied! An error path is [iA, oW, iE, oX, iC] ([iA, oZ, iC, oW, iE, oX, iC])* --------------- Formula: (false R (! ((oW & ! oU) & (true U oU)) | (! oV U oU))) "output V does never occur between output W and output U" Formula is satisfied. --------------- Formula: (false R (! ((iB & ! iC) & (true U iC)) | (! oU U iC))) "output U does never occur between input B and input C" Formula is not satisfied! An error path is [iD, oZ, iB, oU, iC] ([oZ, iB, oU, iC])* --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iA, oW] ([iB, oU, iA, oW])* --------------- Formula: (false R ! oU) "output U does never occur" Formula is not satisfied! An error path is [iC, oU] ([iA, oZ, iB])* --------------- Formula: (false R (! (oW & ! iE) | (! iE U (oY & ! iE)))) "output Y occurs after output W until input E" Formula is not satisfied! An error path is [iA, oW] ([iA, oZ, iB])* --------------- Formula: (false R (! iC | (true U oW))) "output W responds to input C" Formula is not satisfied! An error path is [iC, oU] ([iA, oZ, iB])* --------------- Formula: (false R ! oZ) "output Z does never occur" Formula is not satisfied! An error path is [iD, oZ] ([iB, oU, iA, oZ])* --------------- Formula: (false R (! (oZ & ! iE) | (! iE WU (oW & ! iE)))) "output W occurs between output Z and input E" Formula is not satisfied! An error path is [iD, oZ, iE] ([oX, iC, oX, iA, oZ, iE])* --------------- Formula: (false R (! ((iA & ! iE) & (true U iE)) | (! oW U iE))) "output W does never occur between input A and input E" Formula is not satisfied! An error path is [iA, oW, iE] ([oX, iD, oW, iE])* --------------- Formula: (false R (! (oX & ! iD) | (! oU WU iD))) "output U does never occur after output X until input D" Formula is not satisfied! An error path is [iA, oW, iE, oX, iE, iB, oU] ([iA, oW, iB, oU])* --------------- Formula: (false R (! (oU & ! oX) | (! oZ WU oX))) "output Z does never occur after output U until output X" Formula is not satisfied! An error path is [iC, oU, iA, oZ] ([iA, oU, iA, oZ])* --------------- Formula: (false R (! (oY & ! iF) | (! iF U (oX & ! iF)))) "output X occurs after output Y until input F" Formula is not satisfied! An error path is [iA, oW, iC, oY] ([iA, oW, iC, oY])* --------------- Formula: (false R (! (oY & ! oW) | (! oW U (oV & ! oW)))) "output V occurs after output Y until output W" Formula is not satisfied! An error path is [iA, oW, iC, oY] ([iA, oW, iC, oY])* --------------- Formula: (true U oU) "output U occurs eventually" Formula is not satisfied! An error path is [iA, oW] ([iA, oZ, iB])* --------------- Formula: (false R (! (iE & ! iB) | (! oW WU iB))) "output W does never occur after input E until input B" Formula is not satisfied! An error path is [iA, oW, iE, oX, iD, oW] ([iA, oZ, iB])* --------------- Formula: (! (true U oX) | ((! oU & ! oX) U (oX | ((oU & ! oX) U (oX | ((! oU & ! oX) U (oX | ((oU & ! oX) U (oX | (! oU U oX)))))))))) "output U occurs at most twice before output X" Formula is not satisfied! An error path is [iC, oU, iD, oU, iA, iE, oU, iA, oZ, iE, oX] ([iA, oY])* --------------- Formula: (true U oX) "output X occurs eventually" Formula is not satisfied! An error path is [iA, oW] ([iA, oZ, iB])* --------------- Formula: (! oX WU (oV & ! oX)) "output V occurs before output X" Formula is not satisfied! An error path is [iA, oW, iE, oX] ([iC, iC, oW, iE, oX])* --------------- Formula: (! (true U iB) | (! oZ U (oV | iB))) "output V precedes output Z before input B" Formula is not satisfied! An error path is [iD, oZ, iB] ([oU, iA, oZ, iB])* --------------- Formula: (false R (! iF | (true U oW))) "output W responds to input F" Formula is satisfied. --------------- Formula: (! (true U oV) | (! oZ U (iA | oV))) "input A precedes output Z before output V" Formula is satisfied. --------------- Formula: (! oU WU (oU WU (! oU WU (oU WU (false R ! oU))))) "output U occurs at most twice" Formula is not satisfied! An error path is [iC, oU, iA] ([oZ, iA, oU, iA])* --------------- Formula: ((false R ! iC) | (true U (iC & (true U oZ)))) "output Z occurs after input C" Formula is not satisfied! An error path is [iC, oU] ([iD, oU, iC, iB])* --------------- Formula: (! oW WU iF) "output W does never occur before input F" Formula is not satisfied! An error path is [iA, oW] ([iA, oZ, iB])* --------------- Formula: ((false R ! iF) | (true U (iF & (true U oY)))) "output Y occurs after input F" Formula is satisfied. --------------- Formula: (! (true U oY) | (! oZ U (iA | oY))) "input A precedes output Z before output Y" Formula is not satisfied! An error path is [iD, oZ, iD, oY] ([iA])* --------------- Formula: (! (true U iF) | (! oY U (iC | iF))) "input C precedes output Y before input F" Formula is satisfied. --------------- Formula: (false R (! iA | (true U oV))) "output V responds to input A" Formula is not satisfied! An error path is [iA, oW] ([iA, oZ, iB])* --------------- 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 not satisfied! An error path is [iA, oW, iA, oZ, iA, oW, iA, oZ, iA, oW, iE] ([oX, iD, oW, iE])* --------------- Formula: (! iA WU (oU & ! iA)) "output U occurs before input A" Formula is not satisfied! An error path is [iA, oW] ([iA, oZ, iB])* --------------- Formula: (true U oX) "output X occurs eventually" Formula is not satisfied! An error path is [iA, oW] ([iA, oZ, iB])* --------------- Formula: (! (true U iD) | (! oZ U (iE | iD))) "input E precedes output Z before input D" Formula is not satisfied! An error path is [iC, oU, iA, oZ, iD] ([iA, oZ, iB])* --------------- Formula: (false R (! (iD & ! oY) | (! oY U (oX & ! oY)))) "output X occurs after input D until output Y" Formula is not satisfied! An error path is [iD, oZ] ([iB, oU, iA, oZ])* --------------- Formula: ((false R ! iD) | (true U (iD & (true U oU)))) "output U occurs after input D" Formula is not satisfied! An error path is [iD, oZ] ([iD, oY, iC, oZ])* --------------- Formula: (false R (! oW | (false R ! oV))) "output V does never occur after output W" Formula is satisfied. --------------- Formula: (true U oU) "output U occurs eventually" Formula is not satisfied! An error path is [iA, oW] ([iA, oZ, iB])* --------------- Formula: (false R (! ((iD & ! oY) & (true U oY)) | (! oU U oY))) "output U does never occur between input D and output Y" Formula is not satisfied! An error path is [iC, oU, iD, oU, iD, iB, oY] ([iA])* --------------- Formula: (false R (! oU | (false R ! oW))) "output W does never occur after output U" Formula is not satisfied! An error path is [iA, oW, iB, oU, iA, oW] ([iA, oZ, iB])* --------------- Formula: (false R (! oW | (false R ! oV))) "output V does never occur after output W" Formula is satisfied. --------------- Formula: (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) "output X occurs at most twice" Formula is not satisfied! An error path is [iA, oW, iE, oX, iC] ([iA, oZ, iC, oW, iE, oX, iC])* --------------- Formula: (false R (! (iA & ! iD) | (! iD U (oZ & ! iD)))) "output Z occurs after input A until input D" Formula is not satisfied! An error path is [iA, oW] ([iB, oU, iA, oW])* --------------- Formula: (! (true U iD) | ((! oV & ! iD) U (iD | ((oV & ! iD) U (iD | ((! oV & ! iD) U (iD | ((oV & ! iD) U (iD | (! oV U iD)))))))))) "output V occurs at most twice before input D" Formula is satisfied. --------------- Formula: (false R (! oV | (false R ! oU))) "output U does never occur after output V" Formula is satisfied. --------------- Formula: (! oZ WU oW) "output Z does never occur before output W" Formula is not satisfied! An error path is [iD, oZ] ([iB, oU, iA, oZ])* --------------- Formula: (false R (! ((oZ & ! oU) & (true U oU)) | (! oX U oU))) "output X does never occur between output Z and output U" Formula is not satisfied! An error path is [iD, oZ, iE, oX, iC, oX, iE, oU] ([iA, oZ, iB, oU])* --------------- Formula: (false R (! oU | (false R ! oZ))) "output Z does never occur after output U" Formula is not satisfied! An error path is [iC, oU, iA, oZ] ([iA, oU, iA, oZ])* --------------- Formula: (false R (! (iF & ! oU) | (! oU U (oV & ! oU)))) "output V occurs after input F until output U" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iA) | (! oV WU iA))) "output V does never occur after input B until input A" Formula is satisfied. --------------- Formula: (false R (! iD | (false R ! oW))) "output W does never occur after input D" Formula is not satisfied! An error path is [iA, oW, iD, oZ, iC, oW] ([iA, oZ, iB])* --------------- Formula: (false R (! (oW & ! iA) | (! iA U (oZ & ! iA)))) "output Z occurs after output W until input A" Formula is not satisfied! An error path is [iA, oW] ([iB, oU, iA, oW])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iA, oW, iC, oY] ([iA, oW, iC, oY])* --------------- Formula: (false R (! oU | (true U oZ))) "output Z responds to output U" Formula is not satisfied! An error path is [iC, oU] ([iD, oU, iC, iB])* --------------- Formula: (false R (! iC | (true U oW))) "output W responds to input C" Formula is not satisfied! An error path is [iC, oU] ([iA, oZ, iB])* --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iA, oW] ([iB, oU, iA, oW])* --------------- Formula: (false R (! (iC & ! iB) | (! iB U (oU & ! iB)))) "output U occurs after input C until input B" Formula is not satisfied! An error path is [iA, oW, iC] ([oY, iA, oW, iC])* --------------- Formula: (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) "output X occurs at most twice" Formula is not satisfied! An error path is [iA, oW, iE, oX, iC] ([iA, oZ, iC, oW, iE, oX, iC])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iA, oW, iC, oY] ([iA, oW, iC, oY])* --------------- Formula: (false R (! (oZ & ! oY) | (! oY WU (oU & ! oY)))) "output U occurs between output Z and output Y" Formula is not satisfied! An error path is [iD, oZ, iD, oY] ([iA])* --------------- Formula: (false R (! iF | (false R ! oX))) "output X does never occur after input F" Formula is satisfied. --------------- Formula: (false R (! ((iC & ! oV) & (true U oV)) | (! oY U oV))) "output Y does never occur between input C and output V" Formula is satisfied. --------------- Formula: (false R (! ((oV & ! oU) & (true U oU)) | (! oZ U oU))) "output Z does never occur between output V and output U" Formula is satisfied. --------------- Formula: (false R (! oV | (false R ! oU))) "output U does never occur after output V" Formula is satisfied. --------------- Formula: (false R (! ((iA & ! iF) & (true U iF)) | (! oX U iF))) "output X does never occur between input A and input F" Formula is satisfied. --------------- Formula: (! (true U iA) | ((! oX & ! iA) U (iA | ((oX & ! iA) U (iA | ((! oX & ! iA) U (iA | ((oX & ! iA) U (iA | (! oX U iA)))))))))) "output X occurs at most twice before input A" Formula is not satisfied! An error path is [iD, oZ, iE, oX, iC, oX, iB, oZ, iE, oX, iA] ([oY, iA])* --------------- Formula: (false R (! ((oV & ! iB) & (true U iB)) | (! oX U iB))) "output X does never occur between output V and input B" Formula is satisfied. --------------- Formula: (! iF WU (oX & ! iF)) "output X occurs before input F" Formula is satisfied. --------------- Formula: ((false R ! iF) | (true U (iF & (true U oU)))) "output U occurs after input F" Formula is satisfied. --------------- Formula: (! (true U iA) | (! oY U (iF | iA))) "input F precedes output Y before input A" Formula is not satisfied! An error path is [iC, oU, iB, oY, iA] ([iA])* --------------- Formula: (false R (! (oW & ! oU) | (! oZ WU oU))) "output Z does never occur after output W until output U" Formula is not satisfied! An error path is [iA, oW, iA, oZ] ([iA, oW, iA, oZ])* --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iA, oW] ([iA, oZ, iB])* --------------- Formula: (false R (! iD | (true U oV))) "output V responds to input D" Formula is not satisfied! An error path is [iD, oZ] ([iB, oU, iA, oZ])* --------------- Formula: (! oV WU (oV WU (! oV WU (oV WU (false R ! oV))))) "output V occurs at most twice" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iC) | (! oX WU iC))) "output X does never occur after input B until input C" Formula is not satisfied! An error path is [iA, oW, iA, oZ, iB, iE, oX] ([iC, iC, oW, iE, oX])* --------------- Formula: (false R (! (iE & ! oU) | (! oU U (oX & ! oU)))) "output X occurs after input E until output U" Formula is not satisfied! An error path is [iC, oU, iE] ([oZ, iB, iE])* --------------- Formula: (false R (! (oX & ! iA) | (! oZ WU iA))) "output Z does never occur after output X until input A" Formula is not satisfied! An error path is [iD, oZ, iE, oX, iB, oZ] ([iA, iB, iC, oZ])* --------------- Formula: (false R (! ((iE & ! oW) & (true U oW)) | (! oV U oW))) "output V does never occur between input E and output W" Formula is satisfied. --------------- Formula: ((false R ! oU) | (true U (oU & (true U oW)))) "output W occurs after output U" Formula is not satisfied! An error path is [iC, oU] ([iA, oZ, iB])* --------------- 32 constraints satisfied, 68 unsatisfied.