[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Beginner Question: Working with the Prisoners Example
Got it, the model ran successfully after turning off profiling. Thanks!
On Mon, Oct 14, 2019 at 7:26 PM Markus Kuppe
> 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
> > [...]
> 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  for when a fix will
> be available.
> Sorry for the inconvenience,
>  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.
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.