====== Debugging and rootcausing issues ======

===== Start from the MRE =====

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 regression test =====

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?

===== Generate the state graph =====

See [[using:generating_state_graphs|generating state graphs]] page. State graphs can help visualize what’s going on.

===== Run your spec with assertion turned 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.

===== Run with debugging logs =====

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.

===== Attaching a debugger =====

To the final jar:

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

===== Eliminate randomness =====

To enanche reproducibility. Use -fp and -seed.

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

====== CustomBuild parameters ======

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

===== Running a test with a debugger =====

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

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

===== Specify number of threads =====

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

<code>
ant -f customBuild.xml test -Dthreads=4
</code>

===== Halt tests when a failure is found =====

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%%''.

<code>
ant -f customBuild.xml test -Dtest.halt=true
</code>