/* ========================================================================
A COMPOSITIONAL NETWORK MODEL IN ALLOY: FORWARDING AND REACHABILITY
   The purpose of this model is to study routing and forwarding, and their
effects on reachability.
======================================================================== */
/* ------------------------------------------------------------------------
BASIC TYPES
------------------------------------------------------------------------ */

sig Node, Hash { }

one sig Self { }

sig Link { transmitter, acquirer: Node } 

sig Header { source, destination: Node, hash: Hash }

/* ------------------------------------------------------------------------
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 NetworkState { 
-- necessary state
   nodes: set Node,
   links: set Link,
   forwarding: Header -> (links + Self) -> links,
-- derived state
   allHops: Header -> (links + Self) -> links, 
   reaches: Header -> nodes -> nodes,
   receives: Header -> nodes -> nodes,
-- extra state for expressing requirements
   positiveReach: nodes -> nodes,
   negativeReach: nodes -> nodes
}  {
-- The endpoints of a link must be distinct member nodes.
   all k: links | 
      (k.transmitter + k.acquirer) in nodes && k.transmitter != k.acquirer

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

-- Routing is deterministic, taking the hash into account for multipath
-- routing.
   all h: Header, k: (links + Self) | lone k.(h.forwarding)

-- Derivation allHops.
   all h: Header | h.allHops = ^(h.forwarding)

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

-- Nodes absorb packets destined for them.
   all h: Header, k: links, n: nodes | 
      h.destination = n && k.transmitter = n => no h.forwarding.k 

-- Derivation of receives.  If (h -> n0 -> n1) is in receives, then if n0
-- sends a packet with header h, it will be received at n1.
   receives = { h: Header, n0, n1: nodes |  
      (h -> n0 -> n1) in reaches && h.destination = n1 }
}

/* ------------------------------------------------------------------------
POSSIBLE NETWORK PROPERTIES
------------------------------------------------------------------------ */

pred Headers_are_sent_authentic [w: NetworkState] {
   all h: Header, k: w.links, n: w.nodes | 
      (h -> Self -> k) in (w.forwarding) && k.transmitter = n
   => h.source = n                                          }

pred No_routing_loops [w: NetworkState] {
   all h: Header | no k: w.links | (k -> k) in h.(w.allHops) }

pred Positive_reach_requirements_satisfied [w: NetworkState] {
   all n0, n1: w.nodes | 
      (n0 -> n1) in w.positiveReach => (n0 -> n1) in Header.(w.reaches) }

pred Negative_reach_requirements_satisfied [w: NetworkState] {
   all n0, n1: w.nodes | 
      (n0 -> n1) in w.negativeReach => (n0 -> n1) ! in Header.(w.reaches) }

pred Multipath_consistent_reach [w: NetworkState] {
   all h0, h1: Header |
   (  h0.source = h1.source && h0.destination = h1.destination 
   && h0.hash != h1.hash
   ) => h0.(w.reaches) = h1.(w.reaches)                      }

pred Multipath_consistent_receives [w: NetworkState] {
   all h0, h1: Header |
   (  h0.source = h1.source && h0.destination = h1.destination 
   && h0.hash != h1.hash
   ) => h0.(w.receives) = h1.(w.receives)                    }

/* ------------------------------------------------------------------------
VALIDATION AND VERIFICATION
   Even if the theorems seem trivial, they help to validate the model.
------------------------------------------------------------------------ */

pred Good_network_exists [w: NetworkState] {
      some w.receives && some w.positiveReach && some w.negativeReach
      Headers_are_sent_authentic [w]
      No_routing_loops [w]
      Positive_reach_requirements_satisfied [w]
      Negative_reach_requirements_satisfied [w]  }
run Good_network_exists for 1 but 2 Node, 1 Link, 1 Header, 1 Hash    -- OK
run Good_network_exists for 1 but 4 Node, 4 Link, 4 Header, 2 Hash    -- OK

assert Positive_and_negative_requirements_cannot_overlap {
   all w: NetworkState |
      Positive_reach_requirements_satisfied [w] 
   && Negative_reach_requirements_satisfied [w] 
   => no (w.positiveReach & w.negativeReach)  }
check Positive_and_negative_requirements_cannot_overlap for 1 but 
   5 Node, 9 Link, 5 Header, 2 Hash                                   -- OK

assert Multipath_consistent_reach_implies_consistent_receives {
   all w: NetworkState |
      Multipath_consistent_reach [w] => Multipath_consistent_receives [w] }
check Multipath_consistent_reach_implies_consistent_receives for 1 but 
   5 Node, 9 Link, 5 Header, 2 Hash                                   -- OK

pred Multipath_consistent_receives_not_consistent_reach [w: NetworkState] {
   Multipath_consistent_receives [w] && ! Multipath_consistent_reach [w]  }
run Multipath_consistent_receives_not_consistent_reach for 1 but 
   3 Node, 3 Link, 2 Header, 2 Hash                                   -- OK

/* ------------------------------------------------------------------------
NetworkState, Node, Link, Header, Hash
------------------------------------------------------------------------ */
/* ------------------------------------------------------------------------
Simplifications for modeling and analysis:
 * There is a one-to-one correspondence between nodes and names.
 * No distinction is made between a node and its name.
 * There is a one-to-one correspondence between links and unique 
   identifiers.
 * No distinction is made between a link and its identifier.
 * The network state is global--we say nothing about where it is stored.
 * Forwarding tables do not have header patterns.
 * There are no node or link failures.
------------------------------------------------------------------------ */