minimal trace mode

[Smattr]

When bringing up a model, you typically want to run with max errors 1 and multithreaded but also get a minimal trace. This is not currently possible but we could implement this by not actually signaling an error until all other threads have exceeded the depth at which the error was found.

[Smattr]

After some protracted debugging, I realised there's a fundamental blocker to implementing this. Because of the way multithreaded exploration works, the first time a state is encountered it is not guaranteed to be found via the shortest path. E.g. consider the following FSM:

A -> B -> C
 \        ^
  \______/

Thread 0 might discover C first via the path A -> B -> C. Later thread 1 might rediscover C via the path A -> C. Thread 1 will notice its C is a duplicate and discard it. Now any error path involving C will trace back through the A -> B prefix rather than simply A.

There are a couple of ways I can think of solving this, neither of them good:

1. When de-duping against an existing state, update its previous pointer (or depth member) if the duplicate has a shorter path. This introduces pointer chasing overhead in the case where we don't have a depth member as well as some interesting race conditions with updating a pointer that may be being walked elsewhere.
2. Synchronise at the end of expanding each depth. This introduces an otherwise-unnecessary blocking condition and would need some careful interaction with rendezvous to avoid a deadlock. The advantage of this approach is that it guarantees we find the shortest path first, instead of having to juggle to fix this up later.

Bottom line, both of these introduce unacceptable overhead. I think we either need a third option or give up on this feature.