mod IP is

protecting COMMON .

--- -----------------------------------------------------------------------------------
--- This module provides an abstract model of the IP level. 
--- The  routing table is defined here as a list of routes bound to a node. 
--- In actuality, a call to an ip send doesn't return until the message is on the
--- wire. To prevent messy concurrency we had to model this behavior.  Thus this
--- version has some concurrency issues.
 
--- ----------------------------------------------------------------------------------
including MESSAGE .
including IP-MESSAGE .
protecting ROUTING-TABLE .

including STATE .

var node node' : Node .
var addr addr' : Addr .
var src dest : Addr .
var addrset : AddrSet .
var message message' : Message .
var interfaces interfaces' : AddrSet .
var rinterface : Addr .

--- ip interface

op ip-send : Agent Node Message -> State .

op ip-received : Node Addr Message -> State .

op ip-delivered : Node Addr Message -> State .

op ip-forward-term : Node Addr Addr Message -> State .

--- ip layer state

op routetab : Node RouteList -> State . --- routing table

------------------------------- IP -------------------------------------

--- node capabilities

op host : Node -> State .  --- node has ip host capabilities 
op gw : Node -> State .    --- node has additionally ip gateway capabilities

var subnet : AddrSet .
var routetab : RouteList .
var nexthop : Addr .

var agent : Agent .



--- outgoing ip traffic 

crl [ip-receive]:
    subnet(subnet)
    ip-send(agent,node,ip(src,dest,message))
    routetab(node,routetab)
    interfaces(node',interfaces') =>
    subnet(subnet)
    routetab(node,routetab)
    interfaces(node',interfaces') 
    ip-received(node',nexthop(routetab,dest),ip(src,dest,message))
    if contains(routetab,dest) and
       contains(interfaces',nexthop(routetab,dest)) and 
       contains(subnet,sinterface(routetab,dest))   and
       contains(subnet,nexthop(routetab,dest)) .

crl [ip-deliver]:
    host(node)
    ip-received(node, rinterface, ip(src,dest,message)) =>
    host(node)
    ip-delivered(node, rinterface, ip(src,dest,message))
    if dest == rinterface .

--- forwarding incoming ip traffic

op gwagent : Node -> Agent . --- each node has a forwarding gw agent running represented by gw(node)

crl [ip-forward]:
    gw(node)
    ip-received(node, rinterface, ip(src,dest,message)) =>
    ip-send(gwagent(node), node, ip(src,dest,message)) 
    gw(node)
    if dest =/= rinterface .

endm