Re: [tlaplus] How to collect all states of a behavior?

Hello,

I have understood your answer.

(Please ignore my second post.)

Thanks for your efforts.

Hengfeng Wei

On Saturday, August 11, 2018 at 1:28:39 AM UTC+8, Stephan Merz wrote:

Hello,

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).

Hope this helps,

Stephan

--
Stephan Merz

On 10 Aug 2018, at 07:07, Hengfeng Wei <heng...@xxxxxxxxx> wrote:

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

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplu...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.