-- Sigma_gold

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

-- Sigma_gold is discussed in Section 9 of CS-TR-963.

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

types

Cid = token;
Aid = token;
Uid = token;
Did = token;
Document = token;
doc_type = <Exper_rep> | <Mngt_rep> | <Safety_rep> | <Memo>;
Time = token;
User = token;

AuthRel = set of (Aid * Aid);
aRole = <Leader> | <Subordinate>;
uRole = <Chemist> | <LabAssistant>;

Coalition:: members: set of Aid
	aroles: map Aid to set of aRole
	uroles: map Uid to set of uRole
	dr: map Did to Document
	auth: AuthRel
inv mk_Coalition(-,aroles,-,-,auth) == 
LeaderInvariant(aroles) and
AuthInvariant(auth);

Agent :: employees: set of Uid
	dr: map Did to Document;

Archive:: doc: map Did to DocInfo;

DocInfo:: document: doc_type
	author: Uid|Aid
	predecessor: [Did]
	successor: [Did]
	date_of_creation: Time
	transfers: set of (Aid * Aid * Aid * Time);

state Sigma_gold of
	coals: map Cid to Coalition
	agents: map Aid to Agent
	users: map Uid to User
end

functions

-- There is exactly one leader of any GOLD coalition

LeaderInvariant: map Aid to set of aRole -> bool 
LeaderInvariant(aroles) == 
  exists1 aid in set dom aroles & <Leader> in set aroles(aid);

-- 

AuthInvariant: set of (Aid * Aid) -> bool
AuthInvariant(auth) ==
  forall aset: set of Aid & aset subset domain(auth) and
    (aset <> {} => exists a in set aset & not (exists aa in set aset & mk_(a,aa) in set auth));
  
domain: set of (Aid * Aid) -> set of Aid
domain(auth) == 
{a1|a1:Aid & (exists a2:Aid & mk_(a1,a2) in set auth)} 

operations

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

Join(a, b: 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 
    <Leader> in set coals(c).aroles(b) and 
    authorise_join(b,a,c)
post coals(c).members = coals~(c).members union {a};

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

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

-- Empty coalitions are precluded by the invariant.

-- an agent transfers one document to another agent, with the permission of the 
-- coalition

InfoTransfer(from_: Aid, to_: Aid, d: Document, did: Did, c:Cid)
ext	wr agents: map Aid to Agent
pre	{from_, to_} subset dom agents and 
        d in set rng agents(from_).dr and 
        did not in set dom coals(c).dr and 
        c in set dom coals and 
        {from_, to_} subset coals(c).members and 
        exists a in set dom agents & authorises(a, from_, to_, {d}, c)
post agents = agents~ ++ 
     {to_ |-> mu(agents~(to_), dr |-> agents~(to_).dr munion {did |-> d})};

-- an agent "discovers" (creates) a document and places it in its document repository. 

Discover(a:Aid,d:Document,did:Did)
ext	wr agents: map Aid to Agent
pre     a in set dom agents and 
        did not in set dom agents(a).dr
post    agents(a).dr = agents~(a).dr munion {did |-> d};

-- an agent adds a document to a coalition repository 

AddToVO(from_: Aid, d:Document, did:Did, c:Cid)
ext	wr coals: map Cid to Coalition
pre	from_ in set dom agents and 
        from_ in set coals(c).members and
	d in set rng agents(from_).dr and
	did not in set dom coals(c).dr and
	c in set dom coals and
	exists a in set dom agents & a in set coals(c).members and permits(a,from_,{d},c)
post	coals = coals~ ++ {c |-> mu(coals~(c), dr |-> coals~(c).dr munion {did |-> d})};

permits(a: Aid, from_: Aid, ds: set of Document, c:Cid) b:bool
ext	rd coals: map Cid to Coalition
pre	{a, from_} subset coals(c).members
post	b = true or b = false;

authorises(a: Aid, from_: Aid, to_: Aid, ds: set of Document, c: Cid) b:bool
ext	rd coals: map Cid to Coalition
pre 	{a, from_, to_} subset coals(c).members
post 	b = (mk_(a, from_) in set coals(c).auth);

authorise_join(new_guy: Aid, leader: Aid, c:Cid) b:bool
ext	rd coals: map Cid to Coalition
pre	leader in set coals(c).members and 
        <Leader> in set coals(c).aroles(leader) and 
        new_guy not in set coals(c).members
post	b = true or b = false;