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

[Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx>]

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

-- 
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/d40e269e-2625-a412-a6e3-38bf5cd06182%40lemmster.de.