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