Beginner Question: Working with the Prisoners Example

49 views
Skip to first unread message

hans...@gmail.com

unread,
Oct 14, 2019, 7:04:15 PM10/14/19
to tlaplus
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

I then modified the constants in the model as follows:

Capture.PNG





















When running the model I get the following NullPointerException error with no error trace:




Capture2.PNG
How would I go about debugging this? I've tried different values for the constants (integers, strings) and still get a similar issue. Is anyone able to reproduce this?
Thanks,Hans   

Markus Kuppe

unread,
Oct 14, 2019, 7:26:47 PM10/14/19
to tla...@googlegroups.com
On 14.10.19 16:03, hans...@gmail.com 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
DisableProfiler.gif

Hans He

unread,
Oct 15, 2019, 1:12:03 PM10/15/19
to tla...@googlegroups.com
Got it, the model ran successfully after turning off profiling. Thanks!

Hans
> --
> 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+u...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4b8330db-67df-b14e-60ba-248fe3a96c7d%40lemmster.de.



--
Hans He
Reply all
Reply to author
Forward
0 new messages