MODULE main
   VAR
      pr1: process prc(pr2.st, turn, 0);
      pr2: process prc(pr1.st, turn, 1);
      turn: boolean;
   ASSIGN
      init(turn) := 0;
   -- safety
   SPEC AG!((pr1.st = c) & (pr2.st = c))
   -- liveness
   SPEC AG((pr1.st = t) -> AF (pr1.st = c))
   -- SPEC AG((pr2.st = t) -> AF (pr2.st = c))
   -- nonblocking
   SPEC AG((pr1.st = n) -> EX (pr1.st = t))
   SPEC AG((pr2.st = n) -> EX (pr2.st = t))
   -- no strict sequencing
   SPEC EF(pr1.st=c & E[pr1.st=c U 
                      (!pr1.st=c & E[!pr2.st=c U pr1.st=c ])])

MODULE prc(other-st, turn, myturn)
   VAR
      st: {n, t, c};
   ASSIGN
      init(st) := n;
      next(st) :=
         case
            (st = n)                                   : {t,n};
            (st = t) & (other-st = n)                  : c;
            (st = t) & (other-st = t) & (turn = myturn): c;
            (st = c)                                   : {c,n};
            1                                          : st;
         esac;
      next(turn) :=
         case
            turn = myturn & st = c : !turn;
            1                      : turn;
         esac;
   FAIRNESS running
   FAIRNESS  !(st = c)