tribuchet: building on jamie
An example execution:

[State 0]
{
  hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::hLen: 0,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set(),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: true,
  hubBlock::relay::hubOutbox: Set(),
  hubBlock::relay::hubSent: Set(),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 0,
  hubBlock::relay::pending: Set(),
  hubBlock::relay::phase: Init,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set(),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
  hubBlock::relay::wLen: 0,
  hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 1]
{
  hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::hLen: 1,
  hubBlock::relay::hPaths: Map(0 -> Set("a", "b", "c"), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set(),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: true,
  hubBlock::relay::hubOutbox: Set(),
  hubBlock::relay::hubSent: Set(),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 0,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set(),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
  hubBlock::relay::wLen: 0,
  hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 2]
{
  hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::hLen: 0,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set("a", "b", "c"),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set(),
  hubBlock::relay::hubSent: Set(),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 0,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set(),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
  hubBlock::relay::wLen: 0,
  hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 3]
{
  hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::hLen: 0,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set("b", "c"),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set("a"),
  hubBlock::relay::hubSent: Set(),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 0,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set(),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
  hubBlock::relay::wLen: 0,
  hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 4]
{
  hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::hLen: 0,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set("b", "c"),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set(),
  hubBlock::relay::hubSent: Set("a"),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 0,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set(),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Man, 1 -> Nil, 2 -> Nil),
  hubBlock::relay::wLen: 1,
  hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 5]
{
  hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),
  hubBlock::relay::hLen: 1,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set("b", "c"),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set(),
  hubBlock::relay::hubSent: Set("a"),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 1,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set("a"),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
  hubBlock::relay::wLen: 0,
  hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 6]
{
  hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),
  hubBlock::relay::hLen: 1,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set("c"),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set("b"),
  hubBlock::relay::hubSent: Set("a"),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 1,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set("a"),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
  hubBlock::relay::wLen: 0,
  hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 7]
{
  hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),
  hubBlock::relay::hLen: 1,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set("c"),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set(),
  hubBlock::relay::hubSent: Set("a", "b"),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 1,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set("a"),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Man, 1 -> Nil, 2 -> Nil),
  hubBlock::relay::wLen: 1,
  hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")
}

[State 8]
{
  hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),
  hubBlock::relay::hLen: 1,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set("c"),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set(),
  hubBlock::relay::hubSent: Set("a", "b"),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 1,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set("a"),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Man, 1 -> Other, 2 -> Nil),
  hubBlock::relay::wLen: 2,
  hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")
}

[State 9]
{
  hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),
  hubBlock::relay::hLen: 1,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set("c"),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set(),
  hubBlock::relay::hubSent: Set("a", "b"),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 1,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set("a"),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Man, 1 -> Other, 2 -> Other),
  hubBlock::relay::wLen: 3,
  hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")
}

[State 10]
{
  hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),
  hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),
  hubBlock::relay::hLen: 1,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set(),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set("c"),
  hubBlock::relay::hubSent: Set("a", "b"),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 1,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set("a"),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Man, 1 -> Other, 2 -> Other),
  hubBlock::relay::wLen: 3,
  hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")
}

[State 11]
{
  hubBlock::relay::awaiting:
    Map(1 -> Set("a"), 2 -> Set("a", "b"), 3 -> Set("b")),
  hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set(3)),
  hubBlock::relay::hLen: 2,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set(),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set("c"),
  hubBlock::relay::hubSent: Set("a", "b"),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 2,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set("a", "b"),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Other, 1 -> Other, 2 -> Nil),
  hubBlock::relay::wLen: 2,
  hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[State 12]
{
  hubBlock::relay::awaiting:
    Map(1 -> Set("a"), 2 -> Set("a", "b"), 3 -> Set("b")),
  hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set(3)),
  hubBlock::relay::hLen: 2,
  hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
  hubBlock::relay::have: Set(),
  hubBlock::relay::hubComputing: Set(),
  hubBlock::relay::hubErr: false,
  hubBlock::relay::hubFirstNeed: false,
  hubBlock::relay::hubOutbox: Set("c"),
  hubBlock::relay::hubSent: Set("a", "b"),
  hubBlock::relay::imported: Set(),
  hubBlock::relay::inline: Set(),
  hubBlock::relay::outstanding: 2,
  hubBlock::relay::pending: Set("a", "b", "c"),
  hubBlock::relay::phase: Staging,
  hubBlock::relay::qHashes:
    Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
  hubBlock::relay::qLen: 0,
  hubBlock::relay::recipes: Set("a", "b"),
  hubBlock::relay::rounds: 0,
  hubBlock::relay::store: Set(),
  hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
  hubBlock::relay::wKind: Map(0 -> Other, 1 -> Other, 2 -> Other),
  hubBlock::relay::wLen: 3,
  hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
}

[violation] Found an issue (1104ms at 42581 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x69f7b1f81455c0bc --backend=rust to reproduce.
error: Invariant violated