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. 
--- ip send message has the form ip-send-req/ip-send-ack. 
--- 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. So our
--- ip-send-req  is equivalent to a send call and the ack the same as the return from
--- such a call. We had to make sure the model blocks until the message is out in the soup.
--- A message is reveived from the soup and delivered to a consuming rule. 
 
--- Note that the forward operator forwards a message along using an ip-send-req so it
--- must process the reception of the ack. 
--- ----------------------------------------------------------------------------------
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-req : Agent Node Message -> State .
op ip-send-ack : Agent Node  -> State .

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

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

op ip-forward-send-expect-ack : Node Addr 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-req(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))
    ip-send-ack(agent,node) 
    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-req(gwagent(node), node, ip(src,dest,message)) 
    ip-forward-send-expect-ack(node,src,dest,message)
    if dest =/= rinterface .

rl  [ipforward-expect-ack]:
    ip-forward-send-expect-ack(node,src,dest,message)
    ip-send-ack(gwagent(node),node) =>
    gw(node) .


   
endm