TLC unexpected exception

[Zeinab Nehaï]

Hello everyone,

I am a PhD student, and I use the TLA+ tool to apply verification methods to my distributed model. I encountered a problem when I ran the TLC model checker, and although I researched the reason for this error, I did not find anything.
My model represents a system with senders and recipients, and there may be Byzantines. Therefore, my study aims not to increase or decrease the number of processes but to vary the share of Byzantines processes in my system and check if my liveness properties are still valid.
I don't know if giving details of my model is necessary to understand my problem, but if it is, please let me know.
So, I run TLC on a docker using :

java -cp tla2tools.jar tlc2.TLC -nowarning -deadlock -workers 30 model.tla.
Runs with a small number of Byzantine processes are not a problem, and TLC manages to finish.
However, I got the following error with one correct process and five Byzantine processes after 10 hours of running.

Error: TLC threw an unexpected exception.

This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.io.EOFException
java.io.EOFException
at java.base/java.io.RandomAccessFile.readInt(RandomAccessFile.java:837)
at java.base/java.io.RandomAccessFile.readLong(RandomAccessFile.java:870)
at tlc2.util.BitVector.read(BitVector.java:216)
at tlc2.tool.liveness.GraphNode.read(GraphNode.java:388)
at tlc2.tool.liveness.AbstractDiskGraph.getNodeFromDisk(AbstractDiskGraph.java:246)
at tlc2.tool.liveness.AbstractDiskGraph.getNode(AbstractDiskGraph.java:225)
at tlc2.tool.liveness.LiveWorker.checkSccs(LiveWorker.java:351)
at tlc2.tool.liveness.LiveWorker.call(LiveWorker.java:1257)
at tlc2.tool.liveness.LiveWorker.call(LiveWorker.java:41)
at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
at java.base/java.util.concurrent.Executors$RunnableAdapter.call(Executors.java:515)
at java.base/java.util.concurrent.FutureTask.run(FutureTask.java:264)
at java.base/java.util.concurrent.ThreadPoolExecutor.runWorker(ThreadPoolExecutor.java:1128)
at java.base/java.util.concurrent.ThreadPoolExecutor$Worker.run(ThreadPoolExecutor.java:628)
at java.base/java.lang.Thread.run(Thread.java:829)

Could you please help with this error and tell me what it means? I have the last version of TLC, and the docker has enough memory.

Thank you for your help,

Zeinab

[tlaplus-go...@lemmster.de]

Hi Zeinab,

is it possible that you ran out of disk space? If that's not it, please open a Github issue at https://github.com/tlaplus/tlaplus/issues/.

Markus