[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

How to collect all states of a behavior?

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? 

Hengfeng Wei