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).
On Monday, August 17, 2020 at 9:53:20 AM UTC-5 Markus Alexander Kuppe wrote:
On 15.08.20 17:08, Varun Gandhi wrote:
> 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
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