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

Reading in file: "test.maude"
==========================================
mod TEST
Advisory: redefining module TEST.
Done reading in file: "test.maude"
==========================================
mod TEST13
==========================================
rewrite in TEST13 : start .
rewrites: 43749 in 1180ms cpu (1190ms real) (37075 rewrites/second)
result State: multicast-ack(proc("a"))
multicast-ack(proc("b"))
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")) sProcSet(proc("b")), 4))
localconf(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4))
localconf(proc("c"), regconf(sProcSet(proc("c")), 2))
delivered(proc("a"), sMessageList(datamsg(proc("b"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test1"))) sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 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), 1, sNatSet(0), data(
    "test2"))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), sProcSet(proc("a")) sProcSet(proc("b")))))
delivered(proc("b"), sMessageList(datamsg(proc("b"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet, data(
    "test1"))) sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 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), 1, sNatSet(0), data(
    "test2"))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), sProcSet(proc("a")) sProcSet(proc("b")))))
delivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("c")), 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), 1, sNatSet(0), data("test2")))
    sMessageList(confmsg(regconf(sProcSet(proc("c")), 2), sProcSet(proc("c")))))
alldelivered(proc("a"), sMessageList(datamsg(proc("b"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test1"))) sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 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), 1, sNatSet(0), data(
    "test2"))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), sProcSet(proc("a")) sProcSet(proc("b")))))
alldelivered(proc("b"), sMessageList(datamsg(proc("b"), agreed, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 0, eNatSet,
    data("test1"))) sMessageList(transmsg(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 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), 1, sNatSet(0), data(
    "test2"))) sMessageList(confmsg(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), sProcSet(proc("a")) sProcSet(proc("b")))))
alldelivered(proc("c"), sMessageList(transmsg(transconf(sProcSet(proc("c")), 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), 1, sNatSet(0), data("test2")))
    sMessageList(confmsg(regconf(sProcSet(proc("c")), 2), sProcSet(proc("c")))))
reachable(proc("a"), sProcSet(proc("a")) sProcSet(proc("b")))
reachable(proc("b"), sProcSet(proc("a")) sProcSet(proc("b")))
reachable(proc("c"), sProcSet(proc("c")))
sent(proc("a"), sBroadcastSet(broadcast(sProcSet(proc("b")), ackmsg(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0),
    2, 1))) sBroadcastSet(broadcast(sProcSet(proc("c")), ackmsg(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), 2,
    1))))
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("c")), 2), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eConstraintSet)
causalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sConstraintSet(constraint(proc("a"), 0, 1)))
causalorder(transconf(sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sConstraintSet(constraint(proc(
    "a"), 0, 1)))
causalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    sConstraintSet(constraint(proc("a"), 0, 1)))
totalorder(regconf(sProcSet(proc("c")), 2), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eEventList)
totalorder(regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sEventList(event(proc("b"), 0)) sEventList(event(proc("b"), 0)))
totalorder(transconf(sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(event(proc("b"), 0))
    sEventList(event(proc("b"), 0)) sEventList(event(proc("a"), 1)))
totalorder(transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sEventList(
    event(proc("b"), 0)) sEventList(event(proc("b"), 0)) sEventList(event(proc("a"), 1)) sEventList(event(proc("a"), 1)))
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eNatSet)
localmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(1))
localmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eNatSet)
localmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
localmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("c")), 2), eNatSet)
localmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
localmsgs(proc("c"), transconf(sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eNatSet)
knownmsgs(proc("a"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0) sNatSet(1))
knownmsgs(proc("a"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    sNatSet(0) sNatSet(1))
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")), 4), eNatSet)
knownmsgs(proc("b"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), sNatSet(0))
knownmsgs(proc("b"), transconf(sProcSet(proc("a")) sProcSet(proc("b")), 3, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)),
    sNatSet(0) sNatSet(1))
knownmsgs(proc("c"), regconf(sProcSet(proc("c")), 2), eNatSet)
knownmsgs(proc("c"), regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0), eNatSet)
knownmsgs(proc("c"), transconf(sProcSet(proc("c")), 1, regconf(sProcSet(proc("a")) sProcSet(proc("b")) sProcSet(proc("c")), 0)), sNatSet(0) sNatSet(1))
Done reading in file: "test13.maude"