| 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. Regards, Stephan
|