Video Tutorial Series Lecture 4

Ravi Shankar

unread,

May 27, 2022, 8:43:49 AM5/27/22

to tlaplus

I was following along on the Die Hard 4 Gallon problem. What I noticed with my version (details below) is that when I invoke the model checker with both the invariant conditions, I see error notification but I can't see the errors details screen as was shown in the video. I am on Mac Catalina 10.15.7 version. The tool details are given below as I gathered from about toolbox dialog

TLA+ Toolbox provides a user interface for TLA+ Tools.

This is Version 1.7.1 of 31 December 2020 and includes:
- SANY Version 2.2 of 20 April 2020
- TLC Version 2.16 of 31 December 2020
- PlusCal Version 1.11 of 31 December 2020
- TLATeX Version 1.0 of 20 September 2017

Any suggestions?

Thanks in advance.

Markus Kuppe

unread,

May 27, 2022, 10:37:04 AM5/27/22

to tla...@googlegroups.com

Hi Ravi,

what happens if you click on the “Error” notification on the model editor’s result page?

Markus

Ravi Shankar

unread,

May 28, 2022, 7:20:36 AM5/28/22

to tlaplus

Markus,

Nothing shows up when I click the errors link.

Ravi

Sean Peisert

unread,

Jul 18, 2022, 4:24:00 PM7/18/22

to tlaplus

I see the same issue.

Sean

Sean Peisert

unread,

Jul 18, 2022, 4:34:23 PM7/18/22

to tla...@googlegroups.com

Typo on my part; apologies. It is now working.

Sean

> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/818b4a5d-8a9d-4050-a240-c7e2fc728677n%40googlegroups.com.

Reply all

Reply to author

Forward