logger.tla

------------------------------- MODULE logger -------------------------------
EXTENDS Integers

CONSTANTS Clients

(*--algorithm logger

variables time = 0,
          log_start = [c \in Clients |-> 0];

define
  FilenameInvariant == \A c1, c2 \in Clients: 
                         (log_start[c1] = log_start[c2] 
                         /\ c1 /= c2)
                         
                         => log_start[c1] = 0
end define;

process Tick = "Tick"
begin
  Tick:
    while TRUE do
      time := time + 1;
    end while;
end process;

process client \in Clients
begin
  Client:
    either
        skip; \* No need to acquire a log file yet
    or
        \* We need to log something. If we haven't yet
        \* acquired a log file, then grab one at the current
        \* time. Otherwise, skip
        if (log_start[self] = 0) then
          log_start[self] := time;
        else
            skip; \* We already have a log file
        end if;
    end either;
    goto Client;
end process;

end algorithm;*)