--------------------------  plan-network.m  -----------------------------------
--- Date: Sat, 25 Aug 2001 00:44:24 -0700
--- From: Mark-Oliver Stehr <stehr@csl.sri.com>
--- requires PLAN-ADDR defined in plan-syntax.m


fmod PLAN-NETWORK is

protecting BOOL .
protecting STRING .
protecting PLAN-ADDR .

---------------------------
--- More Network Sorts

sort Loc .   --- physical locations (i.e. hosts)
op loc : String -> Loc .

sort LocList .
subsort Loc < LocList .
op empty-ll : -> LocList .
op _`,_ : LocList LocList -> LocList 
          [ assoc id: empty-ll ] .

sort AddrList .
subsort Addr < AddrList .
op empty-al : -> AddrList .
op _`,_ : AddrList AddrList -> AddrList 
          [ assoc id: empty-al ] .

sort Connection .
op _>>_ : Addr Addr -> Connection . --- network connection

sort ConnectionList .
subsort Connection < ConnectionList .
op empty-conl : -> ConnectionList .
op _`,_ : ConnectionList ConnectionList -> ConnectionList 
          [ assoc id: empty-conl ] .

sort Route .
op _via_ : Addr Connection -> Route . --- network route from node viewpoint

sort RouteList .
subsort Route < RouteList .
op empty-rl : -> RouteList .
op _`,_ : RouteList RouteList -> RouteList 
          [ assoc id: empty-rl ] .

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 .

op  contains : AddrList Addr -> Bool .
eq  contains(empty-al,a') = false . 
ceq contains((a,al),a') = true if a == a' .
ceq contains((a,al),a') = contains(al,a') if a =/= a' . 

op  remove : AddrList Addr -> AddrList .
eq  remove(empty-al,a') = empty-al .
ceq remove((a,al),a') = remove(al,a') if a == a' .
ceq remove((a,al),a') = (a,remove(al,a')) if a =/= a' .
 
op  contains : ConnectionList Connection -> Bool .
eq  contains(empty-conl,con') = false . 
ceq contains((con,conl),con') = true if con == con' .
ceq contains((con,conl),con') = contains(conl,con') if con =/= con' .

op  contains : ConnectionList Addr  -> Bool .
eq  contains(empty-conl,a') = false . 
ceq contains(((from >> to),conl),a') = true if to == a' .
ceq contains(((from >> to),conl),a') = contains(conl,a') if to =/= a' .

op  devtohost : ConnectionList Addr -> Addr .
ceq devtohost(((from >> to),conl),a') = from if to == a' .
ceq devtohost(((from >> to),conl),a') = devtohost(conl,a') if to =/= a' .

op  connection : AddrList ConnectionList Connection -> Bool .
eq  connection(al,conl,(from >> to)) = 
      contains(al,from) and (contains(conl,(from >> to)) or (from == to)) .

op  defaultroute : RouteList Addr -> Connection .
ceq defaultroute(((a via con),routel),a') = con if a == a' .
ceq defaultroute(((a via con),routel),a') = defaultroute(routel,a') if a =/= a' .

op  defaultroutepresent : RouteList Addr -> Bool .
eq  defaultroutepresent(empty-rl,a') = false .
ceq defaultroutepresent(((a via con),routel),a') = true if a == a' .
ceq defaultroutepresent(((a via con),routel),a') = defaultroutepresent(routel,a') if a =/= a' .

op  defaultroute : AddrList RouteList Addr -> Connection .
eq  defaultroute(al,routel,a) = 
      if contains(al,a) then (a >> a) else defaultroute(routel,a) fi .

op  defaultroutepresent : AddrList RouteList Addr -> Bool .
eq  defaultroutepresent(al,routel,a) = 
      if contains(al,a) then true else defaultroutepresent(routel,a) fi .

endfm