Reading in file: "gtest1.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
Done reading in file: "gtest.maude"
==========================================
mod TEST-SPREAD
==========================================
rewrite in TEST-SPREAD : init .
rewrites: 57541 in 1950ms cpu (2010ms real) (29508 rewrites/second)
result State: network(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))
freshconf(8)
operational(agent("a"))
operational(agent("b"))
operational(agent("c"))
freshseq(11)
gclients(sAgentList(agent("a")) sAgentList(agent("c")))
CONTROLLER(eController)
a(7)
b(7)
c(3)
localconf(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7))
localconf(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7))
localconf(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7))
delivered(agent("a"), eMessageList)
delivered(agent("b"), sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 10, sNatSet(6)
    sNatSet(7) sNatSet(8) sNatSet(9), gdisconnectmsg(agent("b"), nogroup, noview))))
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), 2, eNatSet, ggroupmsg(agent("a"), sGroupAgentsList(groupagents(group(
    "Winners"), sAgentList(agent("a"))))))) sMessageList(transmsg(transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)))) sMessageList(
    confmsg(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sProcSet(agent("a")))) sMessageList(datamsg(agent("a"), agreed,
    regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 6, eNatSet, ggroupmsg(agent("a"), sGroupAgentsList(groupagents(group(
    "Winners"), sAgentList(agent("a"))))))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent(
    "c")), 7), 7, sNatSet(6), ggroupmsg(agent("b"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("b"))))))) sMessageList(datamsg(
    agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 8, sNatSet(6) sNatSet(7), ggroupmsg(agent("c"),
    sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("c"))))))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a"))
    sProcSet(agent("b")) sProcSet(agent("c")), 7), 9, sNatSet(6) sNatSet(7) sNatSet(8), gleavemsg(agent("a"), group("Winners"), noview))) sMessageList(
    datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 10, sNatSet(6) sNatSet(7) sNatSet(8) sNatSet(
    9), gdisconnectmsg(agent("b"), nogroup, noview))))
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(transmsg(transconf(sProcSet(agent("b")) sProcSet(agent(
    "c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)))) 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), 3, eNatSet, ggroupmsg(agent("b"), eGroupAgentsList))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("b")) sProcSet(
    agent("c")), 4), 4, sNatSet(3), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("c"))))))) sMessageList(
    datamsg(agent("b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 5, sNatSet(3) sNatSet(4), gjoinmsg(agent("b"), group("Winners"),
    noview))) sMessageList(transmsg(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4))))
    sMessageList(confmsg(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sProcSet(agent("b")) sProcSet(agent("c"))))
    sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 6, eNatSet, ggroupmsg(agent(
    "a"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("a"))))))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent(
    "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 7, sNatSet(6), ggroupmsg(agent("b"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(
    agent("b"))))))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 8, sNatSet(6)
    sNatSet(7), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("c"))))))) sMessageList(datamsg(agent("a"), agreed,
    regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 9, sNatSet(6) sNatSet(7) sNatSet(8), gleavemsg(agent("a"), group(
    "Winners"), noview))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 10,
    sNatSet(6) sNatSet(7) sNatSet(8) sNatSet(9), gdisconnectmsg(agent("b"), nogroup, noview))))
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(transmsg(transconf(sProcSet(agent("b")) sProcSet(agent(
    "c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)))) 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), 3, eNatSet, ggroupmsg(agent("b"), eGroupAgentsList))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("b")) sProcSet(
    agent("c")), 4), 4, sNatSet(3), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("c"))))))) sMessageList(
    datamsg(agent("b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 5, sNatSet(3) sNatSet(4), gjoinmsg(agent("b"), group("Winners"),
    noview))) sMessageList(transmsg(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4))))
    sMessageList(confmsg(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sProcSet(agent("b")) sProcSet(agent("c"))))
    sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 6, eNatSet, ggroupmsg(agent(
    "a"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("a"))))))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent(
    "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 7, sNatSet(6), ggroupmsg(agent("b"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(
    agent("b"))))))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 8, sNatSet(6)
    sNatSet(7), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("c"))))))) sMessageList(datamsg(agent("a"), agreed,
    regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 9, sNatSet(6) sNatSet(7) sNatSet(8), gleavemsg(agent("a"), group(
    "Winners"), noview))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 10,
    sNatSet(6) sNatSet(7) sNatSet(8) sNatSet(9), gdisconnectmsg(agent("b"), nogroup, noview))))
reachable(agent("a"), sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))
reachable(agent("b"), sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))
reachable(agent("c"), sProcSet(agent("a")) 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("b"), 3, 5)) sConstraintSet(constraint(agent("b"), 4,
    5)) sConstraintSet(constraint(agent("c"), 3, 4)))
causalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sConstraintSet(constraint(agent("a"), 0, 1)))
causalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sConstraintSet(constraint(agent("a"), 6, 9)) sConstraintSet(
    constraint(agent("a"), 7, 9)) sConstraintSet(constraint(agent("a"), 8, 9)) sConstraintSet(constraint(agent("b"), 6, 7)) sConstraintSet(constraint(
    agent("b"), 6, 10)) sConstraintSet(constraint(agent("b"), 7, 10)) sConstraintSet(constraint(agent("b"), 8, 10)) sConstraintSet(constraint(agent("b"),
    9, 10)) sConstraintSet(constraint(agent("c"), 6, 8)) sConstraintSet(constraint(agent("c"), 7, 8)))
causalorder(transconf(sProcSet(agent("a")), 1, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)), sConstraintSet(constraint(
    agent("a"), 0, 1)))
causalorder(transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)), eConstraintSet)
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)))
causalorder(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), sConstraintSet(constraint(
    agent("b"), 3, 5)) sConstraintSet(constraint(agent("b"), 4, 5)) sConstraintSet(constraint(agent("c"), 3, 4)))
totalorder(regconf(sProcSet(agent("a")), 2), sEventList(event(agent("a"), 2)))
totalorder(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sEventList(event(agent("b"), 3)) sEventList(event(agent("b"), 3)) sEventList(event(
    agent("c"), 4)) sEventList(event(agent("c"), 4)) sEventList(event(agent("b"), 5)) sEventList(event(agent("b"), 5)))
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)))
totalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sEventList(event(agent("a"), 6)) sEventList(event(agent("a"), 6))
    sEventList(event(agent("a"), 6)) sEventList(event(agent("b"), 7)) sEventList(event(agent("b"), 7)) sEventList(event(agent("b"), 7)) sEventList(event(
    agent("c"), 8)) sEventList(event(agent("c"), 8)) sEventList(event(agent("c"), 8)) sEventList(event(agent("a"), 9)) sEventList(event(agent("a"), 9))
    sEventList(event(agent("a"), 9)) sEventList(event(agent("b"), 10)) sEventList(event(agent("b"), 10)) sEventList(event(agent("b"), 10)))
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)))
totalorder(transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)), sEventList(event(agent("a"), 2)))
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)))
totalorder(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), sEventList(event(agent("b"),
    3)) sEventList(event(agent("b"), 3)) sEventList(event(agent("c"), 4)) sEventList(event(agent("c"), 4)) sEventList(event(agent("b"), 5)) sEventList(
    event(agent("b"), 5)))
gjoined(agent("a"), eGroupList)
gjoined(agent("b"), eGroupList)
gjoined(agent("c"), sGroupList(group("Winners")))
gview(agent("a"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("c")),
    2)))
gview(agent("b"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b"))
    sAgentList(agent("c")), 1)))
gview(agent("c"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("c")),
    2)))
glocalconf(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7))
glocalconf(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7))
glocalconf(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7))
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")))) sGMessageList(gtransmsg(
    group("Winners"))) sGMessageList(gconfmsg(group("Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group(
    "Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), 0), sAgentSet(agent("a")))) sGMessageList(gselfleavemsg(agent("a"),
    group("Winners"))))
gdelivered(agent("b"), eGMessageList)
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(gtransmsg(group(
    "Winners"))) sGMessageList(gconfmsg(group("Winners"), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent(
    "c")), 0), sAgentSet(agent("c")))) sGMessageList(gjoinmsg(agent("b"), group("Winners"), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4),
    group("Winners"), sAgentList(agent("c")) sAgentList(agent("b")), 1))) sGMessageList(gtransmsg(group("Winners"))) sGMessageList(gconfmsg(group(
    "Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(
    agent("b")) sAgentList(agent("c")), 0), sAgentSet(agent("b")) sAgentSet(agent("c")))) sGMessageList(gleavemsg(agent("a"), group("Winners"), view(
    regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1)))
    sGMessageList(gdisconnectmsg(agent("b"), group("Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group(
    "Winners"), sAgentList(agent("c")), 2))))
localmsgs(agent("a"), regconf(sProcSet(agent("a")), 2), sNatSet(2))
localmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(1))
localmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(6) sNatSet(9))
localmsgs(agent("a"), transconf(sProcSet(agent("a")), 1, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)), eNatSet)
localmsgs(agent("a"), transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)), eNatSet)
localmsgs(agent("b"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sNatSet(3) sNatSet(5))
localmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), eNatSet)
localmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(7) sNatSet(10))
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("b"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), eNatSet)
localmsgs(agent("c"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sNatSet(4))
localmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0))
localmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(8))
localmsgs(agent("c"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0)), eNatSet)
localmsgs(agent("c"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), eNatSet)
knownmsgs(agent("a"), regconf(sProcSet(agent("a")), 2), sNatSet(2))
knownmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1))
knownmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(6) sNatSet(7) sNatSet(8) sNatSet(9) sNatSet(
    10))
knownmsgs(agent("a"), transconf(sProcSet(agent("a")), 1, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)), eNatSet)
knownmsgs(agent("a"), transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)), eNatSet)
knownmsgs(agent("b"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sNatSet(3) sNatSet(4) sNatSet(5))
knownmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1))
knownmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(6) sNatSet(7) sNatSet(8) sNatSet(9) sNatSet(
    10))
knownmsgs(agent("b"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0)), eNatSet)
knownmsgs(agent("b"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), eNatSet)
knownmsgs(agent("c"), regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sNatSet(3) sNatSet(4) sNatSet(5))
knownmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1))
knownmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(6) sNatSet(7) sNatSet(8) sNatSet(9) sNatSet(
    10))
knownmsgs(agent("c"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 3, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")),
    0)), eNatSet)
knownmsgs(agent("c"), transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), eNatSet)
gstate(goperational(agent("a"))
goperational(agent("b"))
goperational(agent("c")), eState, eState, eState)
Done reading in file: "gtest1.maude"