-- Sigma_p_star

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

-- Sigma_p_star is discussed in Section 6 of CS-TR-963.

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

types

Cid = token;
Aid = token;

Agent :: info : set of Information;

Information :: item : token
	prov : seq of Aid;

state Sigma_p_star of 
      coals: map Cid to set of Aid
      agents: map Aid to Agent
inv mk_Sigma_p_star(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~;

-- If information is discovered, provenance is set to self.

Discover(a:Aid,ts:set of token)
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 newinfoset(ts,a))}; 

-- Agents transfer the entire provenance information.
-- The receiving agent adds the sending agent to the head of 
-- the provenance information.

InfoTransfer(f,t:Aid, infs:set of Information)
ext wr agents: map Aid to Agent
pre {f,t} subset dom agents and infs subset agents(f).info
post agents = agents~ ++ {t |-> mu(agents(t), info |-> agents~(t).info union updateprovs(infs,f))}; 

functions

updateprovs : set of Information * Aid -> set of Information
updateprovs(infs,aid) ==
  {mk_Information(i.item,p) | i in set infs, p:seq of Aid & p = [aid] ^ i.prov };

newinfoset : set of token * Aid -> set of Information
newinfoset(ts,aid) ==
  {mk_Information(tok,[aid]) | tok in set ts};