Hello,
Thanks for your help. However, I am still confused.
Now I am not sure whether I have asked a right question.
Let me explain it more concretely with an artificial example adopted from the real system I am working on
(which is too complex to describe).
Consider an implementation of a replicated list object consisting of n replicas.
Each replica simply applies the operations issued by users locally and then asynchronously broadcasts them to other replicas.
The desired global property requires that for any two list states, e.g., s1 and s2, of the 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.
Given two list states, I am able to express the "if, then" part of the property above as a TLA+ formula.
However, I don't know how to express the "for any two ... of the system" part.
(Note that "of the system" is not "of a snapshot of the system".)
Specifically, what should be "???" in the formula "\A s1, s2 \in ???"?
Is it necessary for us to explicitly collect all list states of each behavior?
I think so because the transition system of the protocol implicitly computed by the model checker contains
all states of all behaviors and the global property above is only defined on an individual behavior.
Is this clear?
(If necessary, I will write a sample TLA+ spec for the protocol and the global property described above.)
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
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.