--- got stuck because the multicast to a private group is sent in agreed mode!
--- therefore can not proceed without the message that we dropped!


Maude> in stestevs6
==========================================

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: "stest.maude"
==========================================
mod STEST
Advisory: redefining module STEST.
Done reading in file: "stest.maude"
==========================================
mod TEST-SECURESPREAD
Advisory: redefining module TEST-SECURESPREAD.
Advisory: "cliques.maude", line 67 (mod CLIQUES): collapse at top of x:PartialKey * inv(x:PartialKey) may cause it
    to match more than you expect.
Advisory: "cliques.maude", line 84 (mod CLIQUES): collapse at top of x:KeyShare * inv(x:KeyShare) may cause it to
    match more than you expect.
==========================================
rewrite in TEST-SECURESPREAD : init .
rewrites: 205072 in 2910ms cpu (5970ms real) (70471 rewrites/second)
result State: ENABLED(MULTICAST(agent("c"), privategroup(agent("a"))))
network(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))
freshconf(1)
operational(agent("a"))
operational(agent("b"))
operational(agent("c"))
freshseq(6)
sp-receive-req(agent("a"))
sp-receive-req(agent("b"))
sp-receive-req(agent("c"))
gclients(sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")))
f-receive-req'(agent("a"))
f-receive-req'(agent("b"))
f-receive-req'(agent("c"))
fresh(0)
freshkeyid(1)
ssp-receive-req'(agent("a"))
ssp-receive-req'(agent("b"))
ssp-receive-req'(agent("c"))
CONTROLLER(WAITFOR(MULTICAST(agent("c"), privategroup(agent("a")))) ; PERFORM(SEND(agent("c"), 6)) ; PERFORM(
    RECEIVE(agent("a"), 6)) ; PERFORM(RECEIVE(agent("b"), 6)) ; PERFORM(RECEIVE(agent("c"), 6)) ; PERFORM(
    MULTICAST(agent("a"), group("Winners"))) ; PERFORM(SEND(agent("a"), 7)) ; PERFORM(RECEIVE(agent("a"), 7)) ;
    PERFORM(RECEIVE(agent("b"), 7)) ; PERFORM(RECEIVE(agent("c"), 7)) ; PERFORM(MULTICAST(agent("c"),
    privategroup(agent("a")))) ; PERFORM(SEND(agent("c"), 8)) ; PERFORM(RECEIVE(agent("a"), 8)) ; PERFORM(RECEIVE(
    agent("b"), 8)) ; PERFORM(RECEIVE(agent("c"), 8)) ; PERFORM(MULTICAST(agent("a"), group("Winners"))) ;
    PERFORM(SEND(agent("a"), 9)) ; PERFORM(RECEIVE(agent("a"), 9)) ; PERFORM(RECEIVE(agent("b"), 9)) ; PERFORM(
    RECEIVE(agent("c"), 9)) ; PERFORM(DELIVERCHANGE(agent("a"))) ; PERFORM(DELIVERCHANGE(agent("c"))) ; PERFORM(
    RECEIVE(agent("a"), 2)) ; PERFORM(RECEIVE(agent("b"), 2)) ; PERFORM(RECEIVE(agent("c"), 2)) ; PERFORM(CHANGE(
    agent("a"), sProcSet(agent("a")))) ; PERFORM(CHANGE(agent("b"), sProcSet(agent("b")) sProcSet(agent("c")))) ;
    PERFORM(CHANGE(agent("c"), sProcSet(agent("b")) sProcSet(agent("c")))) ; (PERFORM(EVS-START(agent("a"), true))
    || PERFORM(EVS-START(agent("b"), true)) || PERFORM(EVS-START'(agent("c"), true))) ; PERFORM(SENDGROUPMSG(
    agent("a"))) ; PERFORM(SEND(agent("a"), 10)) ; PERFORM(RECEIVE(agent("a"), 10)) ; PERFORM(LOSE(agent("b"),
    10)) ; PERFORM(LOSE(agent("c"), 10)) ; PERFORM(SENDGROUPMSG(agent("b"))) ; PERFORM(SEND(agent("b"), 11)) ;
    PERFORM(LOSE(agent("a"), 11)) ; PERFORM(RECEIVE(agent("b"), 11)) ; PERFORM(RECEIVE(agent("c"), 11)) ; PERFORM(
    SENDGROUPMSG(agent("c"))) ; PERFORM(SEND(agent("c"), 12)) ; PERFORM(LOSE(agent("a"), 12)) ; PERFORM(RECEIVE(
    agent("b"), 12)) ; PERFORM(RECEIVE(agent("c"), 12)) ; PERFORM(DELIVERCHANGE(agent("a"))) ; PERFORM(
    DELIVERCHANGE(agent("c"))) ; PERFORM(FLUSHOK(agent("a"))) ; PERFORM(MULTICAST(agent("a"), group("Winners"))) ;
    PERFORM(SEND(agent("a"), 13)) ; PERFORM(RECEIVE(agent("a"), 13)) ; PERFORM(LOSE(agent("b"), 13)) ; PERFORM(
    LOSE(agent("c"), 13)) ; PERFORM(FLUSHOK(agent("c"))) ; PERFORM(MULTICAST(agent("c"), group("Winners"))) ;
    PERFORM(SEND(agent("c"), 14)) ; PERFORM(LOSE(agent("a"), 14)) ; PERFORM(RECEIVE(agent("b"), 14)) ; PERFORM(
    RECEIVE(agent("c"), 14)) ; PERFORM(DELIVERCHANGE(agent("a"))) ; PERFORM(DELIVERCHANGE(agent("c"))) ; PERFORM(
    JOIN(agent("b"), group("Winners"))) ; PERFORM(SEND(agent("b"), 15)) ; PERFORM(LOSE(agent("a"), 15)) ; PERFORM(
    RECEIVE(agent("b"), 15)) ; PERFORM(RECEIVE(agent("c"), 15)) ; PERFORM(FLUSHOK(agent("b"))) ; PERFORM(
    MULTICAST(agent("b"), group("Winners"))) ; PERFORM(SEND(agent("b"), 16)) ; PERFORM(LOSE(agent("a"), 16)) ;
    PERFORM(RECEIVE(agent("b"), 16)) ; PERFORM(RECEIVE(agent("c"), 16)) ; PERFORM(FLUSHOK(agent("c"))) ; PERFORM(
    MULTICAST(agent("c"), group("Winners"))) ; PERFORM(SEND(agent("c"), 17)) ; PERFORM(LOSE(agent("a"), 17)) ;
    PERFORM(RECEIVE(agent("b"), 17)) ; PERFORM(RECEIVE(agent("c"), 17)) ; PERFORM(MULTICAST(agent("c"),
    privategroup(agent("b")))) ; PERFORM(SEND(agent("c"), 18)) ; PERFORM(LOSE(agent("a"), 18)) ; PERFORM(RECEIVE(
    agent("b"), 18)) ; PERFORM(RECEIVE(agent("c"), 18)) ; PERFORM(MULTICAST(agent("b"), group("Winners"))) ;
    PERFORM(SEND(agent("b"), 19)) ; PERFORM(LOSE(agent("a"), 19)) ; PERFORM(RECEIVE(agent("b"), 19)) ; PERFORM(
    RECEIVE(agent("c"), 19)) ; PERFORM(MULTICAST(agent("c"), privategroup(agent("b")))) ; PERFORM(SEND(agent("c"),
    20)) ; PERFORM(LOSE(agent("a"), 20)) ; PERFORM(RECEIVE(agent("b"), 20)) ; PERFORM(RECEIVE(agent("c"), 20)) ;
    PERFORM(MULTICAST(agent("b"), group("Winners"))) ; PERFORM(SEND(agent("b"), 21)) ; PERFORM(LOSE(agent("a"),
    21)) ; PERFORM(RECEIVE(agent("b"), 21)) ; PERFORM(RECEIVE(agent("c"), 21)) ; PERFORM(DELIVERCHANGE(agent(
    "b"))) ; PERFORM(DELIVERCHANGE(agent("c"))) ; PERFORM(CHANGE(agent("a"), sProcSet(agent("a")) sProcSet(agent(
    "b")) sProcSet(agent("c")))) ; PERFORM(CHANGE(agent("b"), sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(
    agent("c")))) ; PERFORM(CHANGE(agent("c"), sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")))) ;
    (PERFORM(EVS-START(agent("a"), true)) || PERFORM(EVS-START(agent("b"), true)) || PERFORM(EVS-START'(agent(
    "c"), true))) ; PERFORM(SENDGROUPMSG(agent("a"))) ; PERFORM(SEND(agent("a"), 22)) ; PERFORM(RECEIVE(agent(
    "a"), 22)) ; PERFORM(RECEIVE(agent("b"), 22)) ; PERFORM(RECEIVE(agent("c"), 22)) ; PERFORM(SENDGROUPMSG(agent(
    "b"))) ; PERFORM(SEND(agent("b"), 23)) ; PERFORM(RECEIVE(agent("a"), 23)) ; PERFORM(RECEIVE(agent("b"), 23)) ;
    PERFORM(RECEIVE(agent("c"), 23)) ; PERFORM(SENDGROUPMSG(agent("c"))) ; PERFORM(SEND(agent("c"), 24)) ;
    PERFORM(RECEIVE(agent("a"), 24)) ; PERFORM(RECEIVE(agent("b"), 24)) ; PERFORM(RECEIVE(agent("c"), 24)) ;
    PERFORM(DELIVERCHANGE(agent("a"))) ; PERFORM(DELIVERCHANGE(agent("b"))) ; PERFORM(DELIVERCHANGE(agent("c"))) ;
    PERFORM(FLUSHOK(agent("a"))) ; PERFORM(MULTICAST(agent("a"), group("Winners"))) ; PERFORM(SEND(agent("a"),
    25)) ; PERFORM(RECEIVE(agent("a"), 25)) ; PERFORM(RECEIVE(agent("b"), 25)) ; PERFORM(RECEIVE(agent("c"), 25))
    ; PERFORM(FLUSHOK(agent("b"))) ; PERFORM(MULTICAST(agent("b"), group("Winners"))) ; PERFORM(SEND(agent("b"),
    26)) ; PERFORM(RECEIVE(agent("a"), 26)) ; PERFORM(RECEIVE(agent("b"), 26)) ; PERFORM(RECEIVE(agent("c"), 26))
    ; PERFORM(FLUSHOK(agent("c"))) ; PERFORM(MULTICAST(agent("c"), group("Winners"))) ; PERFORM(SEND(agent("c"),
    27)) ; PERFORM(RECEIVE(agent("a"), 27)) ; PERFORM(RECEIVE(agent("b"), 27)) ; PERFORM(RECEIVE(agent("c"), 27))
    ; PERFORM(MULTICAST(agent("a"), privategroup(agent("b")))) ; PERFORM(SEND(agent("a"), 28)) ; PERFORM(RECEIVE(
    agent("a"), 28)) ; PERFORM(RECEIVE(agent("b"), 28)) ; PERFORM(RECEIVE(agent("c"), 28)) ; PERFORM(MULTICAST(
    agent("b"), privategroup(agent("c")))) ; PERFORM(SEND(agent("b"), 29)) ; PERFORM(RECEIVE(agent("a"), 29)) ;
    PERFORM(RECEIVE(agent("b"), 29)) ; PERFORM(RECEIVE(agent("c"), 29)) ; PERFORM(MULTICAST(agent("c"), group(
    "Winners"))) ; PERFORM(SEND(agent("c"), 30)) ; PERFORM(RECEIVE(agent("a"), 30)) ; PERFORM(RECEIVE(agent("b"),
    30)) ; PERFORM(RECEIVE(agent("c"), 30)) ; PERFORM(MULTICAST(agent("a"), privategroup(agent("c")))) ; PERFORM(
    SEND(agent("a"), 31)) ; PERFORM(RECEIVE(agent("a"), 31)) ; PERFORM(RECEIVE(agent("b"), 31)) ; PERFORM(RECEIVE(
    agent("c"), 31)) ; PERFORM(MULTICAST(agent("b"), privategroup(agent("c")))) ; PERFORM(SEND(agent("b"), 32)) ;
    PERFORM(RECEIVE(agent("a"), 32)) ; PERFORM(RECEIVE(agent("b"), 32)) ; PERFORM(RECEIVE(agent("c"), 32)) ;
    PERFORM(MULTICAST(agent("c"), group("Winners"))) ; PERFORM(SEND(agent("c"), 33)) ; PERFORM(RECEIVE(agent("a"),
    33)) ; PERFORM(RECEIVE(agent("b"), 33)) ; PERFORM(RECEIVE(agent("c"), 33)) ; PERFORM(DELIVERCHANGE(agent(
    "a"))) ; PERFORM(DELIVERCHANGE(agent("b"))) ; PERFORM(DELIVERCHANGE(agent("c"))) ; PERFORM(MULTICAST-TEST) ;
    PERFORM(MULTICAST(agent("c"), group("Winners"))) ; PERFORM(SEND(agent("c"), 34)) ; PERFORM(RECEIVE(agent("a"),
    34)) ; PERFORM(RECEIVE(agent("b"), 34)) ; PERFORM(RECEIVE(agent("c"), 34)) ; PERFORM(LEAVE(agent("a"), group(
    "Winners"))) ; PERFORM(SEND(agent("a"), 35)) ; PERFORM(RECEIVE(agent("a"), 35)) ; PERFORM(RECEIVE(agent("b"),
    35)) ; PERFORM(RECEIVE(agent("c"), 35)) ; PERFORM(FLUSHOK(agent("b"))) ; PERFORM(MULTICAST(agent("b"), group(
    "Winners"))) ; PERFORM(SEND(agent("b"), 36)) ; PERFORM(RECEIVE(agent("a"), 36)) ; PERFORM(RECEIVE(agent("b"),
    36)) ; PERFORM(RECEIVE(agent("c"), 36)) ; PERFORM(FLUSHOK(agent("c"))) ; PERFORM(MULTICAST(agent("c"), group(
    "Winners"))) ; PERFORM(SEND(agent("c"), 37)) ; PERFORM(RECEIVE(agent("a"), 37)) ; PERFORM(RECEIVE(agent("b"),
    37)) ; PERFORM(RECEIVE(agent("c"), 37)) ; PERFORM(DELIVERCHANGE(agent("a"))) ; PERFORM(DELIVERCHANGE(agent(
    "b"))) ; PERFORM(DELIVERCHANGE(agent("c"))) ; PERFORM(DISCONNECT(agent("b"))) ; PERFORM(SEND(agent("b"), 38))
    ; PERFORM(RECEIVE(agent("a"), 38)) ; PERFORM(RECEIVE(agent("b"), 38)) ; PERFORM(RECEIVE(agent("c"), 38)) ;
    PERFORM(FLUSHOK(agent("c"))) ; PERFORM(MULTICAST(agent("c"), group("Winners"))) ; PERFORM(SEND(agent("c"),
    39)) ; PERFORM(RECEIVE(agent("a"), 39)) ; PERFORM(RECEIVE(agent("b"), 39)) ; PERFORM(RECEIVE(agent("c"), 39))
    ; PERFORM(DELIVERCHANGE(agent("c"))))
a(4)
b(2)
c(5)
localconf(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
localconf(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
localconf(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
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("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), 3,
    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), 4, sNatSet(0) sNatSet(1) sNatSet(
    3), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), 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), 3,
    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), 4, sNatSet(0) sNatSet(1) sNatSet(
    3), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), 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), 3,
    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), 4, sNatSet(0) sNatSet(1) sNatSet(
    3), gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), 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"), sBroadcastSet(broadcast(sProcSet(agent("a")), datamsg(agent("c"), agreed, regconf(sProcSet(agent(
    "a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 2, sNatSet(0) sNatSet(1), gdatamsg(agent("c"), group(
    "Winners"), fdatamsg(agent("c"), group("Winners"), sdatamsg(keyid(0), idPartialKey, sdata("MyTEST")), view(
    regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(
    agent("c")), 0)))))) sBroadcastSet(broadcast(sProcSet(agent("b")), datamsg(agent("c"), agreed, regconf(
    sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 2, sNatSet(0) sNatSet(1), gdatamsg(agent(
    "c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), sdatamsg(keyid(0), idPartialKey, sdata(
    "MyTEST")), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"),
    sAgentList(agent("c")), 0)))))) sBroadcastSet(broadcast(sProcSet(agent("c")), datamsg(agent("c"), agreed,
    regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 2, sNatSet(0) sNatSet(1),
    gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), sdatamsg(keyid(0), idPartialKey,
    sdata("MyTEST")), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group(
    "Winners"), sAgentList(agent("c")), 0)))))))
received(agent("a"), sMessageSet(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b"))
    sProcSet(agent("c")), 0), 5, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4), gdatamsg(agent("c"),
    group("Winners"), fokmsg(agent("c"), group("Winners"))))))
received(agent("b"), sMessageSet(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b"))
    sProcSet(agent("c")), 0), 5, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4), gdatamsg(agent("c"),
    group("Winners"), fokmsg(agent("c"), group("Winners"))))))
received(agent("c"), sMessageSet(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b"))
    sProcSet(agent("c")), 0), 5, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4), gdatamsg(agent("c"),
    group("Winners"), fokmsg(agent("c"), group("Winners"))))))
acked(agent("a"), eMessageSet)
acked(agent("b"), eMessageSet)
acked(agent("c"), eMessageSet)
causalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sConstraintSet(constraint(
    agent("a"), 0, 3)) sConstraintSet(constraint(agent("a"), 1, 3)) sConstraintSet(constraint(agent("a"), 3, 4))
    sConstraintSet(constraint(agent("c"), 0, 1)) sConstraintSet(constraint(agent("c"), 0, 2)) sConstraintSet(
    constraint(agent("c"), 0, 5)) sConstraintSet(constraint(agent("c"), 1, 2)) sConstraintSet(constraint(agent(
    "c"), 1, 5)) sConstraintSet(constraint(agent("c"), 2, 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"), 3))
    sEventList(event(agent("a"), 3)) sEventList(event(agent("a"), 3)))
sp-join-req(agent("b"), group("Winners"))
sp-leave-req(agent("a"), group("Winners"))
gjoined(agent("a"), sGroupList(group("Winners")))
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")), 0), group(
    "Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1)))
gview(agent("b"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group(
    "Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1)))
gview(agent("c"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group(
    "Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1)))
glocalconf(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
glocalconf(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
glocalconf(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0))
gdelivered(agent("a"), eGMessageList)
gdelivered(agent("b"), eGMessageList)
gdelivered(agent("c"), eGMessageList)
fmembers(agent("a"), sGroupAgentsAgentsSet(groupagentsagents(group("Winners"), sAgentSet(agent("a")) sAgentSet(
    agent("c")), sAgentSet(agent("a")) sAgentSet(agent("c")))))
fmembers(agent("b"), eGroupAgentsAgentsSet)
fmembers(agent("c"), sGroupAgentsAgentsSet(groupagentsagents(group("Winners"), sAgentSet(agent("a")) sAgentSet(
    agent("c")), sAgentSet(agent("a")) sAgentSet(agent("c")))))
fpending(agent("a"), sGroupOpSet(joining(agent("a"), group("Winners"))))
fpending(agent("b"), eGroupOpSet)
fpending(agent("c"), sGroupOpSet(joining(agent("a"), group("Winners"))))
ftrans(agent("a"), eGroupSet)
ftrans(agent("b"), eGroupSet)
ftrans(agent("c"), eGroupSet)
fbuffer(agent("a"), sGMessageList(gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), group("Winners")))))
fbuffer(agent("b"), eGMessageList)
fbuffer(agent("c"), sGMessageList(gdatamsg(agent("a"), group("Winners"), fokmsg(agent("a"), group("Winners")))))
fiview(agent("a"), eViewSet)
fiview(agent("b"), eViewSet)
fiview(agent("c"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0),
    group("Winners"), sAgentList(agent("c")), 0)))
fpview(agent("a"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0),
    group("Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1)))
fpview(agent("b"), eViewSet)
fpview(agent("c"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0),
    group("Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1)))
fkainprogress(agent("a"), eGroupSet)
fkainprogress(agent("b"), eGroupSet)
fkainprogress(agent("c"), eGroupSet)
fkamessage(agent("a"), eFMessageList)
fkamessage(agent("b"), eFMessageList)
fkamessage(agent("c"), sFMessageList(fjoinmsg(agent("c"), group("Winners"), view(regconf(sProcSet(agent("a"))
    sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(agent("c")), 0))))
f-leave-req'(agent("a"), group("Winners"))
siview(agent("a"), eViewSet)
siview(agent("b"), eViewSet)
siview(agent("c"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0),
    group("Winners"), sAgentList(agent("c")), 0)))
snotfirsttrans(agent("a"), eGroupSet)
snotfirsttrans(agent("b"), eGroupSet)
snotfirsttrans(agent("c"), eGroupSet)
svstrans(agent("a"), eGroupSet)
svstrans(agent("b"), eGroupSet)
svstrans(agent("c"), eGroupSet)
snotfirstcm(agent("a"), eGroupSet)
snotfirstcm(agent("b"), eGroupSet)
snotfirstcm(agent("c"), sGroupSet(group("Winners")))
swaitforsfok(agent("a"), eGroupSet)
swaitforsfok(agent("b"), eGroupSet)
swaitforsfok(agent("c"), eGroupSet)
sklgotfreq(agent("a"), eGroupSet)
sklgotfreq(agent("b"), eGroupSet)
sklgotfreq(agent("c"), eGroupSet)
svsset(agent("a"), eGroupAgentSetSet)
svsset(agent("b"), eGroupAgentSetSet)
svsset(agent("c"), sGroupAgentSetSet(groupagentset(group("Winners"), sAgentSet(agent("c")))))
snewmembmsg(agent("a"), eGroupSMessageSet)
snewmembmsg(agent("b"), eGroupSMessageSet)
snewmembmsg(agent("c"), sGroupSMessageSet(groupsmessage(group("Winners"), sjoinmsg(agent("c"), group("Winners"),
    view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(
    agent("c")), 0)))))
snewcontroller(agent("a"), eGroupSet)
snewcontroller(agent("b"), eGroupSet)
snewcontroller(agent("c"), sGroupSet(group("Winners")))
sforeceived(agent("a"), eGroupAgentSetSet)
sforeceived(agent("b"), eGroupAgentSetSet)
sforeceived(agent("c"), sGroupAgentSetSet(groupagentset(group("Winners"), eAgentSet)))
sgroupkeylist(agent("a"), sGroupAssocKeyListSet(groupassockeylist(group("Winners"), eAssocKeyList)))
sgroupkeylist(agent("b"), eGroupAssocKeyListSet)
sgroupkeylist(agent("c"), sGroupAssocKeyListSet(groupassockeylist(group("Winners"), sAssocKeyList(assockey(
    idPartialKey, keyid(0))))))
sgroupmembsetlist(agent("a"), sGroupAssocMembSetListSet(groupassocmembsetlist(group("Winners"),
    eAssocMembSetList)))
sgroupmembsetlist(agent("b"), eGroupAssocMembSetListSet)
sgroupmembsetlist(agent("c"), sGroupAssocMembSetListSet(groupassocmembsetlist(group("Winners"), sAssocMembSetList(
    assocmembset(sAgentSet(agent("c")), keyid(0))))))
sfreshness(agent("a"), eGroupSet)
sfreshness(agent("b"), eGroupSet)
sfreshness(agent("c"), sGroupSet(group("Winners")))
sforceka(agent("a"), sGroupSet(group("Winners")))
sforceka(agent("b"), sGroupSet(group("Winners")))
sforceka(agent("c"), sGroupSet(group("Winners")))
skainprogress(agent("a"), eGroupSet)
skainprogress(agent("b"), eGroupSet)
skainprogress(agent("c"), eGroupSet)
sshadowmessage(agent("a"), eFMessageList)
sshadowmessage(agent("b"), eFMessageList)
sshadowmessage(agent("c"), eFMessageList)
sbuffer(agent("a"), eSMessageList)
sbuffer(agent("b"), eSMessageList)
sbuffer(agent("c"), eSMessageList)
ssp-leave-req'(agent("a"), group("Winners"))
sdelivered(agent("a"), eSMessageList)
sdelivered(agent("b"), eSMessageList)
sdelivered(agent("c"), eSMessageList)
sdelivered'(agent("a"), sSMessageList(sfreqmsg(agent("a"), group("Winners"))))
sdelivered'(agent("b"), eSMessageList)
sdelivered'(agent("c"), sSMessageList(sfreqmsg(agent("c"), group("Winners"))) sSMessageList(sjoinmsg(agent("c"),
    group("Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group(
    "Winners"), sAgentList(agent("c")), 0))) sSMessageList(sfreqmsg(agent("c"), group("Winners"))))
localmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(3)
    sNatSet(4))
localmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), eNatSet)
localmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0)
    sNatSet(1) sNatSet(2) sNatSet(5))
knownmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0)
    sNatSet(1) sNatSet(3) sNatSet(4))
knownmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0)
    sNatSet(1) sNatSet(3) sNatSet(4))
knownmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0)
    sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5))
fgrptype(agent("a"), eGroupSet, sGroupSet(group("Winners")))
fgrptype(agent("b"), eGroupSet, sGroupSet(group("Winners")))
fgrptype(agent("c"), eGroupSet, sGroupSet(group("Winners")))
f-join-req'(agent("b"), group("Winners"), group-evs)
scontext(agent("a"), keyid(0), eGroupContextSet)
scontext(agent("b"), keyid(0), eGroupContextSet)
scontext(agent("c"), keyid(0), sGroupContextSet(groupcontext(group("Winners"), context(idKeyShare, idPartialKey,
    sGroupMemberList(groupmember(agent("c"), alpha))))))
sgrptype(agent("a"), eGroupSet, eGroupSet)
sgrptype(agent("b"), eGroupSet, sGroupSet(group("Winners")))
sgrptype(agent("c"), eGroupSet, sGroupSet(group("Winners")))
skatype(agent("a"), eGroupSet, sGroupSet(group("Winners")))
skatype(agent("b"), eGroupSet, sGroupSet(group("Winners")))
skatype(agent("c"), eGroupSet, sGroupSet(group("Winners")))
gstate(goperational(agent("a"))
goperational(agent("b"))
goperational(agent("c")), eState, eState, eState)
fstate(agent("a"), eGroupSet, eGroupSet, sGroupSet(group("Winners")))
fstate(agent("b"), eGroupSet, eGroupSet, eGroupSet)
fstate(agent("c"), eGroupSet, eGroupSet, sGroupSet(group("Winners")))
slaziness(agent("a"), eGroupSet, sGroupSet(group("Winners")), eGroupSet)
slaziness(agent("b"), eGroupSet, sGroupSet(group("Winners")), eGroupSet)
slaziness(agent("c"), eGroupSet, sGroupSet(group("Winners")), eGroupSet)
ssp-join-req'(agent("b"), group("Winners"), group-evs, changing-time, non-blocking)
sstate(agent("a"), eGroupSet, sGroupSet(group("Winners")), eGroupSet, eGroupSet, eGroupSet, eGroupSet)
sstate(agent("b"), eGroupSet, eGroupSet, eGroupSet, eGroupSet, eGroupSet, eGroupSet)
sstate(agent("c"), eGroupSet, sGroupSet(group("Winners")), eGroupSet, eGroupSet, eGroupSet, eGroupSet)
Maude>