[]P means that P is true in every state. When on the outside of a predicate, this is equivalent to an invariant, and in fact is how TLC supports them: writing INVARIANT P is the same as writing PROPERTY []P.
Having read through core linearly up to here, I don't know what "writing INVARIANT P" means. Examples have only configured invariants with the Model Overview GUI - is this referencing a way to write the model checker properties as config?
always/box section says:
Having read through core linearly up to here, I don't know what "writing
INVARIANT P" means. Examples have only configured invariants with the Model Overview GUI - is this referencing a way to write the model checker properties as config?