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