Description of the problem:
I am modeling checking a distributed protocol against a global property with tlaplus.
The global property is defined on all states of a behavior (more details can be found below).
However, by the exhaustive enumeration nature 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 consisting of n replicas.
The property requires that for any two list states, e.g., s1 and s2, across the whole system,
if they contain two common elements such as a and b,
then a precedes b in s1 if and only if a precedes b in s2.
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?
Thanks.
Hengfeng Wei