Reachability problems: =============================== error_0 reachable via input sequence [F, C, B, A] --------------- error_1 reachable via input sequence [F, C, E, A] --------------- error_2 reachable via input sequence [F, D, B, A] --------------- error_3 reachable via input sequence [F, F, B, A] --------------- error_4 reachable via input sequence [F, E, B, A] --------------- error_5 reachable via input sequence [D, E, A, A] --------------- error_6 reachable via input sequence [D, E, B, A] --------------- error_7 reachable via input sequence [D, C, B, A] --------------- All other errors unreachable LTL problems: =============================== Formula: (! iB WU (oW & ! iB)) "output W occurs before input B" Formula is satisfied. --------------- Formula: (false R (! (iC & ! iF) | (! oV WU iF))) "output V does never occur after input C until input F" Formula is satisfied. --------------- Formula: (! oZ WU iB) "output Z does never occur before input B" Formula is satisfied. --------------- Formula: ((false R ! oV) | (true U (oV & (true U oX)))) "output X occurs after output V" Formula is satisfied. --------------- Formula: (false R (! oY | (true U oW))) "output W responds to output Y" Formula is not satisfied! An error path is [iC, oY] ([iC, oU, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (false R ! oX) "output X does never occur" Formula is not satisfied! An error path is [iD, oX] ([iA, oX, iA, iE, oX])* --------------- Formula: (false R (! (iE & ! iD) | (! iD U (oZ & ! iD)))) "output Z occurs after input E until input D" Formula is not satisfied! An error path is [iC, oY, iE] ([oX, iE, iE])* --------------- Formula: (false R (! (iC & ! oY) | (! oX WU oY))) "output X does never occur after input C until output Y" Formula is not satisfied! An error path is [iD, oX, iC, oX] ([iA, iA, iC, oY, iC, oY, iA])* --------------- Formula: (! oW WU (oY & ! oW)) "output Y occurs before output W" Formula is not satisfied! An error path is [iD, oX, iF, oW] ([iA, iF, oW])* --------------- Formula: (! iA WU (oX & ! iA)) "output X occurs before input A" Formula is not satisfied! An error path is [iC, oY, iA] ([oW, iD, iA, iC, oY, iD, oY, iE, iA])* --------------- Formula: (! oY WU oX) "output X precedes output Y" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (! oZ WU iB) "output Z does never occur before input B" Formula is satisfied. --------------- Formula: (! (true U iE) | (! oU U (iD | iE))) "input D precedes output U before input E" Formula is not satisfied! An error path is [iF, oU, iE] ([oW, iC, iA, iE])* --------------- Formula: (false R (! (oX & ! oZ) | (! oZ U (oY & ! oZ)))) "output Y occurs after output X until output Z" Formula is not satisfied! An error path is [iD, oX] ([iA, oX, iA, iE, oX])* --------------- Formula: (false R (! (oV & ! iA) | (! iA WU (oZ & ! iA)))) "output Z occurs between output V and input A" Formula is satisfied. --------------- Formula: (false R (! ((iA & ! oV) & (true U oV)) | (! oU U oV))) "output U does never occur between input A and output V" Formula is satisfied. --------------- Formula: (! (true U iD) | (! oV U (oX | iD))) "output X precedes output V before input D" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! iE) | (! oU WU iE))) "output U does never occur after output Z until input E" Formula is satisfied. --------------- Formula: ((false R ! iC) | (true U (iC & (true U oZ)))) "output Z occurs after input C" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (false R ! oV) "output V does never occur" Formula is satisfied. --------------- Formula: (false R (! iD | (true U oY))) "output Y responds to input D" Formula is not satisfied! An error path is [iD, oX] ([iA, oX, iA, iE, oX])* --------------- Formula: (false R (! (oY & ! oV) | (! oV U (oX & ! oV)))) "output X occurs after output Y until output V" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (false R (! oZ | (false R ! oW))) "output W does never occur after output Z" Formula is satisfied. --------------- Formula: (! iC WU (oW & ! iC)) "output W occurs before input C" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (false R (! oW | (true U oX))) "output X responds to output W" Formula is not satisfied! An error path is [iC, oY, iA, oW] ([iA, iA, iA, iC, oY, iD, oY, iE, iA, oW])* --------------- 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, oU, iC] ([oY, iC, oY, iC, iA, oU, iC])* --------------- Formula: (false R (! ((iE & ! iA) & (true U iA)) | (! oX U iA))) "output X does never occur between input E and input A" Formula is not satisfied! An error path is [iC, oY, iE, oX, iC, iA] ([iC, oY, iA, oY, iC, iA])* --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (! (true U iE) | ((! oU & ! iE) U (iE | ((oU & ! iE) U (iE | ((! oU & ! iE) U (iE | ((oU & ! iE) U (iE | (! oU U iE)))))))))) "output U occurs at most twice before input E" Formula is not satisfied! An error path is [iC, oY, iC, oU, iA, iC, oU, iC, oU, iE] ([iA, oU, iD, oY])* --------------- Formula: (false R (! (iF & ! oY) | (! oZ WU oY))) "output Z does never occur after input F until output Y" Formula is satisfied. --------------- Formula: (true U oU) "output U occurs eventually" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (! oV WU iB) "output V does never occur before input B" Formula is satisfied. --------------- Formula: (true U oZ) "output Z occurs eventually" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (! (true U oW) | ((! oU & ! oW) U (oW | ((oU & ! oW) U (oW | ((! oU & ! oW) U (oW | ((oU & ! oW) U (oW | (! oU U oW)))))))))) "output U occurs at most twice before output W" Formula is not satisfied! An error path is [iC, oY, iF, oU, iE, oU, iE, oU, iF, iD, oW] ([iA, iF, oW])* --------------- Formula: (false R (! ((oW & ! oX) & (true U oX)) | (! oZ U oX))) "output Z does never occur between output W and output X" Formula is satisfied. --------------- Formula: (! oX WU (oX WU (! oX WU (oX WU (false R ! oX))))) "output X occurs at most twice" Formula is not satisfied! An error path is [iD, oX, iA] ([oX, iA, iE, oX, iA])* --------------- Formula: (! (true U iF) | (! oV U (iA | iF))) "input A precedes output V before input F" Formula is satisfied. --------------- Formula: (false R (! (oW & ! iD) | (! iD WU (oX & ! iD)))) "output X occurs between output W and input D" Formula is not satisfied! An error path is [iC, oY, iA, oW, iD] ([iA, iF, oW])* --------------- Formula: (false R (! (iD & ! iC) | (! iC WU (oV & ! iC)))) "output V occurs between input D and input C" Formula is not satisfied! An error path is [iD, oX, iC] ([oX, iE, oX, iC])* --------------- Formula: (! oZ WU iE) "input E precedes output Z" Formula is satisfied. --------------- Formula: (false R (! iA | (true U oY))) "output Y responds to input A" Formula is not satisfied! An error path is [iD, oX, iA] ([oX, iA, iE, oX, iA])* --------------- Formula: (false R ! oW) "output W does never occur" Formula is not satisfied! An error path is [iC, oY, iA, oW] ([iA, iA, iA, iC, oY, iD, oY, iE, iA, oW])* --------------- Formula: (! oU WU iB) "output U does never occur before input B" Formula is not satisfied! An error path is [iF, oU] ([iC, oY, iA, oY, iC, iA])* --------------- Formula: (false R (! iD | (true U oW))) "output W responds to input D" Formula is not satisfied! An error path is [iD, oX] ([iA, oX, iA, iE, oX])* --------------- Formula: (false R (! (oV & ! oZ) | (! oZ WU (oX & ! oZ)))) "output X occurs between output V and output Z" 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 not satisfied! An error path is [iC, oY, iA, oW, iE, iE, iF, oW, iD, oW, iE, oX] ([iA, oX, iA, iE, oX])* --------------- Formula: ((false R ! oY) | (true U (oY & (true U oX)))) "output X occurs after output Y" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (false R (! oW | (false R ! oX))) "output X does never occur after output W" Formula is not satisfied! An error path is [iD, oX, iF, oW, iE, oX] ([iA, oX, iA, iE, oX])* --------------- Formula: (false R (! (oV & ! oX) | (! oX U (oZ & ! oX)))) "output Z occurs after output V until output X" Formula is satisfied. --------------- Formula: (false R (! iA | (false R ! oV))) "output V does never occur after input A" Formula is satisfied. --------------- Formula: (false R (! (oY & ! oZ) | (! oZ WU (oU & ! oZ)))) "output U occurs between output Y and output Z" Formula is satisfied. --------------- Formula: (! (true U oV) | ((! oZ & ! oV) U (oV | ((oZ & ! oV) U (oV | ((! oZ & ! oV) U (oV | ((oZ & ! oV) U (oV | (! oZ U oV)))))))))) "output Z occurs at most twice before output V" Formula is satisfied. --------------- Formula: (! oU WU iA) "input A precedes output U" Formula is not satisfied! An error path is [iF, oU] ([iC, oY, iA, oY, iC, iA])* --------------- Formula: (! oV WU (oX & ! oV)) "output X occurs before output V" Formula is satisfied. --------------- Formula: (! iE WU (oX & ! iE)) "output X occurs before input E" Formula is not satisfied! An error path is [iC, oY, iE] ([oX, iE, iE])* --------------- Formula: ((false R ! iA) | (true U (iA & (true U oU)))) "output U occurs after input A" Formula is not satisfied! An error path is [iC, oY, iA] ([oW, iD, iA, iC, oY, iD, oY, iE, iA])* --------------- Formula: (false R (! oY | (false R ! oW))) "output W does never occur after output Y" Formula is not satisfied! An error path is [iC, oY, iA, oW] ([iA, iA, iA, iC, oY, iD, oY, iE, iA, oW])* --------------- Formula: (! oW WU oZ) "output W does never occur before output Z" Formula is not satisfied! An error path is [iC, oY, iA, oW] ([iA, iA, iA, iC, oY, iD, oY, iE, iA, oW])* --------------- Formula: (! oZ WU iE) "input E precedes output Z" Formula is satisfied. --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- 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 not satisfied! An error path is [iD, oX, iF, oW, iD, oW, iD, oW, iA, iD, oU] ([iA, iE, oX, iD, oU])* --------------- Formula: (! (true U iD) | (! oV U (oW | iD))) "output W precedes output V before input D" Formula is satisfied. --------------- Formula: (false R (! (oZ & ! iE) | (! iE WU (oV & ! iE)))) "output V occurs between output Z and input E" Formula is satisfied. --------------- Formula: (false R (! (oW & ! iC) | (! oX WU iC))) "output X does never occur after output W until input C" Formula is not satisfied! An error path is [iD, oX, iF, oW, iE, oX] ([iA, oX, iA, iE, oX])* --------------- Formula: ((false R ! oU) | (true U (oU & (true U oZ)))) "output Z occurs after output U" Formula is not satisfied! An error path is [iF, oU] ([iC, oY, iA, oY, iC, iA])* --------------- Formula: (! (true U iD) | (! oW U (iA | iD))) "input A precedes output W before input D" Formula is not satisfied! An error path is [iF, oU, iE, oW, iD] ([oW, iD])* --------------- Formula: (! oU WU oY) "output U does never occur before output Y" Formula is not satisfied! An error path is [iF, oU] ([iC, oY, iA, oY, iC, iA])* --------------- Formula: (false R (! (oU & ! iD) | (! oY WU iD))) "output Y does never occur after output U until input D" Formula is not satisfied! An error path is [iF, oU, iC, oY] ([iA, oY, iC, iA, iC, oY])* --------------- Formula: (! oZ WU iA) "output Z does never occur before input A" Formula is satisfied. --------------- Formula: ((false R ! oZ) | (true U (oZ & (true U oU)))) "output U occurs after output Z" Formula is satisfied. --------------- Formula: (false R (! (iF & ! iD) | (! iD WU (oU & ! iD)))) "output U occurs between input F and input D" Formula is not satisfied! An error path is [iD, oX, iF, oW, iD] ([oW, iD])* --------------- Formula: (false R ! oU) "output U does never occur" Formula is not satisfied! An error path is [iF, oU] ([iC, oY, iA, oY, iC, iA])* --------------- Formula: (false R (! (oV & ! oW) | (! oW U (oY & ! oW)))) "output Y occurs after output V until output W" Formula is satisfied. --------------- Formula: (false R (! oZ | (false R ! oY))) "output Y does never occur after output Z" Formula is satisfied. --------------- Formula: (! (true U oZ) | ((! oW & ! oZ) U (oZ | ((oW & ! oZ) U (oZ | ((! oW & ! oZ) U (oZ | ((oW & ! oZ) U (oZ | (! oW U oZ)))))))))) "output W occurs at most twice before output Z" Formula is satisfied. --------------- Formula: (! oU WU oZ) "output Z precedes output U" Formula is not satisfied! An error path is [iF, oU] ([iC, oY, iA, oY, iC, iA])* --------------- Formula: (! iB WU (oZ & ! iB)) "output Z occurs before input B" Formula is satisfied. --------------- Formula: (false R ! oZ) "output Z does never occur" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iC) | (! iC U (oZ & ! iC)))) "output Z occurs after input B until input C" Formula is satisfied. --------------- Formula: ((false R ! iE) | (true U (iE & (true U oX)))) "output X occurs after input E" Formula is not satisfied! An error path is [iD, oX, iE] ([oU, iE, iC, oW, iF, iA, iE])* --------------- Formula: (false R (! ((iE & ! iB) & (true U iB)) | (! oX U iB))) "output X does never occur between input E and input B" Formula is satisfied. --------------- Formula: (false R (! ((iC & ! oW) & (true U oW)) | (! oU U oW))) "output U does never occur between input C and output W" Formula is not satisfied! An error path is [iC, oY, iC, oU, iD, iC, oW] ([iA, iF, oW])* --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- 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 [iC, oY, iA] ([oW, iD, iA, iC, oY, iD, oY, iE, iA])* --------------- Formula: (false R (! (oV & ! oX) | (! oX U (oZ & ! oX)))) "output Z occurs after output V until output X" Formula is satisfied. --------------- Formula: (false R (! (iB & ! oY) | (! oY WU (oV & ! oY)))) "output V occurs between input B and output Y" Formula is satisfied. --------------- Formula: (true U oV) "output V occurs eventually" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (false R (! (iD & ! iB) | (! oV WU iB))) "output V does never occur after input D until input B" Formula is satisfied. --------------- Formula: (false R (! (iB & ! iC) | (! iC U (oV & ! iC)))) "output V occurs after input B until input C" Formula is satisfied. --------------- Formula: (false R ! oY) "output Y does never occur" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (! (true U oY) | (! oZ U (oX | oY))) "output X precedes output Z before output Y" Formula is satisfied. --------------- Formula: (false R (! oZ | (true U oW))) "output W responds to output Z" Formula is satisfied. --------------- Formula: (! (true U iA) | (! oV U (oU | iA))) "output U precedes output V before input A" Formula is satisfied. --------------- Formula: (false R (! ((iD & ! iB) & (true U iB)) | (! oX U iB))) "output X does never occur between input D and input B" Formula is satisfied. --------------- Formula: (! oU WU (oY & ! oU)) "output Y occurs before output U" Formula is not satisfied! An error path is [iF, oU] ([iC, oY, iA, oY, iC, iA])* --------------- Formula: (! oW WU (oW WU (! oW WU (oW WU (false R ! oW))))) "output W occurs at most twice" Formula is not satisfied! An error path is [iC, oY, iA, oW, iA] ([iA, iE, iC, oW, iF, iA, iC, oX])* --------------- Formula: (false R (! (iB & ! iD) | (! iD WU (oW & ! iD)))) "output W occurs between input B and input D" Formula is satisfied. --------------- Formula: (false R (! (iC & ! oV) | (! oY WU oV))) "output Y does never occur after input C until output V" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- Formula: (false R (! (iE & ! oY) | (! oY U (oV & ! oY)))) "output V occurs after input E until output Y" Formula is not satisfied! An error path is [iC, oY, iE] ([oX, iE, iE])* --------------- Formula: (true U oU) "output U occurs eventually" Formula is not satisfied! An error path is [iC, oY] ([iA, oW, iD, iA, iC, oY, iD, oY, iE])* --------------- 43 constraints satisfied, 57 unsatisfied.