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

Re: [tlaplus] How can I verify spec satisfies the properties for infinite states?

TLC is an explicit-state model checker that will compute the graph of reachable states, so it can only check properties of finite instances of specifications. For an infinite-state model, you will have to bound the state space using state constraints as you did (and/or override operator definitions, such as redefining Nat == 0..3 etc.). Any counter-example generated for the restricted state space is a valid counter-example and can be useful for debugging your specification. When no error is found, you cannot infer that your original model is correct, although you gain some confidence because no error was detected over the restricted state space. You have to use engineering judgment to decide what parameter sizes and bounds to use in order to be satisfied that your spec is correct. In practice, specification errors show up in small instances of the specification, and those will be checked exhaustively by TLC.

You can use TLAPS for reasoning about infinite-state specifications, but the user effort is much bigger.


On 19 Aug 2018, at 10:54, myjul...@xxxxxxxxx wrote:


I wonder how can I verify spec satisfies the properties for infinite states.
In my spec, there are infinitely states so TLC is executed infinitely.
In this case, I wonder how can I verify spec satisfies the properties.

For example, 
I want to prove "Theorem Spec  => []TypeInv".
When i check by the bound length constraint because of infinite states, TypeInV is satisfied.
But, I think it can be not proved that spec satisfies the properties for infinitely states by this bounded checking. 


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 tlaplus+u...@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.