Maude> in stestevs1 ========================================== 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: 11574745 in 220550ms cpu (272074ms real) (52481 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(44) 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(10) freshkeyid(8) ssp-receive-req'(agent("a")) ssp-receive-req'(agent("c")) CONTROLLER(eController) a(7) b(7) c(5) 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), 42, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41), gdisconnectmsg(agent("b"), nogroup, noview))) sMessageList(datamsg(agent("c"), fifo, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 43, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41) sNatSet(42), 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), 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"))))) sMessageList(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"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent( "c")), 0), 6, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5), gdatamsg(agent("c"), privategroup(agent( "a")), fdatamsg(agent("c"), privategroup(agent("a")), stokenmsg(token(agent("c"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("c"), alpha)) sGroupMemberList(groupmember(agent("a"), alpha ^ random(0))))), noview)))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 7, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6), gdatamsg(agent("a"), group("Winners"), fdatamsg(agent("a"), group("Winners"), stokenmsg(token(agent("a"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember(agent("c"), alpha)) sGroupMemberList(groupmember(agent("a"), alpha ^ random(0))))), view( regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 8, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6) sNatSet(7), gdatamsg(agent("c"), privategroup(agent("a")), fdatamsg(agent("c"), privategroup(agent("a")), stokenmsg(token(agent("c"), group("Winners"), merge-factor-out-message, sGroupMemberList(groupmember(agent("c"), alpha)))), noview)))) sMessageList( datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 9, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6) sNatSet(7) sNatSet(8), gdatamsg(agent("a"), group( "Winners"), fdatamsg(agent("a"), group("Winners"), stokenmsg(token(agent("a"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("c"), alpha ^ random(1))) sGroupMemberList(groupmember(agent("a"), alpha ^ random(0)))), keyid(1)), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList( agent("c")) sAgentList(agent("a")), 1))))) sMessageList(datamsg(agent("c"), reliable, 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))))) 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), 10, eNatSet, ggroupmsg(agent("a"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent("a"))))))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")), 2), 13, sNatSet(10), 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), 22, 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), 23, sNatSet(22), 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), 24, sNatSet(22) sNatSet(23), 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), 25, sNatSet(22) sNatSet(23) sNatSet(24), 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), 26, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25), 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), 27, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26), 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), 28, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27), 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(4))) sGroupMemberList(groupmember(agent("c"), idPartialKey)))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 29, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28), 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(4))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(4) * random(5))))), noview)))) sMessageList(datamsg( agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 30, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29), 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(4))) sGroupMemberList(groupmember( agent("c"), alpha ^ random(4) * random(5))))), 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), 31, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30), 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(5))))), noview)))) sMessageList(datamsg( agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 32, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31), 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(4))))), noview)))) sMessageList(datamsg( agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 33, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29) sNatSet(30) sNatSet(31) sNatSet(32), 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(5) * random(6))) sGroupMemberList( groupmember(agent("b"), alpha ^ random(4) * random(6))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(4) * random(5)))), keyid(5)), 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), 34, 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"), fdatamsg(agent("c"), group("Winners"), sdatamsg(keyid(5), alpha ^ random(4) * random(5) * random(6), 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), 35, 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), gleavemsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 36, 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) sNatSet(35), 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), 37, 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) sNatSet(35) sNatSet(36), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 38, 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) sNatSet(35) sNatSet(36) sNatSet(37), gdatamsg(agent("b"), privategroup(agent("c")), fdatamsg(agent("b"), privategroup( agent("c")), stokenmsg(token(agent("b"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("b"), alpha)) sGroupMemberList(groupmember(agent("c"), alpha ^ random(8))))), noview)))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 39, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group( "Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember(agent("b"), alpha)) sGroupMemberList(groupmember(agent("c"), alpha ^ random(8))))), view(regconf(sProcSet(agent("a")) sProcSet(agent( "b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1))))) sMessageList( datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 40, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39), 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)))), noview)))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 41, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40), gdatamsg(agent("c"), group("Winners"), fdatamsg( agent("c"), group("Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-key-update-message, sGroupMemberList( groupmember(agent("b"), alpha ^ random(9))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(8)))), keyid(6)), view( regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1))))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 42, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41), gdisconnectmsg(agent("b"), nogroup, noview))) sMessageList(datamsg(agent("c"), fifo, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 43, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41) sNatSet(42), 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), 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"))))) sMessageList(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"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent( "c")), 0), 6, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5), gdatamsg(agent("c"), privategroup(agent( "a")), fdatamsg(agent("c"), privategroup(agent("a")), stokenmsg(token(agent("c"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("c"), alpha)) sGroupMemberList(groupmember(agent("a"), alpha ^ random(0))))), noview)))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 7, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6), gdatamsg(agent("a"), group("Winners"), fdatamsg(agent("a"), group("Winners"), stokenmsg(token(agent("a"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember(agent("c"), alpha)) sGroupMemberList(groupmember(agent("a"), alpha ^ random(0))))), view( regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 8, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6) sNatSet(7), gdatamsg(agent("c"), privategroup(agent("a")), fdatamsg(agent("c"), privategroup(agent("a")), stokenmsg(token(agent("c"), group("Winners"), merge-factor-out-message, sGroupMemberList(groupmember(agent("c"), alpha)))), noview)))) sMessageList( datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 9, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6) sNatSet(7) sNatSet(8), gdatamsg(agent("a"), group( "Winners"), fdatamsg(agent("a"), group("Winners"), stokenmsg(token(agent("a"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("c"), alpha ^ random(1))) sGroupMemberList(groupmember(agent("a"), alpha ^ random(0)))), keyid(1)), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList( agent("c")) sAgentList(agent("a")), 1))))) sMessageList(datamsg(agent("c"), reliable, 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))))) 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), 11, eNatSet, ggroupmsg(agent("b"), eGroupAgentsList))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("b")) sProcSet( agent("c")), 4), 12, sNatSet(11), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent( "c"))))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 14, sNatSet(11) sNatSet(12), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent( "b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 15, sNatSet(11) sNatSet(12) sNatSet(14), gjoinmsg( agent("b"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent( "c")), 4), 16, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15), gdatamsg(agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 17, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 18, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17), gdatamsg(agent("c"), privategroup(agent("b")), fdatamsg(agent("c"), privategroup(agent("b")), stokenmsg(token(agent("c"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("c"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(2))))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 19, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18), gdatamsg(agent("b"), group("Winners"), fdatamsg(agent("b"), group("Winners"), stokenmsg(token(agent("b"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember( agent("c"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(2))))), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("c")) sAgentList(agent("b")), 1))))) sMessageList(datamsg( agent("c"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 20, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet( 15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19), gdatamsg(agent("c"), privategroup(agent("b")), fdatamsg(agent("c"), privategroup(agent("b")), stokenmsg(token(agent("c"), group("Winners"), merge-factor-out-message, sGroupMemberList( groupmember(agent("c"), alpha)))), noview)))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 21, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet( 19) sNatSet(20), gdatamsg(agent("b"), group("Winners"), fdatamsg(agent("b"), group("Winners"), stokenmsg(token(agent("b"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("c"), alpha ^ random(3))) sGroupMemberList( groupmember(agent("b"), alpha ^ random(2)))), keyid(4)), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group( "Winners"), sAgentList(agent("c")) sAgentList(agent("b")), 1))))) 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), 22, 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), 23, sNatSet(22), 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), 24, sNatSet(22) sNatSet(23), 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), 25, sNatSet(22) sNatSet(23) sNatSet(24), 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), 26, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25), 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), 27, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26), 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), 28, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27), 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(4))) sGroupMemberList(groupmember(agent("c"), idPartialKey)))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 29, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28), 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(4))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(4) * random(5))))), noview)))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent( "b")) sProcSet(agent("c")), 7), 30, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29), 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(4))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(4) * random(5))))), 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), 31, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet( 28) sNatSet(29) sNatSet(30), 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(5))))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 32, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet( 29) sNatSet(30) sNatSet(31), 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(4))))), noview)))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 33, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet( 29) sNatSet(30) sNatSet(31) sNatSet(32), 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(5) * random(6))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(4) * random(6))) sGroupMemberList( groupmember(agent("c"), alpha ^ random(4) * random(5)))), keyid(5)), 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), 34, 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"), fdatamsg(agent("c"), group("Winners"), sdatamsg(keyid(5), alpha ^ random(4) * random(5) * random(6), 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), 35, 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), gleavemsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 36, 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) sNatSet(35), 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), 37, 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) sNatSet(35) sNatSet(36), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 38, 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) sNatSet(35) sNatSet(36) sNatSet(37), gdatamsg(agent("b"), privategroup(agent("c")), fdatamsg(agent("b"), privategroup(agent("c")), stokenmsg(token(agent("b"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("b"), alpha)) sGroupMemberList(groupmember(agent("c"), alpha ^ random(8))))), noview)))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 39, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember(agent("b"), alpha)) sGroupMemberList(groupmember(agent("c"), alpha ^ random(8))))), view( regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1))))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 40, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet( 39), 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)))), noview)))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 41, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40), gdatamsg( agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("b"), alpha ^ random(9))) sGroupMemberList(groupmember(agent( "c"), alpha ^ random(8)))), keyid(6)), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1))))) sMessageList(datamsg(agent("b"), agreed, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 42, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41), gdisconnectmsg(agent("b"), nogroup, noview))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 43, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41) sNatSet(42), 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), 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"))))) sMessageList(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"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent( "c")), 0), 6, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5), gdatamsg(agent("c"), privategroup(agent( "a")), fdatamsg(agent("c"), privategroup(agent("a")), stokenmsg(token(agent("c"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("c"), alpha)) sGroupMemberList(groupmember(agent("a"), alpha ^ random(0))))), noview)))) sMessageList(datamsg(agent("a"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 7, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6), gdatamsg(agent("a"), group("Winners"), fdatamsg(agent("a"), group("Winners"), stokenmsg(token(agent("a"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember(agent("c"), alpha)) sGroupMemberList(groupmember(agent("a"), alpha ^ random(0))))), view( regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(agent("c")) sAgentList(agent("a")), 1))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 8, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6) sNatSet(7), gdatamsg(agent("c"), privategroup(agent("a")), fdatamsg(agent("c"), privategroup(agent("a")), stokenmsg(token(agent("c"), group("Winners"), merge-factor-out-message, sGroupMemberList(groupmember(agent("c"), alpha)))), noview)))) sMessageList( datamsg(agent("a"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), 9, sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6) sNatSet(7) sNatSet(8), gdatamsg(agent("a"), group( "Winners"), fdatamsg(agent("a"), group("Winners"), stokenmsg(token(agent("a"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("c"), alpha ^ random(1))) sGroupMemberList(groupmember(agent("a"), alpha ^ random(0)))), keyid(1)), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList( agent("c")) sAgentList(agent("a")), 1))))) sMessageList(datamsg(agent("c"), reliable, 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))))) 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), 11, eNatSet, ggroupmsg(agent("b"), eGroupAgentsList))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("b")) sProcSet( agent("c")), 4), 12, sNatSet(11), ggroupmsg(agent("c"), sGroupAgentsList(groupagents(group("Winners"), sAgentList(agent( "c"))))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 14, sNatSet(11) sNatSet(12), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent( "b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 15, sNatSet(11) sNatSet(12) sNatSet(14), gjoinmsg( agent("b"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent( "c")), 4), 16, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15), gdatamsg(agent("b"), group("Winners"), fokmsg(agent("b"), group("Winners"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 17, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 18, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17), gdatamsg(agent("c"), privategroup(agent("b")), fdatamsg(agent("c"), privategroup(agent("b")), stokenmsg(token(agent("c"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("c"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(2))))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 19, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18), gdatamsg(agent("b"), group("Winners"), fdatamsg(agent("b"), group("Winners"), stokenmsg(token(agent("b"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember( agent("c"), alpha)) sGroupMemberList(groupmember(agent("b"), alpha ^ random(2))))), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group("Winners"), sAgentList(agent("c")) sAgentList(agent("b")), 1))))) sMessageList(datamsg( agent("c"), fifo, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 20, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet( 15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19), gdatamsg(agent("c"), privategroup(agent("b")), fdatamsg(agent("c"), privategroup(agent("b")), stokenmsg(token(agent("c"), group("Winners"), merge-factor-out-message, sGroupMemberList( groupmember(agent("c"), alpha)))), noview)))) sMessageList(datamsg(agent("b"), agreed, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), 21, sNatSet(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet( 19) sNatSet(20), gdatamsg(agent("b"), group("Winners"), fdatamsg(agent("b"), group("Winners"), stokenmsg(token(agent("b"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("c"), alpha ^ random(3))) sGroupMemberList( groupmember(agent("b"), alpha ^ random(2)))), keyid(4)), view(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), group( "Winners"), sAgentList(agent("c")) sAgentList(agent("b")), 1))))) 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), 22, 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), 23, sNatSet(22), 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), 24, sNatSet(22) sNatSet(23), 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), 25, sNatSet(22) sNatSet(23) sNatSet(24), 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), 26, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25), 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), 27, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26), 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), 28, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27), 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(4))) sGroupMemberList(groupmember(agent("c"), idPartialKey)))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 29, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28), 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(4))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(4) * random(5))))), noview)))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent( "b")) sProcSet(agent("c")), 7), 30, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet(29), 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(4))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(4) * random(5))))), 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), 31, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet( 28) sNatSet(29) sNatSet(30), 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(5))))), noview)))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 32, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet( 29) sNatSet(30) sNatSet(31), 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(4))))), noview)))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 33, sNatSet(22) sNatSet(23) sNatSet(24) sNatSet(25) sNatSet(26) sNatSet(27) sNatSet(28) sNatSet( 29) sNatSet(30) sNatSet(31) sNatSet(32), 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(5) * random(6))) sGroupMemberList(groupmember(agent("b"), alpha ^ random(4) * random(6))) sGroupMemberList( groupmember(agent("c"), alpha ^ random(4) * random(5)))), keyid(5)), 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), 34, 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"), fdatamsg(agent("c"), group("Winners"), sdatamsg(keyid(5), alpha ^ random(4) * random(5) * random(6), 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), 35, 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), gleavemsg(agent("a"), group("Winners"), noview))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 36, 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) sNatSet(35), 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), 37, 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) sNatSet(35) sNatSet(36), gdatamsg(agent("c"), group("Winners"), fokmsg(agent("c"), group("Winners"))))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 38, 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) sNatSet(35) sNatSet(36) sNatSet(37), gdatamsg(agent("b"), privategroup(agent("c")), fdatamsg(agent("b"), privategroup(agent("c")), stokenmsg(token(agent("b"), group("Winners"), mass-join-message, sGroupMemberList(groupmember(agent("b"), alpha)) sGroupMemberList(groupmember(agent("c"), alpha ^ random(8))))), noview)))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 39, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38), gdatamsg(agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-broadcast-message, sGroupMemberList(groupmember(agent("b"), alpha)) sGroupMemberList(groupmember(agent("c"), alpha ^ random(8))))), view( regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1))))) sMessageList(datamsg(agent("b"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 40, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet( 39), 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)))), noview)))) sMessageList(datamsg(agent("c"), agreed, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 41, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40), gdatamsg( agent("c"), group("Winners"), fdatamsg(agent("c"), group("Winners"), stokenmsg(token(agent("c"), group("Winners"), merge-key-update-message, sGroupMemberList(groupmember(agent("b"), alpha ^ random(9))) sGroupMemberList(groupmember(agent( "c"), alpha ^ random(8)))), keyid(6)), view(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), group("Winners"), sAgentList(agent("b")) sAgentList(agent("c")), 1))))) sMessageList(datamsg(agent("b"), agreed, regconf( sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 42, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41), gdisconnectmsg(agent("b"), nogroup, noview))) sMessageList(datamsg(agent("c"), fifo, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 43, 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41) sNatSet(42), 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"), 10, 13))) causalorder(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sConstraintSet(constraint(agent("b"), 11, 15)) sConstraintSet(constraint(agent("b"), 11, 16)) sConstraintSet(constraint(agent("b"), 11, 19)) sConstraintSet(constraint( agent("b"), 11, 21)) sConstraintSet(constraint(agent("b"), 12, 15)) sConstraintSet(constraint(agent("b"), 12, 21)) sConstraintSet(constraint(agent("b"), 14, 15)) sConstraintSet(constraint(agent("b"), 14, 21)) sConstraintSet(constraint( agent("b"), 15, 16)) sConstraintSet(constraint(agent("b"), 15, 19)) sConstraintSet(constraint(agent("b"), 15, 21)) sConstraintSet(constraint(agent("b"), 16, 19)) sConstraintSet(constraint(agent("b"), 16, 21)) sConstraintSet(constraint( agent("b"), 17, 21)) sConstraintSet(constraint(agent("b"), 18, 21)) sConstraintSet(constraint(agent("b"), 19, 21)) sConstraintSet(constraint(agent("b"), 20, 21)) sConstraintSet(constraint(agent("c"), 11, 12)) sConstraintSet(constraint( agent("c"), 12, 14)) sConstraintSet(constraint(agent("c"), 12, 17)) sConstraintSet(constraint(agent("c"), 12, 18)) sConstraintSet(constraint(agent("c"), 12, 20)) sConstraintSet(constraint(agent("c"), 14, 17)) sConstraintSet(constraint( agent("c"), 14, 18)) sConstraintSet(constraint(agent("c"), 14, 20)) sConstraintSet(constraint(agent("c"), 17, 18)) sConstraintSet(constraint(agent("c"), 17, 20)) sConstraintSet(constraint(agent("c"), 18, 20))) causalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sConstraintSet(constraint(agent("a"), 0, 3)) sConstraintSet(constraint(agent("a"), 0, 9)) sConstraintSet(constraint(agent("a"), 1, 3)) sConstraintSet(constraint( agent("a"), 1, 9)) sConstraintSet(constraint(agent("a"), 2, 9)) sConstraintSet(constraint(agent("a"), 3, 4)) sConstraintSet(constraint(agent("a"), 3, 7)) sConstraintSet(constraint(agent("a"), 3, 9)) sConstraintSet(constraint(agent( "a"), 4, 7)) sConstraintSet(constraint(agent("a"), 4, 9)) sConstraintSet(constraint(agent("a"), 5, 9)) sConstraintSet( constraint(agent("a"), 6, 9)) sConstraintSet(constraint(agent("a"), 7, 9)) sConstraintSet(constraint(agent("a"), 8, 9)) sConstraintSet(constraint(agent("c"), 0, 1)) sConstraintSet(constraint(agent("c"), 0, 5)) sConstraintSet(constraint(agent( "c"), 0, 6)) sConstraintSet(constraint(agent("c"), 0, 8)) sConstraintSet(constraint(agent("c"), 1, 5)) sConstraintSet( constraint(agent("c"), 1, 6)) sConstraintSet(constraint(agent("c"), 1, 8)) sConstraintSet(constraint(agent("c"), 2, 5)) sConstraintSet(constraint(agent("c"), 2, 6)) sConstraintSet(constraint(agent("c"), 2, 8)) sConstraintSet(constraint(agent( "c"), 5, 6)) sConstraintSet(constraint(agent("c"), 5, 8)) sConstraintSet(constraint(agent("c"), 6, 8))) causalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sConstraintSet(constraint(agent("a"), 22, 25)) sConstraintSet(constraint(agent("a"), 22, 28)) sConstraintSet(constraint(agent("a"), 22, 31)) sConstraintSet( constraint(agent("a"), 22, 35)) sConstraintSet(constraint(agent("a"), 23, 35)) sConstraintSet(constraint(agent("a"), 24, 35)) sConstraintSet(constraint(agent("a"), 25, 28)) sConstraintSet(constraint(agent("a"), 25, 31)) sConstraintSet( constraint(agent("a"), 25, 35)) sConstraintSet(constraint(agent("a"), 26, 35)) sConstraintSet(constraint(agent("a"), 27, 35)) sConstraintSet(constraint(agent("a"), 28, 31)) sConstraintSet(constraint(agent("a"), 28, 35)) sConstraintSet( constraint(agent("a"), 29, 35)) sConstraintSet(constraint(agent("a"), 30, 35)) sConstraintSet(constraint(agent("a"), 31, 35)) sConstraintSet(constraint(agent("a"), 32, 35)) sConstraintSet(constraint(agent("a"), 33, 35)) sConstraintSet( constraint(agent("a"), 34, 35)) sConstraintSet(constraint(agent("b"), 22, 23)) sConstraintSet(constraint(agent("b"), 22, 42)) sConstraintSet(constraint(agent("b"), 23, 26)) sConstraintSet(constraint(agent("b"), 23, 29)) sConstraintSet( constraint(agent("b"), 23, 32)) sConstraintSet(constraint(agent("b"), 23, 36)) sConstraintSet(constraint(agent("b"), 23, 38)) sConstraintSet(constraint(agent("b"), 23, 40)) sConstraintSet(constraint(agent("b"), 23, 42)) sConstraintSet( constraint(agent("b"), 24, 42)) sConstraintSet(constraint(agent("b"), 25, 42)) sConstraintSet(constraint(agent("b"), 26, 29)) sConstraintSet(constraint(agent("b"), 26, 32)) sConstraintSet(constraint(agent("b"), 26, 36)) sConstraintSet( constraint(agent("b"), 26, 38)) sConstraintSet(constraint(agent("b"), 26, 40)) sConstraintSet(constraint(agent("b"), 26, 42)) sConstraintSet(constraint(agent("b"), 27, 42)) sConstraintSet(constraint(agent("b"), 28, 42)) sConstraintSet( constraint(agent("b"), 29, 32)) sConstraintSet(constraint(agent("b"), 29, 36)) sConstraintSet(constraint(agent("b"), 29, 38)) sConstraintSet(constraint(agent("b"), 29, 40)) sConstraintSet(constraint(agent("b"), 29, 42)) sConstraintSet( constraint(agent("b"), 30, 42)) sConstraintSet(constraint(agent("b"), 31, 42)) sConstraintSet(constraint(agent("b"), 32, 36)) sConstraintSet(constraint(agent("b"), 32, 38)) sConstraintSet(constraint(agent("b"), 32, 40)) sConstraintSet( constraint(agent("b"), 32, 42)) sConstraintSet(constraint(agent("b"), 33, 42)) sConstraintSet(constraint(agent("b"), 34, 42)) sConstraintSet(constraint(agent("b"), 35, 42)) sConstraintSet(constraint(agent("b"), 36, 38)) sConstraintSet( constraint(agent("b"), 36, 40)) sConstraintSet(constraint(agent("b"), 36, 42)) sConstraintSet(constraint(agent("b"), 37, 42)) sConstraintSet(constraint(agent("b"), 38, 40)) sConstraintSet(constraint(agent("b"), 38, 42)) sConstraintSet( constraint(agent("b"), 39, 42)) sConstraintSet(constraint(agent("b"), 40, 42)) sConstraintSet(constraint(agent("b"), 41, 42)) sConstraintSet(constraint(agent("c"), 22, 24)) sConstraintSet(constraint(agent("c"), 22, 33)) sConstraintSet( constraint(agent("c"), 22, 41)) sConstraintSet(constraint(agent("c"), 23, 24)) sConstraintSet(constraint(agent("c"), 23, 33)) sConstraintSet(constraint(agent("c"), 23, 41)) sConstraintSet(constraint(agent("c"), 24, 27)) sConstraintSet( constraint(agent("c"), 24, 30)) sConstraintSet(constraint(agent("c"), 24, 33)) sConstraintSet(constraint(agent("c"), 24, 37)) sConstraintSet(constraint(agent("c"), 24, 39)) sConstraintSet(constraint(agent("c"), 24, 41)) sConstraintSet( constraint(agent("c"), 24, 43)) sConstraintSet(constraint(agent("c"), 25, 33)) sConstraintSet(constraint(agent("c"), 25, 41)) sConstraintSet(constraint(agent("c"), 26, 33)) sConstraintSet(constraint(agent("c"), 26, 41)) sConstraintSet( constraint(agent("c"), 27, 30)) sConstraintSet(constraint(agent("c"), 27, 33)) sConstraintSet(constraint(agent("c"), 27, 37)) sConstraintSet(constraint(agent("c"), 27, 39)) sConstraintSet(constraint(agent("c"), 27, 41)) sConstraintSet( constraint(agent("c"), 27, 43)) sConstraintSet(constraint(agent("c"), 28, 33)) sConstraintSet(constraint(agent("c"), 28, 41)) sConstraintSet(constraint(agent("c"), 29, 33)) sConstraintSet(constraint(agent("c"), 29, 41)) sConstraintSet( constraint(agent("c"), 30, 33)) sConstraintSet(constraint(agent("c"), 30, 37)) sConstraintSet(constraint(agent("c"), 30, 39)) sConstraintSet(constraint(agent("c"), 30, 41)) sConstraintSet(constraint(agent("c"), 30, 43)) sConstraintSet( constraint(agent("c"), 31, 33)) sConstraintSet(constraint(agent("c"), 31, 41)) sConstraintSet(constraint(agent("c"), 32, 33)) sConstraintSet(constraint(agent("c"), 32, 41)) sConstraintSet(constraint(agent("c"), 33, 37)) sConstraintSet( constraint(agent("c"), 33, 39)) sConstraintSet(constraint(agent("c"), 33, 41)) sConstraintSet(constraint(agent("c"), 33, 43)) sConstraintSet(constraint(agent("c"), 34, 37)) sConstraintSet(constraint(agent("c"), 34, 39)) sConstraintSet( constraint(agent("c"), 34, 41)) sConstraintSet(constraint(agent("c"), 34, 43)) sConstraintSet(constraint(agent("c"), 35, 41)) sConstraintSet(constraint(agent("c"), 36, 41)) sConstraintSet(constraint(agent("c"), 37, 39)) sConstraintSet( constraint(agent("c"), 37, 41)) sConstraintSet(constraint(agent("c"), 37, 43)) sConstraintSet(constraint(agent("c"), 38, 41)) sConstraintSet(constraint(agent("c"), 39, 41)) sConstraintSet(constraint(agent("c"), 39, 43)) sConstraintSet( constraint(agent("c"), 40, 41)) sConstraintSet(constraint(agent("c"), 41, 43))) causalorder(transconf(sProcSet(agent("a")), 1, regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0)), sConstraintSet(constraint(agent("a"), 0, 3)) sConstraintSet(constraint(agent("a"), 0, 9)) sConstraintSet(constraint(agent( "a"), 1, 3)) sConstraintSet(constraint(agent("a"), 1, 9)) sConstraintSet(constraint(agent("a"), 2, 9)) sConstraintSet( constraint(agent("a"), 3, 4)) sConstraintSet(constraint(agent("a"), 3, 7)) sConstraintSet(constraint(agent("a"), 3, 9)) sConstraintSet(constraint(agent("a"), 4, 7)) sConstraintSet(constraint(agent("a"), 4, 9)) sConstraintSet(constraint(agent( "a"), 5, 9)) sConstraintSet(constraint(agent("a"), 6, 9)) sConstraintSet(constraint(agent("a"), 7, 9)) sConstraintSet( constraint(agent("a"), 8, 9)) sConstraintSet(constraint(agent("c"), 0, 1)) sConstraintSet(constraint(agent("c"), 0, 5)) sConstraintSet(constraint(agent("c"), 0, 6)) sConstraintSet(constraint(agent("c"), 0, 8)) sConstraintSet(constraint(agent( "c"), 1, 5)) sConstraintSet(constraint(agent("c"), 1, 6)) sConstraintSet(constraint(agent("c"), 1, 8)) sConstraintSet( constraint(agent("c"), 2, 5)) sConstraintSet(constraint(agent("c"), 2, 6)) sConstraintSet(constraint(agent("c"), 2, 8)) sConstraintSet(constraint(agent("c"), 5, 6)) sConstraintSet(constraint(agent("c"), 5, 8)) sConstraintSet(constraint(agent( "c"), 6, 8))) causalorder(transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)), sConstraintSet(constraint(agent("a"), 10, 13))) 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, 3)) sConstraintSet(constraint(agent("a"), 0, 9)) sConstraintSet( constraint(agent("a"), 1, 3)) sConstraintSet(constraint(agent("a"), 1, 9)) sConstraintSet(constraint(agent("a"), 2, 9)) sConstraintSet(constraint(agent("a"), 3, 4)) sConstraintSet(constraint(agent("a"), 3, 7)) sConstraintSet(constraint(agent( "a"), 3, 9)) sConstraintSet(constraint(agent("a"), 4, 7)) sConstraintSet(constraint(agent("a"), 4, 9)) sConstraintSet( constraint(agent("a"), 5, 9)) sConstraintSet(constraint(agent("a"), 6, 9)) sConstraintSet(constraint(agent("a"), 7, 9)) sConstraintSet(constraint(agent("a"), 8, 9)) sConstraintSet(constraint(agent("c"), 0, 1)) sConstraintSet(constraint(agent( "c"), 0, 5)) sConstraintSet(constraint(agent("c"), 0, 6)) sConstraintSet(constraint(agent("c"), 0, 8)) sConstraintSet( constraint(agent("c"), 1, 5)) sConstraintSet(constraint(agent("c"), 1, 6)) sConstraintSet(constraint(agent("c"), 1, 8)) sConstraintSet(constraint(agent("c"), 2, 5)) sConstraintSet(constraint(agent("c"), 2, 6)) sConstraintSet(constraint(agent( "c"), 2, 8)) sConstraintSet(constraint(agent("c"), 5, 6)) sConstraintSet(constraint(agent("c"), 5, 8)) sConstraintSet( constraint(agent("c"), 6, 8))) causalorder(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), sConstraintSet(constraint(agent("b"), 11, 15)) sConstraintSet(constraint(agent("b"), 11, 16)) sConstraintSet(constraint( agent("b"), 11, 19)) sConstraintSet(constraint(agent("b"), 11, 21)) sConstraintSet(constraint(agent("b"), 12, 15)) sConstraintSet(constraint(agent("b"), 12, 21)) sConstraintSet(constraint(agent("b"), 14, 15)) sConstraintSet(constraint( agent("b"), 14, 21)) sConstraintSet(constraint(agent("b"), 15, 16)) sConstraintSet(constraint(agent("b"), 15, 19)) sConstraintSet(constraint(agent("b"), 15, 21)) sConstraintSet(constraint(agent("b"), 16, 19)) sConstraintSet(constraint( agent("b"), 16, 21)) sConstraintSet(constraint(agent("b"), 17, 21)) sConstraintSet(constraint(agent("b"), 18, 21)) sConstraintSet(constraint(agent("b"), 19, 21)) sConstraintSet(constraint(agent("b"), 20, 21)) sConstraintSet(constraint( agent("c"), 11, 12)) sConstraintSet(constraint(agent("c"), 12, 14)) sConstraintSet(constraint(agent("c"), 12, 17)) sConstraintSet(constraint(agent("c"), 12, 18)) sConstraintSet(constraint(agent("c"), 12, 20)) sConstraintSet(constraint( agent("c"), 14, 17)) sConstraintSet(constraint(agent("c"), 14, 18)) sConstraintSet(constraint(agent("c"), 14, 20)) sConstraintSet(constraint(agent("c"), 17, 18)) sConstraintSet(constraint(agent("c"), 17, 20)) sConstraintSet(constraint( agent("c"), 18, 20))) totalorder(regconf(sProcSet(agent("a")), 2), sEventList(event(agent("a"), 10))) totalorder(regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4), sEventList(event(agent("b"), 11)) sEventList(event(agent( "b"), 11)) sEventList(event(agent("c"), 12)) sEventList(event(agent("c"), 12)) sEventList(event(agent("b"), 15)) sEventList(event(agent("b"), 15)) sEventList(event(agent("b"), 21)) sEventList(event(agent("b"), 21))) 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)) sEventList(event(agent("a"), 9)) sEventList(event(agent("a"), 9)) sEventList( event(agent("a"), 9))) totalorder(regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sEventList(event(agent("a"), 22)) sEventList(event(agent("a"), 22)) sEventList(event(agent("a"), 22)) sEventList(event(agent("b"), 23)) sEventList(event( agent("b"), 23)) sEventList(event(agent("b"), 23)) sEventList(event(agent("c"), 24)) sEventList(event(agent("c"), 24)) sEventList(event(agent("c"), 24)) sEventList(event(agent("c"), 33)) sEventList(event(agent("c"), 33)) sEventList(event( agent("c"), 33)) sEventList(event(agent("a"), 35)) sEventList(event(agent("a"), 35)) sEventList(event(agent("a"), 35)) sEventList(event(agent("c"), 41)) sEventList(event(agent("c"), 41)) sEventList(event(agent("c"), 41)) sEventList(event( agent("b"), 42)) sEventList(event(agent("b"), 42)) sEventList(event(agent("b"), 42))) 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"), 3)) sEventList(event(agent("a"), 3)) sEventList(event(agent("a"), 3)) sEventList(event(agent("a"), 9)) sEventList( event(agent("a"), 9)) sEventList(event(agent("a"), 9))) totalorder(transconf(sProcSet(agent("a")), 5, regconf(sProcSet(agent("a")), 2)), sEventList(event(agent("a"), 10))) 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"), 3)) sEventList(event(agent("a"), 3)) sEventList(event(agent("a"), 3)) sEventList(event(agent( "a"), 9)) sEventList(event(agent("a"), 9)) sEventList(event(agent("a"), 9))) totalorder(transconf(sProcSet(agent("b")) sProcSet(agent("c")), 6, regconf(sProcSet(agent("b")) sProcSet(agent("c")), 4)), sEventList(event(agent("b"), 11)) sEventList(event(agent("b"), 11)) sEventList(event(agent("c"), 12)) sEventList(event( agent("c"), 12)) sEventList(event(agent("b"), 15)) sEventList(event(agent("b"), 15)) sEventList(event(agent("b"), 21)) sEventList(event(agent("b"), 21))) 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"), eGMessageList) 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"))))) 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")) sGroupSet(group("Winners")) 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), keyid(1))) sAssocKeyList(assockey(idPartialKey, keyid(2))) sAssocKeyList(assockey(alpha ^ random(4) * random(5) * random(6), keyid(5)))))) sgroupkeylist(agent("c"), sGroupAssocKeyListSet(groupassockeylist(group("Winners"), sAssocKeyList(assockey(idPartialKey, keyid( 0))) sAssocKeyList(assockey(alpha ^ random(0) * random(1), keyid(1))) sAssocKeyList(assockey(idPartialKey, keyid(3))) sAssocKeyList(assockey(alpha ^ random(2) * random(3), keyid(4))) sAssocKeyList(assockey(alpha ^ random(4) * random(5) * random(6), keyid(5))) sAssocKeyList(assockey(alpha ^ random(8) * random(9), keyid(6))) sAssocKeyList(assockey(idPartialKey, keyid(7)))))) sgroupmembsetlist(agent("a"), sGroupAssocMembSetListSet(groupassocmembsetlist(group("Winners"), sAssocMembSetList(assocmembset( sAgentSet(agent("a")) sAgentSet(agent("c")), keyid(1))) sAssocMembSetList(assocmembset(sAgentSet(agent("a")), keyid(2))) sAssocMembSetList(assocmembset(sAgentSet(agent("a")) sAgentSet(agent("b")) sAgentSet(agent("c")), keyid(5)))))) sgroupmembsetlist(agent("c"), sGroupAssocMembSetListSet(groupassocmembsetlist(group("Winners"), sAssocMembSetList(assocmembset( sAgentSet(agent("c")), keyid(0))) sAssocMembSetList(assocmembset(sAgentSet(agent("a")) sAgentSet(agent("c")), keyid(1))) sAssocMembSetList(assocmembset(sAgentSet(agent("c")), keyid(3))) sAssocMembSetList(assocmembset(sAgentSet(agent("b")) sAgentSet(agent("c")), keyid(4))) sAssocMembSetList(assocmembset(sAgentSet(agent("a")) sAgentSet(agent("b")) sAgentSet( agent("c")), keyid(5))) sAssocMembSetList(assocmembset(sAgentSet(agent("b")) sAgentSet(agent("c")), keyid(6))) sAssocMembSetList(assocmembset(sAgentSet(agent("c")), keyid(7)))))) sfreshness(agent("a"), sGroupSet(group("Winners"))) sfreshness(agent("c"), sGroupSet(group("Winners"))) sforceka(agent("a"), sGroupSet(group("Winners"))) sforceka(agent("c"), sGroupSet(group("Winners"))) skainprogress(agent("a"), eGroupSet) skainprogress(agent("c"), eGroupSet) sshadowmessage(agent("a"), eFMessageList) sshadowmessage(agent("c"), eFMessageList) 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(sdatamsg(agent("a"), group("Winners"), nondecryptable(sdatamsg( keyid(0), idPartialKey, sdata("MyTEST"))), 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(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(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(sdatamsg(agent("c"), group("Winners"), sdata("MyTEST"), view( regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), group("Winners"), sAgentList(agent("c")), 0))) 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(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(10) sNatSet(13)) localmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(3) sNatSet(4) sNatSet(7) sNatSet(9)) localmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(22) sNatSet(25) sNatSet(28) sNatSet(31) sNatSet(35)) 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(11) sNatSet(15) sNatSet(16) sNatSet(19) sNatSet(21)) 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(23) sNatSet(26) sNatSet(29) sNatSet(32) sNatSet(36) sNatSet(38) sNatSet(40) sNatSet(42)) 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(12) sNatSet(14) sNatSet(17) sNatSet(18) sNatSet(20)) localmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(5) sNatSet(6) sNatSet(8)) localmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), sNatSet(24) sNatSet(27) sNatSet(30) sNatSet(33) sNatSet(34) sNatSet(37) sNatSet(39) sNatSet(41) sNatSet(43)) 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(10) sNatSet(13)) knownmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6) sNatSet(7) sNatSet(8) sNatSet(9)) knownmsgs(agent("a"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41) sNatSet(42) sNatSet(43)) 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(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21)) knownmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 0), sNatSet(0) sNatSet(1) sNatSet(2) sNatSet(3) sNatSet(4) sNatSet(5) sNatSet(6) sNatSet(7) sNatSet(8) sNatSet(9)) knownmsgs(agent("b"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41) sNatSet(42) sNatSet(43)) 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(11) sNatSet(12) sNatSet(14) sNatSet(15) sNatSet(16) sNatSet(17) sNatSet(18) sNatSet(19) sNatSet(20) sNatSet(21)) 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) sNatSet(6) sNatSet(7) sNatSet(8) sNatSet(9)) knownmsgs(agent("c"), regconf(sProcSet(agent("a")) sProcSet(agent("b")) sProcSet(agent("c")), 7), 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) sNatSet(35) sNatSet(36) sNatSet(37) sNatSet(38) sNatSet(39) sNatSet(40) sNatSet(41) sNatSet(42) sNatSet(43)) 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(5), sGroupContextSet(groupcontext(group("Winners"), context(random(4), alpha ^ random(4) * random(5) * random(6), sGroupMemberList(groupmember(agent("a"), alpha ^ random(5) * random(6))) sGroupMemberList(groupmember(agent( "b"), alpha ^ random(4) * random(6))) sGroupMemberList(groupmember(agent("c"), alpha ^ random(4) * random(5))))))) scontext(agent("c"), keyid(7), sGroupContextSet(groupcontext(group("Winners"), context(idKeyShare, idPartialKey, sGroupMemberList(groupmember(agent("c"), alpha)))))) 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"), eGroupSet, eGroupSet, sGroupSet(group("Winners")), eGroupSet) slaziness(agent("c"), eGroupSet, eGroupSet, sGroupSet(group("Winners")), eGroupSet) sstate(agent("a"), eGroupSet, eGroupSet, eGroupSet, eGroupSet, eGroupSet, eGroupSet) sstate(agent("c"), sGroupSet(group("Winners")), eGroupSet, eGroupSet, eGroupSet, eGroupSet, eGroupSet) Maude>