[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Trouble replicating figure 1-5 of _Practical TLA+_

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
     people = {"alice", "bob"},
     acc = [p \in people |-> 5],
     sender = "alice",
     receiver = "bob",
     amount = 1..6;
     NoOverdrafts == \A p \in people: acc[p] >= 0
    end define;
     acc[sender] := acc[sender] - amount;
     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,