library-wip.tla

EXTENDS Integers, TLC, Sequences
CONSTANTS Books,
          People,
          NumCopies
          
ASSUME NumCopies \in Nat \ {0}  
        
PT == INSTANCE PT

(*--algorithm library
variables library \in [Books -> 1..NumCopies]

define
  AvailableBooks == {b \in Books: library[b] > 0}
end define;

fair process person \in People
variables books = {},
          wants \in SUBSET Books;
begin
Person:
  either \* Checkout
    with b \in AvailableBooks \ books do
      library[b] := library[b] - 1;
      books      := books \union b;
      wants      := wants \ {b};
    end with;
    
  or \* Return
    with b \in books do
      library[b] := library[b] + 1;
      books      := books \ b;
    end with;
  end either;
  
  goto Person;
end process;
end algorithm;*)

The mistakes are line 25 and 32, where it should read {b}, not b.

Running this yields:

TLC encountered a non-enumerable quantifier bound
b1.

Evaluating {} \union b3 in the Evaluate constant expression tab yields:

b3