-- Sigma_p_time

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

-- Sigma_p_time is discussed in Section 7.2 of CS-TR-963.

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

types

Cid = token;
Aid = token;

Agent:: agentinfo: set of TimedInformation
        current_time : Time;

--
-- Time is refined from token to nat in this model to allow comparison 
-- of timestamps. 
--
Time = nat;

Information :: item: token
               expire: [Time];

--
-- TimedInformation models a set of Information with its own
-- expiry time as a set, allowing for the possibility that a set of 
-- Information has a value beyond that of the individual elements. 
-- Invariant that the expiry time of the set must be later or equal to 
-- that of each of its elements.
--
TimedInformation :: info: set of Information
                    prov: Aid
                    set_expire: [Time]
inv mk_TimedInformation(info,-,set_expire) == 
       set_expire <> nil <=> 
         forall i in set info & i.expire <> nil and i.expire <= set_expire;

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

functions

still_valid: Information * Time -> bool
still_valid(info,time) == info.expire = nil or 
                          info.expire >= time;

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

-- The discovering agent records itself as the provenance of the information.

Discover(a:Aid,ti: set of Information)
ext wr agents: map Aid to Agent
pre a in set dom agents
post agents = agents~ ++ {a |-> mu(agents(a), agentinfo |-> agents~(a).agentinfo union {ExpiryProv(ti,a)})}; 

--
-- InfoTransfer transfers information stripped of its expiry time, allowing the recipient t to 
-- attach a new expiry time if required. 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. 
-- The sending agent is recorded as the provider of the information.
--
InfoTransfer(f,t:Aid, ti:set of Information)
ext wr agents: map Aid to Agent
pre {f,t} subset dom agents and 
    ti subset dunion  {ati.info | ati in set agents(f).agentinfo}
post agents = agents~ ++ {t |-> mu(agents(t), agentinfo |-> agents~(t).agentinfo union {ExpiryProv(ti,f)})};


functions
--
-- ExpiryProv builds a timed information set with expiry time,
-- and adds a provenance agent.
-- Selection of the set expiry time is beyond the scope of the model. 
-- Replace this with an algorithm for a particular instantiation of the model. 
--
ExpiryProv(i:set of Information, f:Aid)tis:TimedInformation
post tis.info = i and tis.prov = f;