system token;

const N = 8;

signal token();
signal claim(pid, boolean);

signal open(integer);
signal close(integer);

signalroute link(N) #lossy #delay[1,2]
  from station to station
  with token, claim;

process station(N);

var worried clock;
var round boolean;
var k integer;

var a pid;
var r boolean;

state init #start ;
    task k := {integer}self;
    set worried := 0;
    task round := true;	
      nextstate wait;
endstate;
state wait;
  input token();
    reset worried;
    output open({integer} self);
      nextstate critical;
  when worried>=N+1;
    set worried := 0;
    output claim(self, round) via {link}k to {station}(k+1)%N;
      nextstate wait;
  input claim(a,r);
      nextstate decision;
endstate;
state critical;
    output close({integer} self);
    task round := not round;
    set worried := 0;
    output token() via {link}k to {station}(k+1)%N;
      nextstate wait;
endstate;
state decision #unstable ;
  provided ({integer}a) < k;
      nextstate wait;
  provided ({integer}a) = k and r = round;
    reset worried;
    output open({integer} self);
      nextstate critical;
  provided ({integer}a) = k and r <> round;
      nextstate wait;
  provided ({integer}a) > k;
    output claim(a,r) via {link}k to {station}(k+1)%N;
      nextstate wait;
endstate;
endprocess;

endsystem;