Reachability problems: =============================== error_22 reachable via input sequence [A, F, A, B, A, E, F, A] --------------- error_18 reachable via input sequence [A, F, A, B, A, E, D, A] --------------- error_19 reachable via input sequence [F, A, F, B, C, C, D, A, A] --------------- error_59 reachable via input sequence [F, A, F, B, C, C, D, F, A] --------------- error_26 reachable via input sequence [F, A, F, B, C, C, D, D, A] --------------- error_27 reachable via input sequence [F, A, F, B, C, C, D, C, A] --------------- error_11 reachable via input sequence [F, A, F, B, C, C, A, F, A] --------------- error_51 reachable via input sequence [F, A, F, B, C, C, A, D, A] --------------- error_31 reachable via input sequence [F, A, F, B, C, C, A, C, A] --------------- error_32 reachable via input sequence [F, A, F, B, C, C, A, E, A] --------------- error_50 reachable via input sequence [F, A, F, F, F, B, B, A, A] --------------- error_29 reachable via input sequence [F, A, F, F, F, B, B, D, A] --------------- error_43 reachable via input sequence [F, A, F, F, F, B, B, C, A] --------------- error_28 reachable via input sequence [F, A, F, F, F, B, B, E, A] --------------- error_53 reachable via input sequence [F, A, F, B, C, C, D, B, A, A] --------------- error_14 reachable via input sequence [F, A, F, B, C, C, D, B, F, A] --------------- error_58 reachable via input sequence [F, A, F, B, C, C, D, B, C, A] --------------- error_55 reachable via input sequence [F, A, F, B, C, C, D, B, B, A] --------------- error_21 reachable via input sequence [F, A, F, B, C, C, D, B, E, A] --------------- error_41 reachable via input sequence [F, A, F, B, C, C, A, B, A, A] --------------- error_10 reachable via input sequence [F, A, F, B, C, C, A, B, F, A] --------------- error_47 reachable via input sequence [F, A, F, B, C, C, A, B, C, A] --------------- error_42 reachable via input sequence [F, A, F, B, C, C, A, B, B, A] --------------- error_17 reachable via input sequence [F, A, F, B, C, C, A, B, E, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (false R (! (iD & ! iE) | (! oX WU iE))) "output X does never occur after input D until input E" Formula is satisfied. --------------- Formula: (false R (! oZ | (true U oX))) "output X responds to output Z" Formula is satisfied. --------------- Formula: (false R (! iE | (true U oU))) "output U responds to input E" Formula is satisfied. --------------- Formula: (! oV WU oY) "output Y precedes output V" Formula is satisfied. --------------- Formula: (false R (! (oV & ! iB) | (! iB WU (oW & ! iB)))) "output W occurs between output V and input B" Formula is satisfied. --------------- Formula: (false R (! ((oW & ! iC) & (true U iC)) | (! oV U iC))) "output V does never occur between output W and input C" Formula is satisfied. --------------- Formula: (! (true U iC) | (! oV U (oZ | iC))) "output Z precedes output V before input C" Formula is satisfied. --------------- Formula: (! oU WU iE) "output U does never occur before input E" Formula is not satisfied! An error path is [iF, oW, iA, oY, iB, oU] ([iD, oW, iC, oY, iD, oY, iC])* --------------- Formula: (false R ! oZ) "output Z does never occur" Formula is satisfied. --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iA, oW, iF, oY] ([iA, oW, iB, oU, iB, oU, iD, oW, iB, oU])* --------------- Formula: (false R (! (iF & ! iE) | (! iE U (oU & ! iE)))) "output U occurs after input F until input E" Formula is not satisfied! An error path is [iF, oW, iD, oY, iC, oW, iE] ([oW, iC, oW, iF, oU, iF, oY, iC, iD, oY, iC, oW, iE])* --------------- Formula: (false R (! ((iF & ! oV) & (true U oV)) | (! oX U oV))) "output X does never occur between input F and output V" Formula is satisfied. --------------- Formula: (! (true U oZ) | ((! oU & ! oZ) U (oZ | ((oU & ! oZ) U (oZ | ((! oU & ! oZ) U (oZ | ((oU & ! oZ) U (oZ | (! oU U oZ)))))))))) "output U occurs at most twice before output Z" Formula is satisfied. --------------- Formula: (false R (! oV | (true U oU))) "output U responds to output V" 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, oW, iF, oY, iA] ([oW, iB, oU, iB, oU, iD, oW, iB, oU, iC, oW, iF, oY, iB, oW, iD, oW, iD, oU, iF, oY, iA])* --------------- Formula: (false R (! ((oU & ! iD) & (true U iD)) | (! oX U iD))) "output X does never occur between output U and input D" Formula is satisfied. --------------- Formula: ((false R ! iB) | (true U (iB & (true U oV)))) "output V occurs after input B" Formula is not satisfied! An error path is [iF, oW, iA, oY, iB] ([oU, iC, oY, iD, oU, iA, oU, iF, iB, oY, iB])* --------------- 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 [iF, oW, iA, oY, iB, oU, iD] ([oW, iE, oU, iA, oW, iB, oU, iD])* --------------- Formula: (false R (! oY | (true U oU))) "output U responds to output Y" Formula is not satisfied! An error path is [iF, oW, iA, oY, iB, oU, iD, oW, iC, oY] ([iD, oY, iB, oY])* --------------- Formula: (! (true U oZ) | (! oU U (oX | oZ))) "output X precedes output U before output Z" 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 ! oV) "output V does never occur" Formula is satisfied. --------------- Formula: (false R (! ((iE & ! iF) & (true U iF)) | (! oV U iF))) "output V does never occur between input E and input F" Formula is satisfied. --------------- Formula: (true U oU) "output U occurs eventually" Formula is not satisfied! An error path is [iA, oW, iF, oY, iA, oW, iC, oW, iF, oW, iC, oY, iC, oY] ([iD, oW])* --------------- 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, oW, iF, oY, iA] ([oW, iB, oU, iB, oU, iD, oW, iB, oU, iC, oW, iF, oY, iB, oW, iD, oW, iD, oU, iF, oY, iA])* --------------- Formula: (false R (! iB | (true U oU))) "output U responds to input B" Formula is not satisfied! An error path is [iF, oW, iD, oY, iC, oW, iF, oU, iD, oY, iB, oY] ([iC, iC, oY])* --------------- Formula: (false R (! ((oU & ! oZ) & (true U oZ)) | (! oW U oZ))) "output W does never occur between output U and output Z" 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 oV) "output V occurs eventually" Formula is not satisfied! An error path is [iA, oW] ([iF, oY, iC, oW, iF, oY, iB, oW, iD, oW, iD, oU])* --------------- Formula: (true U oX) "output X occurs eventually" Formula is not satisfied! An error path is [iA, oW] ([iF, oY, iC, oW, iF, oY, iB, oW, iD, oW, iD, oU])* --------------- Formula: (false R (! (oZ & ! iA) | (! iA U (oV & ! iA)))) "output V occurs after output Z until input A" Formula is satisfied. --------------- Formula: (false R (! (oX & ! oV) | (! oV WU (oY & ! oV)))) "output Y occurs between output X and output V" Formula is satisfied. --------------- Formula: (false R (! (iB & ! oV) | (! oX WU oV))) "output X does never occur after input B until output V" Formula is satisfied. --------------- 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 [iF, oW, iA, oY, iB, oU, iE] ([oU, iF, oY, iB, oW, iF, iE])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iA, oW, iF, oY] ([iA, oW, iB, oU, iB, oU, iD, oW, iB, oU])* --------------- Formula: ((false R ! oU) | (true U (oU & (true U oV)))) "output V occurs after output U" Formula is not satisfied! An error path is [iF, oW, iA, oY, iB, oU] ([iD, oW, iC, oY, iD, oY, iC])* --------------- 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, oW] ([iF, oY, iC, oW, iF, oY, iB, oW, iD, oW, iD, oU])* --------------- Formula: (false R (! (iE & ! iB) | (! iB WU (oV & ! iB)))) "output V occurs between input E and input B" Formula is not satisfied! An error path is [iF, oW, iA, oY, iB, oU, iE, oU, iB] ([oW, iD, oY, iB, oU, iE, oU, iB])* --------------- Formula: (false R (! (iC & ! iA) | (! oW WU iA))) "output W does never occur after input C until input A" Formula is not satisfied! An error path is [iA, oW, iF, oY, iC, oW] ([iD, oU, iB, oU, iA, oW, iF, oU])* --------------- Formula: ((false R ! iC) | (true U (iC & (true U oY)))) "output Y occurs after input C" Formula is not satisfied! An error path is [iA, oW, iF, oY, iC, oW] ([iD, oU, iB, oU, iA, oW, iF, oU])* --------------- Formula: (false R (! iB | (true U oX))) "output X responds to input B" Formula is not satisfied! An error path is [iF, oW, iA, oY, iB] ([oU, iC, oY, iD, oU, iA, oU, iF, iB, oY, iB])* --------------- Formula: (false R (! ((oX & ! oW) & (true U oW)) | (! oV U oW))) "output V does never occur between output X and output W" Formula is satisfied. --------------- Formula: (! oU WU iC) "input C precedes output U" Formula is not satisfied! An error path is [iF, oW, iA, oY, iB, oU] ([iD, oW, iC, oY, iD, oY, iC])* --------------- Formula: (false R (! ((oZ & ! iB) & (true U iB)) | (! oU U iB))) "output U does never occur between output Z and input B" Formula is satisfied. --------------- Formula: (! (true U oX) | ((! oW & ! oX) U (oX | ((oW & ! oX) U (oX | ((! oW & ! oX) U (oX | ((oW & ! oX) U (oX | (! oW U oX)))))))))) "output W occurs at most twice before output X" Formula is satisfied. --------------- Formula: (false R ! oU) "output U does never occur" Formula is not satisfied! An error path is [iF, oW, iA, oY, iB, oU] ([iD, oW, iC, oY, iD, oY, iC])* --------------- Formula: (! (true U oX) | (! oW U (oU | oX))) "output U precedes output W before output X" Formula is satisfied. --------------- Formula: (! (true U iE) | (! oY U (oV | iE))) "output V precedes output Y before input E" Formula is not satisfied! An error path is [iF, oW, iA, oY, iB, oU, iE] ([oU, iF, oY, iB, oW, iF, iE])* --------------- Formula: (false R (! ((iB & ! oZ) & (true U oZ)) | (! oV U oZ))) "output V does never occur between input B and output Z" Formula is satisfied. --------------- 27 constraints satisfied, 23 unsatisfied.