peterson: CONTEXT =
BEGIN
  PC: TYPE = {sleeping, trying, critical};

  process [tval : BOOLEAN]: MODULE =
    BEGIN
      INPUT pc2 : PC
      INPUT x2 : BOOLEAN
      OUTPUT pc1 : PC
      OUTPUT x1 : BOOLEAN
      INITIALIZATION pc1 = sleeping
      TRANSITION
        [
         wakening: 
           pc1 = sleeping --> pc1' = trying; x1' = x2 = tval
         []
         entering_critical: 
           pc1 = trying AND (pc2 = sleeping OR x1 = (x2 /= tval))
           --> pc1' = critical
         []
         leaving_critical: 
           pc1 = critical --> pc1' = sleeping; x1' = x2 = tval
        ]
    END;

  system: MODULE =
     process[FALSE]
     [] 
     RENAME pc2 TO pc1, pc1 TO pc2, 
            x2 TO x1, x1 TO x2
     IN process[TRUE];

  mutex: THEOREM system |- G(NOT(pc1 = critical AND pc2 = critical));

  invalid: THEOREM system |- G(NOT(pc1 = trying AND pc2 = critical));

  livenessbug1: THEOREM system |- G(F(pc1 = critical));

  livenessbug2: THEOREM system |- G(F(pc2 = critical));

  liveness1: THEOREM system |- G(pc2 = trying => F(pc2 = critical));

  liveness2: THEOREM system |- G(pc1 = trying => F(pc1 = critical));

  liveness3: THEOREM system |- G(F(pc1 = trying)) => G(F(pc1 = critical));

  liveness4: THEOREM system |- G(F(pc2 = trying)) => G(F(pc2 = critical));

END