module LE_LANN_STATION_ORIGINAL (DATA) is

process STATION [OPEN, CLOSE:ACCESS, PRED, SUCC:PORT] (Ai:ADDR, INIT:BOOL) is
   use INIT;
   var S:STATE in
      S := ALPHA;
      loop
         alt
            -- timeout: start an election
            SUCC (CLAIM, Ai);
            S := BETA
         []
            PRED (TOKEN);
            PRIVILEDGE [OPEN, CLOSE, SUCC] (Ai);
            S := ALPHA
         []
            var Aj:ADDR in
               PRED (CLAIM, ?Aj);
               if Ai < Aj then
                  SUCC (CLAIM, Aj)
               elsif Ai > Aj then
                  SUCC (CLAIM, Aj);
                  if S == BETA then
                     S := GAMMA
                  end if
               else -- Ai == Aj
                  if S == BETA then
                     PRIVILEDGE [OPEN, CLOSE, SUCC] (Ai)
                  end if;
                  S := ALPHA
               end if
            end var
         end alt
      end loop
   end var
end process

end module