Reading in file: "gtest4.maude"
==========================================
 
Reading in file: "test.maude"
==========================================
mod TEST
Advisory: redefining module TEST.
Done reading in file: "test.maude"
==========================================

Reading in file: "gtest.maude"
==========================================
fmod GTEST
Advisory: redefining module GTEST.
Done reading in file: "gtest.maude"
==========================================
mod TEST-SPREAD
Advisory: redefining module TEST-SPREAD.
==========================================
rewrite in TEST-SPREAD : init .
rewrites: 133746 in 1250ms cpu (1250ms real) (106996 rewrites/second)
result State: network(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))
freshconf(5)
operational(agent("a"))
operational(agent("b"))
operational(agent("c"))
freshseq(9)
gclients(sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
CONTROLLER(eController)
a(7)
b(7)
c(3)
localconf(agent("a"), regconf(sProcSet(agent("a")), 2))
localconf(agent("b"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4))
localconf(agent("c"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4))
delivered(agent("a"), eMessageList)
delivered(agent("b"), eMessageList)
delivered(agent("c"), eMessageList)
alldelivered(agent("a"), sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 0, eNatSet,
    gjoinmsg(agent("c"), group("Winners"), noview))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(
    agent("c")), 0), 1, sNatSet(0), gjoinmsg(agent("a"), group("Winners"), noview))) sMessageList(transmsg(transconf(sProcSet(agent("a")), 1, regconf(
    sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)))) sMessageList(confmsg(regconf(sProcSet(agent("a")), 2), sProcSet(agent("a"))))
    sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")), 2), 6, eNatSet, ggroupmsg(agent("a"), sGroupAgentsList(groupagents(group(
    "Winners"), sAgentList(agent("a"))))))))
alldelivered(agent("b"), sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 0, eNatSet,
    gjoinmsg(agent("c"), group("Winners"), noview))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(
    agent("c")), 0), 1, sNatSet(0), gjoinmsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent(
    "a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 5, sNatSet(0) sNatSet(1), gjoinmsg(agent("b"), group("Winners"), noview))) sMessageList(
    transmsg(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))))
    sMessageList(datamsg(agent("c"), safe, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 2, sNatSet(0) sNatSet(1),
    gdatamsg(agent("c"), group("Winners"), gdata("test")))) sMessageList(confmsg(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sProcSet(agent(
    "b")) sProcSet(agent("c")))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 7, eNatSet, ggroupmsg(
    agent("b"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("b"))))))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(
    agent("b")) sProcSet(agent("c")), 4), 8, sNatSet(7), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent(
    "c"))))))))
alldelivered(agent("c"), sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 0, eNatSet,
    gjoinmsg(agent("c"), group("Winners"), noview))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(
    agent("c")), 0), 1, sNatSet(0), gjoinmsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent(
    "a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 5, sNatSet(0) sNatSet(1), gjoinmsg(agent("b"), group("Winners"), noview))) sMessageList(
    transmsg(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))))
    sMessageList(datamsg(agent("c"), safe, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 2, sNatSet(0) sNatSet(1),
    gdatamsg(agent("c"), group("Winners"), gdata("test")))) sMessageList(confmsg(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sProcSet(agent(
    "b")) sProcSet(agent("c")))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 7, eNatSet, ggroupmsg(
    agent("b"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("b"))))))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(
    agent("b")) sProcSet(agent("c")), 4), 8, sNatSet(7), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent(
    "c"))))))))
reachable(agent("a"), sProcSet(agent("a")))
reachable(agent("b"), sProcSet(agent("b")) sProcSet(agent("c")))
reachable(agent("c"), sProcSet(agent("b")) sProcSet(agent("c")))
sent(agent("a"), eBroadcastSet)
sent(agent("b"), eBroadcastSet)
sent(agent("c"), eBroadcastSet)
received(agent("a"), eMessageSet)
received(agent("b"), eMessageSet)
received(agent("c"), eMessageSet)
acked(agent("a"), eMessageSet)
acked(agent("b"), eMessageSet)
acked(agent("c"), eMessageSet)
causalorder(regconf(sProcSet(agent("a")), 2), eConstraintSet)
causalorder(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sConstraintSet(constraint(agent("c"), 7, 8)))
causalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sConstraintSet(constraint(agent("a"), 0, 1)) sConstraintSet(
    constraint(agent("b"), 0, 5)) sConstraintSet(constraint(agent("b"), 1, 5)) sConstraintSet(constraint(agent("c"), 0, 2)) sConstraintSet(constraint(
    agent("c"), 1, 2)))
causalorder(transconf(sProcSet(agent("a")), 1, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)), sConstraintSet(constraint(
    agent("a"), 0, 1)) sConstraintSet(constraint(agent("b"), 0, 5)) sConstraintSet(constraint(agent("b"), 1, 5)) sConstraintSet(constraint(agent("c"), 0,
    2)) sConstraintSet(constraint(agent("c"), 1, 2)))
causalorder(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)),
    sConstraintSet(constraint(agent("a"), 0, 1)) sConstraintSet(constraint(agent("b"), 0, 5)) sConstraintSet(constraint(agent("b"), 1, 5))
    sConstraintSet(constraint(agent("c"), 0, 2)) sConstraintSet(constraint(agent("c"), 1, 2)))
totalorder(regconf(sProcSet(agent("a")), 2), sEventList(event(agent("a"), 6)))
totalorder(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sEventList(event(agent("b"), 7)) sEventList(event(agent("b"), 7)) sEventList(event(
    agent("c"), 8)) sEventList(event(agent("c"), 8)))
totalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sEventList(event(agent("c"), 0)) sEventList(event(agent("c"), 0))
    sEventList(event(agent("c"), 0)) sEventList(event(agent("a"), 1)) sEventList(event(agent("a"), 1)) sEventList(event(agent("a"), 1)) sEventList(event(
    agent("b"), 5)) sEventList(event(agent("b"), 5)))
totalorder(transconf(sProcSet(agent("a")), 1, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)), sEventList(event(agent("c"),
    0)) sEventList(event(agent("c"), 0)) sEventList(event(agent("c"), 0)) sEventList(event(agent("a"), 1)) sEventList(event(agent("a"), 1)) sEventList(
    event(agent("a"), 1)) sEventList(event(agent("b"), 5)) sEventList(event(agent("b"), 5)))
totalorder(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)),
    sEventList(event(agent("c"), 0)) sEventList(event(agent("c"), 0)) sEventList(event(agent("c"), 0)) sEventList(event(agent("a"), 1)) sEventList(event(
    agent("a"), 1)) sEventList(event(agent("a"), 1)) sEventList(event(agent("b"), 5)) sEventList(event(agent("b"), 5)) sEventList(event(agent("c"), 2))
    sEventList(event(agent("c"), 2)))
gjoined(agent("a"), sGroupList(group("Winners")))
gjoined(agent("b"), sGroupList(group("Winners")))
gjoined(agent("c"), sGroupList(group("Winners")))
gview(agent("a"), sViewSet(view(regconf(sProcSet(agent("a")), 2), group("Winners"), sAgentList(agent("a")), 0)))
gview(agent("b"), sViewSet(view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")),
    0)))
gview(agent("c"), sViewSet(view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")),
    0)))
glocalconf(agent("a"), regconf(sProcSet(agent("a")), 2))
glocalconf(agent("b"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4))
glocalconf(agent("c"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4))
gdelivered(agent("a"), sGMessageList(gjoinmsg(agent("a"), group("Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0), group("Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1))) sGMessageList(gtransmsg(group("Winners"))) sGMessageList(gconfmsg(group(
    "Winners"), view(regconf(sProcSet(agent("a")), 2), group("Winners"), sAgentList(agent("a")), 0), sAgentSet(agent("a")))))
gdelivered(agent("b"), sGMessageList(gjoinmsg(agent("b"), group("Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0), group("Winners"), sAgentList(agent("c")) sAgentList(agent("a")) sAgentList(agent("b")), 2))) sGMessageList(gtransmsg(group("Winners")))
    sGMessageList(gdatamsg(agent("c"), group("Winners"), gdata("test"))) sGMessageList(gconfmsg(group("Winners"), view(regconf(sProcSet(agent("b"))
    sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 0), sAgentSet(agent("b")) sAgentSet(agent("c")))))
gdelivered(agent("c"), sGMessageList(gjoinmsg(agent("c"), group("Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0), group("Winners"), sAgentList(agent("c")), 0))) sGMessageList(gjoinmsg(agent("a"), group("Winners"), view(regconf(sProcSet(agent("a")) sProcSet(
    agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1))) sGMessageList(gjoinmsg(agent("b"), group(
    "Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(agent("c")) sAgentList(
    agent("a")) sAgentList(agent("b")), 2))) sGMessageList(gtransmsg(group("Winners"))) sGMessageList(gdatamsg(agent("c"), group("Winners"), gdata(
    "test"))) sGMessageList(gconfmsg(group("Winners"), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent(
    "b")) sAgentList(agent("c")), 0), sAgentSet(agent("b")) sAgentSet(agent("c")))))
localmsgs(agent("a"), regconf(sProcSet(agent("a")), 2), sNatSet(6))
localmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(1))
localmsgs(agent("a"), transconf(sProcSet(agent("a")), 1, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)), eNatSet)
localmsgs(agent("b"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sNatSet(7))
localmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(5))
localmsgs(agent("b"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0)), eNatSet)
localmsgs(agent("c"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sNatSet(8))
localmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(2))
localmsgs(agent("c"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0)), eNatSet)
knownmsgs(agent("a"), regconf(sProcSet(agent("a")), 2), sNatSet(6))
knownmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1))
knownmsgs(agent("a"), transconf(sProcSet(agent("a")), 1, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)), eNatSet)
knownmsgs(agent("b"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sNatSet(7) sNatSet(8))
knownmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1) sNatSet(5))
knownmsgs(agent("b"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0)), sNatSet(0) sNatSet(1) sNatSet(2))
knownmsgs(agent("c"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sNatSet(7) sNatSet(8))
knownmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(5))
knownmsgs(agent("c"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0)), sNatSet(0) sNatSet(1) sNatSet(2))
gstate(goperational(agent("a"))
goperational(agent("b"))
goperational(agent("c")), eState, eState, eState)
Done reading in file: "gtest4.maude"