/* ========================================================================
A COMPOSITIONAL NETWORK MODEL IN ALLOY
======================================================================== */
/* ------------------------------------------------------------------------
BASIC TYPES
------------------------------------------------------------------------ */

sig Node { }

one sig Self { }

sig Link { transmitter, receiver: Node } 

sig Header { sender, acceptor: Node }

fact Headers_are_distinct { 
   all disj h0, h1: Header | 
      (h0.sender != h1.sender || h0.acceptor != h1.acceptor) }

/* ------------------------------------------------------------------------
NETWORK STATE
   Functional Semantics:
      If a packet with header h is acquired at node n on link i and...
   ...there is a single forwarding tuple (n->h->i->o), and o has not
      failed, then forward the packet on link o;
   ...there are two or more such tuples, then choose one and forward the
      message on its link o;
   ...there is no such tuple, then do not forward the message.
   Similar rules apply if the packet is sent by node n and the tuple 
   pattern is (n->h->Self->o).
------------------------------------------------------------------------ */

sig Network { 
-- necessary state
   nodes: set Node,
   links: set Link,
   forwarding: Header -> (links + Self) -> links,      -- inlink -> outlink
   routers: set nodes,
-- derived state 
   nodePaths: Header -> nodes -> nodes,
   reaches: Header -> nodes -> nodes,
-- extra state for expressing requirements
   headers: set Header,  -- the session in every header in this set should
                         -- be implemented by forwarding
   firstMbox: headers -> lone (nodes - routers),
       -- all packets in this session should go through the first middlebox
   secondMbox: headers -> lone (nodes - routers)
                    -- all packets in this session should go through the 
                    -- middlebox, after they go through the first middlebox
}  {
-- The endpoints of a link must be distinct member nodes.
   all k: links | 
      (k.transmitter + k.receiver) in nodes && k.transmitter != k.receiver

-- The endpoints of a session must be distinct member nodes.
   all h: Header | 
      (h.sender + h.acceptor) in nodes && h.sender != h.acceptor
 
-- Headers sent are authentic.
   all h: Header, k: links, n: nodes | 
      (h -> Self -> k) in forwarding && k.transmitter = n => h.sender = n 

-- Forwarding is performed by a particular node.
   all k0, k1: links | (k0 -> k1) in Header.forwarding 
   => (some n: nodes | n = k0.receiver && n = k1.transmitter )

-- Forwarding is deterministic.
   all h: Header, k: (links + Self) | lone k.(h.forwarding)

-- There are no link-based routing loops.
   all h: Header | no k: links | (k -> k) in ^(h.forwarding)

-- There are no orphan forwarding rules, which make paths look possible 
-- that actually are not.
   all h: headers, k0: links + Self, k1: links |
      (h -> k0 -> k1) in forwarding
   => (k0 = Self || (some k: links + Self | (h -> k -> k0) in forwarding) )

-- Nodes absorb messages meant for them.
   all h: Header, k: links, n: nodes | 
      h.acceptor = n && k.transmitter = n => no h.forwarding.k

-- Derivation of nodePaths. 
   all h: Header | h.nodePaths = { n0, n1: nodes | 
      some k0, k1: links | 
         (k0 -> k1) in ^(h.forwarding) && 
         k0.receiver = n0 && k1.receiver = n1    }

-- Derivation of reaches.  If (h -> n0 -> n1) is in reaches, then if n0
-- sends a packet with header h, it will reach n1.
   reaches = { h: Header, n0, n1: nodes | some k0, k1: links |
      (h -> Self -> k0) in forwarding && k0.transmitter = n0 &&
      (Self -> k1) in ^(h.forwarding) && k1.receiver = n1     }

-- Middleboxes are not session endpoints.
   all h: headers | 
      h in firstMbox.nodes
   => h.sender != h.firstMbox && h.acceptor != h.firstMbox
   all h: headers | 
      h in secondMbox.nodes 
   => h.sender != h.secondMbox && h.acceptor != h.secondMbox

-- There cannot be a second middlebox requirement unless there is a first.
   secondMbox.nodes in firstMbox.nodes

-- First and second middleboxes for a header cannot be the same.
   no (firstMbox & secondMbox)
}

/* ------------------------------------------------------------------------
OPTIONAL PROPERTIES
------------------------------------------------------------------------ */

pred Routed_network [w: Network] {
-- Network endpoints (not routers) have no more than one in [out] link.
   all n: Node - w.routers |
      (lone k: w.links | k.transmitter = n) 
   && (lone k: w.links | k.receiver = n)  }

pred Peer_network [w: Network] {
-- There are no node loops in routing.
   all h: w.headers | no (iden & h.(w.nodePaths)) }

/* ------------------------------------------------------------------------
SATISFYING THE REQUIREMENTS
------------------------------------------------------------------------ */

pred Forwarding_requirements_satisfied [w: Network] {
   all h: w.headers |
      (h.sender -> h.acceptor) in h.(w.reaches) }

pred First_middlebox_requirements_satisfied [w: Network] {
   all h: w.headers |
      h in w.firstMbox.Node 
  => (h.sender -> h.(w.firstMbox)) in h.(w.reaches) }

pred Second_middlebox_requirements_satisfied [w: Network] {
   all h: w.headers |
      h in w.secondMbox.Node
   =>   (h.sender -> h.(w.secondMbox)) in h.(w.reaches) 
     && (h.(w.firstMbox) -> h.(w.secondMbox)) in h.(w.nodePaths)  }

/* ------------------------------------------------------------------------
VALIDATION AND VERIFICATION
------------------------------------------------------------------------ */

pred Good_routed_network_exists [w: Network] {
   some w.headers && some w.firstMbox && some w.secondMbox
   Routed_network [w]
   Forwarding_requirements_satisfied [w]
   First_middlebox_requirements_satisfied [w]
   Second_middlebox_requirements_satisfied [w]
}
run Good_routed_network_exists for 4 but 1 Network

assert Middlebox_ordering_makes_sense_in_routed_network {
   all w: Network, h: w.headers, m1, m2: w.nodes |
      (h -> m1) in w.firstMbox && (h -> m2) in w.secondMbox
   && Routed_network [w]
   && Forwarding_requirements_satisfied [w]
   && First_middlebox_requirements_satisfied [w]
   && Second_middlebox_requirements_satisfied [w]
   => (h.(w.secondMbox) -> h.(w.firstMbox)) ! in h.(w.nodePaths)  }
check Middlebox_ordering_makes_sense_in_routed_network for 4 but 1 Network 
check Middlebox_ordering_makes_sense_in_routed_network for 8 but 1 Network 

pred Good_peer_network_exists [w: Network] {
   some w.headers && some w.firstMbox && some w.secondMbox
   Peer_network [w]
   Forwarding_requirements_satisfied [w]
   First_middlebox_requirements_satisfied [w]
   Second_middlebox_requirements_satisfied [w]
}
run Good_peer_network_exists for 4 but 1 Network

assert Middlebox_ordering_makes_sense_in_peer_network {
   all w: Network, h: w.headers, m1, m2: w.nodes |
      (h -> m1) in w.firstMbox && (h -> m2) in w.secondMbox
   && Peer_network [w]
   && Forwarding_requirements_satisfied [w]
   && First_middlebox_requirements_satisfied [w]
   && Second_middlebox_requirements_satisfied [w]
   => (h.(w.secondMbox) -> h.(w.firstMbox)) ! in h.(w.nodePaths)  }
check Middlebox_ordering_makes_sense_in_peer_network for 4 but 1 Network 
check Middlebox_ordering_makes_sense_in_peer_network for 8 but 1 Network 

/* ------------------------------------------------------------------------
Network, Node, Link, Header, Session
------------------------------------------------------------------------ */