Reachability problems: =============================== error_14 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, E, A] --------------- error_34 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, F, A] --------------- error_10 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, A, A] --------------- error_27 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, B, A] --------------- error_57 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, D, A] --------------- error_11 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, E, A] --------------- error_52 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, F, A] --------------- error_31 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, A, A] --------------- error_13 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, D, A] --------------- error_39 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, C, A] --------------- error_29 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, E, A] --------------- error_56 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, A, A] --------------- error_37 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, B, A] --------------- error_40 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, D, A] --------------- error_18 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, C, A] --------------- error_8 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, A, A] --------------- error_22 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, B, A] --------------- error_58 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, D, A] --------------- error_43 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, C, A] --------------- error_54 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, F, E, A] --------------- error_41 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, F, F, A] --------------- error_12 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, F, D, A] --------------- error_2 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, E, A, A] --------------- error_28 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, E, D, A] --------------- error_44 reachable via input sequence [E, F, A, E, E, B, E, C, B, D, C, B, F, E, C, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (! oW WU iB) "input B precedes output W" Formula is satisfied. --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is satisfied. --------------- Formula: (false R (! iD | (true U oV))) "output V responds to input D" Formula is satisfied. --------------- Formula: (true U oY) "output Y occurs eventually" Formula is satisfied. --------------- Formula: (false R (! oX | (false R ! oU))) "output U does never occur after output X" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iE, oX, iE, oY, iB, oV, iE, oZ, iC, oV, iB, oY, iD, oV, iC, oU, iB, oV, iF, oZ] ([iE, oY, iF])* --------------- Formula: (false R (! (oY & ! iB) | (! oZ WU iB))) "output Z does never occur after output Y until input B" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV, iE, oZ] ([iE, oZ])* --------------- Formula: (false R (! iE | (false R ! oY))) "output Y does never occur after input E" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (! (true U oW) | (! oV U (oZ | oW))) "output Z precedes output V before output W" Formula is satisfied. --------------- Formula: (false R (! ((iF & ! iB) & (true U iB)) | (! oX U iB))) "output X does never occur between input F and input B" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iE, oX, iE, oY, iB, oV, iE, oZ, iC, oV, iB, oY, iD, oV, iC, oU, iB, oV, iF, oZ] ([iE, oY, iF])* --------------- Formula: (false R (! ((oV & ! iE) & (true U iE)) | (! oY U iE))) "output Y does never occur between output V and input E" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: ((false R ! iA) | (true U (iA & (true U oY)))) "output Y occurs after input A" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! oX) | (! oX WU (oW & ! oX)))) "output W occurs between output Z and output X" Formula is satisfied. --------------- Formula: (! oY WU iF) "input F precedes output Y" Formula is satisfied. --------------- Formula: (false R ! oW) "output W does never occur" Formula is satisfied. --------------- Formula: (! (true U iF) | (! oV U (iA | iF))) "input A precedes output V before input F" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: ((false R ! oV) | (true U (oV & (true U oX)))) "output X occurs after output V" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (! oX WU (oV & ! oX)) "output V occurs before output X" Formula is satisfied. --------------- Formula: (! iD WU (oX & ! iD)) "output X occurs before input D" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (! oX WU oV) "output X does never occur before output V" Formula is satisfied. --------------- Formula: (false R (! iE | (true U oX))) "output X responds to input E" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R ! oX) "output X does never occur" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iE, oX, iE, oY, iB, oV, iE, oZ, iC, oV, iB, oY, iD, oV, iC, oU, iB, oV, iF, oZ] ([iE, oY, iF])* --------------- Formula: (false R (! (iB & ! iF) | (! oZ WU iF))) "output Z does never occur after input B until input F" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R (! oZ | (true U oX))) "output X responds to output Z" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R (! ((oX & ! iB) & (true U iB)) | (! oW U iB))) "output W does never occur between output X and input B" Formula is satisfied. --------------- Formula: (false R (! ((iA & ! oW) & (true U oW)) | (! oV U oW))) "output V does never occur between input A and output W" Formula is satisfied. --------------- Formula: (false R (! (oU & ! oY) | (! oW WU oY))) "output W does never occur after output U until output Y" 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: (! oX WU oZ) "output X does never occur before output Z" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iE, oX, iE, oY, iB, oV, iE, oZ, iC, oV, iB, oY, iD, oV, iC, oU, iB, oV, iF, oZ] ([iE, oY, iF])* --------------- 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 [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV, iE] ([oZ, iE])* --------------- Formula: (false R (! (iD & ! oU) | (! oU U (oW & ! oU)))) "output W occurs after input D until output U" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R ! oW) "output W does never occur" Formula is satisfied. --------------- Formula: (false R (! (oX & ! oU) | (! oU WU (oZ & ! oU)))) "output Z occurs between output X and output U" Formula is satisfied. --------------- Formula: (! oW WU iF) "output W does never occur before input F" Formula is satisfied. --------------- Formula: (false R (! iC | (true U oZ))) "output Z responds to input C" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iE, oX, iE, oY, iB, oV, iE, oZ, iC, oV, iB, oY, iD, oV, iC, oU, iB, oV, iF, oZ, iF, oZ, iC] ([iB, iE, oY, iB])* --------------- Formula: (! oU WU oX) "output X precedes output U" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (true U oX) "output X occurs eventually" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R (! iF | (true U oV))) "output V responds to input F" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iE, oX, iE, oY, iB, oV, iE, oZ, iC, oV, iB, oY, iD, oV, iC, oU, iB, oV, iF, oZ] ([iE, oY, iF])* --------------- Formula: (! (true U oU) | ((! oX & ! oU) U (oU | ((oX & ! oU) U (oU | ((! oX & ! oU) U (oU | ((oX & ! oU) U (oU | (! oX U oU)))))))))) "output X occurs at most twice before output U" 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: (! oV WU iB) "input B precedes output V" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R (! (iE & ! iD) | (! iD U (oZ & ! iD)))) "output Z occurs after input E until input D" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (! oU WU iE) "output U does never occur before input E" Formula is satisfied. --------------- Formula: (! (true U iC) | (! oY U (iA | iC))) "input A precedes output Y before input C" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iE, oX, iE, oY, iB, oV, iE, oZ, iC, oV, iB, oY, iD, oV, iC, oU, iB, oV, iF, oZ] ([iE, oY, iF])* --------------- Formula: (false R (! ((iE & ! oY) & (true U oY)) | (! oV U oY))) "output V does never occur between input E and output Y" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R (! iA | (false R ! oU))) "output U does never occur after input A" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (false R (! (oV & ! oW) | (! oZ WU oW))) "output Z does never occur after output V until output W" Formula is not satisfied! An error path is [iE, oV, iF, oY, iA, oU, iB, oZ, iE, oY, iD, oV] ([iE, oZ])* --------------- Formula: (! (true U oY) | ((! oZ & ! oY) U (oY | ((oZ & ! oY) U (oY | ((! oZ & ! oY) U (oY | ((oZ & ! oY) U (oY | (! oZ U oY)))))))))) "output Z occurs at most twice before output Y" Formula is satisfied. --------------- Formula: (! (true U iE) | ((! oZ & ! iE) U (iE | ((oZ & ! iE) U (iE | ((! oZ & ! iE) U (iE | ((oZ & ! iE) U (iE | (! oZ U iE)))))))))) "output Z occurs at most twice before input E" Formula is satisfied. --------------- 23 constraints satisfied, 27 unsatisfied.