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