TLA+ State Sweeping

SweepingExample.tla

---- MODULE SweepingExample ----

EXTENDS Integers, TLC, Sequences, FiniteSets
CONSTANTS BuffLen, NumThreads
ASSUME BuffLen \in Nat
ASSUME NumThreads >= 2

Threads == 1..NumThreads

(* --algorithm xp
variables
Getters \in (SUBSET Threads) \ {{}, Threads};
Putters = Threads \ Getters;
buffer = <<>>;
put_at = 1;
get_at = 1;
awake = [t \in Threads |-> TRUE];
occupied = 0;

define
  IsFull == occupied = BuffLen
  IsEmpty == occupied = 0
  SleepingThreads == {t \in Threads: ~awake[t]}
end define;

macro notify() begin
  if SleepingThreads /= {} then
    with t \in SleepingThreads do
      awake[t] := TRUE;
    end with;
  end if;
end macro;

process get \in Getters
begin Get:
  await awake[self];
  if IsEmpty then
    awake[self] := FALSE;
  else
    notify();
    occupied := occupied - 1;
  end if;
  goto Get;
end process;

process put \in Putters
begin Put:
  await awake[self];
  if IsFull then
    awake[self] := FALSE;
  else
    notify();
    occupied := occupied + 1;
  end if;
  goto Put;
end process;
end algorithm; *)

\* BEGIN TRANSLATION - the hash of the PCal code: PCal-b1cbb17fbd0721296cec00eed6357daf
VARIABLES Getters, Putters, buffer, put_at, get_at, awake, occupied, pc

(* define statement *)
IsFull == occupied = BuffLen
IsEmpty == occupied = 0
SleepingThreads == {t \in Threads: ~awake[t]}


vars == << Getters, Putters, buffer, put_at, get_at, awake, occupied, pc >>

ProcSet == (Getters) \cup (Putters)

Init == (* Global variables *)
        /\ Getters \in (SUBSET Threads) \ {{}, Threads}
        /\ Putters = Threads \ Getters
        /\ buffer = <<>>
        /\ put_at = 1
        /\ get_at = 1
        /\ awake = [t \in Threads |-> TRUE]
        /\ occupied = 0
        /\ pc = [self \in ProcSet |-> CASE self \in Getters -> "Get"
                                        [] self \in Putters -> "Put"]

Get(self) == /\ pc[self] = "Get"
             /\ awake[self]
             /\ IF IsEmpty
                   THEN /\ awake' = [awake EXCEPT ![self] = FALSE]
                        /\ UNCHANGED occupied
                   ELSE /\ IF SleepingThreads /= {}
                              THEN /\ \E t \in SleepingThreads:
                                        awake' = [awake EXCEPT ![t] = TRUE]
                              ELSE /\ TRUE
                                   /\ awake' = awake
                        /\ occupied' = occupied - 1
             /\ pc' = [pc EXCEPT ![self] = "Get"]
             /\ UNCHANGED << Getters, Putters, buffer, put_at, get_at >>

get(self) == Get(self)

Put(self) == /\ pc[self] = "Put"
             /\ awake[self]
             /\ IF IsFull
                   THEN /\ awake' = [awake EXCEPT ![self] = FALSE]
                        /\ UNCHANGED occupied
                   ELSE /\ IF SleepingThreads /= {}
                              THEN /\ \E t \in SleepingThreads:
                                        awake' = [awake EXCEPT ![t] = TRUE]
                              ELSE /\ TRUE
                                   /\ awake' = awake
                        /\ occupied' = occupied + 1
             /\ pc' = [pc EXCEPT ![self] = "Put"]
             /\ UNCHANGED << Getters, Putters, buffer, put_at, get_at >>

put(self) == Put(self)

(* Allow infinite stuttering to prevent deadlock on termination. *)
Terminating == /\ \A self \in ProcSet: pc[self] = "Done"
               /\ UNCHANGED vars

Next == (\E self \in Getters: get(self))
           \/ (\E self \in Putters: put(self))
           \/ Terminating

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION - the hash of the generated TLA code (remove to silence divergence warnings): TLA-bfec9b4faf22e179a64b8133b02dc9fc
====

SweepTLC.ps1

function template($t) {
    @"
SPECIFICATION Spec

CONSTANTS
    BuffLen = 2
    NumThreads = $t

CHECK_DEADLOCK TRUE
"@
}

foreach ($i in 2..6) {
    Write-Output "Testing with NumThreads = $i"
    (template $i) > "MCSweepingExample.cfg"
    java -jar /path/to/tla2tools.jar -noGenerateSpecTE SweepingExample.tla -config MCSweepingExample.cfg > out
    if($LASTEXITCODE) {
        Write-Output "Error, see `out` for deets"
        exit
    } 
}