A rough routing protocol implementation based on Distributed Bellman-Ford algorithm in Promela.

router.pml

#define NODES 5
#define LINKS 25

#define INVALID  255
#define INFINITY 16

#define _(from, to) ((from) * NODES + (to))

mtype = {msg};

typedef ROUTES  { byte route[NODES] = INVALID; }
typedef METRICS { byte  hops[NODES] = INFINITY; }
typedef TOLDBY  { byte route[NODES] = INVALID; }

bool link_enabled[LINKS] = false;
chan link[LINKS] = [NODES] of {mtype, byte, byte};

bool found = false;

ROUTES routes[NODES];
METRICS metrics[NODES];

byte forward_check = 0;

inline inc(i) {
  d_step {
    if
    :: i != INVALID -> i = i + 1
    :: else
    fi
  }
}

inline inc_cur(r) {
  inc(r);

  if
  :: r == NODES -> r = 0
  :: else
  fi
}

inline random_x(r, max) {
  byte n;

  n = max-1;
  do
  :: n > 0 -> n = n - 1
  :: true -> r = n; break
  od
}

inline random_nodes(r) {
  random_x(r, NODES)
}

inline random_links(r) {
  random_x(r, LINKS)
}

inline connect(r1, r2) {
  link_enabled[_(r1, r2)] = true;
  link_enabled[_(r2, r1)] = true;
}

inline disconnect(r1, r2) {
  link_enabled[_(r1, r2)] = false;
  link_enabled[_(r2, r1)] = false;
}

inline show_router(from) {
  byte ans[NODES];
  byte n;

  d_step {
    n=0;
    do
    :: n<NODES -> ans[n] = routes[from].route[n]; inc(n)
    :: else -> break
    od;

    printf("router: %d\n", from);
    n=0;
    do
    :: n<NODES -> printf("\tto: %d next: %d\n", n, ans[n]); inc(n)
    :: else -> break
    od;
  }
}

inline show_all_router() {
  byte iii;

  d_step {
    iii = 0;
    do
    :: iii < NODES -> show_router(iii); inc(iii)
    :: else -> break
    od;
  }
}

inline route_exist(b1, r1, r2) {
  byte from, to;
  byte new_from;
  byte count;
  byte hops;
  byte new_hops;

  count = 0;
  from = r1;
  to = r2;
  hops = INFINITY;

  do
  :: count < INFINITY ->
     if
     :: to == from -> b1 = true; break
     :: else ->
        new_from = routes[from].route[to];
        if
        :: (new_from != INVALID) && link_enabled[_(from, new_from)] ->
            new_hops = metrics[new_from].hops[to];
	          if
	          :: new_hops < hops -> skip;
	          :: else -> b1 = false; break
	          fi
        :: else -> b1 = false; break
        fi;
        from = new_from;
	      hops = new_hops
     fi;
     inc(count);
  :: else -> b1 = false; break;
  od
}

inline check_route(b) {
  byte n1, m1;
  bool b1;
  
  b1 = true;
  n1=0;
  do
  :: (n1<NODES) ->
     m1=0;
     do
     :: (m1<NODES) -> route_exist(b1, n1, m1);
        if
	:: (b1 == false) -> goto done
	:: else
	fi;
	inc(m1)
     :: else -> break;
     od;
     inc(n1);
  :: else -> break
  od;

done:
  b = b1;
}

inline sendmsg(from, to, dst, hs) {
  if
  :: true ->link[_(from, to)]!msg(dst, hs)
  :: true ->
drop:
     skip;
  fi
}

inline recvmsg(from, to, dst, hs) {
  link[_(from, to)]?msg(dst, hs);
}

inline send_route(send_id) {
  byte send_peer;
  byte send_dst;

  send_peer = 0;
  do
  :: (send_peer != NODES) ->
     if
     :: link_enabled[_(send_id, send_peer)]  ->
        send_dst = 0;

        do
        :: (send_dst != NODES) ->
          if
          :: (routes[send_id].route[send_dst] != INVALID) ->
              sendmsg(send_id, send_peer, send_dst, metrics[send_id].hops[send_dst])
          :: else
          fi;
	        inc(send_dst)
	      :: else  -> break
	      od;
     :: else
     fi;
     inc(send_peer)
  :: else -> break
  od;
}

inline clear_route(clear_id) {
  byte clear_dst;

  clear_dst = 0;
  do
  :: (clear_dst != NODES) ->
     if
     :: clear_id != clear_dst  ->
        if
	      :: routes[clear_id].route[clear_dst] == INVALID
	      :: else ->
	        if
    	    :: link_enabled[_(clear_id, routes[clear_id].route[clear_dst])]
	        :: else ->
              metrics[clear_id].hops[clear_dst] = INFINITY;
	            routes[clear_id].route[clear_dst] = INVALID
	        fi
	      fi
     :: else
     fi;
     inc(clear_dst)
  :: else -> break
  od;
}

inline update_route(update_id) {
  byte update_peer;
  byte update_dst;

  update_peer = 0;
  do
  :: (update_peer != NODES) ->
     do
     :: empty(link[_(update_peer, update_id)]) -> break;
     :: nempty(link[_(update_peer, update_id)]) -> recvmsg(update_peer, update_id, update_dst, h);
        inc(h);
        if
	:: routes[update_id].route[update_dst] == update_peer ->
	   metrics[update_id].hops[update_dst] = h
	:: else ->
	   if
	   :: h < metrics[update_id].hops[update_dst] ->
	     metrics[update_id].hops[update_dst] = h;
	     routes[update_id].route[update_dst] = update_peer
	   :: else
	   fi
	fi
     od;
     inc(update_peer)
  :: else -> break
  od;
}

byte cur = 0;

proctype router(byte id) {
  byte peer;
  byte dst;
  byte h;
  byte i;

  d_step {
    cur == id ->
    routes[id].route[id] = id;
    metrics[id].hops[id]  = 0;
    inc_cur(cur);
  }

again:
  cur == id ->
    send_route(id);
  d_step {inc_cur(cur);}

  cur == id ->
    clear_route(id);
    update_route(id);

  d_step {
    inc_cur(cur);

    if
    :: cur == 0 -> check_route(found)
    :: else
    fi
  }
  goto again
}

inline run_routers(num) {
  int i;

  i=0;
  do
  :: i < num -> run router(i); inc(i)
  :: else -> break
  od
}

init {

  atomic {
    connect(0, 1);
    connect(1, 2);
    connect(2, 3);
    connect(1, 3);
    connect(3, 4);

    run_routers(NODES);
  }

/*
  do
  :: found -> show_all_router(); break
  od;

  disconnect(1, 2);
  found = false;

  do
  :: found -> show_all_router(); assert(false)
  od
  */
}

#define p found
// 
never  {    /* !(<>[]p) */
T0_init:
  if
  :: (! ((p))) -> goto accept_S9
	:: (1) -> goto T0_init
	fi;
accept_S9:
	if
	:: (1) -> goto T0_init
	fi;
}