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

  job: MODULE =
    BEGIN
      INPUT y2 : NATURAL
      OUTPUT y1 : NATURAL
      LOCAL pc : PC 
      INITIALIZATION
				 pc = sleeping; 
				 y1 = 0
      TRANSITION
        [ pc = sleeping --> y1' = y2 + 1; 
                            pc' = trying
          []
          pc = trying AND (y2 = 0 OR y1 < y2) --> pc' = critical
          []
          pc = critical --> y1' = 0; 
                            pc' = sleeping 
        ]
    END;

  system: MODULE =
    job
    [] 
    RENAME y2 TO y1, y1 TO y2
    IN job;

  mutex: THEOREM system
                 |- G(NOT(pc.1 = critical AND pc.2 = critical));

  invalid: THEOREM system
                   |- G(NOT(pc.1 = trying AND pc.2 = critical));

  aux1: THEOREM system |- G(pc.1 = trying => y1 > 0);

  aux2: THEOREM system |- G(pc.2 = trying => y2 > 0);
END