Re: How to define Hexa decimal sets/Vectors in TLA+

Here you can see a spec which uses both approaches (natural number incremented then converted to hex, and hex number incremented as a hex) which are then checked for equality:

https://github.com/ahelwer/tla-experiments/blob/master/Hex.tla

On Friday, April 20, 2018 at 1:23:50 PM UTC-7, Andrew Helwer wrote:

Here's one approach to a Hex module which continually increments then prints out a hex value:

-------------------------------- MODULE Hex --------------------------------

EXTENDS
Naturals,
Sequences,
TLC

VARIABLES
hexValue

HexDigit == 0 .. 15

Hex == Seq(HexDigit)

HexChar ==
<<"0","1","2","3","4","5","6","7","8","9","A","B","C","D","E","F">>

RECURSIVE HexToString(_)
HexToString(hex) ==
IF hex = <<>>
THEN ""
ELSE HexChar[Head(hex) + 1] \o HexToString(Tail(hex))

TypeInvariant ==
/\ hexValue \in Hex

Init ==
/\ hexValue = <<0>>

RECURSIVE IncrementedHexValue(_)
IncrementedHexValue(hex) ==
LET
prefix == SubSeq(hex, 1, Len(hex) - 1)
last == hex[Len(hex)]
IN
IF hex = <<>>
THEN <<1>>
ELSE
IF last < 15
THEN Append(prefix, last + 1)
ELSE Append(IncrementedHexValue(prefix), 0)

Increment ==
/\ Print(HexToString(hexValue), TRUE)
/\ hexValue' = IncrementedHexValue(hexValue)

Next ==
\/ Increment

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

Another approach is to consider hex values as simple natural numbers, and operate on them as natural numbers. You can then write a function to convert from natural number to hex string representation.

As an aside, this was my first encounter with string manipulation in TLA+ - I wish TLC treated them as sequences!

Andrew

On Monday, April 16, 2018 at 11:08:38 PM UTC-7, knni...@xxxxxxxxx wrote:
Hi All,

Currently, I am working with sets and vectors.
My set and vector contain hexadecimal numbers.
I need to define subsets of a hexadecimal superset and need to perform some set operations on the same.

-Regards Nikhila K N