threads.tla

EXTENDS Integers, Sequences, TLC, FiniteSets

(* --algorithm deadlock
variable mq = <<>>;

macro add_message(msg) begin
    await Len(mq) < 5;
    mq := Append(mq, <<msg>>);
end macro

procedure garbage_collector() begin
    GC:
        either
          Add: 
            add_message(<<self, "gc">>);
            return;
        or 
            skip;
            return;
        end either;
end procedure;
 
process reader = "reader"
begin
  Read:
    while TRUE do
      await Len(mq) /= 0;
      mq := Tail(mq);
      call garbage_collector();
    end while;
end process;

process writer = "writer"
begin
  Write:
    while TRUE do
      add_message("write");
    end while;
end process;


end algorithm;
*)