Reachability problems: =============================== error_25 reachable via input sequence [B, C, F, B, A] --------------- error_50 reachable via input sequence [B, B, C, B, A] --------------- error_3 reachable via input sequence [B, B, C, A, A] --------------- error_37 reachable via input sequence [B, F, E, B, A] --------------- error_28 reachable via input sequence [B, F, B, A, A] --------------- error_7 reachable via input sequence [F, F, D, B, A] --------------- error_48 reachable via input sequence [E, F, A, D, A] --------------- error_51 reachable via input sequence [E, F, A, F, A] --------------- error_13 reachable via input sequence [E, C, A, C, A] --------------- error_8 reachable via input sequence [E, C, A, E, A] --------------- error_52 reachable via input sequence [E, C, A, A, A] --------------- error_39 reachable via input sequence [E, A, C, B, A] --------------- error_21 reachable via input sequence [E, A, C, C, A] --------------- error_6 reachable via input sequence [E, A, C, E, A] --------------- error_19 reachable via input sequence [E, A, B, B, A] --------------- error_0 reachable via input sequence [E, A, B, D, A] --------------- error_34 reachable via input sequence [E, A, B, A, A] --------------- error_55 reachable via input sequence [D, E, E, B, A] --------------- error_38 reachable via input sequence [D, A, C, B, A] --------------- error_30 reachable via input sequence [D, A, C, D, A] --------------- error_42 reachable via input sequence [D, A, C, A, A] --------------- error_40 reachable via input sequence [D, A, E, B, A] --------------- error_10 reachable via input sequence [D, C, F, B, A] --------------- error_20 reachable via input sequence [C, F, E, B, A] --------------- error_35 reachable via input sequence [C, F, A, B, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (! oV WU (oW & ! oV)) "output W occurs before output V" Formula is satisfied. --------------- Formula: (! (true U iB) | (! oU U (iE | iB))) "input E precedes output U before input B" Formula is satisfied. --------------- Formula: (! oY WU (oV & ! oY)) "output V occurs before output Y" Formula is satisfied. --------------- Formula: (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) "output X occurs at most twice" Formula is satisfied. --------------- Formula: (true U oU) "output U occurs eventually" Formula is not satisfied! An error path is [iE, oW] ([iC, oW, iC, oZ, iF])* --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (false R (! (oY & ! iF) | (! iF U (oZ & ! iF)))) "output Z occurs after output Y until input F" Formula is satisfied. --------------- Formula: (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) "output X occurs at most twice" Formula is satisfied. --------------- Formula: (false R (! iB | (true U oZ))) "output Z responds to input B" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (! (true U oU) | (! oY U (iE | oU))) "input E precedes output Y before output U" Formula is satisfied. --------------- Formula: (! (true U oV) | ((! oW & ! oV) U (oV | ((oW & ! oV) U (oV | ((! oW & ! oV) U (oV | ((oW & ! oV) U (oV | (! oW U oV)))))))))) "output W occurs at most twice before output V" Formula is satisfied. --------------- Formula: (! iC WU (oV & ! iC)) "output V occurs before input C" Formula is not satisfied! An error path is [iC, oU] ([iC, oW, iD, oW, iF])* --------------- Formula: (! (true U oU) | ((! oY & ! oU) U (oU | ((oY & ! oU) U (oU | ((! oY & ! oU) U (oU | ((oY & ! oU) U (oU | (! oY U oU)))))))))) "output Y occurs at most twice before output U" Formula is satisfied. --------------- Formula: ((false R ! oU) | (true U (oU & (true U oW)))) "output W occurs after output U" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: ((false R ! oW) | (true U (oW & (true U oY)))) "output Y occurs after output W" Formula is not satisfied! An error path is [iE, oW] ([iB, oW, iA, oU, iC])* --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (false R (! oU | (true U oV))) "output V responds to output U" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (false R (! oU | (true U oW))) "output W responds to output U" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- 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 [iE, oW, iB] ([oW, iB, oW, iE, iB, oW, iB])* --------------- Formula: (! oY WU oZ) "output Z precedes output Y" Formula is satisfied. --------------- Formula: (! (true U oV) | (! oW U (iB | oV))) "input B precedes output W before output V" Formula is satisfied. --------------- Formula: (! oX WU iE) "input E precedes output X" Formula is satisfied. --------------- Formula: (true U oX) "output X occurs eventually" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (false R (! iF | (false R ! oU))) "output U does never occur after input F" Formula is not satisfied! An error path is [iF, oU] ([iC, oZ, iE, oZ, iA])* --------------- Formula: (! oV WU (oV WU (! oV WU (oV WU (false R ! oV))))) "output V occurs at most twice" Formula is satisfied. --------------- Formula: (! oZ WU oU) "output Z does never occur before output U" Formula is not satisfied! An error path is [iE, oW, iF, oZ] ([iE, oW, iE])* --------------- 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: (! (true U oX) | (! oZ U (iD | oX))) "input D precedes output Z before output X" Formula is satisfied. --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (! oW WU iB) "input B precedes output W" Formula is not satisfied! An error path is [iE, oW] ([iB, oW, iA, oU, iC])* --------------- Formula: (false R (! iB | (false R ! oX))) "output X does never occur after input B" 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 (! (oX & ! iE) | (! iE U (oY & ! iE)))) "output Y occurs after output X until input E" Formula is satisfied. --------------- Formula: (false R (! iF | (true U oW))) "output W responds to input F" Formula is not satisfied! An error path is [iF, oU] ([iC, oZ, iE, oZ, iA])* --------------- Formula: ((false R ! iC) | (true U (iC & (true U oW)))) "output W occurs after input C" Formula is not satisfied! An error path is [iC, oU] ([iF, oZ, iE, oU, iE])* --------------- Formula: (false R (! iE | (false R ! oV))) "output V does never occur after input E" Formula is satisfied. --------------- Formula: (! (true U oZ) | (! oV U (oW | oZ))) "output W precedes output V before output Z" 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 [iE, oW, iB] ([oW, iA, oU, iC, iB])* --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (false R (! (oY & ! iC) | (! iC U (oZ & ! iC)))) "output Z occurs after output Y until input C" Formula is satisfied. --------------- Formula: (! (true U iA) | (! oU U (oW | iA))) "output W precedes output U before input A" Formula is not satisfied! An error path is [iB, oU, iA] ([oW, iC, oZ, iC, oU, iA])* --------------- Formula: (false R ! oX) "output X does never occur" Formula is satisfied. --------------- Formula: (false R (! (iF & ! iB) | (! oY WU iB))) "output Y does never occur after input F until input B" Formula is satisfied. --------------- Formula: (false R (! (iA & ! iD) | (! oX WU iD))) "output X does never occur after input A until input D" Formula is satisfied. --------------- Formula: (! (true U iF) | (! oX U (oV | iF))) "output V precedes output X before input F" Formula is satisfied. --------------- Formula: (! (true U iD) | ((! oX & ! iD) U (iD | ((oX & ! iD) U (iD | ((! oX & ! iD) U (iD | ((oX & ! iD) U (iD | (! oX U iD)))))))))) "output X occurs at most twice before input D" Formula is satisfied. --------------- Formula: (false R (! ((oY & ! iB) & (true U iB)) | (! oZ U iB))) "output Z does never occur between output Y and input B" Formula is satisfied. --------------- Formula: (false R (! ((oV & ! oZ) & (true U oZ)) | (! oX U oZ))) "output X does never occur between output V and output Z" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! oY) | (! oY U (oV & ! oY)))) "output V occurs after output Z until output Y" Formula is not satisfied! An error path is [iB, oU, iB, oZ] ([iC, oW, iD, oU])* --------------- Formula: (! oX WU oV) "output X does never occur before output V" Formula is satisfied. --------------- Formula: (! (true U iD) | ((! oX & ! iD) U (iD | ((oX & ! iD) U (iD | ((! oX & ! iD) U (iD | ((oX & ! iD) U (iD | (! oX U iD)))))))))) "output X occurs at most twice before input D" Formula is satisfied. --------------- Formula: (false R (! (iF & ! iE) | (! iE U (oY & ! iE)))) "output Y occurs after input F until input E" Formula is not satisfied! An error path is [iF, oU] ([iC, oZ, iE, oZ, iA])* --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (! (true U oY) | (! oW U (oU | oY))) "output U precedes output W before output Y" Formula is satisfied. --------------- Formula: ((false R ! oY) | (true U (oY & (true U oV)))) "output V occurs after output Y" Formula is satisfied. --------------- Formula: (false R (! ((iE & ! iB) & (true U iB)) | (! oW U iB))) "output W does never occur between input E and input B" Formula is not satisfied! An error path is [iE, oW, iB] ([oW, iA, oU, iC, 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 [iB, oU, iB, oZ, iB] ([oZ, iB, oU, iB, iF, iB, oZ, iB])* --------------- Formula: ((false R ! iE) | (true U (iE & (true U oW)))) "output W occurs after input E" Formula is not satisfied! An error path is [iF, oU, iE] ([oZ, iF, oU, iE, iE])* --------------- Formula: (false R (! (oW & ! iD) | (! iD WU (oY & ! iD)))) "output Y occurs between output W and input D" Formula is not satisfied! An error path is [iC, oU, iC, oW, iD] ([oW, iF, iC, oW, iD])* --------------- Formula: (! oY WU (oX & ! oY)) "output X occurs before output Y" Formula is satisfied. --------------- Formula: (! oZ WU iB) "input B precedes output Z" Formula is not satisfied! An error path is [iC, oU, iD, oZ] ([iF, oW, iD, oZ])* --------------- Formula: (false R (! (oZ & ! oU) | (! oX WU oU))) "output X does never occur after output Z until 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 [iE, oW, iB] ([oW, iA, oU, iC, iB])* --------------- Formula: (false R ! oV) "output V does never occur" Formula is satisfied. --------------- Formula: (false R (! (oV & ! oX) | (! oX WU (oU & ! oX)))) "output U occurs between output V and output X" Formula is satisfied. --------------- Formula: (! oV WU (oY & ! oV)) "output Y occurs before output V" Formula is satisfied. --------------- Formula: (false R (! iE | (true U oY))) "output Y responds to input E" Formula is not satisfied! An error path is [iE, oW] ([iB, oW, iA, oU, iC])* --------------- Formula: (false R (! ((oZ & ! oW) & (true U oW)) | (! oU U oW))) "output U does never occur between output Z and output W" Formula is not satisfied! An error path is [iB, oU, iB, oZ, iF, oU, iE, oW] ([iE, oW])* --------------- Formula: (false R (! ((iA & ! iE) & (true U iE)) | (! oU U iE))) "output U does never occur between input A and input E" Formula is not satisfied! An error path is [iB, oU, iA, oW, iF, oU, iE] ([oZ, iB, iD, iF, iA, oW, iF, oU, iE])* --------------- Formula: (false R (! oX | (true U oY))) "output Y responds to output X" Formula is satisfied. --------------- Formula: ((false R ! oW) | (true U (oW & (true U oZ)))) "output Z occurs after output W" Formula is not satisfied! An error path is [iE, oW] ([iB, oW, iA, oU, iC])* --------------- Formula: (! iC WU (oV & ! iC)) "output V occurs before input C" Formula is not satisfied! An error path is [iC, oU] ([iC, oW, iD, oW, iF])* --------------- Formula: (true U oY) "output Y occurs eventually" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (! oW WU oV) "output W does never occur before output V" Formula is not satisfied! An error path is [iE, oW] ([iB, oW, iA, oU, iC])* --------------- Formula: (false R (! ((oW & ! iA) & (true U iA)) | (! oV U iA))) "output V does never occur between output W and input A" Formula is satisfied. --------------- Formula: (false R (! ((iE & ! oW) & (true U oW)) | (! oU U oW))) "output U does never occur between input E and output W" Formula is not satisfied! An error path is [iC, oU, iE, oU, iD, oW] ([iA, iF, iE, oU, iD, oW])* --------------- Formula: (false R (! iC | (true U oY))) "output Y responds to input C" Formula is not satisfied! An error path is [iC, oU] ([iC, oW, iD, oW, iF])* --------------- Formula: (! oU WU oZ) "output Z precedes output U" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (false R ! oU) "output U does never occur" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (false R (! (iF & ! oV) | (! oV WU (oY & ! oV)))) "output Y occurs between input F and output V" Formula is satisfied. --------------- Formula: ((false R ! iC) | (true U (iC & (true U oW)))) "output W occurs after input C" Formula is not satisfied! An error path is [iC, oU] ([iF, oZ, iE, oU, iE])* --------------- Formula: (false R (! iC | (false R ! oY))) "output Y does never occur after input C" Formula is satisfied. --------------- Formula: (false R (! iC | (true U oW))) "output W responds to input C" Formula is not satisfied! An error path is [iC, oU] ([iF, oZ, iE, oU, iE])* --------------- Formula: (! (true U iC) | (! oZ U (iA | iC))) "input A precedes output Z before input C" Formula is not satisfied! An error path is [iB, oU, iB, oZ, iC] ([oW, iD, oU, iC])* --------------- Formula: (false R (! (oU & ! iA) | (! iA WU (oW & ! iA)))) "output W occurs between output U and input A" Formula is not satisfied! An error path is [iB, oU, iA] ([oW, iC, oZ, iC, oU, iA])* --------------- Formula: (false R (! ((iD & ! iE) & (true U iE)) | (! oZ U iE))) "output Z does never occur between input D and input E" Formula is not satisfied! An error path is [iC, oU, iD, oZ, iE] ([oW, iF, iF, iD, oZ, iE])* --------------- Formula: (false R (! (oX & ! iD) | (! oV WU iD))) "output V does never occur after output X until input D" Formula is satisfied. --------------- Formula: (false R (! (oW & ! oZ) | (! oV WU oZ))) "output V does never occur after output W until output Z" Formula is satisfied. --------------- Formula: (false R (! (iE & ! iF) | (! iF U (oU & ! iF)))) "output U occurs after input E until input F" Formula is not satisfied! An error path is [iE, oW] ([iC, oW, iC, oZ, iF])* --------------- Formula: (false R (! oX | (true U oZ))) "output Z responds to output X" Formula is satisfied. --------------- Formula: (false R (! ((iE & ! oV) & (true U oV)) | (! oW U oV))) "output W does never occur between input E and output V" Formula is satisfied. --------------- Formula: ((false R ! iC) | (true U (iC & (true U oY)))) "output Y occurs after input C" Formula is not satisfied! An error path is [iC, oU] ([iC, oW, iD, oW, iF])* --------------- Formula: (! (true U iA) | ((! oY & ! iA) U (iA | ((oY & ! iA) U (iA | ((! oY & ! iA) U (iA | ((oY & ! iA) U (iA | (! oY U iA)))))))))) "output Y occurs at most twice before input A" Formula is satisfied. --------------- Formula: (false R (! (iB & ! oX) | (! oX WU (oV & ! oX)))) "output V occurs between input B and output X" Formula is satisfied. --------------- Formula: ((false R ! oY) | (true U (oY & (true U oU)))) "output U occurs after output Y" Formula is satisfied. --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- 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 [iE, oW, iB] ([oW, iB, oW, iE, iB, oW, iB])* --------------- Formula: (! oY WU (oY WU (! oY WU (oY WU (false R ! oY))))) "output Y occurs at most twice" Formula is satisfied. --------------- Formula: (true U oY) "output Y occurs eventually" Formula is not satisfied! An error path is [iB, oU] ([iF, oU, iB, oU, iF])* --------------- Formula: (false R (! ((oZ & ! iC) & (true U iC)) | (! oV U iC))) "output V does never occur between output Z and input C" Formula is satisfied. --------------- 50 constraints satisfied, 50 unsatisfied.