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

Re: [tlaplus] Represent an arbitrary 32 bit number in binary form



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? :

------------------------------- MODULE model -------------------------------

EXTENDS Integers, 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.

Stephan

On 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 as

BV32 == [ 1 .. 32 -> {0,1} ]

Hope this helps,
Stephan


On 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.

--
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.