Having trouble with the final step of the first example

[axelson]

This is the specific page: https://www.learntla.com/introduction/example/

After adding in the process I'm getting the error

Attempted to apply the operator overridden by the Java method
public static tlc2.value.BoolValue tlc2.module.Naturals.GEQ(tlc2.value.Value,tlc2.value.Value),
but it produced the following error:

The first argument of > should be an integer, but instead it is:
<<1, 1>>

While working on the initial state:
/\ bob_account = 10
/\ money = <<1, 1>>
/\ alice_account = 10
/\ pc = <<"Transfer_", "Transfer_">>
/\ account_total = 20

The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 29, column 9 to line 34, column 50 in transfer
1. Line 29, column 12 to line 29, column 29 in transfer
2. Line 30, column 12 to line 30, column 27 in transfer
3. Line 31, column 12 to line 31, column 54 in transfer
... Omitted for brevity ...
1597. Line 34, column 17 to line 34, column 50 in transfer
1598. Line 34, column 27 to line 34, column 33 in transfer
1599. Line 34, column 39 to line 34, column 49 in transfer

Here is my full tla file:

---- MODULE transfer ----
EXTENDS Naturals, TLC

(* --algorithm transfer
variables alice_account = 10, bob_account = 10,
          account_total = alice_account + bob_account;

process Transfer \in 1..2
  variable money \in 1..20;
begin
Transfer:
  if alice_account >= money then
    A: alice_account := alice_account - money;
       bob_account := bob_account + money;
end if;
C: assert alice_account >= 0;
end process

end algorithm *)
\* BEGIN TRANSLATION
\* Label Transfer of process Transfer at line 12 col 3 changed to Transfer_
VARIABLES alice_account, bob_account, account_total, pc, money

vars == << alice_account, bob_account, account_total, pc, money >>

ProcSet == (1..2)

Init == (* Global variables *)
        /\ alice_account = 10
        /\ bob_account = 10
        /\ account_total = alice_account + bob_account
        (* Process Transfer *)
        /\ money \in [1..2 -> 1..20]
        /\ pc = [self \in ProcSet |-> "Transfer_"]

Transfer_(self) == /\ pc[self] = "Transfer_"
                   /\ IF alice_account >= money[self]
                         THEN /\ pc' = [pc EXCEPT ![self] = "A"]
                         ELSE /\ pc' = [pc EXCEPT ![self] = "C"]
                   /\ UNCHANGED << alice_account, bob_account, account_total, 
                                   money >>

A(self) == /\ pc[self] = "A"
           /\ alice_account' = alice_account - money[self]
           /\ bob_account' = bob_account + money[self]
           /\ pc' = [pc EXCEPT ![self] = "C"]
           /\ UNCHANGED << account_total, money >>

C(self) == /\ pc[self] = "C"
           /\ Assert(alice_account >= 0, 
                     "Failure of assertion at line 16, column 4.")
           /\ pc' = [pc EXCEPT ![self] = "Done"]
           /\ UNCHANGED << alice_account, bob_account, account_total, money >>

Transfer(self) == Transfer_(self) \/ A(self) \/ C(self)

Next == (\E self \in 1..2: Transfer(self))
           \/ (* Disjunct to prevent deadlock on termination *)
              ((\A self \in ProcSet: pc[self] = "Done") /\ UNCHANGED vars)

Spec == Init /\ [][Next]_vars

Termination == <>(\A self \in ProcSet: pc[self] = "Done")

\* END TRANSLATION

MoneyNotNegative == money >= 0
MoneyInvariant == alice_account + bob_account = account_total

====

Is there some sort of problem in how I wrote my specification?

[hwayne]

No, it looks like a mistake in how I wrote the tutorial. money becomes a pair of values, so money >= 0 becomes nonsensical. Do you have MoneyNotNegative still listed as a checked invariant?

The fact the error trace is 1600 lines is super weird and might be a bug in the toolbox. I'm trying to make a minimum-spanning example right now. It doesn't seem to change the behavior, though, just how errors are presented.

[axelson]

Thanks for the response! Yes I still have the MoneyNotNegative checked. Removing it does kind of fix the error, or at least now I can get an actual "successful" error-trace.

But I still have the following error:

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 tlc2.tool.EvalException
: 
Attempted to apply the operator overridden by the Java method
public static tlc2.value.Value tlc2.module.TLC.Assert(tlc2.value.Value,tlc2.value.Value),
but it produced the following error:

The first argument of Assert evaluated to FALSE; the second argument was:
"Failure of assertion at line 16, column 4."

The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 49, column 12 to line 53, column 78 in transfer
1. Line 49, column 15 to line 49, column 28 in transfer
2. Line 50, column 15 to line 51, column 66 in transfer

But I think I was getting that for nearly every run I've done so far.

[hwayne]

Hm, you should be getting something along the lines of "MoneyInvariant violated".

checks tutorial again

...I also forgot to specify that you're supposed to add "MoneyInvariant" as an invariant.

Well that's two things to fix now!

[hwayne]

Error trace bug added to TLA+ repo: https://github.com/tlaplus/tlaplus/issues/132

Gonna fix tutorial tomorrow morning. Let me know if you run into any other issues with this, and sorry for the roadblocks :(

[axelson]

Are you sure MoneyInvariant is supposed to be invalidated on this step? Even in your screenshot it looks like the error is that Alice's account goes negative.

I'm still confused about the TLC threw an unexpected exception. "error". But perhaps it seems that I should expect that message whenever TLC finds an error in my specification (plus it is included in your screenshot as well)? If so than I think that is confusing UX for me.

[hwayne]

Yup you're right and I'm wrong. It's been a while since I wrote the tutorial so any confusion is on me.

Tla+ shows that dump if an assert fails, which is definitely a usability issue. For invariants, though, it should just say "invariant FOO violated" and not an exception.

On Sun, Jan 7, 2018, 12:46 PM Jason Axelson notifications@github.com wrote:

Are you sure MoneyInvariant is supposed to be invalidated on this step? Even in your screenshot it looks like the error is that Alice's account goes negative.

I'm still confused about the TLC threw an unexpected exception. "error". But perhaps it seems that I should expect that message whenever TLC finds an error in my specification (plus it is included in your screenshot as well)? If so than I think that is confusing UX for me.

— You are receiving this because you commented.

Reply to this email directly, view it on GitHub https://github.com/hwayne/learntla/issues/47#issuecomment-355843197, or mute the thread https://github.com/notifications/unsubscribe-auth/ACiXdLZHYFtud6_CXCT3L2fSYvQNiA1yks5tIREegaJpZM4RVN5C .

[axelson]

Great, thanks!