Reading in file: "test6.maude" ========================================== Reading in file: "test.maude" ========================================== mod TEST Advisory: redefining module TEST. Done reading in file: "test.maude" ========================================== mod TEST6 ========================================== search in TEST6 : start =>! state:State . Solution 1 (state 130568) states: 130583 rewrites: 8469331 in 96320ms cpu (97950ms real) (87929 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 2)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 2), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("a")), 2), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 2 (state 130569) states: 130583 rewrites: 8469333 in 96340ms cpu (98340ms real) (87910 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 3)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("a")), 3), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 3 (state 130570) states: 130583 rewrites: 8469335 in 96360ms cpu (98790ms real) (87892 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 4)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("a")), 4), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 4 (state 130571) states: 130583 rewrites: 8469337 in 96360ms cpu (98970ms real) (87892 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 3)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("a")), 3), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 5 (state 130572) states: 130583 rewrites: 8469339 in 96360ms cpu (99100ms real) (87892 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 4)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("a")), 4), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 6 (state 130573) states: 130583 rewrites: 8469341 in 96360ms cpu (99200ms real) (87892 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 2)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 2), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("a")), 2), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 7 (state 130574) states: 130583 rewrites: 8469343 in 96360ms cpu (99380ms real) (87892 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 3)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), 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("a")), 3), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 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")), 3), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 8 (state 130575) states: 130583 rewrites: 8469345 in 96360ms cpu (99520ms real) (87892 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 4)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), 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("a")), 4), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 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")), 4), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 9 (state 130576) states: 130583 rewrites: 8469347 in 96370ms cpu (99660ms real) (87883 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 4)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), 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("a")), 4), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 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")), 4), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 10 (state 130577) states: 130583 rewrites: 8469349 in 96370ms cpu (99820ms real) (87883 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 2)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 2), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("a")), 2), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 11 (state 130578) states: 130583 rewrites: 8469351 in 96370ms cpu (99970ms real) (87883 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 3)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("a")), 3), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 12 (state 130579) states: 130583 rewrites: 8469353 in 96370ms cpu (100140ms real) (87883 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 4)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc( "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet( proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet) totalorder(regconf(sProcSet(proc("a")), 4), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 13 (state 130580) states: 130583 rewrites: 8469355 in 96370ms cpu (100170ms real) (87883 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 3)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 3), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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")), 4), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), 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("a")), 3), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 3), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 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")), 3), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 14 (state 130581) states: 130583 rewrites: 8469357 in 96370ms cpu (100190ms real) (87883 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 4)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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")), 3), sProcSet(proc("b")) sProcSet(proc("c"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), 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("a")), 4), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 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")), 4), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 2, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 3), eNatSet) knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) Solution 15 (state 130582) states: 130583 rewrites: 8469359 in 96370ms cpu (100220ms real) (87883 rewrites/second) state:State --> multicast-ack(proc("a")) network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c"))) freshconf(5) operational(proc("a")) operational(proc("b")) operational(proc("c")) freshseq(1) CONTROLLER(eController) localconf(proc("a"), regconf(sProcSet(proc("a")), 4)) localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)) localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2)) delivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) delivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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"))))) delivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data( "test"))) 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"))))) alldelivered(proc("a"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a"))))) alldelivered(proc("b"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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"))))) alldelivered(proc("c"), sMessageList(datamsg(proc("a"), reliable, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("test"))) 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"))))) reachable(proc("a"), sProcSet(proc("a"))) 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("a")), 4), eConstraintSet) causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eConstraintSet) causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet) causalorder(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), 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("a")), 4), eEventList) totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eEventList) totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))) totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList( event(proc("a"), 0)) sEventList(event(proc("a"), 0))) localmsgs(proc("a"), regconf(sProcSet(proc("a")), 4), eNatSet) localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) localmsgs(proc("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet) localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet) localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 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")), 4), eNatSet) knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 2), eNatSet) knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 1, 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) 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: 130583 rewrites: 8469359 in 96380ms cpu (100260ms real) (87874 rewrites/second) Done reading in file: "test6.maude"