Learning with count

relation pending(P, S, T) # A pednding packet P at on the link from S to T oof distance Di
relation rp(H, S, D) # There is a path from S to D for H
relation dist(H, S, Di) # There is a path from S to H of length Di

Packet fields

relation src(P, H)
relation dst(P, H)
relation hopcount(P, Z)
relation pid(P, ID) # The identity of the packet

relation link(S, T)


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

Numerics

individual zero

relation le(X, Y)
axiom le(zero, X)
axiom le(X, X) # Reflexivity
axiom ~le(X, Y) | ~le(Y, Z) | le(X, Z) # transitivity
axiom ~le(X, Y) | ~le(Y, X) | X = Y # anti-symmetric
axiom le(X, Y) | le(Y, X) # totality
derived lt(X,Y) = le(X,Y) & X ~= Y

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)
instantiate partial_function(pid)
instantiate partial_function(hopcount)

Partial function on pairs

axiom ~dist(X, Y, Dist1) | ~dist(X, Y, Dist2) |  Dist1 = Dist2


individual n0,n1,n2

module extra(c) = {
   derived pend[c](X,Y) = pending(c,X,Y)
   derived route[c](X,Y) = rp(c,X,Y)
}

instantiate extra(n0) instantiate extra(n1) instantiate extra(n2)

axiom n0 ~= n1
axiom n0 ~= n2
axiom n1 ~= n2
axiom (X = n0 | X = n1 | X = n2)

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


individual p0, p1, sw0, sw1,sw2, s0, t0, di, cdi, ndi


action easy = {
  p0 := *
}

action receive = {
  p0 := *;
  p1 := *;
  sw0 := *;
  sw1 := *;
  s0 := *;
  t0 := *;
  di := *;
  cdi := *;
  ndi := *;
  assume dst(p0, t0);
  assume src(p0, s0);
  assume (pending(p0, sw0, sw1) & hopcount(p0, cdi))  | (s0 = sw1 & sw0 = sw1 & cdi = zero);

Abstract the number of received packets

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

  if (sw0 ~= sw1) {

      if ((~rp(s0, sw1, X) | X = sw1)) # First entry
      {

assert ~rp(s0,sw0,sw1) // error 1

       rp(s0, S, D) := rp(s0, S, D) | rp(s0, S, sw1) &  rp(s0, sw0, D) ;
       dist(s0, sw1, X) := X = cdi
      }
      else {

assert dist(s0, sw1, X) // error 2

           assume dist(s0, sw1, di) ;
           if (lt(cdi, di)) { # Shorter path

assert ~rp(s0,sw0,sw1) // error 3

        rp(s0, S, D) := rp(s0, S, D) & (S = D |  ~ (rp(s0, S, sw1) &  rp(s0, sw1, D))) ;  # Remove deleted entries
        rp(s0, S, D) := rp(s0, S, D) | rp(s0, S, sw1) &  rp(s0, sw0, D) ;
        dist(s0, sw1, X) := X = cdi
           }
      }
  };


  assume(lt(cdi, ndi) & (~lt(cdi, X) | le(ndi, X))); # ndi is the immedidate successor of cdi
  assume src(p1, X) <-> src(p0, X);
  assume dst(p1, X) <-> dst(p0, X);
  assume pid(p1, X) <-> pid(p0, X);
  assume hopcount(p1,X) <-> X = ndi;
  if (t0 ~= sw1) {
      if (~rp(t0, sw1, X) | X = sw1)  {
         pending(p1, 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(p1, sw1, sw2) := true
      }
  }
}


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


action error2 = {
  p0 := *;
  sw0 := *;
  sw1 := *;
  s0 := *;
  t0 := *;
  cdi := * ;
  sw2 := * ;
  assume dst(p0, t0);
  assume src(p0, s0);
  assume (pending(p0,sw0, sw1) & hopcount(p0, cdi))  | (s0 = sw1 & sw0 = sw1 & cdi=zero);
  assume sw0 ~= sw1 ;
  assume rp(s0, sw1, sw2) & sw2 ~= sw1 ;
  assume ~dist(s0, sw1, X)
}

action error3 = {
  p0 := *;
  sw0 := *;
  sw1 := *;
  s0 := *;
  t0 := *;
  cdi := * ;
  sw2 := * ;
  di := * ;
  assume dst(p0, t0);
  assume src(p0, s0);
  assume (pending(p0,sw0, sw1) & hopcount(p0, cdi))  | (s0 = sw1 & sw0 = sw1 & cdi=zero);
  assume (rp(s0, sw1, sw2) & sw2 ~= sw1) | sw0 = sw1 ;
  assume dist(s0, sw1, di) ;
  assume lt(cdi, di) ;
  assume rp(s0, sw0, sw1)
}