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