TLA+ Temporal Formula

---- MODULE dbm ----

EXTENDS TLC, Integers, Sequences

(* --algorithm dbm

variables 
  Ids = {1..100},
  requested = [i \in Ids |-> FALSE],
  processed = [i \in Ids |-> FALSE];

begin
A:
    print "Hello, world";
end algorithm; *)
\* BEGIN TRANSLATION
VARIABLES Ids, requested, processed, pc

vars == << Ids, requested, processed, pc >>

Init == (* Global variables *)
        /\ Ids = {1..100}
        /\ requested = [i \in Ids |-> FALSE]
        /\ processed = [i \in Ids |-> FALSE]
        /\ pc = "A"

A == /\ pc = "A"
     /\ PrintT("Hello, world")
     /\ pc' = "Done"
     /\ UNCHANGED << Ids, requested, processed >>

Next == A
           \/ (* Disjunct to prevent deadlock on termination *)
              (pc = "Done" /\ UNCHANGED vars)

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

Termination == <>(pc = "Done")

\* END TRANSLATION

RequestsAreFulfilled == \A id \in Ids: requested[id] ~> processed[id]
====

Couple of comments on the spec:

• {1..100} is the set containing the set 1..100, not the set 1..100. I think you want Ids = 1..100 instead.
• RequestsAreFulfilled is breaking because TLC can check temporal properties of constant sets, but Ids is a variable. You want either make Ids a constant (CONSTANT Ids) or an operator (Ids == 1..100).

Word of warning: 100 ids will probably take a long time to validate any spec. Consider trying it with a smaller numbers first.