Reading in file: "test7.maude" ========================================== Reading in file: "test.maude" ========================================== mod TEST Advisory: redefining module TEST. Done reading in file: "test.maude" ========================================== mod TEST7 ========================================== search in TEST7 : start =>! state:State . Solution 1 (state 275355) states: 275383 rewrites: 18064133 in 462070ms cpu (466620ms real) (39093 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 2 (state 275356) states: 275383 rewrites: 18064135 in 462070ms cpu (466670ms real) (39093 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 3 (state 275357) states: 275383 rewrites: 18064137 in 462080ms cpu (466810ms real) (39093 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 4 (state 275358) states: 275383 rewrites: 18064139 in 462090ms cpu (466920ms real) (39092 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 5 (state 275359) states: 275383 rewrites: 18064141 in 462090ms cpu (467030ms real) (39092 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 6 (state 275360) states: 275383 rewrites: 18064143 in 462090ms cpu (467170ms real) (39092 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 7 (state 275361) states: 275383 rewrites: 18064145 in 462090ms cpu (467220ms real) (39092 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 8 (state 275362) states: 275383 rewrites: 18064147 in 462090ms cpu (467360ms real) (39092 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 9 (state 275363) states: 275383 rewrites: 18064149 in 462100ms cpu (467420ms real) (39091 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 10 (state 275364) states: 275383 rewrites: 18064151 in 462100ms cpu (467570ms real) (39091 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 11 (state 275365) states: 275383 rewrites: 18064153 in 462100ms cpu (467620ms real) (39091 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 12 (state 275366) states: 275383 rewrites: 18064155 in 462100ms cpu (467740ms real) (39091 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 13 (state 275367) states: 275383 rewrites: 18064157 in 462100ms cpu (467830ms real) (39091 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 14 (state 275368) states: 275383 rewrites: 18064159 in 462100ms cpu (467890ms real) (39091 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 15 (state 275369) states: 275383 rewrites: 18064161 in 462120ms cpu (468000ms real) (39089 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 16 (state 275370) states: 275383 rewrites: 18064163 in 462120ms cpu (468070ms real) (39089 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 17 (state 275371) states: 275383 rewrites: 18064165 in 462140ms cpu (468180ms real) (39088 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 18 (state 275372) states: 275383 rewrites: 18064167 in 462140ms cpu (468250ms real) (39088 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 19 (state 275373) states: 275383 rewrites: 18064169 in 462150ms cpu (468340ms real) (39087 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 20 (state 275374) states: 275383 rewrites: 18064171 in 462160ms cpu (468420ms real) (39086 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 21 (state 275375) states: 275383 rewrites: 18064173 in 462160ms cpu (468540ms real) (39086 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 22 (state 275376) states: 275383 rewrites: 18064175 in 462160ms cpu (468610ms real) (39086 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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))) 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("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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0)) Solution 23 (state 275377) states: 275383 rewrites: 18064177 in 462160ms cpu (468720ms real) (39086 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("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)) 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")))) 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")))) 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"),