-- Sigma_m

-- This model is one of a set of models provided to support Newcastle
-- University Computer Science Technical Report CS-TR-963.  

-- Sigma_m is discussed in Section 2.1 of CS-TR-963.

-- Authors: Jeremy Bryans, John Fitzgerald, Cliff Jones, Igor Mozolevsky
-- 19 January 2007

types
Cid = token;
Aid = token;
Agent = token;

state Sigma_m of
	coals : map Cid to set of Aid
	agents: map Aid to Agent
inv mk_Sigma_m(coals, agents) == dunion rng coals subset dom agents and 
                                 {} not in set rng coals
end

operations

Join(a:Aid, c:Cid)
ext 	wr coals: map Cid to set of Aid
	rd agents: map Aid to Agent
pre  a in set dom agents and 
     c in set dom coals and 
     a not in set coals(c)
post coals = coals~ ++ {c |-> coals~(c) union {a}};

--
-- Remove an agent. This is not defined if the coalition has
-- just one agent left in it. If there is just one agent left, 
-- either add another before removing the first, or use DissolveCoal
-- to dissolve the coalition. 
--
Remove(a:Aid, c:Cid)
ext	wr coals: map Cid to set of Aid
pre  c in set dom coals and 
     a in set coals(c) and
     coals(c) <> {a}
post coals = coals~ ++ {c |-> coals~(c) \ {a}};

--
-- Coalition creation requires that some initial members are supplied.
-- Hence CreateCoal takes a non-empty set of Aid as input. 
--
CreateCoal(c:Cid, ags:set of Aid)
ext	wr coals: map Cid to set of Aid
	rd agents: map Aid to Agent
pre  c not in set dom coals and 
     ags <> {} and 
     ags subset dom agents
post coals = coals~ munion {c |-> ags};

DissolveCoal(c:Cid)
ext	wr coals: map Cid to set of Aid
pre  c in set dom coals
post coals = {c} <-: coals~