DieHardest: compare jug configurations via parallel and interleaved self-composition

[lemmy]

Add DieHardest.tla, which composes two instances of DieHarder to compare which configuration has the shorter path to the Goal (state).

Four composition approaches are contrasted in clearly labeled sections that progressively motivate interleaved composition:

1. Parallel — shows that BFS finds the shortest path for the slower configuration but not the faster one.
2. Parallel + "per-behavior freeze" — shows that freezing after reaching the Goal does not help.
3. Parallel + "global BFS-level freeze" — correct, but relies on TLC-specific operators.
4. Interleaved — each instance steps independently, so BFS minimizes both step counts.

[lemmy]

@hwayne Could you please review this example? It references your “Hypermodeling Hyperproperties” article.

[hwayne]

Also, unless things changed recently, TLC global registers are local to each worker

[lemmy]

Indeed, this would also only work with a single worker.

[hwayne]

These solutions depend on two assumptions: that the states are searched with BFS, and that the BFS is strict. The first is violated with the -depth and -simulate parameters. I've seen the second be violated when using multiple workers:

1. worker 1 picks the last state of length N on the queue
2. worker 2 picks the first state of length N+1
3. Both workers are evaluating a state that violates an invariant, but
4. worker 2 reaches the violation before worker 1 does.

It's pretty rare, but I've seen it happen!

A robust and universal TLA+ spec would probably have to store the diehard traces as data values and implement Dijkstra's algorithm to find the shortest path, with the property that <>[](shortest_c1 <= shortest_c2).

[lemmy]

These solutions depend on two assumptions: that the states are searched with BFS, and that the BFS is strict. The first is violated with the -depth and -simulate parameters. I've seen the second be violated when using multiple workers:

1. worker 1 picks the last state of length N on the queue
2. worker 2 picks the first state of length N+1
3. Both workers are evaluating a state that violates an invariant, but
4. worker 2 reaches the violation before worker 1 does.

It's pretty rare, but I've seen it happen!

A robust and universal TLA+ spec would probably have to store the diehard traces as data values and implement Dijkstra's algorithm to find the shortest path, with the property that <>[](shortest_c1 <= shortest_c2).

Strict BFS has in fact been an implicit assumption in the current formulation. This directly contradicts the spec's own statement: "This approach stays entirely within the logic of TLA+ and is compatible with all TLA+ tools."

Given that contradiction, what do you think about removing that statement and instead making the assumption explicit, for example:

ASSUME TLCGet("config").mode = "bfs" /\ TLCGet("config").worker = 1

In my view, the example would still offer an interesting and valuable perspective on self-composition, even with this assumption made explicit.

[hwayne]

These solutions depend on two assumptions: that the states are searched with BFS, and that the BFS is strict. The first is violated with the -depth and -simulate parameters. I've seen the second be violated when using multiple workers:

1. worker 1 picks the last state of length N on the queue
2. worker 2 picks the first state of length N+1
3. Both workers are evaluating a state that violates an invariant, but
4. worker 2 reaches the violation before worker 1 does.

It's pretty rare, but I've seen it happen!
A robust and universal TLA+ spec would probably have to store the diehard traces as data values and implement Dijkstra's algorithm to find the shortest path, with the property that <>[](shortest_c1 <= shortest_c2).

Strict BFS has in fact been an implicit assumption in the current formulation. This directly contradicts the spec's own statement: "This approach stays entirely within the logic of TLA+ and is compatible with all TLA+ tools."

Given that contradiction, what do you think about removing that statement and instead making the assumption explicit, for example:

ASSUME TLCGet("config").mode = "bfs" /\ TLCGet("config").worker = 1

In my view, the example would still offer an interesting and valuable perspective on self-composition, even with this assumption made explicit.

I think this make sense, but then section 3's main downside (only TLC) then applies to all of the specs.

[lemmy]

Added an Apalache module that, although slightly slower, produces the same counterexample for NextInterleaved as TLC. This confirms that the NextInterleaved approach is not specific to TLC.

That said, it is worth noting that TLA itself does not guarantee that a shortest counterexample will be found. Identifying shortest counterexamples is an implementation detail of particular verification tools, such as TLC and Apalache, rather than a property of the TLA language.

[lemmy]

@ahelwer This PR enhances the GitHub automation to support overriding the -workers parameter.

[ahelwer]

Nice! An alternative way to do it which is less directly bound to TLC would be to have an optional boolean parameter to the model in the manifest.json that is called something like parallelizeStateExploration. If this parameter is missing it defaults to true. Then TLC is run with either all the threads available on the machine or just in one thread. It is unlikely that someone would want to specifically run TLC in only two threads, for example. But this way you've done it is fine.