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.