| Hello, first, TLC will not evaluate your definitions of Numbers because it involves a set comprehension whose base set (Nat) is infinite. I replaced it by Numbers == 10 .. 99 which TLC can evaluate. Concerning your question, you did not describe how exactly you ran the model checker. Your module does not contain a behavior specification, contrary to the most common use case for TLC. Perhaps you believe that TLC checks your THEOREM statement, this is not the case. If you just click on the green triangle in the model checking pane of the Toolbox, TLC doesn't find anything to do and simply terminates successfully. You can however use TLC to check assumptions on constant module parameters: replacing THEOREM by ASSUME will either return in no output (e.g., when you choose the set {10, 14, 22} for input) or in the output "Assumption line ... is false." (when input is {10,16,22}, for example). It is a little nicer to use TLC's facility of evaluating constant expressions. I replaced your THEOREM by the definition ValidInput == input \subseteq NumbersThatDivideBy2Once and then entered ValidInput in the field "Evaluate Constant _expression_" of the sub-pane "Model Checking Results". Running TLC will print TRUE or FALSE in the "Value" field. You can use the same facility for evaluating the operator NumbersThatDivideBy2Once and make TLC output the entire set. Below is the module that I used for my experiments. Hope this helps, Stephan ----------------------------- MODULE TestModule ----------------------------- EXTENDS Naturals CONSTANT input \* Numbers == { n \in Nat : n > 9 /\ n < 100 } Numbers == 10 .. 99 DividesBy2(n) == (n % 2) = 0 DividesBy2Once(n) == DividesBy2(n) /\ ~DividesBy2(n \div 2) NumbersThatDivideBy2Once == { n \in Numbers: DividesBy2Once(n) } ValidInput == input \subseteq NumbersThatDivideBy2Once =============================================================================
|