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