-- Sigma_loc

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

-- Sigma_loc is discussed in Section 3 of CS-TR-963.

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

types

Aid = token;
Cid = token;
Cinf:: info: set of Information;
Agent:: info : set of Information;

Information = token;

state Sigma_loc of
	info: set of Information
	coals: map Cid to Cinf
	agents: map Aid to Agent
end

operations

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

Discover(a:Aid,infs:set of Information)
ext wr agents : map Aid to Agent
pre a in set dom agents
post agents = agents~ ++ {a |-> mu(agents~(a), info |-> agents~(a).info union infs)};

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

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