Division in action expression

[Nipun sehrawat]

Hello,

I am learning TLA+ and trying to write a spec for the weight-throwing algorithm described in: https://ieeexplore.ieee.org/document/37933.

I wrote this simple spec for checking if TLC allows division in an action expression:

----------------------------- MODULE WeightThrowing ----------------------------

EXTENDS Reals

VARIABLES count

VARIABLES num

Init == /\ num = 1

        /\ count = 0

Next == /\ num' = num / 2

        /\ count' = count + 1

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

As expected, TLC didn't like this spec (perhaps because TLC doesn't support arbitrary precision arithmetic?). Here is the error I get:

TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.

See the User Output or TLC Console for clues to what happened.

The exception was a java.lang.RuntimeException

: Attempted to compute the value of an expression of

form CHOOSE x \in S: P, but S was not enumerable.

line 16, col 10 to line 16, col 38 of module Reals

The error occurred when TLC was evaluating the nested

expressions at the following positions:

0. Line 11, column 9 to line 12, column 29 in WeightThrowing

1. Line 11, column 12 to line 11, column 25 in WeightThrowing

2. Line 11, column 19 to line 11, column 25 in WeightThrowing

3. Line 16, column 10 to line 16, column 38 in Reals

Any suggestions around how to express a weight throwing algorithm in TLA+?  I basically want the ability to split a weight, W, into two parts, W1 and W2, such that W1+W2=W.  The splitting will happen multiple times as the system state evolves.  Additionally, the initial value of W should be 1.

Thank you,

Nipun

[Markus Kuppe]

Hi Nipun,

since you want to learn TLA+, the pragmatic approach is to move on and
select an algorithm that does not require Reals. For termination
detection, you could look at EWD840 for which there exist a TLA+
specification [1] to even compare your spec with.

If you want to stick to this particular algorithm, you can obviously
model floating point arithmetic for arbitrary exponent and mantissa
sizes explicitly and model check it for small numbers of bits. This is
likely beyond what you are interested in.

Lastly, you can use a module override [2] to hack division into TLC.
This concept is not well suited for beginners.

Thanks
Markus

[1]
https://github.com/tlaplus/Examples/blob/master/specifications/ewd840/EWD840.tla
[2] https://groups.google.com/forum/#!topic/tlaplus/nxPorb4_BGg

[tlaplus-go...@lemmster.de]

https://github.com/tlaplus/Examples/tree/master/specifications/Huang is a spec of Huang’s weight-throwing algorithm.

Markus

[Abhishek Verma]

Hi Markus,

Thank you for writing a clear spec for Huang's algorithm. I learned a few TLA+ features from it.

I tried executing the spec in TLA+ toolbox, but I got an error message that the DyadicRationals module could not be found. Where can I find the DyadicRationals module used in the spec? I could not find it on Google or in the Community modules: https://github.com/tlaplus/CommunityModules.

Thanks!

-Abhishek.

--
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...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/A85FA054-FF3F-400B-B90C-41CA073E9AEC%40lemmster.de.

[tlaplus-go...@lemmster.de]

Hi Abhishek,

we have plans to eventually move DyadicRationals to the CommunityModules [1], but for now the module is part of the examples [2].

Markus

[1] https://github.com/tlaplus/CommunityModules/issues/63

[2] https://github.com/tlaplus/Examples/blob/master/specifications/Huang/DyadicRationals.tla

[Abhishek Verma]

Thanks Markus. I was able to check the spec in TLA now. Sorry I missed that the DyadicRationals module was right next to the Huang specification.

I am trying to use the ALIAS feature in the generated State Graph visualization, but it doesn't seem to pretty-print it in the TLA+ toolbox UI.

I tried the command-line option to dump a dot file: 

$ java -jar tla2tools.jar Huang -deadlock -dump dot h.dot

But it does not contain the pretty-printed text either. 

Is this a missing feature?

Thanks!

-Abhishek.

--
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...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/25A2EC78-0CC5-416E-81D4-8DC450F0C77C%40lemmster.de.

[tlaplus-go...@lemmster.de]

Hi Abhishek,

the Alias feature is only evaluated when TLC prints traces.  The state graph visualization indeed ignores an Alias.  It wouldn't be impossible to add this feature, but I'm not convinced it's worth the effort.

Markus 

On Jan 28, 2022, at 6:25 PM, Abhishek Verma <vermaab...@gmail.com> wrote:

[…]