-- Sigma_trust_a

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

-- Sigma_trust_a is discussed in Section 8 of CS-TR-963.

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

types 

Aid = token;
Cid = token;

Agent:: aTrust: map Aid to trustvalue;

trustvalue = rat;

state Sigma_trust_a of
	 coals: map Cid to set of Aid
	agents: map Aid to Agent
inv mk_Sigma_trust_a(coals, agents) == dunion rng coals psubset 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}};

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 c not in set dom coals
post coals = {c} <-: coals~;