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