MAYBE TRS: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), start(i) -> busy(F(), closed(), stop(), false(), false(), false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} RUF: Strict: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} Weak: {} DP: Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: { (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i))) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i))) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i))) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)) (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b1, i1)) (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b2, i2)) (busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> or#(b3, i3)) } SCCS: Scc: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)} SCC: Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), idle#(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy#(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i)} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} SPSC: Simple Projection: pi(idle#) = 6, pi(busy#) = 6 Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle#(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} EDG: {(idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i)) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))} SCCS: Scc: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), d, stop(), true(), b2, b3, i) -> idle#(B(), open(), stop(), false(), b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} POLY: Argument Filtering: pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = 3, pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 3, pi(busy) = [] Usable Rules: {} Interpretation: [true] = 1, [false] = 0 Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: {(busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i))} SCCS: Scc: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: { busy#(F(), d, stop(), b1, true(), b3, i) -> idle#(F(), open(), stop(), b1, false(), b3, i), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} POLY: Argument Filtering: pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = [2,4], pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 4, pi(busy) = [] Usable Rules: {} Interpretation: [idle#](x0, x1) = x0 + x1, [true] = 1, [down] = 0, [up] = 0, [false] = 0, [stop] = 0 Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: {(busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i)) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()))} SCCS: Scc: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), d, stop(), b1, b2, true(), i) -> idle#(S(), open(), stop(), b1, b2, false(), i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} POLY: Argument Filtering: pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = 5, pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 5, pi(busy) = [] Usable Rules: {} Interpretation: [true] = 1, [false] = 0 Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: {(busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i))} SCCS: Scc: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), open(), stop(), b1, false(), b3, i) -> idle#(F(), closed(), stop(), b1, false(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(B(), open(), stop(), false(), b2, b3, i) -> idle#(B(), closed(), stop(), false(), b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), busy#(S(), open(), stop(), b1, b2, false(), i) -> idle#(S(), closed(), stop(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} POLY: Argument Filtering: pi(or) = [], pi(true) = [], pi(newbuttons) = [], pi(idle#) = 1, pi(idle) = [], pi(S) = [], pi(empty) = [], pi(B) = [], pi(correct) = [], pi(down) = [], pi(up) = [], pi(open) = [], pi(FS) = [], pi(BF) = [], pi(incorrect) = [], pi(false) = [], pi(stop) = [], pi(closed) = [], pi(F) = [], pi(busy#) = 1, pi(busy) = [] Usable Rules: {} Interpretation: [open] = 1, [closed] = 0 Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} EDG: {(busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i)) (idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty()), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i))} SCCS: Scc: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} SCC: Strict: {busy#(F(), closed(), stop(), false(), false(), true(), i) -> idle#(F(), closed(), up(), false(), false(), true(), i), busy#(F(), closed(), stop(), true(), false(), b3, i) -> idle#(F(), closed(), down(), true(), false(), b3, i), busy#(F(), closed(), up(), b1, false(), b3, i) -> idle#(FS(), closed(), up(), b1, false(), b3, i), busy#(F(), closed(), up(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(F(), closed(), down(), b1, false(), b3, i) -> idle#(BF(), closed(), down(), b1, false(), b3, i), busy#(F(), closed(), down(), b1, true(), b3, i) -> idle#(F(), closed(), stop(), b1, true(), b3, i), busy#(BF(), closed(), up(), b1, b2, b3, i) -> idle#(F(), closed(), up(), b1, b2, b3, i), busy#(BF(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), down(), b1, b2, b3, i), busy#(FS(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), up(), b1, b2, b3, i), busy#(FS(), closed(), down(), b1, b2, b3, i) -> idle#(F(), closed(), down(), b1, b2, b3, i), busy#(B(), closed(), stop(), false(), false(), true(), i) -> idle#(B(), closed(), up(), false(), false(), true(), i), busy#(B(), closed(), stop(), false(), true(), b3, i) -> idle#(B(), closed(), up(), false(), true(), b3, i), busy#(B(), closed(), up(), false(), b2, b3, i) -> idle#(BF(), closed(), up(), false(), b2, b3, i), busy#(B(), closed(), up(), true(), b2, b3, i) -> idle#(B(), closed(), stop(), true(), b2, b3, i), busy#(B(), closed(), down(), b1, b2, b3, i) -> idle#(B(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), stop(), b1, true(), false(), i) -> idle#(S(), closed(), down(), b1, true(), false(), i), busy#(S(), closed(), stop(), true(), false(), false(), i) -> idle#(S(), closed(), down(), true(), false(), false(), i), busy#(S(), closed(), up(), b1, b2, b3, i) -> idle#(S(), closed(), stop(), b1, b2, b3, i), busy#(S(), closed(), down(), b1, b2, false(), i) -> idle#(FS(), closed(), down(), b1, b2, false(), i), busy#(S(), closed(), down(), b1, b2, true(), i) -> idle#(S(), closed(), stop(), b1, b2, true(), i), idle#(fl, d, m, b1, b2, b3, empty()) -> busy#(fl, d, m, b1, b2, b3, empty())} Weak: { busy(fl, open(), up(), b1, b2, b3, i) -> incorrect(), busy(fl, open(), down(), b1, b2, b3, i) -> incorrect(), busy(F(), d, stop(), b1, true(), b3, i) -> idle(F(), open(), stop(), b1, false(), b3, i), busy(F(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(F(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(F(), closed(), stop(), false(), false(), true(), i) -> idle(F(), closed(), up(), false(), false(), true(), i), busy(F(), closed(), stop(), true(), false(), b3, i) -> idle(F(), closed(), down(), true(), false(), b3, i), busy(F(), closed(), up(), b1, false(), b3, i) -> idle(FS(), closed(), up(), b1, false(), b3, i), busy(F(), closed(), up(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), closed(), down(), b1, false(), b3, i) -> idle(BF(), closed(), down(), b1, false(), b3, i), busy(F(), closed(), down(), b1, true(), b3, i) -> idle(F(), closed(), stop(), b1, true(), b3, i), busy(F(), open(), stop(), b1, false(), b3, i) -> idle(F(), closed(), stop(), b1, false(), b3, i), busy(BF(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(BF(), closed(), up(), b1, b2, b3, i) -> idle(F(), closed(), up(), b1, b2, b3, i), busy(BF(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), down(), b1, b2, b3, i), busy(FS(), d, stop(), b1, b2, b3, i) -> incorrect(), busy(FS(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), up(), b1, b2, b3, i), busy(FS(), closed(), down(), b1, b2, b3, i) -> idle(F(), closed(), down(), b1, b2, b3, i), busy(B(), d, stop(), true(), b2, b3, i) -> idle(B(), open(), stop(), false(), b2, b3, i), busy(B(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(B(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(B(), closed(), stop(), false(), false(), true(), i) -> idle(B(), closed(), up(), false(), false(), true(), i), busy(B(), closed(), stop(), false(), true(), b3, i) -> idle(B(), closed(), up(), false(), true(), b3, i), busy(B(), closed(), up(), false(), b2, b3, i) -> idle(BF(), closed(), up(), false(), b2, b3, i), busy(B(), closed(), up(), true(), b2, b3, i) -> idle(B(), closed(), stop(), true(), b2, b3, i), busy(B(), closed(), down(), b1, b2, b3, i) -> idle(B(), closed(), stop(), b1, b2, b3, i), busy(B(), open(), stop(), false(), b2, b3, i) -> idle(B(), closed(), stop(), false(), b2, b3, i), busy(S(), d, stop(), b1, b2, true(), i) -> idle(S(), open(), stop(), b1, b2, false(), i), busy(S(), closed(), stop(), b1, true(), false(), i) -> idle(S(), closed(), down(), b1, true(), false(), i), busy(S(), closed(), stop(), false(), false(), false(), empty()) -> correct(), busy(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)) -> idle(S(), closed(), stop(), false(), false(), false(), newbuttons(i1, i2, i3, i)), busy(S(), closed(), stop(), true(), false(), false(), i) -> idle(S(), closed(), down(), true(), false(), false(), i), busy(S(), closed(), up(), b1, b2, b3, i) -> idle(S(), closed(), stop(), b1, b2, b3, i), busy(S(), closed(), down(), b1, b2, false(), i) -> idle(FS(), closed(), down(), b1, b2, false(), i), busy(S(), closed(), down(), b1, b2, true(), i) -> idle(S(), closed(), stop(), b1, b2, true(), i), busy(S(), open(), stop(), b1, b2, false(), i) -> idle(S(), closed(), stop(), b1, b2, false(), i), idle(fl, d, m, b1, b2, b3, empty()) -> busy(fl, d, m, b1, b2, b3, empty()), idle(fl, d, m, b1, b2, b3, newbuttons(i1, i2, i3, i)) -> busy(fl, d, m, or(b1, i1), or(b2, i2), or(b3, i3), i), or(false(), b) -> b, or(true(), b) -> true()} Fail