Learning

Module describing an acyclic partial function. The function is built by calling the "set" action. This has preconditions that enforce the required invariants. The function can be accessed using "dom" to query if an element is in the domain of the function, and "get" to get its value. The "get" action has a precondition that the given element must be in the domain.

Because of the invariant that the relation re construct by "set" is an acyclic partial function, we can represent it by its transitive closure "tc", while remainin gin EPR.

module inverse_forest(carrier) = {

    relation dom(X:carrier)            # domain of the function
    relation tc(X:carrier,Y:carrier)   # transitive closure of the function

    axiom tc(X,X)                          # Reflexivity
    axiom tc(X, Y) & tc(Y, Z) -> tc(X, Z)  # transitivity
    axiom tc(X, Y) & tc(Y, X) -> X = Y     # anti-symmetry
    axiom tc(X, Y) & tc(X, Z) -> (tc(Y, Z) | tc(Z, Y)) # linearity

    init ~dom(X) & (tc(X,Y) <-> X = Y)     #initially empty

    action set(x:carrier,y:carrier) = {
       assert ~tc(y,x);                # can't create a cycle
       assert ~dom(x);                 # can't remove links
       dom(x) := true;
       tc(X, Y) := tc(X, Y) | tc(X, x) &  tc(y, Y)
    }

    action get(x:carrier) returns (y:carrier) = {
       assert dom(x);
       assume tc(x,y) & ~(tc(x,X) & tc(X,y) & X ~= x & X ~= y)
    }

}

Types, relations and functions describing state of the network

type packet
type host

relation pending(P:packet, S:host, T:host)
individual src(P:packet) : host
individual dst(P:packet) : host
relation link(S:host, T:host)
instantiate route(H:host) : inverse_forest(host)

axiom ~link(X, X)                          # no self-loops
axiom ~link(X, Y) | link(Y, X)             # symmetric

The initial state of the network (empty)

init ~pending(P,S,T)

Protocol description

There is just one action describing the receipt of a pending message by some host.

action receive = {
  local p0:packet, sw0:host, sw1:host, sw2:host, s0:host, t0:host {

The action's guard.

       t0 := dst(p0);
       s0 := src(p0);
       assume pending(p0, sw0, sw1) | s0 = sw1 & sw0 = sw1;

Abstract the number of times that the same packet recieved

       if (pending(p0,sw0, sw1)) {
           pending(p0, sw0, sw1) := *
       };

learn: if no route from receiving switch back to source...

       if (~route(s0).dom(sw1) & sw0 ~= sw1 & s0 ~= sw1) {
           call route(s0).set(sw1,sw0)   # create new route
       };

forward the packet if dest is not self

       if t0 ~= sw1 {

           if ~route(t0).dom(sw1) {                            # if no route to dest...
           pending(p0, sw1, Y) := link(sw1, Y) & Y ~= sw0  # flood
           }

           else {
           sw2 := route(t0).get(sw1);                      # get the out-going link
           pending(p0, sw1, sw2) := true                   # route the packet there
       }
       }
  }
}

export receive

conjecture ~(route(S).dom(V0) & ~route(S).tc(V0, S))
conjecture ~route(V0).dom(V0)
conjecture ~(pending(P, V0, V1) & dst(P) = V0)
conjecture ~(pending(P, V0, V1) & ~route(src(P)).dom(V0) & V0 ~= src(P))
conjecture ~(route(S).tc(V0, V1) & ~V0 = V1 & ~route(S).dom(V0))
conjecture ~(route(S).tc(V0, V1) & ~V0 = V1 & S ~= V1 & ~route(S).dom(V1)) # TODO: needed?
conjecture ~(~V0 = S & route(S).tc(S, V0))

conjecture ~(pending(P, V0, V1) & src(P,S) & ~route(S).dom(V0))