this derivation will be built:
  /nix/store/y4fxypap8whi7v7gvgxw88irnr4hbnv9-spec-refute-hubBlock.drv
building '/nix/store/y4fxypap8whi7v7gvgxw88irnr4hbnv9-spec-refute-hubBlock.drv'
spec-refute-hubBlock> tribuchet: building on jamie
spec-refute-hubBlock> An example execution:
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 0]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 0,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: true,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set(),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 0,
spec-refute-hubBlock>   hubBlock::relay::pending: Set(),
spec-refute-hubBlock>   hubBlock::relay::phase: Init,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set(),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 0,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 1]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 1,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set("a", "b", "c"), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: true,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set(),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 0,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set(),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 0,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 2]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 0,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set(),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 0,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set(),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 0,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 3]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 0,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set("a", "b"),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set(),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 0,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set(),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 0,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 4]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 0,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set("a", "b"),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 0,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set(),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Man, 1 -> Nil, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 1,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "c", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 5]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 0,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("b"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 0,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set(),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Man, 1 -> Nil, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 1,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "c", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 6]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 1,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("b"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 1,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 0,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 7]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 1,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("b"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 1,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Other, 1 -> Nil, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 1,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 8]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 1,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("b", "c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 1,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Other, 1 -> Man, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 2,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "b", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 9]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 1,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("b", "c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 1,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Other, 1 -> Man, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 2,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "b", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 10]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 1,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("b", "c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 1,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Other, 1 -> Man, 2 -> Other),
spec-refute-hubBlock>   hubBlock::relay::wLen: 3,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "b", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 11]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 1,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("b", "c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 1,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Man, 1 -> Other, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 2,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 12]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::hLen: 1,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("b", "c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 1,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set("c"),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Man, 1 -> Other, 2 -> Other),
spec-refute-hubBlock>   hubBlock::relay::wLen: 3,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 13]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set("b"), 3 -> Set("b", "c")),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(3), 1 -> Set(2)),
spec-refute-hubBlock>   hubBlock::relay::hLen: 2,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("b", "c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 2,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set("b", "c"),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Other, 1 -> Other, 2 -> Nil),
spec-refute-hubBlock>   hubBlock::relay::wLen: 2,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [State 14]
spec-refute-hubBlock> {
spec-refute-hubBlock>   hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set("b"), 3 -> Set("b", "c")),
spec-refute-hubBlock>   hubBlock::relay::hHashes: Map(0 -> Set(3), 1 -> Set(2)),
spec-refute-hubBlock>   hubBlock::relay::hLen: 2,
spec-refute-hubBlock>   hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::have: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubComputing: Set(),
spec-refute-hubBlock>   hubBlock::relay::hubErr: false,
spec-refute-hubBlock>   hubBlock::relay::hubFirstNeed: false,
spec-refute-hubBlock>   hubBlock::relay::hubOutbox: Set("a"),
spec-refute-hubBlock>   hubBlock::relay::hubSent: Set("b", "c"),
spec-refute-hubBlock>   hubBlock::relay::imported: Set(),
spec-refute-hubBlock>   hubBlock::relay::inline: Set(),
spec-refute-hubBlock>   hubBlock::relay::outstanding: 2,
spec-refute-hubBlock>   hubBlock::relay::pending: Set("a", "b", "c"),
spec-refute-hubBlock>   hubBlock::relay::phase: Staging,
spec-refute-hubBlock>   hubBlock::relay::qHashes:
spec-refute-hubBlock>     Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::qLen: 0,
spec-refute-hubBlock>   hubBlock::relay::recipes: Set("b", "c"),
spec-refute-hubBlock>   hubBlock::relay::rounds: 0,
spec-refute-hubBlock>   hubBlock::relay::store: Set(),
spec-refute-hubBlock>   hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),
spec-refute-hubBlock>   hubBlock::relay::wKind: Map(0 -> Other, 1 -> Other, 2 -> Other),
spec-refute-hubBlock>   hubBlock::relay::wLen: 3,
spec-refute-hubBlock>   hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")
spec-refute-hubBlock> }
spec-refute-hubBlock> 
spec-refute-hubBlock> [violation] Found an issue (1571ms at 30551 traces/second).
spec-refute-hubBlock> Use --verbosity=3 to show executions.
spec-refute-hubBlock> Use --seed=0xbc68b06630779263 --backend=rust to reproduce.
spec-refute-hubBlock> error: Invariant violated

post-build step Upload coverage to codecov: ok
Skipping codecov: project=Mic92/tribuchet attr=checks.x86_64-linux.spec-refute-hubBlock