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.