-- Sigma_trust_info

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

-- Sigma_trust_info 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:: KnowledgeBase: set of Information;

Information:: item: token
              iTrust: TrustValue;

TrustValue = rat;

state Sigma_trust_info of
	coals: map Cid to set of Aid
	agents: map Aid to Agent
end

operations

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

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 a in set dom agents and c in set dom coals and 
    a in set coals(c)
post coals = coals~ ++ {c |-> coals~(c) \ {a}};  

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

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

-- InfoTransfer transfers information stripped of its trust value,
-- allowing the recipient t to attach a new trust value.  Note the
-- precondition, which allows the transfered information to be
-- drawn from any of the information sets in the structured
-- collection within the source agent f. 

InfoTransfer(f,t:Aid, tset:set of token) 
ext wr agents: map Aid to Agent 
pre {f,t} subset dom agents and tset subset {ati.item | ati in set agents(f).KnowledgeBase}
post agents = agents~ ++ {t |-> mu(agents(t), KnowledgeBase |-> agents~(t).KnowledgeBase union {AddTrust(tset)})};

functions

-- AddTrust builds a information set with trust values.
-- Selection of the trust values is beyond the scope of the model. 
-- Replace this with an algorithm for a particular instantiation of the model. 

AddTrust(tokset:set of token)tset:set of Information
post {t.item | t in set tset} = tokset;