Reading in file: "ftest1.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"
==========================================

Reading in file: "ftest.maude"
==========================================
mod FTEST
Done reading in file: "ftest.maude"
==========================================
mod TEST-SPREAD
Advisory: redefining module TEST-SPREAD.
==========================================
rewrite in TEST-SPREAD : init .
rewrites: 650967 in 20330ms cpu (21270ms real) (32020 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(25)
sp-receive-req(agent("a"))
sp-receive-req(agent("c"))
gclients(sAgentList(agent("a")) sAgentList(agent("c")))
f-receive-req'(agent("a"))
f-receive-req'(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), 23, sNatSet(
    13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22), gdisconnectmsg(agent("b"), nogroup,
    noview))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 24, sNatSet(13) sNatSet(
    14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23), gdatamsg(agent("c"), group(
    "Winners"), fokmsg(agent("c"), group("Winners"))))))
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("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(
    agent("c")), 0), 1, sNatSet(0), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("a"),
    agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 2, sNatSet(0) sNatSet(1), gjoinmsg(agent("a"), group("Winners"),
    noview))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 3, sNatSet(0) sNatSet(1)
    sNatSet(2), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), group("Winners"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(
    agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 4, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3), gdatamsg(agent("c"), group("Winners"),
    fokmsg(agent("c"), group("Winners"))))) 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), 5, eNatSet, ggroupmsg(agent("a"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("a")))))))
    sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")), 2), 8, sNatSet(5), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"),
    group("Winners"))))) 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), 13, 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), 14,
    sNatSet(13), 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), 15, sNatSet(13) sNatSet(14), ggroupmsg(agent("c"),
    sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("c"))))))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a"))
    sProcSet(agent("b")) sProcSet(agent("c")), 7), 16, sNatSet(13) sNatSet(14) sNatSet(15), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"),
    group("Winners"))))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 17, sNatSet(
    13) sNatSet(14) sNatSet(15) sNatSet(16), gdatamsg(agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners"))))) sMessageList(datamsg(agent(
    "c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 18, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(
    17), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent(
    "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 19, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18), gleavemsg(agent(
    "a"), group("Winners"), noview))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7),
    20, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"),
    group("Winners"))))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 21, sNatSet(
    13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20), gdatamsg(agent("b"), group("Winners"), fokmsg(agent("b"),
    group("Winners"))))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 22,
    sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21), gdatamsg(agent("c"), group("Winners"),
    fdatamsg(agent("c"), group("Winners"), fdata("TEST"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group(
    "Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1))))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(
    agent("b")) sProcSet(agent("c")), 7), 23, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21)
    sNatSet(22), gdisconnectmsg(agent("b"), nogroup, noview))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b"))
    sProcSet(agent("c")), 7), 24, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22)
    sNatSet(23), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))))
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("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(
    agent("c")), 0), 1, sNatSet(0), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("a"),
    agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 2, sNatSet(0) sNatSet(1), gjoinmsg(agent("a"), group("Winners"),
    noview))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 3, sNatSet(0) sNatSet(1)
    sNatSet(2), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), group("Winners"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(
    agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 4, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3), gdatamsg(agent("c"), group("Winners"),
    fokmsg(agent("c"), group("Winners"))))) 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), 6, eNatSet, ggroupmsg(agent(
    "b"), eGroupAgentsList))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 7, sNatSet(6), ggroupmsg(
    agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("c"))))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent(
    "b")) sProcSet(agent("c")), 4), 9, sNatSet(6) sNatSet(7), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners")))))
    sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 10, sNatSet(6) sNatSet(7) sNatSet(9), gjoinmsg(agent(
    "b"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 11, sNatSet(6)
    sNatSet(7) sNatSet(9) sNatSet(10), gdatamsg(agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners"))))) sMessageList(datamsg(agent("c"),
    fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 12, sNatSet(6) sNatSet(7) sNatSet(9) sNatSet(10) sNatSet(11), gdatamsg(agent("c"),
    group("Winners"), fokmsg(agent("c"), group("Winners"))))) 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), 13, 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), 14, sNatSet(13), 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), 15, sNatSet(13) sNatSet(14), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"),
    sAgentList(agent("c"))))))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 16,
    sNatSet(13) sNatSet(14) sNatSet(15), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), group("Winners"))))) sMessageList(datamsg(agent("b"),
    fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 17, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16), gdatamsg(
    agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(
    agent("b")) sProcSet(agent("c")), 7), 18, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17), gdatamsg(agent("c"), group("Winners"), fokmsg(
    agent("c"), group("Winners"))))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7),
    19, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18), gleavemsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(
    agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 20, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16)
    sNatSet(17) sNatSet(18) sNatSet(19), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("b"),
    fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 21, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17)
    sNatSet(18) sNatSet(19) sNatSet(20), gdatamsg(agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners"))))) sMessageList(datamsg(agent("c"),
    agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 22, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17)
    sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), fdata("TEST"), view(
    regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1)))))
    sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 23, sNatSet(13) sNatSet(14)
    sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22), gdisconnectmsg(agent("b"), nogroup, noview)))
    sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 24, sNatSet(13) sNatSet(14)
    sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23), gdatamsg(agent("c"), group("Winners"),
    fokmsg(agent("c"), group("Winners"))))))
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("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(
    agent("c")), 0), 1, sNatSet(0), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("a"),
    agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 2, sNatSet(0) sNatSet(1), gjoinmsg(agent("a"), group("Winners"),
    noview))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 3, sNatSet(0) sNatSet(1)
    sNatSet(2), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), group("Winners"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(
    agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 4, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3), gdatamsg(agent("c"), group("Winners"),
    fokmsg(agent("c"), group("Winners"))))) 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), 6, eNatSet, ggroupmsg(agent(
    "b"), eGroupAgentsList))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 7, sNatSet(6), ggroupmsg(
    agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("c"))))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent(
    "b")) sProcSet(agent("c")), 4), 9, sNatSet(6) sNatSet(7), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners")))))
    sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 10, sNatSet(6) sNatSet(7) sNatSet(9), gjoinmsg(agent(
    "b"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 11, sNatSet(6)
    sNatSet(7) sNatSet(9) sNatSet(10), gdatamsg(agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners"))))) sMessageList(datamsg(agent("c"),
    fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 12, sNatSet(6) sNatSet(7) sNatSet(9) sNatSet(10) sNatSet(11), gdatamsg(agent("c"),
    group("Winners"), fokmsg(agent("c"), group("Winners"))))) 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), 13, 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), 14, sNatSet(13), 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), 15, sNatSet(13) sNatSet(14), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"),
    sAgentList(agent("c"))))))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 16,
    sNatSet(13) sNatSet(14) sNatSet(15), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), group("Winners"))))) sMessageList(datamsg(agent("b"),
    fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 17, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16), gdatamsg(
    agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(
    agent("b")) sProcSet(agent("c")), 7), 18, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17), gdatamsg(agent("c"), group("Winners"), fokmsg(
    agent("c"), group("Winners"))))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7),
    19, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18), gleavemsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(
    agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 20, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16)
    sNatSet(17) sNatSet(18) sNatSet(19), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("b"),
    fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 21, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17)
    sNatSet(18) sNatSet(19) sNatSet(20), gdatamsg(agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners"))))) sMessageList(datamsg(agent("c"),
    agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 22, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17)
    sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), fdata("TEST"), view(
    regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1)))))
    sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 23, sNatSet(13) sNatSet(14)
    sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22), gdisconnectmsg(agent("b"), nogroup, noview)))
    sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 24, sNatSet(13) sNatSet(14)
    sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23), gdatamsg(agent("c"), group("Winners"),
    fokmsg(agent("c"), group("Winners"))))))
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), sConstraintSet(constraint(agent("a"), 5, 8)))
causalorder(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sConstraintSet(constraint(agent("b"), 6, 10)) sConstraintSet(constraint(agent("b"), 6,
    11)) sConstraintSet(constraint(agent("b"), 7, 10)) sConstraintSet(constraint(agent("b"), 9, 10)) sConstraintSet(constraint(agent("b"), 10, 11))
    sConstraintSet(constraint(agent("c"), 6, 7)) sConstraintSet(constraint(agent("c"), 7, 9)) sConstraintSet(constraint(agent("c"), 7, 12))
    sConstraintSet(constraint(agent("c"), 9, 12)))
causalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sConstraintSet(constraint(agent("a"), 0, 2)) sConstraintSet(
    constraint(agent("a"), 1, 2)) sConstraintSet(constraint(agent("a"), 2, 3)) sConstraintSet(constraint(agent("c"), 0, 1)) sConstraintSet(constraint(
    agent("c"), 0, 4)) sConstraintSet(constraint(agent("c"), 1, 4)))
causalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sConstraintSet(constraint(agent("a"), 13, 16)) sConstraintSet(
    constraint(agent("a"), 13, 19)) sConstraintSet(constraint(agent("a"), 14, 19)) sConstraintSet(constraint(agent("a"), 15, 19)) sConstraintSet(
    constraint(agent("a"), 16, 19)) sConstraintSet(constraint(agent("a"), 17, 19)) sConstraintSet(constraint(agent("a"), 18, 19)) sConstraintSet(
    constraint(agent("b"), 13, 14)) sConstraintSet(constraint(agent("b"), 13, 23)) sConstraintSet(constraint(agent("b"), 14, 17)) sConstraintSet(
    constraint(agent("b"), 14, 21)) sConstraintSet(constraint(agent("b"), 14, 23)) sConstraintSet(constraint(agent("b"), 15, 23)) sConstraintSet(
    constraint(agent("b"), 16, 23)) sConstraintSet(constraint(agent("b"), 17, 21)) sConstraintSet(constraint(agent("b"), 17, 23)) sConstraintSet(
    constraint(agent("b"), 18, 23)) sConstraintSet(constraint(agent("b"), 19, 23)) sConstraintSet(constraint(agent("b"), 20, 23)) sConstraintSet(
    constraint(agent("b"), 21, 23)) sConstraintSet(constraint(agent("b"), 22, 23)) sConstraintSet(constraint(agent("c"), 13, 15)) sConstraintSet(
    constraint(agent("c"), 13, 22)) sConstraintSet(constraint(agent("c"), 14, 15)) sConstraintSet(constraint(agent("c"), 14, 22)) sConstraintSet(
    constraint(agent("c"), 15, 18)) sConstraintSet(constraint(agent("c"), 15, 20)) sConstraintSet(constraint(agent("c"), 15, 22)) sConstraintSet(
    constraint(agent("c"), 15, 24)) sConstraintSet(constraint(agent("c"), 16, 22)) sConstraintSet(constraint(agent("c"), 17, 22)) sConstraintSet(
    constraint(agent("c"), 18, 20)) sConstraintSet(constraint(agent("c"), 18, 22)) sConstraintSet(constraint(agent("c"), 18, 24)) sConstraintSet(
    constraint(agent("c"), 19, 22)) sConstraintSet(constraint(agent("c"), 20, 22)) sConstraintSet(constraint(agent("c"), 20, 24)) sConstraintSet(
    constraint(agent("c"), 21, 22)) sConstraintSet(constraint(agent("c"), 22, 24)))
causalorder(transconf(sProcSet(agent("a")), 1, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)), sConstraintSet(constraint(
    agent("a"), 0, 2)) sConstraintSet(constraint(agent("a"), 1, 2)) sConstraintSet(constraint(agent("a"), 2, 3)) sConstraintSet(constraint(agent("c"), 0,
    1)) sConstraintSet(constraint(agent("c"), 0, 4)) sConstraintSet(constraint(agent("c"), 1, 4)))
causalorder(transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)), sConstraintSet(constraint(agent("a"), 5, 8)))
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, 2)) sConstraintSet(constraint(agent("a"), 1, 2)) sConstraintSet(constraint(agent("a"), 2, 3))
    sConstraintSet(constraint(agent("c"), 0, 1)) sConstraintSet(constraint(agent("c"), 0, 4)) sConstraintSet(constraint(agent("c"), 1, 4)))
causalorder(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), sConstraintSet(constraint(
    agent("b"), 6, 10)) sConstraintSet(constraint(agent("b"), 6, 11)) sConstraintSet(constraint(agent("b"), 7, 10)) sConstraintSet(constraint(agent("b"),
    9, 10)) sConstraintSet(constraint(agent("b"), 10, 11)) sConstraintSet(constraint(agent("c"), 6, 7)) sConstraintSet(constraint(agent("c"), 7, 9))
    sConstraintSet(constraint(agent("c"), 7, 12)) sConstraintSet(constraint(agent("c"), 9, 12)))
totalorder(regconf(sProcSet(agent("a")), 2), sEventList(event(agent("a"), 5)) sEventList(event(agent("a"), 8)))
totalorder(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sEventList(event(agent("b"), 6)) sEventList(event(agent("b"), 6)) sEventList(event(
    agent("c"), 7)) sEventList(event(agent("c"), 7)) sEventList(event(agent("c"), 9)) sEventList(event(agent("c"), 9)) sEventList(event(agent("b"), 10))
    sEventList(event(agent("b"), 10)) sEventList(event(agent("b"), 11)) sEventList(event(agent("b"), 11)) sEventList(event(agent("c"), 12)) sEventList(
    event(agent("c"), 12)))
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("c"), 1)) sEventList(event(agent("c"), 1)) sEventList(event(agent("c"), 1)) sEventList(event(
    agent("a"), 2)) sEventList(event(agent("a"), 2)) sEventList(event(agent("a"), 2)) sEventList(event(agent("a"), 3)) sEventList(event(agent("a"), 3))
    sEventList(event(agent("a"), 3)) sEventList(event(agent("c"), 4)) sEventList(event(agent("c"), 4)) sEventList(event(agent("c"), 4)))
totalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sEventList(event(agent("a"), 13)) sEventList(event(agent("a"),
    13)) sEventList(event(agent("a"), 13)) sEventList(event(agent("b"), 14)) sEventList(event(agent("b"), 14)) sEventList(event(agent("b"), 14))
    sEventList(event(agent("c"), 15)) sEventList(event(agent("c"), 15)) sEventList(event(agent("c"), 15)) sEventList(event(agent("a"), 16)) sEventList(
    event(agent("a"), 16)) sEventList(event(agent("a"), 16)) sEventList(event(agent("b"), 17)) sEventList(event(agent("b"), 17)) sEventList(event(agent(
    "b"), 17)) sEventList(event(agent("c"), 18)) sEventList(event(agent("c"), 18)) sEventList(event(agent("c"), 18)) sEventList(event(agent("a"), 19))
    sEventList(event(agent("a"), 19)) sEventList(event(agent("a"), 19)) sEventList(event(agent("c"), 20)) sEventList(event(agent("c"), 20)) sEventList(
    event(agent("c"), 20)) sEventList(event(agent("b"), 21)) sEventList(event(agent("b"), 21)) sEventList(event(agent("b"), 21)) sEventList(event(agent(
    "c"), 22)) sEventList(event(agent("c"), 22)) sEventList(event(agent("c"), 22)) sEventList(event(agent("b"), 23)) sEventList(event(agent("b"), 23))
    sEventList(event(agent("b"), 23)) sEventList(event(agent("c"), 24)) sEventList(event(agent("c"), 24)) sEventList(event(agent("c"), 24)))
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("c"), 1)) sEventList(event(agent("c"), 1)) sEventList(
    event(agent("c"), 1)) sEventList(event(agent("a"), 2)) sEventList(event(agent("a"), 2)) sEventList(event(agent("a"), 2)) sEventList(event(agent("a"),
    3)) sEventList(event(agent("a"), 3)) sEventList(event(agent("a"), 3)) sEventList(event(agent("c"), 4)) sEventList(event(agent("c"), 4)) sEventList(
    event(agent("c"), 4)))
totalorder(transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)), sEventList(event(agent("a"), 5)) sEventList(event(agent("a"), 8)))
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("c"), 1)) sEventList(event(
    agent("c"), 1)) sEventList(event(agent("c"), 1)) sEventList(event(agent("a"), 2)) sEventList(event(agent("a"), 2)) sEventList(event(agent("a"), 2))
    sEventList(event(agent("a"), 3)) sEventList(event(agent("a"), 3)) sEventList(event(agent("a"), 3)) sEventList(event(agent("c"), 4)) sEventList(event(
    agent("c"), 4)) sEventList(event(agent("c"), 4)))
totalorder(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), sEventList(event(agent("b"),
    6)) sEventList(event(agent("b"), 6)) sEventList(event(agent("c"), 7)) sEventList(event(agent("c"), 7)) sEventList(event(agent("c"), 9)) sEventList(
    event(agent("c"), 9)) sEventList(event(agent("b"), 10)) sEventList(event(agent("b"), 10)) sEventList(event(agent("b"), 11)) sEventList(event(agent(
    "b"), 11)) sEventList(event(agent("c"), 12)) sEventList(event(agent("c"), 12)))
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"), eGMessageList)
gdelivered(agent("b"), eGMessageList)
gdelivered(agent("c"), eGMessageList)
f-receive-err(agent("b"), IllegalAgent)
fmembers(agent("a"), eGroupAgentsAgentsSet)
fmembers(agent("c"), sGroupAgentsAgentsSet(groupagentsagents(group("Winners"), sAgentSet(agent("c")), sAgentSet(agent("c")))))
fpending(agent("a"), eGroupOpSet)
fpending(agent("c"), eGroupOpSet)
ftrans(agent("a"), eGroupSet)
ftrans(agent("c"), eGroupSet)
fiview(agent("a"), eViewSet)
fiview(agent("c"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("c")),
    2)))
fpview(agent("a"), eViewSet)
fpview(agent("c"), eViewSet)
fbuffer(agent("a"), eGMessageList)
fbuffer(agent("c"), eGMessageList)
fdelivered(agent("a"), eFMessageList)
fdelivered(agent("b"), eFMessageList)
fdelivered(agent("c"), eFMessageList)
fdelivered'(agent("a"), sFMessageList(freqmsg(agent("a"), group("Winners"))) sFMessageList(fjoinmsg(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))) sFMessageList(
    ftransmsg(group("Winners"))) sFMessageList(freqmsg(agent("a"), group("Winners"))) sFMessageList(fconfmsg(group("Winners"), view(regconf(sProcSet(
    agent("a")), 2), group("Winners"), sAgentList(agent("a")), 0), sAgentSet(agent("a")))) sFMessageList(ftransmsg(group("Winners"))) sFMessageList(
    freqmsg(agent("a"), group("Winners"))) sFMessageList(fconfmsg(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")))) sFMessageList(
    fselfleavemsg(agent("a"), group("Winners"))))
fdelivered'(agent("b"), sFMessageList(freqmsg(agent("b"), group("Winners"))) sFMessageList(fjoinmsg(agent("b"), group("Winners"), view(regconf(sProcSet(
    agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("c")) sAgentList(agent("b")), 1))) sFMessageList(ftransmsg(group(
    "Winners"))) sFMessageList(freqmsg(agent("b"), group("Winners"))) sFMessageList(fconfmsg(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")))) sFMessageList(freqmsg(agent("b"), group("Winners"))) sFMessageList(fleavemsg(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)))
    sFMessageList(fdatamsg(agent("c"), group("Winners"), fdata("TEST"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7),
    group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1))))
fdelivered'(agent("c"), sFMessageList(freqmsg(agent("c"), group("Winners"))) sFMessageList(fjoinmsg(agent("c"), group("Winners"), view(regconf(sProcSet(
    agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(agent("c")), 0))) sFMessageList(freqmsg(agent("c"), group(
    "Winners"))) sFMessageList(fjoinmsg(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))) sFMessageList(ftransmsg(group("Winners"))) sFMessageList(freqmsg(agent("c"),
    group("Winners"))) sFMessageList(fconfmsg(group("Winners"), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(
    agent("c")), 0), sAgentSet(agent("c")))) sFMessageList(freqmsg(agent("c"), group("Winners"))) sFMessageList(fjoinmsg(agent("b"), group("Winners"),
    view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("c")) sAgentList(agent("b")), 1))) sFMessageList(
    ftransmsg(group("Winners"))) sFMessageList(freqmsg(agent("c"), group("Winners"))) sFMessageList(fconfmsg(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")))) sFMessageList(freqmsg(agent("c"), group("Winners"))) sFMessageList(fleavemsg(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))) sFMessageList(fdatamsg(agent("c"), group("Winners"), fdata("TEST"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b"))
    sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1))) sFMessageList(freqmsg(agent("c"), group("Winners")))
    sFMessageList(fdisconnectmsg(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(5) sNatSet(8))
localmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(2) sNatSet(3))
localmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(13) sNatSet(16) sNatSet(19))
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(6) sNatSet(10) sNatSet(11))
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(14) sNatSet(17) sNatSet(21) sNatSet(23))
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(7) sNatSet(9) sNatSet(12))
localmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1) sNatSet(4))
localmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(15) sNatSet(18) sNatSet(20) sNatSet(22)
    sNatSet(24))
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(5) sNatSet(8))
knownmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4))
knownmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16)
    sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24))
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(6) sNatSet(7) sNatSet(9) sNatSet(10) sNatSet(11) sNatSet(12))
knownmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4))
knownmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16)
    sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24))
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(6) sNatSet(7) sNatSet(9) sNatSet(10) sNatSet(11) sNatSet(12))
knownmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4))
knownmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16)
    sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24))
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)
fstate(agent("a"), sGroupSet(group("Winners")), eGroupSet, eGroupSet)
fstate(agent("c"), sGroupSet(group("Winners")), eGroupSet, eGroupSet)
Done reading in file: "ftest1.maude"