-------------------------   plan-semantics.m  ---------------------------------
--- Date: Sat, 25 Aug 2001 00:44:24 -0700
--- From: Mark-Oliver Stehr <stehr@csl.sri.com>
--- Revised by CLT 01 Oct

--- requires plan-syntax.m plan-sorts.m plan-network.m 
--- defines PROP PLAN-SEMANTICS

fmod PROP is

sort Prop True .
subsort True < Prop .

endfm

mod PLAN-SEMANTICS is

*** including PLAN-SYNTAX .
including PLAN-SORTS .
including PLAN-NETWORK .
including PROP .

var l l' : Loc .
var ll : LocList .
var a a' : Addr .
var al al' : AddrList .
var con con' : Connection .
var from to : Addr .
var conl conl' : ConnectionList .
var routel : RouteList .

var id id' id'' : Id .
var idl idl' idl'' : IdList .

var type : PlanType .
var typel : PlanTypeList .

var bool bool' : Bool .
var str str' : String .
var int int' : Int .
var const : Const .
var var var' var'' : Var .
var cstr : Cstr .
var ncstr : NonCstr .

var ex ex' ex'' : Ex .
var exl exl' exl'' : ExList .

var nval nval' nval'' : NonVal .
var val val' val'' eval : Val .
var val0 val0' val0'' : Val .
var val1 val1' val1'' : Val .
var vall vall' vall'' : ValList .

vars pl pl' : PlanList .

---------------------------
--- Contexts (Expressions with Holes i.e. Metavariables)

sort Cx .
subsort Ex < Cx .

op ? : -> Cx .
op __ : Cx CxList -> Cx [ prec 21 gather (E e) ] .
op _;_ : Cx Cx -> Cx [ prec 30 gather (e E) ] .
op If_Then_Else_ : Cx Cx Cx -> Cx .
op Let`[_=_`]_ : IdList CxList Cx -> Cx [ prec 30 gather (& & E) ] .
op LetRec`[_=_`]_ : IdList CxList Cx -> Cx [ prec 30 gather (& & E) ] .
op Lam`[_:_`]_ : IdList PlanTypeList Cx -> Cx [ prec 30 gather (& & E) ] .
op Try_Handle`[_`]_ : Cx Id Cx -> Cx [ prec 30 gather (E & E) ] .
op Raise_ : Cx -> Cx .
op _:_ : Cx PlanType -> Cx .

var cx cx' cx'' cx''' : Cx .
var cxl cxl' cxl'' cxl''' : CxList .

---------------------------
--- Lists of Contexts

sort CxList .

subsort ExList < CxList .

subsort Cx < CxList .
op _`,_ : CxList CxList -> CxList 
          [ assoc id: empty-exl ] .


---------------------------
--- Object-Variable Substitution
--- (an instance of the CINNI substitution calculus
---  generalized to simultaneous substitutions)

sort Subst .

op [_:=_] : Id Ex -> Subst [ prec 30 gather (& &) ] .
op [_:=_] : IdList ExList -> Subst [ prec 30 gather (& &) ] .
op [shift_] : Id -> Subst [ prec 30 gather (&) ] .
op [lift__] : Id Subst -> Subst [ prec 30 gather (& &) ] .
op [lift__] : IdList Subst -> Subst [ prec 30 gather (& &) ] .
op __ : Subst Ex -> Ex [ prec 30 gather (E E) ] .
op __ : Subst ExList -> ExList [ prec 30 gather (E E) ] .

var S : Subst .
vars m : Nat .

eq  ([id := ex] (id{0})) = ex .
eq  ([id := ex] (id{s m})) = (id{m}) .
ceq ([id := ex] (id'{m})) = (id'{m}) if id =/= id' .

eq  ([shift id] (id{m})) = (id{s m}) .
ceq ([shift id] (id'{m})) = (id'{m}) if id =/= id' .

eq  ([lift id S] (id{0})) = (id{0}) .
eq  ([lift id S] (id{s m})) = [shift id] (S (id{m})) .
ceq ([lift id S] (id'{m})) = [shift id] (S (id'{m})) if id =/= id' .

eq  ([empty-idl := empty-exl] ex') = ex' .
ceq ([(id,idl) := (ex,exl)] ex') = 
    ([id := ex][idl := [shift id] exl] ex') if idl =/= empty-idl .

eq  ([lift empty-idl S] ex') = (S ex') .
ceq ([lift (id,idl) S] ex') = 
    ([lift idl [lift id S]] ex') if idl =/= empty-idl .

eq  (S const) = const .
eq  (S (ex exl')) = ((S ex) (S exl')) .
eq  (S (ex ; ex')) = ((S ex) ; (S ex')) .
eq  (S (If ex Then ex' Else ex'')) = 
    (If (S ex) Then (S ex') Else (S ex'')) .
eq  (S (Let [idl = exl] ex')) = 
    (Let [idl = (S exl)] ([lift idl S] ex')) .
eq  (S (LetRec [idl = exl] ex')) = 
    (LetRec [idl = ([lift idl S] exl)] ([lift idl S] ex')) .
eq  (S (Lam [idl : typel] ex)) = 
    (Lam [idl : typel] ([lift idl S] ex)) .
eq  (S (Try ex Handle [id] ex')) = 
    (Try (S ex) Handle [id] ([lift id S] ex')) .

eq  (S empty-exl) = empty-exl .
ceq (S (ex , exl')) = ((S ex) , (S exl')) if exl' =/= empty-exl .

---------------------------
--- Hole (Meta-Variable) Substitution
--- (standard textual substitution)


op  <`?`:=_>_ : Cx Cx -> Cx [ prec 10 ] .
op  <`?`:=_>_ : Cx CxList -> CxList [ prec 10 ] .

eq  < ? := cx > ? = cx .
eq  < ? := cx > const = const .
eq  < ? := cx > var = var .
eq  < ? := cx > (cx' cxl'') = 
    ((< ? := cx > cx') (< ? := cx > cxl'')) .
eq  < ? := cx > (cx' ; cx'') = 
    ((< ? := cx > cx') ; (< ? := cx > cx'')) .
eq  < ? := cx > (If cx' Then cx'' Else cx''') = 
    (If (< ? := cx > cx') 
     Then (< ? := cx > cx'') Else (< ? := cx > cx''')) .
eq  < ? := cx > (Let [idl = cxl'] cx'') = 
    (Let [idl = < ? := cx > cxl'] (< ? := cx > cx'')) .
eq  < ? := cx > (LetRec [idl = cxl'] cx'') = 
    (LetRec [idl = < ? := cx > cxl'] (< ? := cx > cx'')) .
eq  < ? := cx > (Lam [idl : typel] cx') = 
    (Lam [idl : typel] (< ? := cx > cx')) .
eq  < ? := cx > (Try cx' Handle [id] cx'') = 
    (Try (< ? := cx > cx')  Handle [id] (< ? := cx > cx'')) .
eq  < ? := cx > ( cx' : type) = 
    ( (< ? := cx > cx') : type ) .
eq  < ? := cx > empty-exl =  empty-exl .
ceq < ? := cx > (cx' , cxl'') = 
    ((< ? := cx > cx') , (< ? := cx > cxl'')) if cxl'' =/= empty-exl .

op  <<`?`:=_>>_ : Cx Cx -> Cx [ prec 10 ] .
op  <<`?`:=_>>_ : Cx CxList -> CxList [ prec 10 ] .


---------------------------
--- Reduction Machine State

sort RedState .

op  RedState : Cx Ex -> RedState .

var devs : AddrList .      --- network devices of a node
var nbrs : ConnectionList .  --- neighbors of a node
var rt   : RouteList . --- routing table

var fdest : Addr . --- final destination address of a packet
var dest : Addr .  --- intermediate destination address of a packet
var orign : Addr . --- originator address of a program/packet
var ariv : Addr .  --- arival device of a program
var rb : Int .  --- resource bound

---------------------------
--- Reduction Machine Rules
--- (no dynamic typechecking yet)

--- control 

rl  RedState(<< ? := cx >> cx', val) 
    =>  
    RedState(cx', < ? := val > cx)  .

rl  RedState(<< ? := cx >> cx', (Raise eval)) 
    =>  
    RedState(cx', < ? := (Raise eval) > cx)  .

---------------------------
--- let statements

--- control (evaluate from left to right)

rl  RedState(cx, Let [idl = (vall', nval', exl')] ex'') 
    => 
    RedState(<< ? := Let [idl = (vall', ?, exl')] ex'' >> cx, nval') .

--- reduction

rl  RedState(cx, Let [idl = vall'] ex'') 
    => 
    RedState(cx, [idl := vall'] ex'') .

---------------------------
--- letrec statements
--- (Assumes that all expressions on the lhs of = can be 
---  evaluated independently of each other, cf. letrec in Scheme.
---  Hence, the main use of letrec is to define 
---  (mutually) recursive functions.)

--- control (evaluate from left to right)

rl  RedState(cx, LetRec [idl = (vall', nval', exl')] ex'') 
    => 
    RedState(<< ? := LetRec [idl = (vall', ?, exl')] ex'' >> cx, nval') .

--- reduction

op  LetRec`[_=_`]_ : IdList ExList ExList -> Ex 
                     [ prec 30 gather (& & E) ] .
eq  (LetRec[idl = exl] empty-exl) = empty-exl .
ceq (LetRec[idl = exl] (ex',exl')) = 
    ((LetRec[idl = exl] ex'),(LetRec[idl = exl] exl')) 
    if exl' =/= empty-exl .

rl  RedState(cx, LetRec [idl = vall'] ex'') 
    => 
    RedState(cx, [idl := (LetRec [idl = vall'] vall')] ex'') .

---------------------------
--- function application 

--- control (evaluate arguments from left to right)

rl  RedState(cx, (nval exl')) 
    => 
    RedState(<< ? := (? exl') >> cx, nval) .

rl  RedState(cx, (val (vall', nval', exl'))) 
    => 
    RedState(<< ? := (val (vall', ?, exl')) >> cx, nval') .

--- reduction: beta

rl  RedState(cx, ((Lam [idl : typel] ex) vall)) 
    =>
    RedState(cx, [idl := vall] ex) .

--- reduction: equality

rl  RedState(cx, (Equal (val,val'))) 
    =>
    RedState(cx, (Bool (val == val'))) .

--- reduction: boolean ops

rl  RedState(cx, (Not (Bool bool))) 
    =>
    RedState(cx, (Bool (not bool))) .

rl  RedState(cx, (And ((Bool bool),(Bool bool')))) 
    =>
    RedState(cx, (Bool (bool and bool'))) .

rl  RedState(cx, (Or ((Bool bool),(Bool bool')))) 
    =>
    RedState(cx, (Bool (bool or bool'))) .

--- reduction: integer ops

rl  RedState(cx, (Plus ((Int int),(Int int')))) 
    =>
    RedState(cx, (Int _+_(int,int'))) .

rl  RedState(cx, (Minus ((Int int),(Int int')))) 
    =>
    RedState(cx, (Int _-_(int,int'))) .

rl  RedState(cx, (Mul ((Int int),(Int int')))) 
    =>
    RedState(cx, (Int _*_(int,int'))) .

crl RedState(cx, (Div ((Int int),(Int int')))) 
    =>
    RedState(cx, (Int (int quo int'))) if int' =/= 0 .

crl RedState(cx, (Div ((Int int),(Int int')))) 
    =>
    RedState(cx, (Raise DivByZero)) if int' == 0 .

--- reduction: pair ops

rl  RedState(cx, (Fst (Pair (val,val')))) 
    =>
    RedState(cx, val) .

rl  RedState(cx, (Snd (Pair (val,val')))) 
    =>
    RedState(cx, val') .

--- reduction: list ops

rl  RedState(cx, (Hd (Cons (val,val')))) 
    =>
    RedState(cx, val) .

rl  RedState(cx, (Tl (Cons (val,val')))) 
    =>
    RedState(cx, val') .

op  length : PlanList  -> PlanInt .
eq  length(Nil) = (Int 0) .
ceq length(Cons (val, pl) ) = (Int _+_(1,int) )
    if (Int int) := length(pl) .

rl  RedState(cx, (Length pl)) 
    =>
    RedState(cx, length(pl)) .

op  member : Val PlanList  -> PlanBool .
eq  member(val,Nil) = (Bool false) .
eq  member(val', Cons (val, pl) ) =
     ( if (val == val') then (Bool true) else member(val',pl) fi ) .

rl  RedState(cx, (Member (val, pl))) 
    =>
    RedState(cx, member(val,pl)) .

op  append : PlanList PlanList -> PlanList .
eq  append(Nil, pl') = pl' .
eq  append(Cons (val, pl), pl') = Cons (val, append(pl, pl')) .

rl  RedState(cx, (Append (pl,pl'))) 
    =>
    RedState(cx, append(pl,pl')) .

op  reverse : PlanList PlanList -> PlanList .
eq  reverse(Nil,pl') = pl' .
eq  reverse(Cons (val, pl), pl' ) = reverse(pl, Cons(val, pl')) .

rl  RedState(cx, (Reverse pl)) 
    =>
    RedState(cx, reverse(pl,Nil)) .

rl  RedState(cx, (Foldr (val,Nil,val''))) 
    =>
    RedState(cx, val'') .

crl RedState(cx, (Foldr (val,(Cons (val0',val1')),val''))) 
    =>
    RedState(cx, (val (val0', (Foldr (val,val1',val''))))) 
    if (Cons (val0',val1')) : PlanList .

rl  RedState(cx, (Foldl (val,val',Nil))) 
    =>
    RedState(cx, val') .

crl RedState(cx, (Foldl (val,val',(Cons (val0'',val1''))))) 
    =>
    RedState(cx, (Foldl (val,(val (val',val0'')),val1'')))
    if (Cons (val0'',val1'')) : PlanList .

---------------------------
--- if-then-else statement

--- control (evaluate condition)

rl  RedState(cx, (If nval Then ex' Else ex'')) 
    => 
    RedState(<< ? := (If ? Then ex' Else ex'') >> cx, nval) .

--- reduction

rl  RedState(cx, (If (Bool true) Then ex' Else ex'')) 
    => 
    RedState(cx, ex') .

rl  RedState(cx, (If (Bool false) Then ex' Else ex'')) 
    => 
    RedState(cx, ex'') .

---------------------------
--- sequential evaluation

--- control (evaluate on the left)

rl  RedState(cx, (nval ; ex')) 
    => 
    RedState(<< ? := (? ; ex')>> cx, nval) .

--- reduction

rl  RedState(cx, (val ; ex')) 
    => 
    RedState(cx, ex') .

---------------------------
--- type assertions

--- control

rl  RedState(cx, (nval : type)) 
    =>
    RedState(<< ? := (? : type) >> cx, nval) .  

--- reduction

rl  RedState(cx, (val : type)) 
    =>
    RedState(cx, val) .  

---------------------------
--- exception handling

--- control

rl  RedState(cx, (Try nval Handle [id] ex')) 
    =>
    RedState(<< ? :=  (Try ? Handle [id] ex') >> cx, nval) .

--- reduction (non error case)

rl  RedState(cx, (Try val Handle [id] ex')) 
    =>
    RedState(cx, val) .

--- reduction (error case)

rl  RedState(cx, (Try (Raise eval) Handle [id] ex'))
    =>
    RedState(cx, [id := eval] ex') .

rl  RedState(cx, ((Raise eval) exl))
    =>
    RedState(cx, (Raise eval)) .

rl  RedState(cx, (val (vall,(Raise eval),exl)))
    =>
    RedState(cx, (Raise eval)) .

rl  RedState(cx, (Raise eval) ; ex)
    =>
    RedState(cx, (Raise eval)) .

rl  RedState(cx, (If (Raise eval) Then ex Else ex'))
    =>
    RedState(cx, (Raise eval)) .

rl  RedState(cx, ((Raise eval) : type))
    =>
    RedState(cx, (Raise eval)) .


--- processes, packets and configurations

sort Node . --- network node

op Node : Loc AddrList ConnectionList RouteList -> Node .

--- contains: physical location (Loc), 
---           network devices (AddrList),
---           connections to neighbors (ConnectionList),
---           routing table (RouteList)

sort Process .  --- process being executed on a node

op Process : Loc Addr Addr Int Int RedState -> Process .

--- contains: physical location (Loc),
---           originator address (Addr)
---           arival device of program (Addr),
---           session key (Int)
---           resource bound (Int),
---           reduction machine state (RedState)

sort Packet . --- packet in transit between nodes

op Packet : Addr Addr Addr Int Int Const Val ValList -> Packet .

--- contains: final destination address (Addr),
---           immediate destination address (Addr),
---           originator address (Addr),
---           session key (Int)
---           resource bound (Int),
---           routing function (Const),
---           chunk, i.e. function (Ex) with arguments (ExList)

sort FreshKey .

op FreshKey : Int -> FreshKey .

--- contains: next fresh session key (Int)

var ssn key key' : Int .

sort DataItem .

op DataItem : String Int Val Int -> DataItem .

sort DataItemList .
subsort DataItem < DataItemList .
op empty-dil : -> DataItemList .
op _`,_ : DataItemList DataItemList -> DataItemList 
          [ assoc id: empty-dil ] .

var dil dil' : DataItemList .

sort Data . --- a piece of data

op  Data : Loc DataItemList -> Data .

--- contains: physical location (Loc)
---           access string (String)
---           session key (Int)
---           data value (Val)
---           time to live (Int)

sort Configuration .
subsort Node < Configuration .
subsort Process < Configuration .
subsort Packet < Configuration .
subsort FreshKey < Configuration .
subsort Data < Configuration .
op empty-conf : -> Configuration .
op __ : Configuration Configuration -> Configuration 
        [assoc comm id: empty-conf] .

---------------------------
--- normal termination

rl  Process(l, orign, ariv, ssn, rb,   
      RedState(?, val)) 
    =>
    empty-conf .

rl  Process(l, orign, ariv, ssn, rb,   
      RedState(?, (Raise eval))) 
    =>
    empty-conf .

---------------------------
--- local execution of chunks 

crl Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (Eval (Chunk (val,vall))))) 
    =>
    Process(l, orign, ariv, ssn, _-_(rb,1),   
      RedState(cx, (val vall))) 
    if rb > 0 .

crl Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (Eval (Chunk (val,vall))))) 
    =>
    Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (Raise NotEnoughRB))) 
    if not(rb > 0) .

---------------------------
--- remote execution of chunks (emitting packet)

var dev : Addr .  --- outgoing network device

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
    RedState(cx, (OnNeighbor ((Chunk (val,vall)),
                    (Addr dest),(Int int),(Addr dev))))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, (rb - int),   
      RedState(cx, Dummy))
    Packet(dest, dest, orign, ssn, (int - 1), DefaultRoute, 
           val, vall)
    if connection(devs,nbrs,(dev >> dest)) and (rb >= int) and (int > 0) .

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
    RedState(cx, (OnNeighbor ((Chunk (val,vall)),
                    (Addr dest),(Int int),(Addr dev))))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (Raise HostNotLocal)))
    if not(connection(devs,nbrs,(dev >> dest))) .

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
    RedState(cx, (OnNeighbor ((Chunk (val,vall)),
                    (Addr dest),(Int int),(Addr dev))))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (Raise NotEnoughRB)))
    if not((rb >= int) and (int > 0)) .

var rf : Const .  --- routing function argument

rl  RedState(cx, (OnRemote ((Chunk (val,vall)),
                    (Addr dest),(Int int),rf))) 
    =>
    RedState(cx, (OnRemote' ((Chunk (val,vall)),
                    (Addr dest),(Int int),rf,
                    (Fst (rf (Addr dest))),(Snd (rf (Addr dest)))))) .

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (OnRemote' ((Chunk (val,vall)),
                      (Addr fdest),(Int int),rf,
                      (Addr dest),(Addr dev))))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, _-_(rb,int),   
      RedState(cx, Dummy))
    Packet(dest, fdest, orign, ssn, _-_(int,1), rf, val, vall)
    if connection(devs,nbrs,(dev >> dest)) and (rb >= int) and (int > 0) .

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (OnRemote' ((Chunk (val,vall)),
                      (Addr fdest),(Int int),rf,
                      (Addr dest),(Addr dev))))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (Raise HostNotLocal)))
    if not(connection(devs,nbrs,(dev >> dest))) .

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (OnRemote' ((Chunk (val,vall)),
                      (Addr fdest),(Int int),rf,
                      (Addr dest),(Addr dev))))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,   
      RedState(cx, (Raise NotEnoughRB)))
    if not((rb >= int) and (int > 0)) .

---------------------------
--- receiving packet 

crl Node(l,devs,nbrs,rt)
    Packet(dest, fdest, orign, ssn, rb, rf, val, vall) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, dest, ssn, rb,  RedState(?,(val vall))) 
    if (dest == fdest) and contains(devs,dest) .

crl Node(l,devs,nbrs,rt)
    Packet(dest, fdest, orign, ssn, rb, rf, val, vall) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, dest, ssn, rb,  
      RedState(?, (OnRemote ((Chunk (val,vall)),
                      (Addr fdest),(Int rb),rf))))
    if (dest =/= fdest) and contains(devs,dest) .

---------------------------
--- service: GetRB (get resource bound)

rl  Process(l, orign, ariv, ssn, rb,  
      RedState(cx, (GetRB empty-exl))) 
    =>
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, (Int rb))) .

---------------------------
--- service: GetSource (get source address)

rl  Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (GetSource empty-exl))) 
    =>
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (Addr orign))) .

---------------------------
--- service: GetSrcDev (get arrival device)

rl  Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (GetSrcDev empty-exl))) 
    =>
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (Addr ariv))) .

---------------------------
--- service: ThisHostIs

rl  Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (ThisHostIs (Addr a)))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (Bool (contains(devs,a))))) .

---------------------------
--- service: ThisHost

op cast : AddrList -> Ex .
eq cast(empty-al) = Nil .
eq cast(a,al) = (Cons ((Addr a),cast(al))) .

rl  Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (ThisHost empty-exl))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, cast(devs))) .

---------------------------
--- service: GetNeighbors

op cast : Connection -> Ex .
eq cast(a >> a') = (Pair ((Addr a'),(Addr a))) .

op castl : ConnectionList -> Ex .
eq castl(empty-conl) = Nil .
eq castl((a >> a'),conl) = (Cons (cast(a >> a'),castl(conl))) .

rl  Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (GetNeighbors empty-exl))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, castl(nbrs))) .

---------------------------
--- service: GetDevToHost

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (GetDevToHost (Addr a)))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, (Addr devtohost(nbrs,a)))) 
    if contains(nbrs,a) .

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (GetDevToHost (Addr a)))) 
    =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, (Raise HostNotLocal))) 
    if not(contains(nbrs,a)) .

---------------------------
--- service: DefaultRoute

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (DefaultRoute (Addr a)))) =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, cast(defaultroute(devs,rt,a)))) 
    if defaultroutepresent(devs,rt,a) .

crl Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (DefaultRoute (Addr a)))) =>
    Node(l,devs,nbrs,rt)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, (Raise NoRouteEntry)))
    if not(defaultroutepresent(devs,rt,a)) .

---------------------------
--- service: GenerateKey

rl  FreshKey(int)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (GenerateKey empty-exl))) 
    =>
    FreshKey(int + 1)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, (Key int))) .

---------------------------
--- service: Exists

var ttl ttl' : Int .

op  contains : DataItemList String Int -> Bool .

eq  contains(empty-dil,str,key) = false .
eq  contains((DataItem(str,key,val,ttl),dil),str,key) = true .
ceq contains((DataItem(str,key,val,ttl),dil),str',key') = 
    contains(dil,str',key') if str =/= str' or key =/= key' .

rl  Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (Exists ((String str),(Key key))))) 
    =>
    Data(l,dil)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, (Bool (contains(dil,str,key))))) .

---------------------------
--- service: Get

op  get : DataItemList String Int -> Val .

eq  get((DataItem(str,key,val,ttl),dil),str,key) = val .
ceq get((DataItem(str,key,val,ttl),dil),str',key') = 
    get(dil,str',key') if str =/= str' or key =/= key' .

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (Get ((String str),(Key key))))) 
    =>
    Data(l,dil)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, get(dil,str,key)))
    if contains(dil,str,key) .

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (Get ((String str),(Key key))))) 
    =>
    Data(l,dil)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, (Raise NotFound)))
    if not(contains(dil,str,key)) .

---------------------------
--- service: Delete

op delete : DataItemList String Int -> DataItemList .

eq  delete(empty-dil,str,key) = empty-dil .
eq  delete((DataItem(str,key,val,ttl),dil),str,key) =
    delete(dil,str,key) . 
ceq delete((DataItem(str,key,val,ttl),dil),str',key') = 
    delete(dil,str',key') if str =/= str' or key =/= key' .

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (Delete ((String str),(Key key))))) 
    =>
    Data(l,delete(dil,str,key))
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, Dummy))
    if contains(dil,str,key) .

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (Delete ((String str),(Key key))))) 
    =>
    Data(l,dil)
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, (Raise NotFound)))
    if not(contains(dil,str,key)) .

---------------------------
--- service: Put

op  put : DataItemList String Int Val Int -> DataItemList .

eq  put(dil,str,key,val,ttl) = 
    (delete(dil,str,key),DataItem(str,key,val,ttl)) .

rl  Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (Put ((String str),(Key key),val,(Int ttl))))) 
    =>
    Data(l,put(dil,str,key,val,ttl))
    Process(l, orign, ariv, ssn, rb,  
      RedState(cx, Dummy)) .

---------------------------
--- service: SetLT

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (SetLT ((String str),(Key key),(Int int'),(Int ttl))))) 
    =>
    Data(l,put(dil,str,key,(Int int'),ttl))
    Process(l, orign, ariv, ssn, rb,
      RedState(cx, (Bool true)))
    if not(contains(dil,str,key)) .

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (SetLT ((String str),(Key key),(Int int'),(Int ttl))))) 
    =>
    Data(l,put(dil,str,key,(Int int'),ttl))
    Process(l, orign, ariv, ssn, rb,
      RedState(cx, (Bool true))) 
    if contains(dil,str,key) /\ (Int int) := get(dil,str,key) /\ int' < int .

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (SetLT ((String str),(Key key),(Int int'),(Int ttl))))) 
    =>
    Data(l,dil)
    Process(l, orign, ariv, ssn, rb,
      RedState(cx, (Bool false))) 
    if contains(dil,str,key) /\ (Int int) := get(dil,str,key) /\ int' >= int .

---------------------------
--- service: SetGT

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (SetGT ((String str),(Key key),(Int int'),(Int ttl))))) 
    =>
    Data(l,put(dil,str,key,(Int int'),ttl))
    Process(l, orign, ariv, ssn, rb,
      RedState(cx, (Bool true)))
    if not(contains(dil,str,key)) .

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (SetGT ((String str),(Key key),(Int int'),(Int ttl))))) 
    =>
    Data(l,put(dil,str,key,(Int int'),ttl))
    Process(l, orign, ariv, ssn, rb,
      RedState(cx, (Bool true))) 
    if contains(dil,str,key) /\ (Int int) := get(dil,str,key) /\ int' > int .

crl Data(l,dil)
    Process(l, orign, ariv, ssn, rb, 
      RedState(cx, (SetGT ((String str),(Key key),(Int int'),(Int ttl))))) 
    =>
    Data(l,dil)
    Process(l, orign, ariv, ssn, rb,
      RedState(cx, (Bool false))) 
    if contains(dil,str,key) /\ (Int int) := get(dil,str,key) /\ int' <= int .

endm