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

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

Thanks to both of you. That was the issue.

On Saturday, November 3, 2018 at 7:03:06 PM UTC-4, Maneet Bansal wrote:
Hi Alex,

As Leslie pointed out, you have a typo in your spec. 

At the beginner level, It is easy to make such mistakes while typing. To debug such problems you can also use the electronic version of spec https://github.com/Apress/practical-tla-plus/blob/master/Chapter%201/wire.tla

Usually, the stack trace is very useful in narrowing down the problem to the particular line. To debug/fix the problem you can cross reference that line with the electronic version. Hope it is helpful. 

On Sat, Nov 3, 2018 at 2:33 PM Leslie Lamport <tlap...@xxxxxxxxx> wrote:
     amount = 1..6;

     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
     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,

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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

Maneet Bansal