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

Reading in file: "test.maude"
==========================================
mod TEST
Advisory: redefining module TEST.
Done reading in file: "test.maude"
==========================================
mod TEST10
==========================================
rewrite in TEST10 : start .
rewrites: 30961 in 200ms cpu (200ms real) (154805 rewrites/second)
result State: multicast-ack(proc("a"))
network(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")))
freshconf(11)
operational(proc("a"))
operational(proc("b"))
operational(proc("c"))
freshseq(4)
CONTROLLER(eController)
localconf(proc("a"), regconf(sProcSet(proc("a")), 4))
localconf(proc("b"), regconf(sProcSet(proc("b")), 8))
localconf(proc("c"), regconf(sProcSet(proc("c")), 10))
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")))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(
    proc("a")), 2)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
delivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 5, 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")), 6), sProcSet(proc("b")) sProcSet(proc("c")))) sMessageList(transmsg(
    transconf(sProcSet(proc("b")), 7, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6)))) sMessageList(confmsg(regconf(sProcSet(proc("b")), 8),
    sProcSet(proc("b")))))
delivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("c")), 9, 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("c")), 10), 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")))) sMessageList(transmsg(transconf(sProcSet(proc("a")), 3, regconf(sProcSet(
    proc("a")), 2)))) sMessageList(confmsg(regconf(sProcSet(proc("a")), 4), sProcSet(proc("a")))))
alldelivered(proc("b"), sMessageList(transmsg(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 5, 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")), 6), sProcSet(proc("b")) sProcSet(proc("c")))) sMessageList(transmsg(
    transconf(sProcSet(proc("b")), 7, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6)))) sMessageList(confmsg(regconf(sProcSet(proc("b")), 8),
    sProcSet(proc("b")))))
alldelivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("c")), 9, 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("c")), 10), sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")))
reachable(proc("b"), sProcSet(proc("b")))
reachable(proc("c"), 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("a")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")), 8), eConstraintSet)
causalorder(regconf(sProcSet(proc("c")), 10), eConstraintSet)
causalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6), 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("a")), 3, regconf(sProcSet(proc("a")), 2)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")), 7, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6)), eConstraintSet)
causalorder(transconf(sProcSet(proc("c")), 9, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eConstraintSet)
causalorder(transconf(sProcSet(proc("b")) sProcSet(proc("c")), 5, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eConstraintSet)
totalorder(regconf(sProcSet(proc("a")), 2), eEventList)
totalorder(regconf(sProcSet(proc("a")), 4), eEventList)
totalorder(regconf(sProcSet(proc("b")), 8), eEventList)
totalorder(regconf(sProcSet(proc("c")), 10), eEventList)
totalorder(regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 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("a")), 3, regconf(sProcSet(proc("a")), 2)), eEventList)
totalorder(transconf(sProcSet(proc("b")), 7, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6)), eEventList)
totalorder(transconf(sProcSet(proc("c")), 9, 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")), 5, 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")), 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("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")), 2)), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")), 8), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")), 7, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6)), eNatSet)
localmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 5, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("c")), 10), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("c")), 9, 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")), 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("a"), transconf(sProcSet(proc("a")), 3, regconf(sProcSet(proc("a")), 2)), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")), 8), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
knownmsgs(proc("b"), transconf(sProcSet(proc("b")), 7, regconf(sProcSet(proc("b")) sProcSet(proc("c")), 6)), eNatSet)
knownmsgs(proc("b"), transconf(sProcSet(proc("b")) sProcSet(proc("c")), 5, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    sNatSet(0))
knownmsgs(proc("c"), regconf(sProcSet(proc("c")), 10), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
knownmsgs(proc("c"), transconf(sProcSet(proc("c")), 9, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sNatSet(0))
Done reading in file: "test10.maude"