Maude> in stestevs3 ========================================== 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 66 (mod CLIQUES): collapse at top of x:PartialKey * inv(x:PartialKey) may cause it to match more than you expect. Advisory: "cliques.maude", line 83 (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: 8300291 in 129240ms cpu (152922ms real) (64223 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(35) 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")) fresh(4) freshkeyid(1) ssp-receive-req'(agent("a")) ssp-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), 33, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32), gdisconnectmsg(agent("b"), nogroup, noview))) sMessageList(datamsg(agent("c"), fifo, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 34, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32) sNatSet(33), 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("c"), fifo, regconf(sProcSet(agent( "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 19, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18), gdatamsg(agent("c"), group("Winners"), freqmsg(agent("c"), group("Winners"), force)))) sMessageList(datamsg( agent("a"), 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("a"), group("Winners"), fokmsg(agent("a"), 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"), fifo, 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"), fokmsg( agent("c"), group("Winners"))))) sMessageList(datamsg(agent("a"), fifo, 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), gdatamsg(agent("a"), privategroup(agent("b")), fdatamsg(agent("a"), privategroup(agent("b")), stokenmsg(token(agent("a"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("a"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0))) sGroupMemberList(groupmember(agent("c"), idPartialKey)))), noview)))) sMessageList(datamsg(agent("b"), 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("b"), privategroup(agent("c")), fdatamsg(agent("b"), privategroup(agent("c")), stokenmsg(token(agent("b"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("a"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1))))), noview)))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 25, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet( 20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group( "Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember(agent("a"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1))))), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group( "Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), 0))))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 26, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25), gdatamsg(agent("a"), privategroup(agent("c")), fdatamsg(agent("a"), privategroup(agent("c")), stokenmsg(token(agent("a"), group("Winners"), merge-factor-out-message, sGroupMemberList(groupmember(agent("a"), alpha ^ random(1))))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 27, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26), gdatamsg(agent("b"), privategroup(agent("c")), fdatamsg(agent("b"), privategroup(agent("c")), stokenmsg(token(agent("b"), group("Winners"), merge-factor-out-message, sGroupMemberList( groupmember(agent("b"), alpha ^ random(0))))), noview)))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent( "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 28, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("a"), alpha ^ random(1) * random(2))) sGroupMemberList( groupmember(agent("b"), alpha ^ random(0) * random(2))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1)))), keyid(0)), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), 0))))) sMessageList(datamsg(agent("c"), reliable, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 29, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), sdatamsg(keyid(0), alpha ^ random(0) * random(1) * random(2), sdata("TEST")), view(regconf(sProcSet(agent("a")) sProcSet( agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent( "c")), 0))))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent( "c")), 7), 30, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29), gleavemsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 31, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet( 20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet( 30), 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), 32, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31), gdatamsg(agent("c"), group("Winners"), fokmsg( agent("c"), group("Winners"))))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 33, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet( 20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32), gdisconnectmsg(agent("b"), nogroup, noview))) sMessageList(datamsg(agent("c"), fifo, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 34, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32) sNatSet(33), 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("c"), fifo, regconf(sProcSet(agent( "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 19, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18), gdatamsg(agent("c"), group("Winners"), freqmsg(agent("c"), group("Winners"), force)))) sMessageList(datamsg( agent("a"), 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("a"), group("Winners"), fokmsg(agent("a"), 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"), fifo, 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"), fokmsg( agent("c"), group("Winners"))))) sMessageList(datamsg(agent("a"), fifo, 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), gdatamsg(agent("a"), privategroup(agent("b")), fdatamsg(agent("a"), privategroup(agent("b")), stokenmsg(token(agent("a"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("a"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0))) sGroupMemberList(groupmember(agent("c"), idPartialKey)))), noview)))) sMessageList(datamsg(agent("b"), 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("b"), privategroup(agent("c")), fdatamsg(agent("b"), privategroup(agent("c")), stokenmsg(token(agent("b"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("a"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1))))), noview)))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 25, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet( 20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group( "Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember(agent("a"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1))))), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group( "Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), 0))))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 26, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25), gdatamsg(agent("a"), privategroup(agent("c")), fdatamsg(agent("a"), privategroup(agent("c")), stokenmsg(token(agent("a"), group("Winners"), merge-factor-out-message, sGroupMemberList(groupmember(agent("a"), alpha ^ random(1))))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 27, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26), gdatamsg(agent("b"), privategroup(agent("c")), fdatamsg(agent("b"), privategroup(agent("c")), stokenmsg(token(agent("b"), group("Winners"), merge-factor-out-message, sGroupMemberList( groupmember(agent("b"), alpha ^ random(0))))), noview)))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent( "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 28, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("a"), alpha ^ random(1) * random(2))) sGroupMemberList( groupmember(agent("b"), alpha ^ random(0) * random(2))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1)))), keyid(0)), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), 0))))) sMessageList(datamsg(agent("c"), reliable, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 29, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), sdatamsg(keyid(0), alpha ^ random(0) * random(1) * random(2), sdata("TEST")), view(regconf(sProcSet(agent("a")) sProcSet( agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent( "c")), 0))))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent( "c")), 7), 30, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29), gleavemsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 31, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet( 20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet( 30), 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), 32, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31), gdatamsg(agent("c"), group("Winners"), fokmsg( agent("c"), group("Winners"))))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 33, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet( 20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32), gdisconnectmsg(agent("b"), nogroup, noview))) sMessageList(datamsg(agent("c"), fifo, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 34, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32) sNatSet(33), 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("c"), fifo, regconf(sProcSet(agent( "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 19, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18), gdatamsg(agent("c"), group("Winners"), freqmsg(agent("c"), group("Winners"), force)))) sMessageList(datamsg( agent("a"), 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("a"), group("Winners"), fokmsg(agent("a"), 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"), fifo, 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"), fokmsg( agent("c"), group("Winners"))))) sMessageList(datamsg(agent("a"), fifo, 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), gdatamsg(agent("a"), privategroup(agent("b")), fdatamsg(agent("a"), privategroup(agent("b")), stokenmsg(token(agent("a"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("a"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0))) sGroupMemberList(groupmember(agent("c"), idPartialKey)))), noview)))) sMessageList(datamsg(agent("b"), 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("b"), privategroup(agent("c")), fdatamsg(agent("b"), privategroup(agent("c")), stokenmsg(token(agent("b"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("a"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1))))), noview)))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 25, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet( 20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group( "Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember(agent("a"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(0))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1))))), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group( "Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), 0))))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 26, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25), gdatamsg(agent("a"), privategroup(agent("c")), fdatamsg(agent("a"), privategroup(agent("c")), stokenmsg(token(agent("a"), group("Winners"), merge-factor-out-message, sGroupMemberList(groupmember(agent("a"), alpha ^ random(1))))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 27, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26), gdatamsg(agent("b"), privategroup(agent("c")), fdatamsg(agent("b"), privategroup(agent("c")), stokenmsg(token(agent("b"), group("Winners"), merge-factor-out-message, sGroupMemberList( groupmember(agent("b"), alpha ^ random(0))))), noview)))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent( "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 28, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("a"), alpha ^ random(1) * random(2))) sGroupMemberList( groupmember(agent("b"), alpha ^ random(0) * random(2))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1)))), keyid(0)), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), 0))))) sMessageList(datamsg(agent("c"), reliable, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 29, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), sdatamsg(keyid(0), alpha ^ random(0) * random(1) * random(2), sdata("TEST")), view(regconf(sProcSet(agent("a")) sProcSet( agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent( "c")), 0))))) sMessageList(datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent( "c")), 7), 30, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29), gleavemsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 31, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet( 20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet( 30), 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), 32, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31), gdatamsg(agent("c"), group("Winners"), fokmsg( agent("c"), group("Winners"))))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 33, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet( 20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32), gdisconnectmsg(agent("b"), nogroup, noview))) sMessageList(datamsg(agent("c"), fifo, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 34, sNatSet(13) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21) sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32) sNatSet(33), 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, 20)) sConstraintSet(constraint(agent("a"), 13, 23)) sConstraintSet( constraint(agent("a"), 13, 26)) sConstraintSet(constraint(agent("a"), 13, 30)) sConstraintSet(constraint(agent("a"), 14, 30)) sConstraintSet(constraint(agent("a"), 15, 30)) sConstraintSet(constraint(agent("a"), 16, 20)) sConstraintSet( constraint(agent("a"), 16, 23)) sConstraintSet(constraint(agent("a"), 16, 26)) sConstraintSet(constraint(agent("a"), 16, 30)) sConstraintSet(constraint(agent("a"), 17, 30)) sConstraintSet(constraint(agent("a"), 18, 30)) sConstraintSet( constraint(agent("a"), 19, 30)) sConstraintSet(constraint(agent("a"), 20, 23)) sConstraintSet(constraint(agent("a"), 20, 26)) sConstraintSet(constraint(agent("a"), 20, 30)) sConstraintSet(constraint(agent("a"), 21, 30)) sConstraintSet( constraint(agent("a"), 22, 30)) sConstraintSet(constraint(agent("a"), 23, 26)) sConstraintSet(constraint(agent("a"), 23, 30)) sConstraintSet(constraint(agent("a"), 24, 30)) sConstraintSet(constraint(agent("a"), 25, 30)) sConstraintSet( constraint(agent("a"), 26, 30)) sConstraintSet(constraint(agent("a"), 27, 30)) sConstraintSet(constraint(agent("a"), 28, 30)) sConstraintSet(constraint(agent("a"), 29, 30)) sConstraintSet(constraint(agent("b"), 13, 14)) sConstraintSet( constraint(agent("b"), 13, 33)) sConstraintSet(constraint(agent("b"), 14, 17)) sConstraintSet(constraint(agent("b"), 14, 21)) sConstraintSet(constraint(agent("b"), 14, 24)) sConstraintSet(constraint(agent("b"), 14, 27)) sConstraintSet( constraint(agent("b"), 14, 31)) sConstraintSet(constraint(agent("b"), 14, 33)) sConstraintSet(constraint(agent("b"), 15, 33)) sConstraintSet(constraint(agent("b"), 16, 33)) sConstraintSet(constraint(agent("b"), 17, 21)) sConstraintSet( constraint(agent("b"), 17, 24)) sConstraintSet(constraint(agent("b"), 17, 27)) sConstraintSet(constraint(agent("b"), 17, 31)) sConstraintSet(constraint(agent("b"), 17, 33)) sConstraintSet(constraint(agent("b"), 18, 33)) sConstraintSet( constraint(agent("b"), 19, 33)) sConstraintSet(constraint(agent("b"), 20, 33)) sConstraintSet(constraint(agent("b"), 21, 24)) sConstraintSet(constraint(agent("b"), 21, 27)) sConstraintSet(constraint(agent("b"), 21, 31)) sConstraintSet( constraint(agent("b"), 21, 33)) sConstraintSet(constraint(agent("b"), 22, 33)) sConstraintSet(constraint(agent("b"), 23, 33)) sConstraintSet(constraint(agent("b"), 24, 27)) sConstraintSet(constraint(agent("b"), 24, 31)) sConstraintSet( constraint(agent("b"), 24, 33)) sConstraintSet(constraint(agent("b"), 25, 33)) sConstraintSet(constraint(agent("b"), 26, 33)) sConstraintSet(constraint(agent("b"), 27, 31)) sConstraintSet(constraint(agent("b"), 27, 33)) sConstraintSet( constraint(agent("b"), 28, 33)) sConstraintSet(constraint(agent("b"), 29, 33)) sConstraintSet(constraint(agent("b"), 30, 33)) sConstraintSet(constraint(agent("b"), 31, 33)) sConstraintSet(constraint(agent("b"), 32, 33)) sConstraintSet( constraint(agent("c"), 13, 15)) sConstraintSet(constraint(agent("c"), 13, 28)) sConstraintSet(constraint(agent("c"), 14, 15)) sConstraintSet(constraint(agent("c"), 14, 28)) sConstraintSet(constraint(agent("c"), 15, 18)) sConstraintSet( constraint(agent("c"), 15, 19)) sConstraintSet(constraint(agent("c"), 15, 22)) sConstraintSet(constraint(agent("c"), 15, 25)) sConstraintSet(constraint(agent("c"), 15, 28)) sConstraintSet(constraint(agent("c"), 15, 32)) sConstraintSet( constraint(agent("c"), 15, 34)) sConstraintSet(constraint(agent("c"), 16, 28)) sConstraintSet(constraint(agent("c"), 17, 28)) sConstraintSet(constraint(agent("c"), 18, 19)) sConstraintSet(constraint(agent("c"), 18, 22)) sConstraintSet( constraint(agent("c"), 18, 25)) sConstraintSet(constraint(agent("c"), 18, 28)) sConstraintSet(constraint(agent("c"), 18, 32)) sConstraintSet(constraint(agent("c"), 18, 34)) sConstraintSet(constraint(agent("c"), 19, 22)) sConstraintSet( constraint(agent("c"), 19, 25)) sConstraintSet(constraint(agent("c"), 19, 28)) sConstraintSet(constraint(agent("c"), 19, 32)) sConstraintSet(constraint(agent("c"), 19, 34)) sConstraintSet(constraint(agent("c"), 20, 28)) sConstraintSet( constraint(agent("c"), 21, 28)) sConstraintSet(constraint(agent("c"), 22, 25)) sConstraintSet(constraint(agent("c"), 22, 28)) sConstraintSet(constraint(agent("c"), 22, 32)) sConstraintSet(constraint(agent("c"), 22, 34)) sConstraintSet( constraint(agent("c"), 23, 28)) sConstraintSet(constraint(agent("c"), 24, 28)) sConstraintSet(constraint(agent("c"), 25, 28)) sConstraintSet(constraint(agent("c"), 25, 32)) sConstraintSet(constraint(agent("c"), 25, 34)) sConstraintSet( constraint(agent("c"), 26, 28)) sConstraintSet(constraint(agent("c"), 27, 28)) sConstraintSet(constraint(agent("c"), 28, 32)) sConstraintSet(constraint(agent("c"), 28, 34)) sConstraintSet(constraint(agent("c"), 29, 32)) sConstraintSet( constraint(agent("c"), 29, 34)) sConstraintSet(constraint(agent("c"), 32, 34))) 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))) 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("b"), 10)) sEventList(event( agent("b"), 10))) 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"), 2)) sEventList(event(agent( "a"), 2)) sEventList(event(agent("a"), 2))) 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("c"), 28)) sEventList(event(agent("c"), 28)) sEventList(event( agent("c"), 28)) sEventList(event(agent("a"), 30)) sEventList(event(agent("a"), 30)) sEventList(event(agent("a"), 30)) sEventList(event(agent("b"), 33)) sEventList(event(agent("b"), 33)) sEventList(event(agent("b"), 33))) 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"), 2)) sEventList(event(agent("a"), 2)) sEventList(event(agent("a"), 2))) totalorder(transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)), sEventList(event(agent("a"), 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"), 2)) sEventList(event(agent("a"), 2)) sEventList(event(agent("a"), 2))) 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("b"), 10)) sEventList(event(agent("b"), 10))) 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) 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) fbuffer(agent("a"), sGMessageList(gdatamsg(agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners")))) sGMessageList( gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) fbuffer(agent("c"), eGMessageList) 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) fkainprogress(agent("a"), eGroupSet) fkainprogress(agent("c"), eGroupSet) fkamessage(agent("a"), 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( fconfmsg(group("Winners"), view(regconf(sProcSet(agent("a")), 2), group("Winners"), sAgentList(agent("a")), 0), sAgentSet( agent("a")))) 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"))))) 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))) 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(fconfmsg(group("Winners"), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("c")), 0), sAgentSet(agent("c")))) 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(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(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(fdisconnectmsg(agent("b"), group("Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("c")), 2)))) ssp-receive-err(agent("b"), IllegalAgent) siview(agent("a"), eViewSet) siview(agent("c"), sViewSet(view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("c")), 2))) snotfirsttrans(agent("a"), eGroupSet) snotfirsttrans(agent("c"), eGroupSet) svstrans(agent("a"), eGroupSet) svstrans(agent("c"), eGroupSet) snotfirstcm(agent("a"), eGroupSet) snotfirstcm(agent("c"), sGroupSet(group("Winners"))) swaitforsfok(agent("a"), eGroupSet) swaitforsfok(agent("c"), eGroupSet) sklgotfreq(agent("a"), eGroupSet) sklgotfreq(agent("c"), eGroupSet) svsset(agent("a"), sGroupAgentSetSet(groupagentset(group("Winners"), sAgentSet(agent("a")) sAgentSet(agent("b")) sAgentSet( agent("c"))))) svsset(agent("c"), sGroupAgentSetSet(groupagentset(group("Winners"), sAgentSet(agent("c"))))) snewmembmsg(agent("a"), sGroupSMessageSet(groupsmessage(group("Winners"), sconfmsg(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")))))) snewmembmsg(agent("c"), sGroupSMessageSet(groupsmessage(group("Winners"), sdisconnectmsg(agent("b"), group("Winners"), view( regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("c")), 2))))) snewcontroller(agent("a"), eGroupSet) snewcontroller(agent("c"), sGroupSet(group("Winners"))) sforeceived(agent("a"), sGroupAgentSetSet(groupagentset(group("Winners"), eAgentSet))) sforeceived(agent("c"), sGroupAgentSetSet(groupagentset(group("Winners"), eAgentSet))) sgroupkeylist(agent("a"), sGroupAssocKeyListSet(groupassockeylist(group("Winners"), sAssocKeyList(assockey(alpha ^ random(0) * random(1) * random(2), keyid(0)))))) sgroupkeylist(agent("c"), sGroupAssocKeyListSet(groupassockeylist(group("Winners"), sAssocKeyList(assockey(alpha ^ random(0) * random(1) * random(2), keyid(0)))))) sgroupmembsetlist(agent("a"), sGroupAssocMembSetListSet(groupassocmembsetlist(group("Winners"), sAssocMembSetList(assocmembset( sAgentSet(agent("a")) sAgentSet(agent("b")) sAgentSet(agent("c")), keyid(0)))))) sgroupmembsetlist(agent("c"), sGroupAssocMembSetListSet(groupassocmembsetlist(group("Winners"), sAssocMembSetList(assocmembset( sAgentSet(agent("a")) sAgentSet(agent("b")) sAgentSet(agent("c")), keyid(0)))))) sfreshness(agent("a"), sGroupSet(group("Winners"))) sfreshness(agent("c"), eGroupSet) sforceka(agent("a"), eGroupSet) sforceka(agent("c"), eGroupSet) skainprogress(agent("a"), eGroupSet) skainprogress(agent("c"), eGroupSet) sshadowmessage(agent("a"), 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"))))) sshadowmessage(agent("c"), sFMessageList(fdisconnectmsg(agent("b"), group("Winners"), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("c")), 2)))) sbuffer(agent("a"), eSMessageList) sbuffer(agent("c"), eSMessageList) sdelivered(agent("a"), eSMessageList) sdelivered(agent("b"), eSMessageList) sdelivered(agent("c"), eSMessageList) sdelivered'(agent("a"), sSMessageList(sfreqmsg(agent("a"), group("Winners"))) sSMessageList(sjoinmsg(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))) sSMessageList(stransmsg(group("Winners"))) sSMessageList(sfreqmsg(agent("a"), group("Winners"))) sSMessageList(sconfmsg(group("Winners"), view(regconf(sProcSet(agent("a")), 2), group("Winners"), sAgentList(agent("a")), 0), sAgentSet(agent("a")))) sSMessageList(stransmsg(group("Winners"))) sSMessageList(sfreqmsg( agent("a"), group("Winners"))) sSMessageList(sconfmsg(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")))) sSMessageList(sfreqmsg(agent("c"), group("Winners"), force)) sSMessageList(sconfmsg(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")) sAgentSet(agent("b")) sAgentSet(agent( "c")))) sSMessageList(sdatamsg(agent("c"), group("Winners"), sdata("TEST"), view(regconf(sProcSet(agent("a")) sProcSet( agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent( "c")), 0))) sSMessageList(sselfleavemsg(agent("a"), group("Winners")))) sdelivered'(agent("b"), sSMessageList(sfreqmsg(agent("b"), group("Winners"))) sSMessageList(sjoinmsg(agent("b"), group( "Winners"), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("c")) sAgentList(agent("b")), 1))) sSMessageList(stransmsg(group("Winners"))) sSMessageList(sfreqmsg(agent("b"), group( "Winners"))) sSMessageList(sconfmsg(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")))) sSMessageList(sfreqmsg(agent("c"), group("Winners"), force)) sSMessageList(sconfmsg( 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")) sAgentSet(agent("b")) sAgentSet(agent("c")))) sSMessageList(sdatamsg(agent("c"), group("Winners"), sdata("TEST"), view(regconf(sProcSet(agent( "a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), 0))) sSMessageList(sfreqmsg(agent("b"), group("Winners"))) sSMessageList(sleavemsg(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)))) 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"))) sSMessageList(sjoinmsg(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))) sSMessageList(stransmsg(group("Winners"))) sSMessageList(sfreqmsg(agent("c"), group("Winners"))) sSMessageList(sconfmsg(group("Winners"), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("c")), 0), sAgentSet(agent("c")))) sSMessageList(sfreqmsg(agent("c"), group("Winners"))) sSMessageList(sjoinmsg(agent("b"), group("Winners"), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group( "Winners"), sAgentList(agent("c")) sAgentList(agent("b")), 1))) sSMessageList(stransmsg(group("Winners"))) sSMessageList( sfreqmsg(agent("c"), group("Winners"))) sSMessageList(sconfmsg(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")))) sSMessageList(sfreqmsg(agent("c"), group("Winners"), force)) sSMessageList(sconfmsg(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")) sAgentSet(agent("b")) sAgentSet(agent("c")))) sSMessageList(sdatamsg(agent("c"), group("Winners"), sdata("TEST"), view( regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")), 0))) sSMessageList(sfreqmsg(agent("c"), group("Winners"))) sSMessageList( sleavemsg(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))) sSMessageList(sfreqmsg(agent("c"), group("Winners"))) sSMessageList(sdisconnectmsg(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(20) sNatSet(23) sNatSet(26) sNatSet(30)) 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(24) sNatSet(27) sNatSet(31) sNatSet(33)) 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(19) sNatSet(22) sNatSet(25) sNatSet(28) sNatSet(29) sNatSet(32) sNatSet(34)) 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) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32) sNatSet(33) sNatSet(34)) 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) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32) sNatSet(33) sNatSet(34)) 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) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32) sNatSet(33) sNatSet(34)) 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) fgrptype(agent("a"), eGroupSet, sGroupSet(group("Winners"))) fgrptype(agent("c"), eGroupSet, sGroupSet(group("Winners"))) scontext(agent("a"), keyid(0), sGroupContextSet(groupcontext(group("Winners"), context(random(0), alpha ^ random(0) * random(1) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1) * random(2))) sGroupMemberList(groupmember(agent( "b"), alpha ^ random(0) * random(2))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1))))))) scontext(agent("c"), keyid(0), sGroupContextSet(groupcontext(group("Winners"), context(random(2), alpha ^ random(0) * random(1) * random(2), sGroupMemberList(groupmember(agent("a"), alpha ^ random(1) * random(2))) sGroupMemberList(groupmember(agent( "b"), alpha ^ random(0) * random(2))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(0) * random(1))))))) sgrptype(agent("a"), eGroupSet, eGroupSet) sgrptype(agent("c"), eGroupSet, sGroupSet(group("Winners"))) 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) slaziness(agent("a"), sGroupSet(group("Winners")), eGroupSet, eGroupSet, eGroupSet) slaziness(agent("c"), sGroupSet(group("Winners")), eGroupSet, eGroupSet, eGroupSet) sstate(agent("a"), eGroupSet, eGroupSet, eGroupSet, eGroupSet, eGroupSet, eGroupSet) sstate(agent("c"), sGroupSet(group("Winners")), eGroupSet, eGroupSet, eGroupSet, eGroupSet, eGroupSet) Maude>