Reachability problems: =============================== error_30 reachable via input sequence [B, F, C, B, A] --------------- error_21 reachable via input sequence [B, F, C, D, A] --------------- error_51 reachable via input sequence [B, F, F, D, A] --------------- error_58 reachable via input sequence [B, F, B, B, A] --------------- error_23 reachable via input sequence [B, F, B, D, A] --------------- error_11 reachable via input sequence [B, C, F, C, A] --------------- error_54 reachable via input sequence [B, C, F, D, A] --------------- error_44 reachable via input sequence [B, C, E, C, A] --------------- error_7 reachable via input sequence [B, B, C, B, A] --------------- error_16 reachable via input sequence [B, B, F, C, A] --------------- error_4 reachable via input sequence [C, B, F, F, A] --------------- error_19 reachable via input sequence [C, F, B, C, A] --------------- error_43 reachable via input sequence [C, F, B, D, A] --------------- error_35 reachable via input sequence [C, C, D, F, A] --------------- error_48 reachable via input sequence [C, C, E, D, A] --------------- error_40 reachable via input sequence [F, B, B, F, A] --------------- error_24 reachable via input sequence [F, B, B, D, A] --------------- error_6 reachable via input sequence [F, B, C, C, A] --------------- error_45 reachable via input sequence [F, C, D, F, A] --------------- error_32 reachable via input sequence [F, C, D, D, A] --------------- error_36 reachable via input sequence [F, C, E, F, A] --------------- error_12 reachable via input sequence [F, D, D, C, A] --------------- error_25 reachable via input sequence [F, F, B, E, A] --------------- error_29 reachable via input sequence [F, F, F, D, A] --------------- error_28 reachable via input sequence [F, F, F, E, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (! oU WU iF) "output U does never occur before input F" Formula is satisfied. --------------- Formula: (false R (! (iE & ! iA) | (! iA WU (oW & ! iA)))) "output W occurs between input E and input A" Formula is satisfied. --------------- Formula: (! oY WU iF) "output Y does never occur before input F" Formula is satisfied. --------------- Formula: (! (true U oW) | ((! oY & ! oW) U (oW | ((oY & ! oW) U (oW | ((! oY & ! oW) U (oW | ((oY & ! oW) U (oW | (! oY U oW)))))))))) "output Y occurs at most twice before output W" Formula is satisfied. --------------- Formula: (! oZ WU iA) "output Z does never occur before input A" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (false R (! ((iC & ! iE) & (true U iE)) | (! oY U iE))) "output Y does never occur between input C and input E" Formula is satisfied. --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iF, oX, iB, oZ])* --------------- Formula: (false R (! iB | (false R ! oZ))) "output Z does never occur after input B" Formula is not satisfied! An error path is [iB, oV, iF, oZ] ([iB, oZ, iC, oV])* --------------- Formula: (! (true U iB) | (! oX U (oW | iB))) "output W precedes output X before input B" Formula is not satisfied! An error path is [iC, oZ, iC, oX, iB] ([oZ, iB, oV, iF, iB, iB])* --------------- Formula: (! iD WU (oU & ! iD)) "output U occurs before input D" Formula is not satisfied! An error path is [iB, oV, iD] ([oX, iC, oX, iC, oZ, iD])* --------------- Formula: (! oU WU (oU WU (! oU WU (oU WU (false R ! oU))))) "output U occurs at most twice" Formula is satisfied. --------------- Formula: (! iB WU (oY & ! iB)) "output Y occurs before input B" Formula is not satisfied! An error path is [iB, oV] ([iB, oX, iC, oX, iC, oZ])* --------------- Formula: (false R (! (oX & ! iF) | (! oZ WU iF))) "output Z does never occur after output X until input F" Formula is not satisfied! An error path is [iC, oZ, iC, oX, iB, oZ] ([iD, oX])* --------------- Formula: ((false R ! oX) | (true U (oX & (true U oY)))) "output Y occurs after output X" Formula is not satisfied! An error path is [iB, oV, iB, oX] ([iC, oX, iD, oV])* --------------- Formula: (! (true U iF) | (! oW U (oY | iF))) "output Y precedes output W before input F" Formula is satisfied. --------------- Formula: (! oW WU oU) "output W does never occur before output U" Formula is satisfied. --------------- Formula: (false R (! iB | (true U oU))) "output U responds to input B" Formula is not satisfied! An error path is [iB, oV] ([iB, oX, iC, oX, iC, oZ])* --------------- Formula: ((false R ! iB) | (true U (iB & (true U oW)))) "output W occurs after input B" Formula is not satisfied! An error path is [iB, oV] ([iB, oX, iC, oX, iC, oZ])* --------------- Formula: (false R (! oU | (false R ! oZ))) "output Z does never occur after output U" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iE) | (! iE U (oV & ! iE)))) "output V occurs after input B until input E" Formula is not satisfied! An error path is [iB, oV, iB] ([oX, iC, oX, iC, oZ, iB])* --------------- Formula: (! (true U oW) | ((! oY & ! oW) U (oW | ((oY & ! oW) U (oW | ((! oY & ! oW) U (oW | ((oY & ! oW) U (oW | (! oY U oW)))))))))) "output Y occurs at most twice before output W" Formula is satisfied. --------------- Formula: (false R (! (iD & ! iC) | (! iC U (oW & ! iC)))) "output W occurs after input D until input C" Formula is not satisfied! An error path is [iB, oV, iD] ([oX, iC, oX, iC, oZ, iD])* --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iF, oX, iB, oZ])* --------------- Formula: (! oZ WU (oV & ! oZ)) "output V occurs before output Z" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (false R (! (oW & ! iC) | (! iC WU (oV & ! iC)))) "output V occurs between output W and input C" Formula is satisfied. --------------- Formula: (false R (! ((oY & ! iD) & (true U iD)) | (! oW U iD))) "output W does never occur between output Y and input D" Formula is satisfied. --------------- Formula: (false R (! ((oW & ! oV) & (true U oV)) | (! oY U oV))) "output Y does never occur between output W and output V" Formula is satisfied. --------------- Formula: (! iC WU (oX & ! iC)) "output X occurs before input C" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (false R (! ((iE & ! iA) & (true U iA)) | (! oU U iA))) "output U does never occur between input E and input A" Formula is satisfied. --------------- Formula: (false R (! (oW & ! oV) | (! oX WU oV))) "output X does never occur after output W until output V" Formula is satisfied. --------------- Formula: (false R (! (iE & ! iC) | (! iC U (oW & ! iC)))) "output W occurs after input E until input C" Formula is not satisfied! An error path is [iC, oZ, iE] ([oZ, iB, oZ, iB, oZ, iE])* --------------- Formula: (false R (! oZ | (true U oU))) "output U responds to output Z" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (false R (! oZ | (true U oV))) "output V responds to output Z" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iF, oX, iB, oZ])* --------------- Formula: ((false R ! oZ) | (true U (oZ & (true U oU)))) "output U occurs after output Z" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (! oU WU oZ) "output Z precedes output U" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iC) | (! oU WU iC))) "output U does never occur after input B until input C" Formula is satisfied. --------------- Formula: (! (true U iF) | ((! oZ & ! iF) U (iF | ((oZ & ! iF) U (iF | ((! oZ & ! iF) U (iF | ((oZ & ! iF) U (iF | (! oZ U iF)))))))))) "output Z occurs at most twice before input F" Formula is not satisfied! An error path is [iC, oZ, iB, oZ, iD, oZ, iF] ([oZ, iB, iC, oZ, iE, oX, iC, iF, iB, oZ, iD, oZ, iF])* --------------- Formula: (! oW WU (oW WU (! oW WU (oW WU (false R ! oW))))) "output W occurs at most twice" Formula is satisfied. --------------- Formula: (! (true U oU) | (! oZ U (oV | oU))) "output V precedes output Z before output U" Formula is satisfied. --------------- Formula: (false R (! (oX & ! oW) | (! oZ WU oW))) "output Z does never occur after output X until output W" Formula is not satisfied! An error path is [iC, oZ, iC, oX, iB, oZ] ([iD, oX])* --------------- Formula: (false R ! oU) "output U does never occur" Formula is satisfied. --------------- Formula: (false R ! oZ) "output Z does never occur" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- 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 satisfied. --------------- Formula: (! iB WU (oX & ! iB)) "output X occurs before input B" Formula is not satisfied! An error path is [iB, oV] ([iB, oX, iC, oX, iC, oZ])* --------------- Formula: (! oZ WU iB) "input B precedes output Z" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (true U oX) "output X occurs eventually" Formula is not satisfied! An error path is [iB, oV] ([iF, oZ, iF, oV, iC, oZ])* --------------- Formula: (! oV WU oZ) "output Z precedes output V" Formula is not satisfied! An error path is [iB, oV] ([iB, oX, iC, oX, iC, oZ])* --------------- Formula: (! oW WU (oU & ! oW)) "output U occurs before output W" 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 [iF, oV] ([iB, oZ, iB, oX, iB])* --------------- 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, oV] ([iB, oZ, iB, oX, iB])* --------------- Formula: (false R (! oV | (true U oX))) "output X responds to output V" Formula is not satisfied! An error path is [iB, oV] ([iF, oZ, iF, oV, iC, oZ])* --------------- Formula: (! oW WU (oW WU (! oW WU (oW WU (false R ! oW))))) "output W occurs at most twice" Formula is satisfied. --------------- Formula: (false R (! iA | (false R ! oV))) "output V does never occur after input A" Formula is satisfied. --------------- Formula: (! (true U iF) | (! oU U (oX | iF))) "output X precedes output U before input F" Formula is satisfied. --------------- Formula: (false R ! oY) "output Y does never occur" Formula is satisfied. --------------- Formula: (! (true U iD) | ((! oY & ! iD) U (iD | ((oY & ! iD) U (iD | ((! oY & ! iD) U (iD | ((oY & ! iD) U (iD | (! oY U iD)))))))))) "output Y occurs at most twice before input D" Formula is satisfied. --------------- Formula: (! oZ WU oW) "output Z does never occur before output W" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (false R (! iC | (false R ! oY))) "output Y does never occur after input C" Formula is satisfied. --------------- Formula: (false R (! (iA & ! iC) | (! iC WU (oY & ! iC)))) "output Y occurs between input A and input C" Formula is satisfied. --------------- Formula: (false R (! iD | (true U oW))) "output W responds to input D" Formula is not satisfied! An error path is [iB, oV, iD] ([oX, iC, oX, iC, oZ, iD])* --------------- Formula: (false R (! oY | (true U oU))) "output U responds to output Y" Formula is satisfied. --------------- Formula: (! (true U iC) | (! oU U (iD | iC))) "input D precedes output U before input C" Formula is satisfied. --------------- Formula: (false R (! (iA & ! oV) | (! oY WU oV))) "output Y does never occur after input A until output V" Formula is satisfied. --------------- Formula: ((false R ! oV) | (true U (oV & (true U oX)))) "output X occurs after output V" Formula is not satisfied! An error path is [iB, oV] ([iF, oZ, iF, oV, iC, oZ])* --------------- Formula: (false R (! (iD & ! oV) | (! oV WU (oU & ! oV)))) "output U occurs between input D and output V" Formula is not satisfied! An error path is [iF, oV, iD, oV] ([iF, oX, iD])* --------------- Formula: (! iA WU (oY & ! iA)) "output Y occurs before input A" Formula is satisfied. --------------- Formula: (false R (! (iF & ! oZ) | (! oW WU oZ))) "output W does never occur after input F until output Z" Formula is satisfied. --------------- Formula: (false R ! oY) "output Y does never occur" Formula is satisfied. --------------- Formula: ((false R ! iA) | (true U (iA & (true U oY)))) "output Y occurs after input A" Formula is satisfied. --------------- Formula: (! oZ WU oX) "output Z does never occur before output X" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (false R (! (iE & ! iF) | (! iF WU (oV & ! iF)))) "output V occurs between input E and input F" Formula is not satisfied! An error path is [iC, oZ, iE, oZ, iF] ([oX, iE, oZ, iF, iE, oZ, iF])* --------------- Formula: (false R ! oX) "output X does never occur" Formula is not satisfied! An error path is [iB, oV, iB, oX] ([iC, oX, iD, oV])* --------------- Formula: (true U oW) "output W occurs eventually" Formula is not satisfied! An error path is [iB, oV] ([iB, oX, iC, oX, iC, oZ])* --------------- Formula: (false R (! iE | (false R ! oY))) "output Y does never occur after input E" Formula is satisfied. --------------- Formula: (! oZ WU (oV & ! oZ)) "output V occurs before output Z" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (! oW WU oV) "output V precedes output W" Formula is satisfied. --------------- Formula: (false R (! (oU & ! iC) | (! iC WU (oV & ! iC)))) "output V occurs between output U and input C" Formula is satisfied. --------------- Formula: (! iD WU (oX & ! iD)) "output X occurs before input D" Formula is not satisfied! An error path is [iB, oV, iD] ([oX, iC, oX, iC, oZ, iD])* --------------- Formula: ((false R ! iF) | (true U (iF & (true U oY)))) "output Y occurs after input F" Formula is not satisfied! An error path is [iF, oV] ([iB, oZ, iB, oX, iB])* --------------- Formula: (false R (! ((oZ & ! iA) & (true U iA)) | (! oY U iA))) "output Y does never occur between output Z and input A" Formula is satisfied. --------------- Formula: (true U oX) "output X occurs eventually" Formula is not satisfied! An error path is [iB, oV] ([iF, oZ, iF, oV, iC, oZ])* --------------- Formula: (! oV WU oU) "output V does never occur before output U" Formula is not satisfied! An error path is [iB, oV] ([iB, oX, iC, oX, iC, oZ])* --------------- 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: (! 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 [iC, oZ, iB] ([oZ, iB, oV, iB, oZ, iE, iF, iB])* --------------- Formula: (false R ! oZ) "output Z does never occur" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iE, oV, iF])* --------------- Formula: (! oY WU oX) "output Y does never occur before output X" Formula is satisfied. --------------- Formula: (! oU WU (oU WU (! oU WU (oU WU (false R ! oU))))) "output U occurs at most twice" Formula is satisfied. --------------- Formula: (false R (! iC | (true U oV))) "output V responds to input C" Formula is not satisfied! An error path is [iC, oZ] ([iC, oX, iF, oX, iB, oZ])* --------------- Formula: (false R (! ((oU & ! oW) & (true U oW)) | (! oZ U oW))) "output Z does never occur between output U and output W" Formula is satisfied. --------------- Formula: (false R (! (iF & ! iD) | (! oZ WU iD))) "output Z does never occur after input F until input D" Formula is not satisfied! An error path is [iB, oV, iF, oZ] ([iB, oZ, iC, oV])* --------------- Formula: (false R (! (iA & ! iD) | (! iD U (oZ & ! iD)))) "output Z occurs after input A until input D" 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 & ! oW) | (! oV WU oW))) "output V does never occur after output Z until output W" Formula is not satisfied! An error path is [iC, oZ, iF, oV] ([iF, oV, iD, oV])* --------------- Formula: ((false R ! iF) | (true U (iF & (true U oV)))) "output V occurs after input F" Formula is not satisfied! An error path is [iC, oZ, iB, oZ, iF] ([oX, iC, oX, iE, iF, iB, oZ, iF])* --------------- Formula: (! (true U iD) | (! oZ U (iC | iD))) "input C precedes output Z before input D" Formula is not satisfied! An error path is [iB, oV, iF, oZ, iD] ([oV, iE, oZ, iD])* --------------- Formula: (false R (! (iF & ! iC) | (! iC WU (oV & ! iC)))) "output V occurs between input F and input C" Formula is not satisfied! An error path is [iB, oV, iF, oZ, iB, oZ, iC] ([oV, iB, oZ, iC])* --------------- Formula: (false R (! oV | (false R ! oU))) "output U does never occur after output V" Formula is satisfied. --------------- 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 satisfied. --------------- Formula: (true U oY) "output Y occurs eventually" Formula is not satisfied! An error path is [iB, oV] ([iB, oX, iC, oX, iC, oZ])* --------------- Formula: (! oX WU oZ) "output X does never occur before output Z" Formula is not satisfied! An error path is [iB, oV, iB, oX] ([iC, oX, iD, oV])* --------------- 48 constraints satisfied, 52 unsatisfied.