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 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/4b8330db-67df-b14e-60ba-248fe3a96c7d%40lemmster.de.
Attachment:
DisableProfiler.gif
Description: GIF image
