Learning switch

type packet
type switch

relation pending(P: packet, S: switch, T: switch)
relation rp(H: switch, S: switch, D: switch) # There is a forwarding path from S to t for P
relation src(P: packet, H: switch)
relation dst(P: packet, H: switch)
relation link(S: switch, T: switch)

axiom rp(H, X,X)  # Reflexivity
axiom ~rp(H, X, Y) | ~rp(H, Y, Z) | rp(H, X, Z) # transitivity
axiom ~rp(H, X, Y) | ~rp(H, Y, X) | X = Y # anti-symmetric
axiom ~rp(H, X, Y) | ~rp(H, X, Z) | rp(H, Y, Z) | rp(H, Z, Y) # linearity

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

module partial_function(f) = {

1) for any x there is at most one y such that f(x,y),

    axiom ~f(X,Y) | ~f(X,Z) | Y = Z
}

instantiate partial_function(src)
instantiate partial_function(dst)

init ~pending(P,S,T)
     & rp(H,X,X)
     & (X = Y | ~rp(H,X,Y))

individual p0, sw0, sw1,sw2, s0, t0


action receive = {
  p0 := *;
  sw0 := *;
  sw1 := *;
  s0 := *;
  t0 := *;
  assume dst(p0, t0);
  assume src(p0, s0);
  assume pending(p0,sw0, sw1) | s0 = sw1 & sw0 = sw1;
  pending(p0, sw0, sw1) := false;

  if ((~rp(s0, sw1, X) | X = sw1) & sw0 ~= sw1) {

assert ~rp(s0,sw0,sw1)

    rp(s0, S, D) := rp(s0, S, D) | rp(s0, S, sw1) &  rp(s0, sw0, D)
  };

  if (t0 ~= sw1) {
      if (~rp(t0, sw1, X) | X = sw1)  {
     pending(p0, sw1, Y) := link(sw1, Y) & Y ~= sw0 # flood
      }
      else {
     sw2 := *;
     assume sw2 ~= sw1 & rp(t0, sw1, sw2) & (~rp(t0, sw1, X) | X = sw1 | rp(t0, sw2, X)) ;
     pending(p0, sw1, sw2) := true
      }
  }
}


action error = {
  p0 := *;
  sw0 := *;
  sw1 := *;
  s0 := *;
  t0 := *;
  assume dst(p0, t0);
  assume src(p0, s0);
  assume pending(p0,sw0, sw1) | s0 = sw1 & sw0 = sw1;
  assume ((~rp(s0, sw1, X) | X = sw1) & sw0 ~= sw1) & rp(s0,sw0,sw1)
}