relation pending(P, S, T)
relation rp(H, S, D) # There is a forwarding path from S to t for P
relation src(P, H)
relation dst(P, H)
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

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)

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

e is really a derived relation defined by e(H, X) = exists Y: rp(H, X, Y) / X ~=Y

relation e(H, X)


individual __n0,__n1,__n2

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))
     & (~e(X,Y) | X = Y)
     & e(X,X)

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;

Abstract the number of times that the same packet recieved

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

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

  if (~e(s0, sw1) & sw0 ~= sw1) {

assert ~rp(s0,sw0,sw1)

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

  if (t0 ~= sw1) {

if (~rp(t0, sw1, X) | X = sw1) {

      if (~e(t0, 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 (~e(s0,sw1) & sw0 ~= sw1) & rp(s0,sw0,sw1)
}


concept c1(S,V0) = (e(S, V0) * ~rp(S, V0, S))
concept c2(V0) = ~e(V0,V0)
concept foo(H,V,W,P) = ((pending(P,V,W) + e(H,V) + rp(H,V,W)) * (pending(P,V,W) + e(H,V) + rp(H,V,W)) * (dst(P,H) + src(P,H)))

concept c3(P,D,V0,V1) = (pending(P, V0, V1) * dst(P,D) * D = V0) concept c4(P,S,V0,V1) = (pending(P, V0, V1) * src(P,S) * ~e(S, V0))

concept c5(S,V0,V1) = (rp(S, V0, V1) * ~V0 = V1 * ~e(S, V0))

concept c6(S,V0,V1) = (rp(S, V0, V1) * ~V0 = V1 * ~e(S, V1)) concept c7(S,V0) = (~V0 = S * rp(S, S, V0))

conjecture ~(e(S, V0) & ~rp(S, V0, S))
conjecture e(V0,V0)
conjecture ~(pending(P, V0, V1) & dst(P,D) & D = V0)
conjecture ~(pending(P, V0, V1) & src(P,S) & ~e(S, V0))

conjecture ~(rp(S, V0, V1) & ~V0 = V1 & ~e(S, V0))

conjecture ~(~V0 = S & rp(S, S, V0))

conjecture ~(pending(P, V0, V1) & src(P,S) & ~e(S, V0))