Reachability problems: =============================== error_34 reachable via input sequence [F, B, B, B, A] --------------- error_4 reachable via input sequence [F, B, B, C, A] --------------- error_23 reachable via input sequence [F, B, B, E, A] --------------- error_49 reachable via input sequence [F, B, D, A, A] --------------- error_33 reachable via input sequence [F, B, D, F, A] --------------- error_57 reachable via input sequence [F, B, D, C, A] --------------- error_37 reachable via input sequence [F, B, D, D, A] --------------- error_31 reachable via input sequence [A, A, C, F, A] --------------- error_50 reachable via input sequence [A, A, C, B, A] --------------- error_46 reachable via input sequence [A, A, C, D, A] --------------- error_52 reachable via input sequence [A, A, A, F, A] --------------- error_35 reachable via input sequence [A, A, A, D, A] --------------- error_40 reachable via input sequence [A, A, F, B, A] --------------- error_25 reachable via input sequence [A, A, F, D, A] --------------- error_26 reachable via input sequence [A, D, F, A, A] --------------- error_13 reachable via input sequence [A, D, F, C, A] --------------- error_20 reachable via input sequence [A, D, D, F, A] --------------- error_7 reachable via input sequence [A, D, D, B, A] --------------- error_30 reachable via input sequence [A, D, C, C, A] --------------- error_16 reachable via input sequence [A, D, C, D, A] --------------- error_55 reachable via input sequence [A, C, E, A, A] --------------- error_9 reachable via input sequence [A, C, E, B, A] --------------- error_54 reachable via input sequence [A, C, E, D, A] --------------- error_53 reachable via input sequence [A, C, E, E, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (false R (! (iF & ! iB) | (! oV WU iB))) "output V does never occur after input F until input B" Formula is satisfied. --------------- Formula: (false R ! oW) "output W does never occur" Formula is satisfied. --------------- Formula: (! (true U oX) | ((! oY & ! oX) U (oX | ((oY & ! oX) U (oX | ((! oY & ! oX) U (oX | ((oY & ! oX) U (oX | (! oY U oX)))))))))) "output Y occurs at most twice before output X" Formula is satisfied. --------------- Formula: (false R ! oV) "output V does never occur" Formula is satisfied. --------------- Formula: ((false R ! iE) | (true U (iE & (true U oX)))) "output X occurs after input E" Formula is not satisfied! An error path is [iA, oY, iC, oZ, iE] ([oZ, iF, oZ, iE])* --------------- Formula: (true U oY) "output Y occurs eventually" 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 [iF, oY] ([iF, oY, iD, oY, iB, oU])* --------------- Formula: (! (true U oY) | ((! oX & ! oY) U (oY | ((oX & ! oY) U (oY | ((! oX & ! oY) U (oY | ((oX & ! oY) U (oY | (! oX U oY)))))))))) "output X occurs at most twice before output Y" Formula is satisfied. --------------- Formula: (false R (! (iD & ! oV) | (! oV WU (oY & ! oV)))) "output Y occurs between input D and output V" Formula is satisfied. --------------- Formula: ((false R ! iF) | (true U (iF & (true U oY)))) "output Y occurs after input F" Formula is not satisfied! An error path is [iA, oY, iA, oU, iF] ([oZ, iC, iF])* --------------- Formula: (! oX WU (oU & ! oX)) "output U occurs before output X" Formula is satisfied. --------------- Formula: (! oX WU oV) "output X does never occur before output V" Formula is satisfied. --------------- Formula: (false R (! iF | (false R ! oY))) "output Y does never occur after input F" Formula is not satisfied! An error path is [iF, oY] ([iF, oY, iD, oY, iB, oU])* --------------- Formula: (false R (! (iE & ! iA) | (! iA WU (oZ & ! iA)))) "output Z occurs between input E and input A" Formula is not satisfied! An error path is [iA, oY, iC, oZ, iC, oZ, iE, iA] ([oY, iA, oU, iF, oZ, iA])* --------------- Formula: ((false R ! iC) | (true U (iC & (true U oU)))) "output U occurs after input C" Formula is not satisfied! An error path is [iA, oY, iC] ([oZ, iC, oZ, iF, iC])* --------------- Formula: (false R (! (oZ & ! oX) | (! oX WU (oU & ! oX)))) "output U occurs between output Z and output X" Formula is satisfied. --------------- Formula: (false R (! (oY & ! oW) | (! oW U (oV & ! oW)))) "output V occurs after output Y until output W" Formula is not satisfied! An error path is [iA, oY] ([iC, oZ, iC, oZ, iF])* --------------- Formula: (! (true U iF) | (! oU U (iA | iF))) "input A precedes output U before input F" Formula is satisfied. --------------- Formula: (false R (! (oU & ! oV) | (! oW WU oV))) "output W does never occur after output U until output V" Formula is satisfied. --------------- Formula: (false R (! (iC & ! oU) | (! oU U (oW & ! oU)))) "output W occurs after input C until output U" Formula is not satisfied! An error path is [iA, oY, iC] ([oZ, iC, oZ, iF, iC])* --------------- Formula: (false R (! ((oV & ! iD) & (true U iD)) | (! oZ U iD))) "output Z does never occur between output V and input D" Formula is satisfied. --------------- Formula: (! oY WU iA) "output Y does never occur before input A" Formula is not satisfied! An error path is [iF, oY] ([iF, oY, iD, oY, iB, oU])* --------------- Formula: (false R ! oV) "output V does never occur" Formula is satisfied. --------------- Formula: (! oV WU (oW & ! oV)) "output W occurs before output V" Formula is satisfied. --------------- Formula: (! (true U iC) | ((! oZ & ! iC) U (iC | ((oZ & ! iC) U (iC | ((! oZ & ! iC) U (iC | ((oZ & ! iC) U (iC | (! oZ U iC)))))))))) "output Z occurs at most twice before input C" Formula is not satisfied! An error path is [iF, oY, iB, oZ, iB, oZ, iF, oZ, iC] ([iF, oZ, iC])* --------------- Formula: (true U oX) "output X occurs eventually" Formula is not satisfied! An error path is [iA, oY] ([iC, oZ, iC, oZ, iF])* --------------- 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: (! (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 (! oV | (false R ! oU))) "output U does never occur after output V" Formula is satisfied. --------------- Formula: ((false R ! iC) | (true U (iC & (true U oU)))) "output U occurs after input C" Formula is not satisfied! An error path is [iA, oY, iC] ([oZ, iC, oZ, iF, iC])* --------------- Formula: (false R (! ((oX & ! iC) & (true U iC)) | (! oV U iC))) "output V does never occur between output X and input C" Formula is satisfied. --------------- Formula: (! oV WU iD) "input D precedes output V" Formula is satisfied. --------------- Formula: (! oW WU iB) "output W does never occur before input B" Formula is satisfied. --------------- Formula: (false R (! iB | (true U oX))) "output X responds to input B" Formula is not satisfied! An error path is [iF, oY, iB] ([oZ, iB, oZ, iA, 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, oY, iC, oZ, iC] ([oZ, iF, iC, oZ, iC])* --------------- Formula: (! (true U iD) | (! oX U (iA | iD))) "input A precedes output X before input D" Formula is satisfied. --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iA, oY] ([iC, oZ, iC, oZ, iF])* --------------- Formula: (false R (! (oX & ! oY) | (! oY U (oV & ! oY)))) "output V occurs after output X until output Y" Formula is satisfied. --------------- Formula: (false R (! oU | (false R ! oV))) "output V does never occur after output U" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! oX) | (! oX U (oV & ! oX)))) "output V occurs after output Z until output X" Formula is not satisfied! An error path is [iA, oY, iC, oZ] ([iD, oU, iC])* --------------- Formula: ((false R ! oZ) | (true U (oZ & (true U oY)))) "output Y occurs after output Z" Formula is not satisfied! An error path is [iA, oY, iC, oZ] ([iD, oU, iC])* --------------- Formula: (! oW WU iB) "output W does never occur before input B" Formula is satisfied. --------------- Formula: (true U oU) "output U occurs eventually" Formula is not satisfied! An error path is [iA, oY] ([iC, oZ, iC, oZ, iF])* --------------- Formula: (! iD WU (oW & ! iD)) "output W occurs before input D" Formula is not satisfied! An error path is [iA, oY, iD] ([oY, iC, oU, iF, iD])* --------------- Formula: (false R (! (oY & ! oZ) | (! oV WU oZ))) "output V does never occur after output Y until output Z" 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, oY, iA, oU] ([iF, oZ, iC])* --------------- Formula: (! oW WU iD) "input D precedes output W" Formula is satisfied. --------------- Formula: ((false R ! iD) | (true U (iD & (true U oU)))) "output U occurs after input D" Formula is not satisfied! An error path is [iA, oY, iD] ([oY, iF, oY, iB, oY, iD])* --------------- Formula: (true U oY) "output Y occurs eventually" Formula is satisfied. --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iA, oY] ([iD, oY, iC, oU, iF])* --------------- 28 constraints satisfied, 22 unsatisfied.