Reading in file: "test5.maude" ========================================== Reading in file: "test.maude" ========================================== mod TEST Advisory: redefining module TEST. Done reading in file: "test.maude" ========================================== mod TEST5 ========================================== search in TEST5 : start =>! state:State . Solution 1 (state 3549) states: 3551 rewrites: 154769 in 1500ms cpu (1920ms real) (103179 rewrites/second) state:State --> network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(6) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(0) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5)) delivered(proc("a"), eMessageList) delivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("b")), 4, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), sProcSet(proc("b"))))) delivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))) sMessageList(transmsg(transconf(sProcSet(proc("c")), 3, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)))) sMessageList(confmsg(regconf(sProcSet( proc("b")) sProcSet(proc("c")), 5), sProcSet(proc("c"))))) alldelivered(proc("a"), eMessageList) alldelivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("b")), 4, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), sProcSet(proc("b"))))) alldelivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))) sMessageList(transmsg(transconf(sProcSet(proc("c")), 3, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)))) sMessageList(confmsg(regconf(sProcSet( proc("b")) sProcSet(proc("c")), 5), sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c"))) reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c"))) sent(proc("a"), eBroadcastSet) sent(proc("b"), eBroadcastSet) sent(proc("c"), eBroadcastSet) received(proc("a"), eMessageSet) received(proc("b"), eMessageSet) received(proc("c"), eMessageSet) acked(proc("a"), eMessageSet) acked(proc("b"), eMessageSet) acked(proc("c"), eMessageSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("b")), 4, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("c")), 3, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eEventList) totalorder(transconf(sProcSet(proc("b")), 4, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eEventList) totalorder(transconf(sProcSet(proc("c")), 3, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)), eEventList) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eEventList) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")), 4, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("c")), 3, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) knownmsgs(proc("b"), transconf(sProcSet(proc("b")), 4, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) knownmsgs(proc("c"), transconf(sProcSet(proc("c")), 3, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)), eNatSet) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 2 (state 3550) states: 3551 rewrites: 154771 in 1500ms cpu (2400ms real) (103180 rewrites/second) state:State --> network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(6) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(0) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5)) delivered(proc("a"), eMessageList) delivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), sProcSet(proc("b"))))) delivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))) sMessageList(transmsg(transconf(sProcSet(proc("c")), 4, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)))) sMessageList(confmsg(regconf(sProcSet( proc("b")) sProcSet(proc("c")), 5), sProcSet(proc("c"))))) alldelivered(proc("a"), eMessageList) alldelivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), sProcSet(proc("b"))))) alldelivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), sProcSet(proc("b")) sProcSet(proc("c")))) sMessageList(transmsg(transconf(sProcSet(proc("c")), 4, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)))) sMessageList(confmsg(regconf(sProcSet( proc("b")) sProcSet(proc("c")), 5), sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c"))) reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c"))) sent(proc("a"), eBroadcastSet) sent(proc("b"), eBroadcastSet) sent(proc("c"), eBroadcastSet) received(proc("a"), eMessageSet) received(proc("b"), eMessageSet) received(proc("c"), eMessageSet) acked(proc("a"), eMessageSet) acked(proc("b"), eMessageSet) acked(proc("c"), eMessageSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("c")), 4, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eEventList) totalorder(transconf(sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eEventList) totalorder(transconf(sProcSet(proc("c")), 4, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)), eEventList) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eEventList) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("c")), 4, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) knownmsgs(proc("b"), transconf(sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 5), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) knownmsgs(proc("c"), transconf(sProcSet(proc("c")), 4, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)), eNatSet) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) No more solutions. states: 3551 rewrites: 154771 in 1500ms cpu (2720ms real) (103180 rewrites/second) Done reading in file: "test5.maude"