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

Reading in file: "test.maude"
==========================================
mod TEST
Advisory: redefining module TEST.
Done reading in file: "test.maude"
==========================================
mod TEST9
==========================================
rewrite in TEST9 : start .
rewrites: 15595 in 130ms cpu (130ms real) (119961 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(3)
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(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0))))
    sMessageList(datamsg(proc("a"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(""))) sMessageList(
    confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b"))
    sProcSet(proc("c")), 0)))) sMessageList(datamsg(proc("a"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data(""))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
delivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b"))
    sProcSet(proc("c")), 0)))) sMessageList(datamsg(proc("a"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data(""))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(transmsg(transconf(sProcSet(proc("a")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")),
    0)))) sMessageList(datamsg(proc("a"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data("")))
    sMessageList(confmsg(regconf(sProcSet(proc("a")), 2), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b"))
    sProcSet(proc("c")), 0)))) sMessageList(datamsg(proc("a"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data(""))) sMessageList(confmsg(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 4), sProcSet(proc("b")) sProcSet(proc("c")))))
alldelivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b"))
    sProcSet(proc("c")), 0)))) sMessageList(datamsg(proc("a"), safe, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data(""))) 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"), sBroadcastSet(broadcast(sProcSet(proc("c")), ackmsg(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0),
    1, 0))))
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), eEventList)
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("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)), sNatSet(0))
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), eNatSet)
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    sNatSet(0))
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), eNatSet)
knownmsgs(proc("c"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    sNatSet(0))
Done reading in file: "test9.maude"