-- Sigma_time_a

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

-- Sigma_time_a is discussed in Section 7 of CS-TR-963.

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

types

Cid = token;
Aid = token;

Agent:: current_time : Time;

Time = token;

state Sigma_time_a of
	coals: map Cid to set of Aid
	agents: map Aid to Agent
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}};

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

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~;