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

*From*: Hengfeng Wei <hengx...@xxxxxxxxx>*Date*: Thu, 9 Aug 2018 22:07:16 -0700 (PDT)

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?

---------------------

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

**Follow-Ups**:**Re: [tlaplus] How to collect all states of a behavior?***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] why `init` will invoke twice** - Next by Date:
**Re: [tlaplus] How to make a concrete value from RandomElement?** - Previous by thread:
**Re: [tlaplus] How to make a concrete value from RandomElement?** - Next by thread:
**Re: [tlaplus] How to collect all states of a behavior?** - Index(es):