-- Sigma_simp

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

-- Sigma_simp is discussed in Section 4 of CS-TR-963.

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

types

Cid = token;
Aid = token;
Agent = set of Information;
Information = token;

state Sigma_simp of
	coals : map Cid to set of Aid
	agents: map Aid to Agent
inv mk_Sigma_simp(coals, agents) == dunion rng coals subset dom agents
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(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)
post coals = coals~ ++ {c |-> coals~(c) \ {a}};

CreateEmptyCoal(c:Cid)
ext	wr coals: map Cid to set of Aid
pre c not in set dom coals
post coals = coals~ munion {c |-> {}};

-- Dissolve a coalition without insisting  that it is empty.

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

-- Dissolve an empty coalition.

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

-- An agent discovers a piece of infomration

Discover(a:Aid,i:Information)
ext wr agents: map Aid to Agent
pre a in set dom agents
post agents(a) = agents~(a) union {i}; 

--An agent transfers a piece of information

InfoTransfer(f,t:Aid, i:Information)
ext wr agents: map Aid to Agent
pre {f,t} subset dom agents and i in set agents(f)
post agents(t) = agents~(t) union {i};