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