in cliques.maude

--- join and leave examples

rew fresh(0)
    start(agent("a"), group("G"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G"))
    join(agent("c"), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))), group("G"))
    join(agent("d"), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))), group("G")) .

rew fresh(0)
    start(agent("a"), group("G"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G"))
    join(agent("c"), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))), group("G"))
    join(agent("d"), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))), group("G")) 
    leave(sAgentList(agent("d")), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))), group("G")) .

--- leave with empty list does key refresh

rew fresh(0)
    start(agent("a"),group("G"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G"))
    join(agent("c"), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))), group("G"))
    join(agent("d"), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))), group("G")) 
    leave(eAgentList, (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))), group("G")) .
    
--- join and merge examples

rew fresh(0)
    start(agent("a"),group("G"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G"))
    join(agent("c"), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))), group("G"))
    merge(sAgentList(agent("d")) sAgentList(agent("e")), 
      (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))  sAgentList(agent("e"))), group("G")) .

rew fresh(0)
    start(agent("a"),group("G"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G"))
    join(agent("c"), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))), group("G"))
    merge(sAgentList(agent("d")) sAgentList(agent("e")) sAgentList(agent("f")), 
      (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))  sAgentList(agent("e")) sAgentList(agent("f"))), 
      group("G")) .

--- some simple search analsysis

search fresh(0)
    start(agent("a"), group("G")) =>! state:State .

search fresh(0)
    start(agent("a"), group("G"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G")) 
    =>! state:State .

search fresh(0)
    start(agent("a"), group("G"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G"))
    join(agent("c"), (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))), group("G")) 
    =>! state:State .

search fresh(0)
    start(agent("a"), group("G"))
    merge(sAgentList(agent("b")) sAgentList(agent("c")),
      (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))), group("G")) =>! state:State .

search fresh(0)
    start(agent("a"), group("G"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G"))
    merge(sAgentList(agent("c")), 
      (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))), group("G")) =>! state:State .

--- the following runs out of memory 
***(
search fresh(0)
    start(agent("a"), group("G"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G"))
    merge(sAgentList(agent("c")) sAgentList(agent("d")), 
      (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))), group("G")) =>! state:State .
)

--- simple search with multiple groups 

search fresh(0)
    start(agent("a"), group("G1"))
    start(agent("a"), group("G2"))
    join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G1")) 
    join(agent("c"), (sAgentList(agent("a")) sAgentList(agent("c"))), group("G2")) 
    =>! state:State .

--- model checking

in model-checker .

mod CLIQUES-MODEL-CHECK-1 is
   protecting CLIQUES .
   protecting MODEL-CHECKER .

   var var : Nat .
   var contexta contextb contextc : Context .
   var memberlista memberlistb memberlistc : AgentList .

   op done : -> Prop .

   ceq fresh(var)
      ready(agent("a"), group("G"), contexta, memberlista)
      ready(agent("b"), group("G"), contextb, memberlistb)
      ready(agent("c"), group("G"), contextc, memberlistc) 
      |= 
      done = true 
      if groupsecret(contexta) == groupsecret(contextb) /\
         groupsecret(contextb) == groupsecret(contextc) .

   op initial : -> State .
   eq initial = fresh(0)
        start(agent("a"),group("G"))
        merge(sAgentList(agent("b")) sAgentList(agent("c")),
          (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c"))), group("G")) .

endm

red modelCheck(initial, <> done) .


--- the following runs out of memory (like the corresponding search)

mod CLIQUES-MODEL-CHECK-2 is
   protecting CLIQUES .
   protecting MODEL-CHECKER .

   var var : Nat .
   var contexta contextb contextc contextd : Context .
   var memberlista memberlistb memberlistc memberlistd : AgentList .

   op done : -> Prop .

   eq fresh(var)
      ready(agent("a"), group("G"), contexta, memberlista)
      ready(agent("b"), group("G"), contextb, memberlistb)
      ready(agent("c"), group("G"), contextc, memberlistc) 
      ready(agent("d"), group("G"), contextd, memberlistd) 
      |= 
      done = true .

   op initial : -> State .
   eq initial = fresh(0)
        start(agent("a"),group("G"))
        join(agent("b"), (sAgentList(agent("a")) sAgentList(agent("b"))), group("G"))
        merge(sAgentList(agent("c")) sAgentList(agent("d")), 
          (sAgentList(agent("a")) sAgentList(agent("b")) sAgentList(agent("c")) sAgentList(agent("d"))), group("G")) .

endm

***(
red modelCheck(initial, <> done) .
)