/* ======================================================================== 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 -- derived state nodeHops: 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, -- all packets in this session should -- go through the node secondMbox: headers -> lone nodes, -- all packets in this session should -- go through the node, 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 routing loops. all h: Header | no k: links | (k -> k) in ^(h.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 nodeHops. Just as the forwarding relation contains -- single hops from link to link, nodeHops contains single hops from node -- to node. nodeHops = { h: Header, disj n0, n1: nodes | some k0: links + Self, k1: links | ( (h -> k0 -> k1) in forwarding && n0 = k1.transmitter && n1 = k1.receiver ) } -- Derivation of reaches. If (h -> n0 -> n1) is in reaches, then if n0 -- sends or forwards a packet with header h, it will reach n1. all h: Header | h.reaches = ^(h.nodeHops) -- 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 } /* ------------------------------------------------------------------------ FORWARDING AND REACHABILITY PROPERTIES ------------------------------------------------------------------------ */ pred Forwarding_requirements_satisfied [w: Network] { all h: w.headers | (h.sender -> h.acceptor) in h.(w.reaches) } /* ------------------------------------------------------------------------ VALIDATION AND VERIFICATION ------------------------------------------------------------------------ */ pred Good_network_exists [w: Network] { some w.headers && some w.firstMbox && some w.secondMbox Forwarding_requirements_satisfied [w] } run Good_network_exists for 4 but 1 Network /* ------------------------------------------------------------------------ Network, Node, Link, Header, Session ------------------------------------------------------------------------ */