-- Sigma_mg

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

-- Sigma_mg is discussed in Section 2.2 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_mg of
	coals: set of Cid
	agents: map Aid to Agent
	membs: set of (Aid * Cid)
inv mk_Sigma_mg(coals, agents, membs) == 
    membs subset {mk_(a,c) |a in set dom agents, c in set coals}
end

operations
Join(a: Aid, c:Cid)
ext	rd coals: set of Cid
	rd agents: map Aid to Agent
	wr membs: set of (Aid * Cid)
pre a in set dom agents and c in set coals and mk_(a, c) not in set membs
post membs = membs~ union {mk_(a,c)};

Remove(a:Aid, c:Cid)
ext	rd coals: set of Cid
	wr membs: set of (Aid * Cid)
pre mk_(a,c) in set membs
post membs = membs~ \ {mk_(a,c)};

CreateCoal(c:Cid)
ext	wr coals: set of Cid
pre  c not in set coals 
post coals = coals~ union {c};
     
DissolveCoal(c:Cid)
ext	wr coals: set of Cid
	wr membs: set of (Aid * Cid)
pre  c in set coals
post coals = coals~ \ {c} and 
     membs = {mk_(a,x) | mk_(a,x) in set membs & x <> c};

DissolveEmptyCoal(c:Cid)
ext	wr coals: set of Cid
	wr membs: set of (Aid * Cid)
pre  c in set coals and 
     not exists mk_(-,x) in set membs & x=c
post coals = coals~ \ {c} and 
     membs = {mk_(a,x) | mk_(a,x) in set membs & x <> c}