Beginner Question: Working with the Prisoners Example

[hans...@gmail.com]

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:

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

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]

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

[Hans He]

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