Minimum Reproducible Example. Often, if you can get one half of your problem is solved. This is why is so important to provide one when creating issues. The smaller the state graph needed to reproduce the issue, the better.

Write a test, and make sure it fails. After your fix is applied, the test should start passing again. When writing the regression test, make sure to think what could happen if you have multiple workers involved. Do you need to test that as well?

See generating state graphs page. State graphs can help visualize what’s going on.

TLC has a -ea option that will enable some assertions in the code. It might be able to help catching some edge case hit by your code.

I don’t find these particular helpful, but it’s worth trying. Run tlc with -debug on and you will get additional debug logs in output.

To the final jar:

java -agentlib:jdwp=transport=dt_socket,server=y,suspend=y,address=*:5005 -jar ./dist/tla2tools.jar /tmp/genereto/Github710a.tla 

To enanche reproducibility. Use -fp and -seed.

java -jar ./dist/tla2tools.jar -lncheck final -fpmem 0.65 -fp 120 -seed -8286054000752913025  -workers 10 /tmp/genereto/Github710a.tla 

customBuild.xml supports different parameters to tune the tests. These can also be combined.

-Dtest.suspend=y will suspend the execution and give you time to hook up a debugger before running a test.

ant -f customBuild.xml compile-test test-set -Dtest.suspend=y -Dtest.testcases="tlc2/tool/InliningTest*"

By default uses all your cores. You can specify a custom amount using -Dthreads=4:

ant -f customBuild.xml test -Dthreads=4

By default the test target will run all the test and report success or failure only at the end. It can be convinient to just stop execution as soon as an error is found, with-Dtest.halt=true.

ant -f customBuild.xml test -Dtest.halt=true