system fischer;

const N = 3; /* number of stations */
const L = 2; /* waiting time */

process lock(1); 
var p pid public;
endprocess;

process station(N);
var c clock;
state init #start ;
  deadline lazy;
  provided ({lock} 0).p = nil;
    set c := 0;
    nextstate wait;
endstate;
state wait;
  deadline delayable;
  when c <= L;
    task ({lock} 0).p := self;
    set c := 0;
    nextstate try;
endstate;
state try;
  provided ({lock} 0).p = self;
  when c > L;
    informal "enter";
    reset c;
    nextstate critical;
  provided ({lock} 0).p <> self;
    reset c;
    nextstate init;
endstate;
state critical;
  deadline lazy;
    informal "exit";
    task ({lock} 0).p := nil;
    nextstate init;
endstate; 
endprocess;

endsystem;