-- Sigma_trust_c

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

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

Coalition :: members : set of Aid
             cTrust : trustvalue;

trustvalue = rat;

state Sigma_trust_c of
	 coals: map Cid to Coalition
	agents: map Aid to Agent
inv mk_Sigma_trust_c(coals,agents) == 
forall c in set dom coals & 
  forall m,n in set coals(c).members & agents(m).aTrust(n) >= coals(c).cTrust
end

operations

CreateCoal(c:Cid,t:trustvalue)
ext	wr coals: map Cid to Coalition
pre c not in set dom coals
post coals = coals~ munion {c |-> mk_Coalition({},t)};

Join(a:Aid, c:Cid)
ext 	wr coals: map Cid to Coalition
	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).members 
    and everybodyhappy(a,c,coals,agents)
post coals = coals~ ++ {c |-> coals~(c).members union {a}};

Remove(a:Aid, c:Cid)
ext  wr coals: map Cid to Coalition  
pre a in set dom agents and c in set dom coals and 
    a in set coals(c).members 
post coals =  coals~ ++ 
 {c |-> mu(coals~(c), members |-> coals~(c).members \ {a})};  

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

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

functions 

-- The trust value the joining agent holds for each member of the
-- coalition must be higher than the minimum stipulated by the coalition,
-- and the trust value of each member of the coalition for the joining
-- member must be higher than the stipulated minimum. 

everybodyhappy: Aid * Cid * map Cid to Coalition * map Aid to Agent -> bool
everybodyhappy(a,c,cls,ags) == 
  forall m in set cls(c).members & 
     ags(a).aTrust(m) >= cls(c).cTrust and
     ags(m).aTrust(a) >= cls(c).cTrust