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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Sun, 6 Nov 2022 09:35:58 +0100*References*: <bcd0ac97-be4f-4b5e-b91b-d347dde2cb61n@googlegroups.com>

Hello, first of all, please do not send screen shots unless you want to illustrate some behavior of the GUI: TLA+ source is pure ASCII and can be copied and pasted into messages. Since you apply Boolean operations to the elements of your bit vectors, you want to change the co-domain from {0,1} to {TRUE, FALSE}. After that change, TLC can easily evaluate your formula. In my version below, I made xor and cmp_bv4 plain operators rather than definitions of functions (which you get with your version using square brackets). This should not make a difference, but I consider this style to be more idiomatic. (See also section 6.4 of Specifying Systems.) I also strengthened the assertion of your theorem to make it an equivalence and to assert equality of the two bit vectors. BV4 == [0..3 -> {TRUE, FALSE}]
-- xor(b0, b1) == (b0 /\ ~ b1) \/ (~ b0 /\ b1) cmp_bv4(bv0, bv1) == /\ ~ xor(bv0[0], bv1[0]) /\ ~ xor(bv0[1], bv1[1]) /\ ~ xor(bv0[2], bv1[2]) /\ ~ xor(bv0[3], bv1[3]) THEOREM CMP_CORRECT == \A x,y \in BV4 : cmp_bv4(x,y) <=> x = y Now, create a model in the Toolbox and click on "evaluate constant _expression_". Paste the assertion of the theorem, i.e., the formula \A x,y \in BV4 : cmp_bv4(x,y) <=> x = y into the "_expression_" field of the window and click on the green triangle. TLC will report that the _expression_ evaluates to TRUE. Stephan
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+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2B4AEC9D-EBDE-4E4D-8380-536FA81C4AD2%40gmail.com. |

**Follow-Ups**:

**References**:

- Prev by Date:
**[tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?** - Next by Date:
**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form** - Previous by thread:
**[tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?** - Next by thread:
**Re: [tlaplus] How to prove my "compare" function on 4-bit binary numbers is correct?** - Index(es):