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