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