Reachability problems: =============================== error_45 reachable via input sequence [B, D, C, E, E, C, D, A] --------------- error_27 reachable via input sequence [B, D, C, E, E, C, A, A] --------------- error_20 reachable via input sequence [B, D, C, E, E, A, A, A] --------------- error_34 reachable via input sequence [B, D, C, E, E, A, F, A] --------------- error_57 reachable via input sequence [B, D, C, A, B, B, D, A] --------------- error_19 reachable via input sequence [B, D, C, A, B, B, E, A] --------------- error_9 reachable via input sequence [B, D, C, A, B, B, A, A] --------------- error_39 reachable via input sequence [B, D, C, C, D, C, D, A] --------------- error_35 reachable via input sequence [B, D, C, C, D, C, C, A] --------------- error_31 reachable via input sequence [B, D, C, C, D, C, A, A] --------------- error_3 reachable via input sequence [B, D, E, A, E, D, E, A] --------------- error_55 reachable via input sequence [B, D, E, A, E, D, F, A] --------------- error_33 reachable via input sequence [B, D, E, A, A, D, E, A] --------------- error_25 reachable via input sequence [B, D, E, A, A, D, F, A] --------------- error_8 reachable via input sequence [B, E, D, A, A, E, D, A] --------------- error_49 reachable via input sequence [B, E, D, A, A, E, F, A] --------------- error_6 reachable via input sequence [B, E, D, E, B, A, B, A] --------------- error_1 reachable via input sequence [B, E, D, E, B, A, E, A] --------------- error_36 reachable via input sequence [B, E, D, E, B, A, C, A] --------------- error_32 reachable via input sequence [B, E, D, E, B, A, F, A] --------------- error_52 reachable via input sequence [B, E, D, C, C, A, B, A] --------------- error_12 reachable via input sequence [B, E, D, C, C, A, D, A] --------------- error_10 reachable via input sequence [B, E, D, C, C, A, C, A] --------------- error_0 reachable via input sequence [B, E, D, C, C, A, A, A] --------------- error_38 reachable via input sequence [B, E, D, C, C, A, F, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (false R (! (iE & ! iF) | (! iF WU (oW & ! iF)))) "output W occurs between input E and input F" Formula is satisfied. --------------- Formula: (false R (! oW | (false R ! oZ))) "output Z does never occur after output W" Formula is satisfied. --------------- Formula: (! (true U oW) | (! oY U (iB | oW))) "input B precedes output Y before output W" Formula is satisfied. --------------- Formula: (false R ! oX) "output X does never occur" Formula is satisfied. --------------- Formula: (! oW WU oY) "output Y precedes output W" Formula is satisfied. --------------- Formula: (! (true U iA) | ((! oU & ! iA) U (iA | ((oU & ! iA) U (iA | ((! oU & ! iA) U (iA | ((oU & ! iA) U (iA | (! oU U iA)))))))))) "output U occurs at most twice before input A" Formula is not satisfied! An error path is [iB, oY, iE, oU, iD, oV, iE, oU, iC, oZ, iE, oU, iE, iA] ([iE, oY, iD, oY, iC, oV])* --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iB, oY] ([iD, oU, iC, oZ, iA, oZ, iB, oY, iC, oU, iA, oY])* --------------- Formula: (false R (! ((iA & ! iF) & (true U iF)) | (! oV U iF))) "output V does never occur between input A and input F" Formula is not satisfied! An error path is [iB, oY, iD, oU, iC, oZ, iF, oY, iF, oY, iC, oU, iA, oZ, iD, oY, iB, oV, iF] ([oU, iD, oY, iF])* --------------- Formula: (false R (! (iA & ! oU) | (! oU WU (oV & ! oU)))) "output V occurs between input A and output U" Formula is not satisfied! An error path is [iB, oY, iD, oU, iE, oV, iA, oU] ([iD, oZ, iC, oU, iC])* --------------- Formula: (! oV WU iD) "output V does never occur before input D" Formula is satisfied. --------------- Formula: (! oX WU oV) "output V precedes output X" Formula is satisfied. --------------- Formula: (false R ! oV) "output V does never occur" Formula is not satisfied! An error path is [iB, oY, iD, oU, iE, oV] ([iA, oU, iA, oV, iA, oU, iA])* --------------- Formula: (! (true U iF) | ((! oY & ! iF) U (iF | ((oY & ! iF) U (iF | ((! oY & ! iF) U (iF | ((oY & ! iF) U (iF | (! oY U iF)))))))))) "output Y occurs at most twice before input F" Formula is not satisfied! An error path is [iB, oY, iD, oU, iC, oZ, iC, oV, iD, oY, iB, oU, iA, oY, iF] ([oY, iF, oY, iD, oY, iC, oU, iF])* --------------- Formula: (false R (! (iE & ! iA) | (! iA U (oU & ! iA)))) "output U occurs after input E until input A" Formula is not satisfied! An error path is [iB, oY, iD, oU, iE, oV] ([iB, oZ, iE, oV, iC, oZ, iE, oY, iC, iE, oZ, iB, iD, oV])* --------------- Formula: (! (true U oZ) | (! oU U (iE | oZ))) "input E precedes output U before output Z" Formula is not satisfied! An error path is [iB, oY, iD, oU, iC, oZ] ([iC, oV, iD, oY, iB, oU, iA, oY])* --------------- Formula: (false R (! ((iB & ! oW) & (true U oW)) | (! oU U oW))) "output U does never occur between input B and output W" Formula is satisfied. --------------- Formula: (! (true U oX) | (! oZ U (iB | oX))) "input B precedes output Z before output X" Formula is satisfied. --------------- Formula: (! (true U iC) | (! oV U (iA | iC))) "input A precedes output V before input C" Formula is not satisfied! An error path is [iB, oY, iE, oU, iD, oV, iC] ([oZ, iC, oV, iE, oV, iD, iC])* --------------- Formula: (false R (! (oV & ! iC) | (! iC WU (oU & ! iC)))) "output U occurs between output V and input C" Formula is not satisfied! An error path is [iB, oY, iE, oU, iD, oV, iC] ([oZ, iC, oV, iE, oV, iD, iC])* --------------- 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 & ! oU) | (! oU U (oW & ! oU)))) "output W occurs after input B until output U" Formula is not satisfied! An error path is [iB, oY] ([iD, oU, iC, oZ, iA, oZ, iB, oY, iC, oU, iA, oY])* --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iB, oY, iE, oU] ([iD, oV, iA, oU, iA, oV, iC, oU, iD])* --------------- Formula: (false R ! oW) "output W does never occur" Formula is satisfied. --------------- Formula: (! oZ WU oX) "output Z does never occur before output X" Formula is not satisfied! An error path is [iB, oY, iD, oU, iC, oZ] ([iC, oV, iD, oY, iB, oU, iA, oY])* --------------- Formula: (! (true U iC) | (! oY U (iB | iC))) "input B precedes output Y before input C" Formula is satisfied. --------------- Formula: (false R (! (iF & ! oZ) | (! oZ WU (oX & ! oZ)))) "output X occurs between input F and output Z" Formula is not satisfied! An error path is [iB, oY, iD, oU, iC, oZ, iA, oZ, iB, oY, iF, oZ] ([iD, oV, iF, oZ])* --------------- Formula: (false R (! (oU & ! oW) | (! oZ WU oW))) "output Z does never occur after output U until output W" Formula is not satisfied! An error path is [iB, oY, iD, oU, iC, oZ] ([iC, oV, iD, oY, iB, oU, iA, oY])* --------------- Formula: (! (true U oX) | (! oU U (iE | oX))) "input E precedes output U before output X" Formula is satisfied. --------------- Formula: (! oY WU oV) "output V precedes output Y" Formula is not satisfied! An error path is [iB, oY] ([iD, oU, iC, oZ, iA, oZ, iB, oY, iC, oU, iA, oY])* --------------- Formula: (false R (! ((iE & ! iD) & (true U iD)) | (! oW U iD))) "output W does never occur between input E and input D" Formula is satisfied. --------------- Formula: (false R (! ((iE & ! oX) & (true U oX)) | (! oY U oX))) "output Y does never occur between input E and output X" 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: (false R (! ((iC & ! iB) & (true U iB)) | (! oV U iB))) "output V does never occur between input C and input B" Formula is not satisfied! An error path is [iB, oY, iD, oU, iC, oZ, iC, oV, iD, oY, iB] ([oU, iA, oY, iC, oV, iD, oY, iB])* --------------- Formula: (false R ! oV) "output V does never occur" Formula is not satisfied! An error path is [iB, oY, iD, oU, iE, oV] ([iA, oU, iA, oV, iA, oU, iA])* --------------- Formula: (false R (! oU | (false R ! oW))) "output W does never occur after output U" Formula is satisfied. --------------- Formula: (false R (! oX | (true U oY))) "output Y responds to output X" Formula is satisfied. --------------- Formula: (false R (! ((oW & ! oU) & (true U oU)) | (! oX U oU))) "output X does never occur between output W and output U" Formula is satisfied. --------------- Formula: ((false R ! oV) | (true U (oV & (true U oY)))) "output Y occurs after output V" Formula is not satisfied! An error path is [iB, oY, iD, oU, iE, oV] ([iA, oU, iA, oV, iA, oU, iA])* --------------- Formula: (! oX WU (oZ & ! oX)) "output Z occurs before output X" Formula is satisfied. --------------- Formula: (false R ! oW) "output W does never occur" Formula is satisfied. --------------- Formula: (false R (! oY | (false R ! oX))) "output X does never occur after output Y" Formula is satisfied. --------------- Formula: (! oY WU oV) "output V precedes output Y" Formula is not satisfied! An error path is [iB, oY] ([iD, oU, iC, oZ, iA, oZ, iB, oY, iC, oU, iA, oY])* --------------- Formula: (false R (! (iA & ! iE) | (! iE U (oU & ! iE)))) "output U occurs after input A until input E" Formula is not satisfied! An error path is [iB, oY, iD, oU, iC, oZ, iA] ([oZ, iB, oY, iF, oZ, iA, oY, iA])* --------------- Formula: (false R ! oX) "output X does never occur" Formula is satisfied. --------------- Formula: (false R (! ((oX & ! iF) & (true U iF)) | (! oZ U iF))) "output Z does never occur between output X and input F" Formula is satisfied. --------------- Formula: (false R (! (iA & ! iD) | (! oY WU iD))) "output Y does never occur after input A until input D" Formula is not satisfied! An error path is [iB, oY, iD, oU, iE, oV, iB, oZ, iA, oY] ([iE, oU, iC, oV, iD, oV, iB, oZ, iA, oY])* --------------- Formula: (false R (! (oY & ! iE) | (! iE WU (oU & ! iE)))) "output U occurs between output Y and input E" Formula is not satisfied! An error path is [iB, oY, iE, oU] ([iD, oV, iD, oY, iD, oY, iE, oZ, iD])* --------------- Formula: (! (true U iB) | ((! oZ & ! iB) U (iB | ((oZ & ! iB) U (iB | ((! oZ & ! iB) U (iB | ((oZ & ! iB) U (iB | (! oZ U iB)))))))))) "output Z occurs at most twice before input B" Formula is satisfied. --------------- Formula: (false R (! (iB & ! oW) | (! oX WU oW))) "output X does never occur after input B until output W" Formula is satisfied. --------------- Formula: (false R (! (iC & ! iD) | (! oZ WU iD))) "output Z does never occur after input C until input D" Formula is not satisfied! An error path is [iB, oY, iD, oU, iC, oZ] ([iC, oV, iD, oY, iB, oU, iA, oY])* --------------- 26 constraints satisfied, 24 unsatisfied.