Reachability problems: =============================== error_40 reachable via input sequence [B, F, A, B, A] --------------- error_48 reachable via input sequence [B, F, A, F, A] --------------- error_2 reachable via input sequence [B, F, A, C, A] --------------- error_22 reachable via input sequence [B, F, D, B, A] --------------- error_15 reachable via input sequence [B, F, D, D, A] --------------- error_37 reachable via input sequence [B, F, D, E, A] --------------- error_29 reachable via input sequence [B, F, D, A, A] --------------- error_0 reachable via input sequence [D, C, E, B, A] --------------- error_9 reachable via input sequence [D, C, E, F, A] --------------- error_18 reachable via input sequence [D, C, E, E, A] --------------- error_47 reachable via input sequence [D, C, E, A, A] --------------- error_30 reachable via input sequence [D, E, C, B, A] --------------- error_14 reachable via input sequence [D, E, C, D, A] --------------- error_51 reachable via input sequence [D, E, C, F, A] --------------- error_23 reachable via input sequence [D, E, C, C, A] --------------- error_33 reachable via input sequence [D, E, A, B, A] --------------- error_3 reachable via input sequence [D, E, A, F, A] --------------- error_25 reachable via input sequence [D, E, A, C, A] --------------- error_41 reachable via input sequence [D, E, A, A, A] --------------- error_7 reachable via input sequence [D, D, C, B, A] --------------- error_39 reachable via input sequence [D, D, C, C, A] --------------- error_50 reachable via input sequence [D, D, C, E, A] --------------- error_34 reachable via input sequence [D, D, C, A, A] --------------- error_45 reachable via input sequence [D, D, D, B, A] --------------- error_38 reachable via input sequence [D, D, D, D, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (! oW WU (oW WU (! oW WU (oW WU (false R ! oW))))) "output W occurs at most twice" Formula is satisfied. --------------- Formula: (false R (! oV | (false R ! oX))) "output X does never occur after output V" Formula is satisfied. --------------- Formula: (false R ! oY) "output Y does never occur" Formula is satisfied. --------------- Formula: (false R (! ((oV & ! iB) & (true U iB)) | (! oW U iB))) "output W does never occur between output V and input B" Formula is satisfied. --------------- Formula: (! (true U iF) | (! oV U (iE | iF))) "input E precedes output V before input F" Formula is not satisfied! An error path is [iD, oV, iD, oZ, iD, oV, iF] ([iC, oZ])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is satisfied. --------------- Formula: (false R (! (oU & ! oV) | (! oV WU (oW & ! oV)))) "output W occurs between output U and output V" Formula is not satisfied! An error path is [iD, oV, iE, oU, iC, oV] ([iA, iE, oU, iC, oV])* --------------- 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 [iB, oU, iF, oZ, iA] ([oU, iA, oZ, iF, oZ, iA])* --------------- Formula: (false R (! (oX & ! iA) | (! iA U (oW & ! iA)))) "output W occurs after output X until input A" Formula is satisfied. --------------- Formula: (false R (! iE | (false R ! oX))) "output X does never occur after input E" Formula is satisfied. --------------- Formula: ((false R ! oW) | (true U (oW & (true U oU)))) "output U occurs after output W" Formula is satisfied. --------------- Formula: (! (true U iF) | (! oX U (iC | iF))) "input C precedes output X before input F" Formula is satisfied. --------------- Formula: (! oU WU iD) "output U does never occur before input D" Formula is not satisfied! An error path is [iB, oU] ([iD, oU, iA, oU, iD, oZ])* --------------- Formula: (! oV WU oW) "output W precedes output V" Formula is not satisfied! An error path is [iD, oV] ([iD, oZ, iA, oZ, iE])* --------------- Formula: (! (true U oU) | (! oX U (oY | oU))) "output Y precedes output X before output U" Formula is satisfied. --------------- Formula: (false R (! ((iC & ! iD) & (true U iD)) | (! oV U iD))) "output V does never occur between input C and input D" Formula is not satisfied! An error path is [iD, oV, iC, oV, iD] ([oZ, iD, oV, iC, oV, iD])* --------------- Formula: (false R ! oX) "output X does never occur" Formula is satisfied. --------------- Formula: ((false R ! iF) | (true U (iF & (true U oV)))) "output V occurs after input F" Formula is not satisfied! An error path is [iB, oU, iF] ([oZ, iA, oU, iA, oZ, iF])* --------------- Formula: (! oW WU oY) "output W does never occur before output Y" Formula is satisfied. --------------- Formula: (! (true U oV) | ((! oX & ! oV) U (oV | ((oX & ! oV) U (oV | ((! oX & ! oV) U (oV | ((oX & ! oV) U (oV | (! oX U oV)))))))))) "output X occurs at most twice before output V" 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 [iB, oU, iF, oZ, iA] ([oU, iA, oZ, iF, oZ, iA])* --------------- Formula: (! oV WU iD) "output V does never occur before input D" Formula is not satisfied! An error path is [iB, oU, iF, oZ, iA, oU, iE, oV] ([iA, iE, oU, iC, oV])* --------------- Formula: (true U oU) "output U occurs eventually" Formula is not satisfied! An error path is [iD, oV] ([iD, oZ, iA, oZ, iE])* --------------- Formula: ((false R ! iD) | (true U (iD & (true U oU)))) "output U occurs after input D" Formula is not satisfied! An error path is [iD, oV] ([iD, oZ, iA, oZ, iE])* --------------- Formula: (! (true U oV) | (! oW U (oU | oV))) "output U precedes output W before output V" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! iB) | (! iB WU (oW & ! iB)))) "output W occurs between output Z and input B" Formula is satisfied. --------------- Formula: (false R ! oZ) "output Z does never occur" Formula is not satisfied! An error path is [iB, oU, iF, oZ] ([iA, oU, iA, oZ, iF, oZ])* --------------- Formula: (! (true U iB) | ((! oY & ! iB) U (iB | ((oY & ! iB) U (iB | ((! oY & ! iB) U (iB | ((oY & ! iB) U (iB | (! oY U iB)))))))))) "output Y occurs at most twice before input B" Formula is satisfied. --------------- 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 [iB, oU, iD] ([oU, iA, oU, iD, oZ, iD])* --------------- Formula: (! (true U iA) | ((! oV & ! iA) U (iA | ((oV & ! iA) U (iA | ((! oV & ! iA) U (iA | ((oV & ! iA) U (iA | (! oV U iA)))))))))) "output V occurs at most twice before input A" Formula is not satisfied! An error path is [iD, oV, iD, oZ, iD, oV, iE, iD, oV, iA] ([oZ, iD, oV, iA])* --------------- Formula: (false R (! (iD & ! oU) | (! oU U (oY & ! oU)))) "output Y occurs after input D until output U" Formula is not satisfied! An error path is [iD, oV] ([iD, oZ, iA, oZ, iE])* --------------- 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 [iB, oU, iD] ([oU, iA, oU, iD, oZ, iD])* --------------- Formula: (false R (! oZ | (true U oX))) "output X responds to output Z" Formula is not satisfied! An error path is [iB, oU, iF, oZ] ([iA, oU, iA, oZ, iF, oZ])* --------------- Formula: (false R ! oX) "output X does never occur" Formula is satisfied. --------------- Formula: (! oY WU (oY WU (! oY WU (oY WU (false R ! oY))))) "output Y occurs at most twice" Formula is satisfied. --------------- Formula: (false R (! (iD & ! iF) | (! iF U (oW & ! iF)))) "output W occurs after input D until input F" Formula is not satisfied! An error path is [iD, oV] ([iD, oZ, iA, oZ, iE])* --------------- Formula: (false R (! iE | (true U oW))) "output W responds to input E" Formula is not satisfied! An error path is [iD, oV, iE] ([oU, iC, oV, iA, iE])* --------------- Formula: (false R (! (iC & ! iF) | (! iF U (oU & ! iF)))) "output U occurs after input C until input F" Formula is not satisfied! An error path is [iD, oV, iC] ([oV, iD, oZ, iD, oV, iC])* --------------- Formula: (! (true U iD) | (! oZ U (oU | iD))) "output U precedes output Z before input D" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! iA) | (! iA U (oU & ! iA)))) "output U occurs after output Z until input A" Formula is not satisfied! An error path is [iD, oV, iD, oZ] ([iD, oV, iE])* --------------- Formula: (false R ! oV) "output V does never occur" Formula is not satisfied! An error path is [iD, oV] ([iD, oZ, iA, oZ, iE])* --------------- Formula: (false R (! iD | (false R ! oZ))) "output Z does never occur after input D" Formula is not satisfied! An error path is [iD, oV, iD, oZ] ([iD, oV, iE])* --------------- 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: (false R (! (oX & ! oU) | (! oY WU oU))) "output Y does never occur after output X until output U" Formula is satisfied. --------------- Formula: (! oY WU (oV & ! oY)) "output V occurs before output Y" Formula is satisfied. --------------- Formula: ((false R ! iB) | (true U (iB & (true U oU)))) "output U occurs after input B" Formula is satisfied. --------------- Formula: (false R (! oX | (true U oU))) "output U responds to output X" Formula is satisfied. --------------- Formula: (! (true U oV) | ((! oX & ! oV) U (oV | ((oX & ! oV) U (oV | ((! oX & ! oV) U (oV | ((oX & ! oV) U (oV | (! oX U oV)))))))))) "output X occurs at most twice before output V" Formula is satisfied. --------------- Formula: (false R (! iE | (true U oW))) "output W responds to input E" Formula is not satisfied! An error path is [iD, oV, iE] ([oU, iC, oV, iA, iE])* --------------- Formula: (false R (! (oX & ! iB) | (! iB U (oU & ! iB)))) "output U occurs after output X until input B" Formula is satisfied. --------------- 26 constraints satisfied, 24 unsatisfied.