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

*From*: Andrew Helwer <andrew...@xxxxxxxxx>*Date*: Thu, 26 Apr 2018 10:31:33 -0700 (PDT)*References*: <13439582-19e9-4c6e-9019-98e5d5a64a4b@googlegroups.com> <da89689a-9eb3-4d95-9a60-bdabe744a9c5@googlegroups.com>

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:

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 ------------------------------ -- EXTENDSNaturals,Sequences,TLCVARIABLEShexValueHexDigit == 0 .. 15Hex == 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 HexInit ==/\ hexValue = <<0>>RECURSIVE IncrementedHexValue(_)IncrementedHexValue(hex) ==LETprefix == SubSeq(hex, 1, Len(hex) - 1)last == hex[Len(hex)]INIF hex = <<>>THEN <<1>>ELSEIF last < 15THEN 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

**References**:**How to define Hexa decimal sets/Vectors in TLA+***From:*knnik . . .

**Re: How to define Hexa decimal sets/Vectors in TLA+***From:*Andrew Helwer

- Prev by Date:
**Re: [tlaplus] How to run models on different modules in the same Spec** - Next by Date:
**How does TLC decide the location to report for an action?** - Previous by thread:
**Re: How to define Hexa decimal sets/Vectors in TLA+** - Next by thread:
**TLATeX** - Index(es):