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

*From*: dominykas....@xxxxxxxxx*Date*: Sat, 8 Dec 2018 09:53:43 -0800 (PST)

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

**Follow-Ups**:**Re: [tlaplus] Trying to figure out how theorems work with this basic example***From:*Stephan Merz

- Prev by Date:
**Re: Is it correct to use symmetry set in this spec?** - Next by Date:
**Re: [tlaplus] Trying to figure out how theorems work with this basic example** - Previous by thread:
**What to do with distributed computing?** - Next by thread:
**Re: [tlaplus] Trying to figure out how theorems work with this basic example** - Index(es):