Issues with seeing error trace and enabling Deadlock setting

[Varun Gandhi]

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

[Markus Kuppe]

Hi Varun,

please use a recent nightly build [1] to get the fix for the missing
error-trace [2].

As to the Deadlock button, this appears to be an incompatibility with
(some of) the Gnome themes in Ubuntu 20.04. The visual difference
between a button being checked and unchecked is minimal. Unfortunately,
we don't have a workaround or fix yet.

Markus

[1] http://nightly.tlapl.us/products/
[2] https://github.com/tlaplus/tlaplus/issues/461

[Martin Harrison]

Do you know which of the Gnome themes make the check mark in the Deadlock button visible?

I can see that check mark, but only when the TLA+ theme is Dark (which is not ideal, because then the values in the states presented in the Error Trace are very hard to see).

[Markus Kuppe]

On 09.12.20 04:48, Martin Harrison wrote:
> Do you know which of the Gnome themes make the check mark in the
> Deadlock button visible?
>
> I can see that check mark, but only when the TLA+ theme is Dark (which
> is not ideal, because then the values in the states presented in the
> Error Trace are very hard to see).

Hi,

it looks fine here with the "Radiance" theme. I also disable theming in
the preferences (screenshot shows it enabled).

Markus