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

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

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.


[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.