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.