Reachability problems: =============================== error_4 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, A, A] --------------- error_52 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, F, A] --------------- error_44 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, E, A] --------------- error_20 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, D, A] --------------- error_54 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, F, A] --------------- error_1 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, E, A] --------------- error_33 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, B, A] --------------- error_37 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, A, A] --------------- error_0 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, D, A] --------------- error_15 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, B, A] --------------- error_41 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, C, A] --------------- error_22 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, C, A, A] --------------- error_51 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, C, B, A] --------------- error_30 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, C, C, A] --------------- error_14 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, A, D, A] --------------- error_5 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, A, E, A] --------------- error_43 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, E, A, A] --------------- error_6 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, E, D, A] --------------- error_38 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, E, F, A] --------------- error_27 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, E, B, A] --------------- error_46 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, F, E, A] --------------- error_8 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, D, F, C, A] --------------- error_3 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, C, D, A, A] --------------- error_18 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, C, D, E, A] --------------- error_31 reachable via input sequence [D, A, A, C, D, E, B, B, F, B, A, B, C, D, B, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (false R (! (oW & ! iD) | (! iD U (oY & ! iD)))) "output Y occurs after output W until input D" Formula is satisfied. --------------- Formula: (false R (! iF | (true U oV))) "output V responds to input F" Formula is satisfied. --------------- Formula: (! oY WU iF) "input F precedes output Y" Formula is satisfied. --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is satisfied. --------------- Formula: (! oX WU iD) "input D precedes output X" Formula is satisfied. --------------- Formula: (! (true U oY) | (! oU U (iE | oY))) "input E precedes output U before output Y" Formula is not satisfied! An error path is [iA, oV, iF, oU, iC, oV, iE, oZ, iF, oZ, iB, oZ, iA, oY] ([iC, oV, iD])* --------------- Formula: (! (true U iC) | ((! oY & ! iC) U (iC | ((oY & ! iC) U (iC | ((! oY & ! iC) U (iC | ((oY & ! iC) U (iC | (! oY U iC)))))))))) "output Y occurs at most twice before input C" Formula is not satisfied! An error path is [iA, oV, iE, oU, iB, oZ, iF, oY, iF, oV, iE, oY, iF, oV, iE, oY, iF, oV, iC] ([oY, iF, oV, iC])* --------------- Formula: (! (true U iE) | (! oY U (oW | iE))) "output W precedes output Y before input E" Formula is satisfied. --------------- Formula: (false R (! ((oX & ! iF) & (true U iF)) | (! oV U iF))) "output V does never occur between output X and input F" Formula is not satisfied! An error path is [iD, oU, iF, oV, iF, oX, iC, oZ, iA, oV, iF] ([iA, oV, 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 [iA, oV, iF, oU, iC, oV, iE, oZ, iF, oZ, iB] ([oZ, iA, oY, iC, oV, iF, iB])* --------------- Formula: (false R (! (iC & ! oV) | (! oW WU oV))) "output W does never occur after input C until output V" Formula is satisfied. --------------- Formula: (false R (! ((oX & ! iB) & (true U iB)) | (! oY U iB))) "output Y does never occur between output X and input B" Formula is satisfied. --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iA, oV, iE, oU, iB, oZ, iF, oY] ([iF, oV, iE, oY])* --------------- Formula: (true U oU) "output U occurs eventually" Formula is satisfied. --------------- Formula: (false R ! oW) "output W does never occur" Formula is satisfied. --------------- Formula: (false R (! ((iF & ! oY) & (true U oY)) | (! oV U oY))) "output V does never occur between input F and output Y" Formula is not satisfied! An error path is [iA, oV, iE, oU, iB, oZ, iF, oY, iF, oV, iE, oY] ([iF, oV, iE, oY])* --------------- Formula: (false R ! oW) "output W does never occur" Formula is satisfied. --------------- Formula: (! oY WU iC) "input C precedes output Y" Formula is not satisfied! An error path is [iA, oV, iE, oU, iB, oZ, iF, oY] ([iF, oV, iE, oY])* --------------- Formula: (false R (! ((oU & ! oV) & (true U oV)) | (! oW U oV))) "output W does never occur between output U and output V" Formula is satisfied. --------------- Formula: (false R (! iB | (true U oY))) "output Y responds to input B" Formula is not satisfied! An error path is [iD, oU, iF, oV, iF, oX, iC, oZ, iC, oV, iB] ([iB])* --------------- Formula: ((false R ! iD) | (true U (iD & (true U oV)))) "output V occurs after input D" Formula is satisfied. --------------- Formula: (false R (! (iF & ! iC) | (! oU WU iC))) "output U does never occur after input F until input C" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ, iA, oU] ([iA, oU])* --------------- Formula: (false R (! ((iA & ! oZ) & (true U oZ)) | (! oU U oZ))) "output U does never occur between input A and output Z" Formula is not satisfied! An error path is [iA, oV, iE, oU, iB, oZ, iF, oY] ([iF, oV, iE, oY])* --------------- 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 ! oU) "output U does never occur" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ] ([iA, oU])* --------------- Formula: (false R (! ((iC & ! oY) & (true U oY)) | (! oX U oY))) "output X does never occur between input C and output Y" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! iA) | (! iA U (oY & ! iA)))) "output Y occurs after output Z until input A" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ] ([iA, oU])* --------------- Formula: (false R (! (iB & ! oX) | (! oX U (oY & ! oX)))) "output Y occurs after input B until output X" Formula is not satisfied! An error path is [iD, oU, iF, oV, iF, oX, iC, oZ, iC, oV, iB] ([iB])* --------------- Formula: (! oX WU (oZ & ! oX)) "output Z occurs before output X" Formula is not satisfied! An error path is [iD, oU, iF, oV, iF, oX, iC, oZ] ([iA, oV, iF])* --------------- Formula: (false R (! ((iC & ! iE) & (true U iE)) | (! oV U iE))) "output V does never occur between input C and input E" Formula is not satisfied! An error path is [iA, oV, iF, oU, iC, oV, iE, oZ, iF, oZ] ([iB, oZ, iA, oY, iC, oV, iF])* --------------- Formula: (false R (! (iF & ! iA) | (! oV WU iA))) "output V does never occur after input F until input A" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ] ([iA, oU])* --------------- Formula: (false R (! (oW & ! iD) | (! oV WU iD))) "output V does never occur after output W until input D" Formula is satisfied. --------------- Formula: (! oU WU (oY & ! oU)) "output Y occurs before output U" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ] ([iA, oU])* --------------- Formula: (! oY WU iB) "input B precedes output Y" 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: (! (true U iE) | ((! oW & ! iE) U (iE | ((oW & ! iE) U (iE | ((! oW & ! iE) U (iE | ((oW & ! iE) U (iE | (! oW U iE)))))))))) "output W occurs at most twice before input E" Formula is satisfied. --------------- Formula: (false R (! (iB & ! oX) | (! oX WU (oW & ! oX)))) "output W occurs between input B and output X" Formula is not satisfied! An error path is [iD, oU, iF, oV, iF, oX, iC, oZ, iA, oV, iB, oU, iE, oX] ([iA, oU])* --------------- Formula: (false R (! (oX & ! oU) | (! oU U (oY & ! oU)))) "output Y occurs after output X until output U" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ, iE, oX] ([iA, oU])* --------------- Formula: ((false R ! oZ) | (true U (oZ & (true U oY)))) "output Y occurs after output Z" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ] ([iA, oU])* --------------- Formula: (false R (! ((iA & ! oX) & (true U oX)) | (! oV U oX))) "output V does never occur between input A and output X" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ, iF, oV, iE, oU, iE, oX] ([iA, oU])* --------------- Formula: ((false R ! oU) | (true U (oU & (true U oY)))) "output Y occurs after output U" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ] ([iA, oU])* --------------- Formula: (false R (! oX | (false R ! oU))) "output U does never occur after output X" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ, iE, oX, iA, oU] ([iA, oU])* --------------- 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 not satisfied! An error path is [iD, oU, iF, oV, iF, oX, iC, oZ, iC, oV, iE, iE, oU, iE, oX, iE, oX, iA] ([oU, iA])* --------------- Formula: (! oU WU (oY & ! oU)) "output Y occurs before output U" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ] ([iA, oU])* --------------- Formula: (false R (! oW | (true U oZ))) "output Z responds to output W" Formula is satisfied. --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is satisfied. --------------- Formula: (false R (! (iE & ! oY) | (! oY U (oX & ! oY)))) "output X occurs after input E until output Y" Formula is not satisfied! An error path is [iA, oV, iE, oU, iB, oZ, iF, oY] ([iF, oV, iE, oY])* --------------- 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 (! (iF & ! oV) | (! oV WU (oZ & ! oV)))) "output Z occurs between input F and output V" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ] ([iA, oU])* --------------- Formula: (! iD WU (oX & ! iD)) "output X occurs before input D" Formula is not satisfied! An error path is [iD, oU, iF, oV, iA, oZ] ([iA, oU])* --------------- 22 constraints satisfied, 28 unsatisfied.