Re: [tlaplus] Video Tutorial Series Lecture 4

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

Hi Ravi,

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

Markus

> On May 27, 2022, at 5:43 AM, Ravi Shankar <sankarsana@xxxxxxxxx> wrote:
> 
> 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.

-- 
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/3DA58A1C-3CA7-4FA7-8DB9-BA2376AFDDD8%40lemmster.de.