Re: Trouble replicating figure 1-5 of _Practical TLA+

variables
...
amount = 1..6;

...

Withdraw:
acc[sender] := acc[sender] - amount;

The statement labeled "Withdraw" is subtracting the interval 1..6 from the value acc[sender]. Perhaps the variable declaration should have "\in" instead of "="?

On Saturday, November 3, 2018 at 2:08:14 PM UTC-7, Alex Coventry wrote:

I started working through Wayne's book _Practical TLA+_, and I'm having trouble getting the error message shown in figure 1-5. Here is the PlusCal code I'm using, from pp. 12-13:
EXTENDS Integers
(*--algorithm wire
variables
people = {"alice", "bob"},
acc = [p \in people |-> 5],
sender = "alice",
receiver = "bob",
amount = 1..6;
define
NoOverdrafts == \A p \in people: acc[p] >= 0
end define;
begin
Withdraw:
acc[sender] := acc[sender] - amount;
Deposit:
acc[receiver] := acc[receiver] + amount;
end algorithm;*)
I've added NoOverdrafts to the invariants of an otherwise unchanged model, as described in the book. When I hit the "play" button, I do get an error, but it is much less legible than the one in the book:
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 apply the operator overridden by the Java method
public static tlc2.value.IntValue tlc2.module.Integers.Minus(tlc2.value.IntValue,tlc2.value.IntValue),
but it produced the following error:
Cannot cast tlc2.value.IntervalValue to tlc2.value.IntValue

The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 38, column 13 to line 41, column 63 in wire
1. Line 38, column 16 to line 38, column 30 in wire
2. Line 39, column 16 to line 39, column 67 in wire
3. Line 39, column 23 to line 39, column 67 in wire
4. Line 39, column 47 to line 39, column 66 in wire
Figure 1-5 in the book has "invariant NoOverdrafts is violated" in the same error box, and "<Action line 40, cc State (num = 2)>" in the Error-Trace box, which is explicit about the failure with amount=6. In my output, there's only an "<initial predicate>" stanza in the Error-Trace box, and just has amount=1..6.
In case it's relevant, I'm running TLAToolbox-1.5.7-linux.gtk.x86_64.zip on ubuntu 18.04.1 with the default-jre package, which is resolving to openjdk-8-jre.
I can move on with the book... It's pretty clear what it's describing, here. But it would be nice to get the better error messages described in the book on my own machine, and I'd welcome any suggestions towards that.
Best regards,
Alex

Re: Trouble replicating figure 1-5 of _Practical TLA+_