spec-refute-hubBlock
checks.x86_64-linux.spec-refute-hubBlock
· build #351
· raw
1tribuchet: building on jamie2An example execution:34[State 0]5{6 hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),7 hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),8 hubBlock::relay::hLen: 0,9 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),10 hubBlock::relay::have: Set(),11 hubBlock::relay::hubComputing: Set(),12 hubBlock::relay::hubErr: false,13 hubBlock::relay::hubFirstNeed: true,14 hubBlock::relay::hubOutbox: Set(),15 hubBlock::relay::hubSent: Set(),16 hubBlock::relay::imported: Set(),17 hubBlock::relay::inline: Set(),18 hubBlock::relay::outstanding: 0,19 hubBlock::relay::pending: Set(),20 hubBlock::relay::phase: Init,21 hubBlock::relay::qHashes:22 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),23 hubBlock::relay::qLen: 0,24 hubBlock::relay::recipes: Set(),25 hubBlock::relay::rounds: 0,26 hubBlock::relay::store: Set(),27 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),28 hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),29 hubBlock::relay::wLen: 0,30 hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")31}3233[State 1]34{35 hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),36 hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),37 hubBlock::relay::hLen: 1,38 hubBlock::relay::hPaths: Map(0 -> Set("a", "b", "c"), 1 -> Set()),39 hubBlock::relay::have: Set(),40 hubBlock::relay::hubComputing: Set(),41 hubBlock::relay::hubErr: false,42 hubBlock::relay::hubFirstNeed: true,43 hubBlock::relay::hubOutbox: Set(),44 hubBlock::relay::hubSent: Set(),45 hubBlock::relay::imported: Set(),46 hubBlock::relay::inline: Set(),47 hubBlock::relay::outstanding: 0,48 hubBlock::relay::pending: Set("a", "b", "c"),49 hubBlock::relay::phase: Staging,50 hubBlock::relay::qHashes:51 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),52 hubBlock::relay::qLen: 0,53 hubBlock::relay::recipes: Set(),54 hubBlock::relay::rounds: 0,55 hubBlock::relay::store: Set(),56 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),57 hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),58 hubBlock::relay::wLen: 0,59 hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")60}6162[State 2]63{64 hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),65 hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),66 hubBlock::relay::hLen: 0,67 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),68 hubBlock::relay::have: Set(),69 hubBlock::relay::hubComputing: Set("a", "b", "c"),70 hubBlock::relay::hubErr: false,71 hubBlock::relay::hubFirstNeed: false,72 hubBlock::relay::hubOutbox: Set(),73 hubBlock::relay::hubSent: Set(),74 hubBlock::relay::imported: Set(),75 hubBlock::relay::inline: Set(),76 hubBlock::relay::outstanding: 0,77 hubBlock::relay::pending: Set("a", "b", "c"),78 hubBlock::relay::phase: Staging,79 hubBlock::relay::qHashes:80 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),81 hubBlock::relay::qLen: 0,82 hubBlock::relay::recipes: Set(),83 hubBlock::relay::rounds: 0,84 hubBlock::relay::store: Set(),85 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),86 hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),87 hubBlock::relay::wLen: 0,88 hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")89}9091[State 3]92{93 hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),94 hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),95 hubBlock::relay::hLen: 0,96 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),97 hubBlock::relay::have: Set(),98 hubBlock::relay::hubComputing: Set("b", "c"),99 hubBlock::relay::hubErr: false,100 hubBlock::relay::hubFirstNeed: false,101 hubBlock::relay::hubOutbox: Set("a"),102 hubBlock::relay::hubSent: Set(),103 hubBlock::relay::imported: Set(),104 hubBlock::relay::inline: Set(),105 hubBlock::relay::outstanding: 0,106 hubBlock::relay::pending: Set("a", "b", "c"),107 hubBlock::relay::phase: Staging,108 hubBlock::relay::qHashes:109 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),110 hubBlock::relay::qLen: 0,111 hubBlock::relay::recipes: Set(),112 hubBlock::relay::rounds: 0,113 hubBlock::relay::store: Set(),114 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),115 hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),116 hubBlock::relay::wLen: 0,117 hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")118}119120[State 4]121{122 hubBlock::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),123 hubBlock::relay::hHashes: Map(0 -> Set(), 1 -> Set()),124 hubBlock::relay::hLen: 0,125 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),126 hubBlock::relay::have: Set(),127 hubBlock::relay::hubComputing: Set("b", "c"),128 hubBlock::relay::hubErr: false,129 hubBlock::relay::hubFirstNeed: false,130 hubBlock::relay::hubOutbox: Set(),131 hubBlock::relay::hubSent: Set("a"),132 hubBlock::relay::imported: Set(),133 hubBlock::relay::inline: Set(),134 hubBlock::relay::outstanding: 0,135 hubBlock::relay::pending: Set("a", "b", "c"),136 hubBlock::relay::phase: Staging,137 hubBlock::relay::qHashes:138 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),139 hubBlock::relay::qLen: 0,140 hubBlock::relay::recipes: Set(),141 hubBlock::relay::rounds: 0,142 hubBlock::relay::store: Set(),143 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),144 hubBlock::relay::wKind: Map(0 -> Man, 1 -> Nil, 2 -> Nil),145 hubBlock::relay::wLen: 1,146 hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")147}148149[State 5]150{151 hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),152 hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),153 hubBlock::relay::hLen: 1,154 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),155 hubBlock::relay::have: Set(),156 hubBlock::relay::hubComputing: Set("b", "c"),157 hubBlock::relay::hubErr: false,158 hubBlock::relay::hubFirstNeed: false,159 hubBlock::relay::hubOutbox: Set(),160 hubBlock::relay::hubSent: Set("a"),161 hubBlock::relay::imported: Set(),162 hubBlock::relay::inline: Set(),163 hubBlock::relay::outstanding: 1,164 hubBlock::relay::pending: Set("a", "b", "c"),165 hubBlock::relay::phase: Staging,166 hubBlock::relay::qHashes:167 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),168 hubBlock::relay::qLen: 0,169 hubBlock::relay::recipes: Set("a"),170 hubBlock::relay::rounds: 0,171 hubBlock::relay::store: Set(),172 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),173 hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),174 hubBlock::relay::wLen: 0,175 hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")176}177178[State 6]179{180 hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),181 hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),182 hubBlock::relay::hLen: 1,183 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),184 hubBlock::relay::have: Set(),185 hubBlock::relay::hubComputing: Set("c"),186 hubBlock::relay::hubErr: false,187 hubBlock::relay::hubFirstNeed: false,188 hubBlock::relay::hubOutbox: Set("b"),189 hubBlock::relay::hubSent: Set("a"),190 hubBlock::relay::imported: Set(),191 hubBlock::relay::inline: Set(),192 hubBlock::relay::outstanding: 1,193 hubBlock::relay::pending: Set("a", "b", "c"),194 hubBlock::relay::phase: Staging,195 hubBlock::relay::qHashes:196 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),197 hubBlock::relay::qLen: 0,198 hubBlock::relay::recipes: Set("a"),199 hubBlock::relay::rounds: 0,200 hubBlock::relay::store: Set(),201 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),202 hubBlock::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),203 hubBlock::relay::wLen: 0,204 hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")205}206207[State 7]208{209 hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),210 hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),211 hubBlock::relay::hLen: 1,212 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),213 hubBlock::relay::have: Set(),214 hubBlock::relay::hubComputing: Set("c"),215 hubBlock::relay::hubErr: false,216 hubBlock::relay::hubFirstNeed: false,217 hubBlock::relay::hubOutbox: Set(),218 hubBlock::relay::hubSent: Set("a", "b"),219 hubBlock::relay::imported: Set(),220 hubBlock::relay::inline: Set(),221 hubBlock::relay::outstanding: 1,222 hubBlock::relay::pending: Set("a", "b", "c"),223 hubBlock::relay::phase: Staging,224 hubBlock::relay::qHashes:225 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),226 hubBlock::relay::qLen: 0,227 hubBlock::relay::recipes: Set("a"),228 hubBlock::relay::rounds: 0,229 hubBlock::relay::store: Set(),230 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),231 hubBlock::relay::wKind: Map(0 -> Man, 1 -> Nil, 2 -> Nil),232 hubBlock::relay::wLen: 1,233 hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")234}235236[State 8]237{238 hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),239 hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),240 hubBlock::relay::hLen: 1,241 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),242 hubBlock::relay::have: Set(),243 hubBlock::relay::hubComputing: Set("c"),244 hubBlock::relay::hubErr: false,245 hubBlock::relay::hubFirstNeed: false,246 hubBlock::relay::hubOutbox: Set(),247 hubBlock::relay::hubSent: Set("a", "b"),248 hubBlock::relay::imported: Set(),249 hubBlock::relay::inline: Set(),250 hubBlock::relay::outstanding: 1,251 hubBlock::relay::pending: Set("a", "b", "c"),252 hubBlock::relay::phase: Staging,253 hubBlock::relay::qHashes:254 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),255 hubBlock::relay::qLen: 0,256 hubBlock::relay::recipes: Set("a"),257 hubBlock::relay::rounds: 0,258 hubBlock::relay::store: Set(),259 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),260 hubBlock::relay::wKind: Map(0 -> Man, 1 -> Other, 2 -> Nil),261 hubBlock::relay::wLen: 2,262 hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")263}264265[State 9]266{267 hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),268 hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),269 hubBlock::relay::hLen: 1,270 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),271 hubBlock::relay::have: Set(),272 hubBlock::relay::hubComputing: Set("c"),273 hubBlock::relay::hubErr: false,274 hubBlock::relay::hubFirstNeed: false,275 hubBlock::relay::hubOutbox: Set(),276 hubBlock::relay::hubSent: Set("a", "b"),277 hubBlock::relay::imported: Set(),278 hubBlock::relay::inline: Set(),279 hubBlock::relay::outstanding: 1,280 hubBlock::relay::pending: Set("a", "b", "c"),281 hubBlock::relay::phase: Staging,282 hubBlock::relay::qHashes:283 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),284 hubBlock::relay::qLen: 0,285 hubBlock::relay::recipes: Set("a"),286 hubBlock::relay::rounds: 0,287 hubBlock::relay::store: Set(),288 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),289 hubBlock::relay::wKind: Map(0 -> Man, 1 -> Other, 2 -> Other),290 hubBlock::relay::wLen: 3,291 hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")292}293294[State 10]295{296 hubBlock::relay::awaiting: Map(1 -> Set("a"), 2 -> Set("a"), 3 -> Set()),297 hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set()),298 hubBlock::relay::hLen: 1,299 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),300 hubBlock::relay::have: Set(),301 hubBlock::relay::hubComputing: Set(),302 hubBlock::relay::hubErr: false,303 hubBlock::relay::hubFirstNeed: false,304 hubBlock::relay::hubOutbox: Set("c"),305 hubBlock::relay::hubSent: Set("a", "b"),306 hubBlock::relay::imported: Set(),307 hubBlock::relay::inline: Set(),308 hubBlock::relay::outstanding: 1,309 hubBlock::relay::pending: Set("a", "b", "c"),310 hubBlock::relay::phase: Staging,311 hubBlock::relay::qHashes:312 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),313 hubBlock::relay::qLen: 0,314 hubBlock::relay::recipes: Set("a"),315 hubBlock::relay::rounds: 0,316 hubBlock::relay::store: Set(),317 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),318 hubBlock::relay::wKind: Map(0 -> Man, 1 -> Other, 2 -> Other),319 hubBlock::relay::wLen: 3,320 hubBlock::relay::wPath: Map(0 -> "b", 1 -> "a", 2 -> "a")321}322323[State 11]324{325 hubBlock::relay::awaiting:326 Map(1 -> Set("a"), 2 -> Set("a", "b"), 3 -> Set("b")),327 hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set(3)),328 hubBlock::relay::hLen: 2,329 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),330 hubBlock::relay::have: Set(),331 hubBlock::relay::hubComputing: Set(),332 hubBlock::relay::hubErr: false,333 hubBlock::relay::hubFirstNeed: false,334 hubBlock::relay::hubOutbox: Set("c"),335 hubBlock::relay::hubSent: Set("a", "b"),336 hubBlock::relay::imported: Set(),337 hubBlock::relay::inline: Set(),338 hubBlock::relay::outstanding: 2,339 hubBlock::relay::pending: Set("a", "b", "c"),340 hubBlock::relay::phase: Staging,341 hubBlock::relay::qHashes:342 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),343 hubBlock::relay::qLen: 0,344 hubBlock::relay::recipes: Set("a", "b"),345 hubBlock::relay::rounds: 0,346 hubBlock::relay::store: Set(),347 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),348 hubBlock::relay::wKind: Map(0 -> Other, 1 -> Other, 2 -> Nil),349 hubBlock::relay::wLen: 2,350 hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")351}352353[State 12]354{355 hubBlock::relay::awaiting:356 Map(1 -> Set("a"), 2 -> Set("a", "b"), 3 -> Set("b")),357 hubBlock::relay::hHashes: Map(0 -> Set(1, 2), 1 -> Set(3)),358 hubBlock::relay::hLen: 2,359 hubBlock::relay::hPaths: Map(0 -> Set(), 1 -> Set()),360 hubBlock::relay::have: Set(),361 hubBlock::relay::hubComputing: Set(),362 hubBlock::relay::hubErr: false,363 hubBlock::relay::hubFirstNeed: false,364 hubBlock::relay::hubOutbox: Set("c"),365 hubBlock::relay::hubSent: Set("a", "b"),366 hubBlock::relay::imported: Set(),367 hubBlock::relay::inline: Set(),368 hubBlock::relay::outstanding: 2,369 hubBlock::relay::pending: Set("a", "b", "c"),370 hubBlock::relay::phase: Staging,371 hubBlock::relay::qHashes:372 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),373 hubBlock::relay::qLen: 0,374 hubBlock::relay::recipes: Set("a", "b"),375 hubBlock::relay::rounds: 0,376 hubBlock::relay::store: Set(),377 hubBlock::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),378 hubBlock::relay::wKind: Map(0 -> Other, 1 -> Other, 2 -> Other),379 hubBlock::relay::wLen: 3,380 hubBlock::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")381}382383[violation] Found an issue (1104ms at 42581 traces/second).384Use --verbosity=3 to show executions.385Use --seed=0x69f7b1f81455c0bc --backend=rust to reproduce.386error: Invariant violated