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

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

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;

    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.


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.