[tlaplus] Issues with seeing error trace and enabling Deadlock setting

[Varun Gandhi <varungandhi15@xxxxxxxxx>]

Hi folks. To get started, I'm tried running the basic example from https://learntla.com/introduction/example/.

    ---- MODULE example ----
    EXTENDS Naturals, TLC

    (* --algorithm transfer
    variables alice_account = 10, bob_account = 10, money \in 1..20;

    begin
    A: alice_account := alice_account - money;
    B: bob_account := bob_account + money;
    C: assert alice_account >= 0;
    end algorithm *)
    =====

Save that to `example.tla`, compile the PlusCal to TLA+, create an empty model and run that model. I do see a similar error but I don't see any error trace as shown in the screenshot here: https://imgur.com/a/AzCEe0a.

Is it because of some misconfiguration? Any suggestions for debugging?

Configuration information: Ubuntu 20.04 LTS, v1.7.0 Aristotle zip from https://github.com/tlaplus/tlaplus/releases/, running javac/JDK 14.0.1.

As an alternative, I did try v1.6.0 Zenobius and that does show the error trace OK, so I'm going to use that for now.

I also noticed that the "Deadlock" box on the Model Overview screen is unchecked by default (and clicking it does nothing), unlike the macOS screenshot on learntla.com. However, I can add/select/unselect Invariants and Properties just fine. This problem seems to be present with both v1.6.0 and v1.7.0.

Varun

-- 
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/fd936683-8ff5-46d0-9e51-dac61add4b6an%40googlegroups.com.