Reading in file: "test8.maude"
==========================================

Reading in file: "test.maude"
==========================================
mod TEST
Advisory: redefining module TEST.
Done reading in file: "test.maude"
==========================================
mod TEST8
==========================================
rewrite in TEST8 : start .
rewrites: 27574 in 160ms cpu (160ms real) (172337 rewrites/second)
result 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(4)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 2))
localconf(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
localconf(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4))
delivered(proc("a"), sMessageList(datamsg(proc("a"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    ""))) 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"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    ""))) 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"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    ""))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("a"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    ""))) 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"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    ""))) 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"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    ""))) sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc(
    "c")), 0)))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")) sProcSet(proc("c")))
reachable(proc("c"), sProcSet(proc("b")) sProcSet(proc("c")))
sent(proc("a"), eBroadcastSet)
sent(proc("b"), eBroadcastSet)
sent(proc("c"), eBroadcastSet)
received(proc("a"), eMessageSet)
received(proc("b"), eMessageSet)
received(proc("c"), eMessageSet)
acked(proc("a"), eMessageSet)
acked(proc("b"), eMessageSet)
acked(proc("c"), eMessageSet)
causalorder(regconf(sProcSet(proc("a")), 2), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eConstraintSet)
causalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 2), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("a"), 0))
    sEventList(event(proc("a"), 0)))
totalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("a"), 0)) sEventList(event(proc("a"), 0)) sEventList(event(proc("a"), 0)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")), 2), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
Done reading in file: "test8.maude"