| Hello, I understand the idea but your definitions do not express what you think they do. (Did you at all play with the Toolbox, which lets you evaluate constant expressions, to test your spec?) You intend to express characters as sequences of bits, and sequences are indeed functions. However, in TLA+, functions are not represented as sets of pairs, so you cannot combine functions using set union or set enumeration. I recommend writing, for example, UTF8_1B == { s \in [ 0 .. 7 -> BIT] : s[0] = 0 } You may also use the :> and @@ operators defined in the TLC standard module for constructing elementary functions and for combining functions, as in UTF8_B234 == { (0 :>1) @@ (1 :> 0) @@ s : s \in [ 2..7 -> BIT ] } Follow up question is there better way to express this repeating pattern: See above how to write what you mean using :> and @@. Alternatively, you could write [ i \in 0..4 |-> IF i=4 THEN 0 ELSE 1 ] And indeed, if you decided to index your bit sequences from 1 instead of from 0, you could use standard TLA+ sequences and write <<1,1,1,0>>. The definition above could similarly be written as UTF8_B234 == { <<1,0>> @ s : s \in [ 1 .. 6 -> BIT ] } Hope this helps, Stephan
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/FFD21116-84CC-4C58-8E39-9005C891E80A%40gmail.com. |