-- Sigma_ma

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

-- Sigma_ma is discussed in Section 2.3 of CS-TR-963.

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

types

Cid = token;
Aid = token;

state Sigma_ma of
	coals: set of Cid
	agents: map Aid to set of Cid
inv mk_Sigma_ma(coals, agents) == dunion rng agents subset coals
end

operations

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

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

CreateCoal(c:Cid)
ext	wr coals: set of Cid
	rd agents: map Aid to set of Cid
pre  c not in set coals 
post coals = coals~ union {c};

DissolveCoal(c:Cid)
ext	wr coals: set of Cid
pre  c in set coals
post coals = coals~ \ {c}; 

DissolveEmptyCoal(c:Cid)
ext	wr coals: set of Cid
	rd agents: map Aid to set of Cid
pre  c not in set dunion rng agents 
post coals = coals~ \ {c}; 

--
-- An operation to determine the membership of a given coalition. 
--
Members(c:Cid) membs: set of Aid
ext	rd coals: set of Cid
	rd agents: map Aid to set of Cid
pre  c  in set coals
post membs = {a | a in set dom agents & c in set agents(a)}