[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Beginner Question: Working with the Prisoners Example


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?

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/f45d74d3-f072-47a2-907a-019040899fc2%40googlegroups.com.