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

*From*: Andrew Helwer <andrew.helwer@xxxxxxxxx>*Date*: Sun, 6 Nov 2022 08:55:56 -0800 (PST)*References*: <acf45a9b-12cc-4189-8094-750721df34cbn@googlegroups.com> <04554D4D-9760-4011-879E-19745E2AACF4@gmail.com> <34306500-8df5-4703-8c90-019a0acbe150n@googlegroups.com> <90B23BE6-AFD9-4407-A80B-5BC1EB759B96@gmail.com> <f1b09c3e-ab57-4466-9eb6-0f4ece826365n@googlegroups.com> <f11a37d4-f71f-441f-ac0d-03489947ce45n@googlegroups.com>

The {0 .. 63} should be 0 .. 63. The .. is an ordinary infix operator, it isn't special set syntax so you don't need the surrounding curly braces. {0 .. 63} would just give you a set with a single element, the nested set generated by 0 .. 63.

Andrew

On Saturday, November 5, 2022 at 11:29:47 PM UTC-4 amjad.h...@xxxxxxxxx wrote:

Also, is this the correct way to define a couple of variable as 64 bit numbers in binary? :-------------------------------

MODULEmodel -------------------------------

EXTENDSIntegers, Sequences

bv64 == [ {0..63} -> {0,1} ]

xR8 == bv64

xR9 == bv64

xR10 == bv64

xR11 == bv64

xR12 == bv64

xR13 == bv64

xR14 == bv64

xR15 == bv64

=============================================================================

On Saturday, November 5, 2022 at 10:00:53 PM UTC-5 Amjad Ali wrote:You made a great point about there being 2^32 elements. I do in fact have to verify and prove some things regarding this in the future. My idea was to prove by induction.On Friday, November 4, 2022 at 4:24:32 AM UTC-5 Stephan Merz wrote:Representing a bit vector as a function seems to be natural. If it's more convenient, you can obviously change the index set and number from 0. In TLA+, functions with domain 1 .. N for some natural number N are identified with sequences, which may be convenient for certain purposes. In particular, TLC will print values of the set that I suggested as sequences. But mathematically there is no real difference.For practical purposes, in particular if you aim at verification using TLC, you may find it convenient to make the length of bit vectors a parameter: the set BV32 has 2^32 elements, and TLC won't like enumerating that set. I presume that many algorithms that are correct for bit vectors of length 3 or 4 will also be correct for length 32.StephanOn 4 Nov 2022, at 10:15, Amjad Ali <amjad.h...@xxxxxxxxx> wrote:

Thank you for the answer! So, would this be considered a set of functions? Also, would I be able to modify the answer as BV32 == [0..32 -> {0,1}]?On Thursday, November 3, 2022 at 4:06:14 AM UTC-5 Stephan Merz wrote:The set of bit vectors of length 32 can be defined asBV32 == [ 1 .. 32 -> {0,1} ]Hope this helps,StephanOn 3 Nov 2022, at 09:46, Amjad Ali <amjad.h...@xxxxxxxxx> wrote:What is the most mathematical way of defining a binary number in TLA+.My guess is something like the following:data32 == << b_0 \in {0,1}, ... , b_31 \in {0,1} >>However, this results in a syntax error.--

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+u...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/acf45a9b-12cc-4189-8094-750721df34cbn%40googlegroups.com.

--

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+u...@xxxxxxxxxxxxxxxx.To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/34306500-8df5-4703-8c90-019a0acbe150n%40googlegroups.com.

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/fe786ec0-6a53-4fa3-9267-8e5b347eb3aan%40googlegroups.com.

**References**:**[tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Amjad Ali

**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Stephan Merz

**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Amjad Ali

**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Stephan Merz

**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Amjad Ali

**Re: [tlaplus] Represent an arbitrary 32 bit number in binary form***From:*Amjad Ali

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