How to collect all states of a behavior in TLA+?

Question

Description of the problem:

I am modeling checking a distributed protocol against a global property with TLA+ developed by Leslie Lamport. The global property is defined on all states of a behavior (more details can be found below). However, by the nature of exhaustive enumeration of model checking, the state transition graph explored consists of all states of all behaviors. How should I collect all states of each behavior against which the global property can be checked?

---

More on the global property:

Consider an implementation of a replicated list object. The property requires that for any two list states, e.g., $l_1$ and $l_2$, across the whole system, if they contain two common elements such as $a$ and $b$, then $a$ precedes $b$ in $l_1$ if and only if $a$ precedes $b$ in $l_2$.

My solution is to check this property against each behavior. This requires to collect all states of a behavior. Is this feasible? Are there better solutions?

---

Note: This is a re-post.

Answer 1

An answer from Stephan Merz at tlaplus-googlegroup:

In a linear-time framework such as TLA+, a system satisfies a property if the property holds of all system behaviors, and from your description it appears to me that this is what you want. TLC will compute all states that are reachable in your system and evaluate the property over all behaviors: there is nothing that you need to do explicitly.

The potential problem with this is that your system may have a lot of states, and TLC may not finish computing the entire state graph (or at least not in a reasonable amount of time). The TLA+ literature and resources give much advice for working around this problem, in short, you will want to choose small parameters and perhaps constrain the set of states considered by TLC using a state constraint (in the advanced options pane of the Toolbox interface).