Thanks, that helped figure out quite a few things.What I'm now trying to understand is the difference between ASSUME and THEOREM, or rather what to use THEOREM for. I've tried looking that up on Specifying Systems, but I'm still somewhat lost. Quoting from 17.7:> More precisely, let A be the conjunction of all the assumptions in Ass. The module asserts that, for every theorem T in Thm, the formula A => T is valid.So Thm defines what the assumptions in Ass imply. Is it just for the human reader? Or is there some way to use that in checking models or specs?On Saturday, December 8, 2018 at 7:15:57 PM UTC+1, Stephan Merz wrote: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 byNumbers == 10 .. 99which 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 definitionValidInput == input \subseteq NumbersThatDivideBy2Onceand 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
============================================================ ================= On 8 Dec 2018, at 18:53, dominy...@xxxxxxxxx wrote:The below module declares a set of numbers that are in the range 10 to 99 that are divisible by 2 only once and call it NumbersThatDivideBy2Once. At the end it declares a theorem that the constant input is a subset of NumbersThatDivideBy2Once.
```
--------------------------- MODULE TestModule ---------------------------
EXTENDS Naturals
CONSTANT input
Numbers == { n \in Nat : n > 9 /\ n < 100 }
DividesBy2(n) == (n % 2) = 0
DividesBy2Once(n) == DividesBy2(n) /\ ~DividesBy2(n \div 2)
NumbersThatDivideBy2Once == { n \in Numbers: DividesBy2Once(n) }
THEOREM input \subseteq NumbersThatDivideBy2Once
=======================
```
How can I check if this theorem holds for a given input? If I run a model check with a provided set of numbers as input, even if some of those numbers are not part of NumbersThatDivideBy2Once I still get no errors.
I've asked this question already on SO, without answers: https://stackoverflow.com/questions/53671776
--
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 .