Re: [tlaplus] Division in action expression

[Markus Kuppe <tlaplus-go...@xxxxxxxxxxx>]

On 05.10.2018 14:58, Nipun sehrawat wrote:
> 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
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