Re: [tlaplus] Beginner Question: Working with the Prisoners Example

[Hans He <hansjhe2@xxxxxxxxx>]

Got it, the model ran successfully after turning off profiling. Thanks!

Hans

On Mon, Oct 14, 2019 at 7:26 PM Markus Kuppe
<tlaplus-google-group@xxxxxxxxxxx> wrote:
>
> On 14.10.19 16:03, hansjhe2@xxxxxxxxx wrote:
> > Hi,
> >
> > I'm attempting to run the Prisoners example on the TLA+ Toolbox to
> > understand how to use TLA+ and TLC. I've copied the Prisoners spec
> > verbatim from
> > here: https://github.com/tlaplus/Examples/blob/master/specifications/Prisoners/Prisoners.tla
> >
> > [...]
>
> Hi,
>
> this is no error of yours but a bug in TLC.  For the moment please turn
> "Profiling" off in the "Feature" section of the "TLC Options" tab of the
> Model (see attached screenshot) and follow issue [1] for when a fix will
> be available.
>
> Sorry for the inconvenience,
> Markus
>
> [1] https://github.com/tlaplus/tlaplus/issues/377
>
> --
> You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
> To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/xu-bB-FJP4g/unsubscribe.
> To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4b8330db-67df-b14e-60ba-248fe3a96c7d%40lemmster.de.



-- 
Hans He

-- 
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/CAA9hw3oMaHDv1bJDtMatGqos-cms-PC01Lbbecu4OA_k33j%3D7g%40mail.gmail.com.