spec-refute-hubDrop
checks.x86_64-linux.spec-refute-hubDrop
· build #298
· raw
1Running... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/50000 samples | 0 samples/sRunning... [ ] 0% | ETA: 6417s | 11/50000 samples | 8 samples/sRunning... [ ] 0% | ETA: 2692s | 28/50000 samples | 19 samples/sRunning... [ ] 0% | ETA: 1890s | 43/50000 samples | 27 samples/sRunning... [ ] 0% | ETA: 1365s | 63/50000 samples | 37 samples/sRunning... [ ] 0% | ETA: 1197s | 76/50000 samples | 42 samples/sRunning... [ ] 0% | ETA: 820s | 117/50000 samples | 61 samples/sRunning... [ ] 0% | ETA: 712s | 142/50000 samples | 70 samples/sRunning... [ ] 0% | ETA: 693s | 153/50000 samples | 72 samples/sRunning... [ ] 0% | ETA: 694s | 160/50000 samples | 72 samples/sRunning... [ ] 0% | ETA: 303s | 162/50000 samples | 70 samples/sRunning... [ ] 0% | ETA: 337s | 165/50000 samples | 68 samples/sAn example execution:23[State 0]4{5 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),6 hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),7 hubDrop::relay::hLen: 0,8 hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),9 hubDrop::relay::have: Set("b"),10 hubDrop::relay::hubComputing: Set(),11 hubDrop::relay::hubErr: false,12 hubDrop::relay::hubFirstNeed: true,13 hubDrop::relay::hubOutbox: Set(),14 hubDrop::relay::hubSent: Set("b", "c"),15 hubDrop::relay::imported: Set(),16 hubDrop::relay::inline: Set("b", "c"),17 hubDrop::relay::outstanding: 0,18 hubDrop::relay::pending: Set(),19 hubDrop::relay::phase: Init,20 hubDrop::relay::qHashes:21 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),22 hubDrop::relay::qLen: 0,23 hubDrop::relay::recipes: Set(),24 hubDrop::relay::rounds: 0,25 hubDrop::relay::store: Set(),26 hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),27 hubDrop::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),28 hubDrop::relay::wLen: 0,29 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")30}3132[State 1]33{34 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),35 hubDrop::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),36 hubDrop::relay::hLen: 1,37 hubDrop::relay::hPaths: Map(0 -> Set("a", "c"), 1 -> Set()),38 hubDrop::relay::have: Set("b"),39 hubDrop::relay::hubComputing: Set(),40 hubDrop::relay::hubErr: false,41 hubDrop::relay::hubFirstNeed: true,42 hubDrop::relay::hubOutbox: Set(),43 hubDrop::relay::hubSent: Set("b", "c"),44 hubDrop::relay::imported: Set(),45 hubDrop::relay::inline: Set("b", "c"),46 hubDrop::relay::outstanding: 1,47 hubDrop::relay::pending: Set("a", "c"),48 hubDrop::relay::phase: Staging,49 hubDrop::relay::qHashes:50 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),51 hubDrop::relay::qLen: 0,52 hubDrop::relay::recipes: Set("c"),53 hubDrop::relay::rounds: 0,54 hubDrop::relay::store: Set(),55 hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),56 hubDrop::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),57 hubDrop::relay::wLen: 0,58 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")59}6061[State 2]62{63 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),64 hubDrop::relay::hHashes: Map(0 -> Set(3), 1 -> Set()),65 hubDrop::relay::hLen: 1,66 hubDrop::relay::hPaths: Map(0 -> Set("a", "c"), 1 -> Set()),67 hubDrop::relay::have: Set("b"),68 hubDrop::relay::hubComputing: Set(),69 hubDrop::relay::hubErr: false,70 hubDrop::relay::hubFirstNeed: true,71 hubDrop::relay::hubOutbox: Set(),72 hubDrop::relay::hubSent: Set("b", "c"),73 hubDrop::relay::imported: Set(),74 hubDrop::relay::inline: Set("b", "c"),75 hubDrop::relay::outstanding: 1,76 hubDrop::relay::pending: Set("a", "c"),77 hubDrop::relay::phase: Staging,78 hubDrop::relay::qHashes:79 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),80 hubDrop::relay::qLen: 0,81 hubDrop::relay::recipes: Set("c"),82 hubDrop::relay::rounds: 0,83 hubDrop::relay::store: Set(),84 hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),85 hubDrop::relay::wKind: Map(0 -> Other, 1 -> Nil, 2 -> Nil),86 hubDrop::relay::wLen: 1,87 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")88}8990[State 3]91{92 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),93 hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),94 hubDrop::relay::hLen: 0,95 hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),96 hubDrop::relay::have: Set("b"),97 hubDrop::relay::hubComputing: Set("a"),98 hubDrop::relay::hubErr: false,99 hubDrop::relay::hubFirstNeed: false,100 hubDrop::relay::hubOutbox: Set(),101 hubDrop::relay::hubSent: Set("b", "c"),102 hubDrop::relay::imported: Set(),103 hubDrop::relay::inline: Set("b", "c"),104 hubDrop::relay::outstanding: 1,105 hubDrop::relay::pending: Set("a", "c"),106 hubDrop::relay::phase: Staging,107 hubDrop::relay::qHashes:108 Map(109 0 -> Set(3),110 1 -> Set(),111 2 -> Set(),112 3 -> Set(),113 4 -> Set(),114 5 -> Set()115 ),116 hubDrop::relay::qLen: 1,117 hubDrop::relay::recipes: Set("c"),118 hubDrop::relay::rounds: 0,119 hubDrop::relay::store: Set(),120 hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),121 hubDrop::relay::wKind: Map(0 -> Other, 1 -> Nil, 2 -> Nil),122 hubDrop::relay::wLen: 1,123 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")124}125126[State 4]127{128 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),129 hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),130 hubDrop::relay::hLen: 0,131 hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),132 hubDrop::relay::have: Set("b"),133 hubDrop::relay::hubComputing: Set(),134 hubDrop::relay::hubErr: false,135 hubDrop::relay::hubFirstNeed: false,136 hubDrop::relay::hubOutbox: Set("a"),137 hubDrop::relay::hubSent: Set("b", "c"),138 hubDrop::relay::imported: Set(),139 hubDrop::relay::inline: Set("b", "c"),140 hubDrop::relay::outstanding: 1,141 hubDrop::relay::pending: Set("a", "c"),142 hubDrop::relay::phase: Staging,143 hubDrop::relay::qHashes:144 Map(145 0 -> Set(3),146 1 -> Set(),147 2 -> Set(),148 3 -> Set(),149 4 -> Set(),150 5 -> Set()151 ),152 hubDrop::relay::qLen: 1,153 hubDrop::relay::recipes: Set("c"),154 hubDrop::relay::rounds: 0,155 hubDrop::relay::store: Set(),156 hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),157 hubDrop::relay::wKind: Map(0 -> Other, 1 -> Nil, 2 -> Nil),158 hubDrop::relay::wLen: 1,159 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")160}161162[State 5]163{164 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),165 hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),166 hubDrop::relay::hLen: 0,167 hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),168 hubDrop::relay::have: Set("b"),169 hubDrop::relay::hubComputing: Set(),170 hubDrop::relay::hubErr: false,171 hubDrop::relay::hubFirstNeed: false,172 hubDrop::relay::hubOutbox: Set("a"),173 hubDrop::relay::hubSent: Set("b", "c"),174 hubDrop::relay::imported: Set(),175 hubDrop::relay::inline: Set("b", "c"),176 hubDrop::relay::outstanding: 1,177 hubDrop::relay::pending: Set("a", "c"),178 hubDrop::relay::phase: Staging,179 hubDrop::relay::qHashes:180 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),181 hubDrop::relay::qLen: 0,182 hubDrop::relay::recipes: Set("c"),183 hubDrop::relay::rounds: 0,184 hubDrop::relay::store: Set(),185 hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(3), 2 -> Set()),186 hubDrop::relay::wKind: Map(0 -> Other, 1 -> Chunks, 2 -> Eof),187 hubDrop::relay::wLen: 3,188 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")189}190191[State 6]192{193 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),194 hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),195 hubDrop::relay::hLen: 0,196 hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),197 hubDrop::relay::have: Set("b"),198 hubDrop::relay::hubComputing: Set(),199 hubDrop::relay::hubErr: false,200 hubDrop::relay::hubFirstNeed: false,201 hubDrop::relay::hubOutbox: Set(),202 hubDrop::relay::hubSent: Set("a", "b", "c"),203 hubDrop::relay::imported: Set(),204 hubDrop::relay::inline: Set("b", "c"),205 hubDrop::relay::outstanding: 1,206 hubDrop::relay::pending: Set("a", "c"),207 hubDrop::relay::phase: Staging,208 hubDrop::relay::qHashes:209 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),210 hubDrop::relay::qLen: 0,211 hubDrop::relay::recipes: Set("c"),212 hubDrop::relay::rounds: 0,213 hubDrop::relay::store: Set(),214 hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(3), 2 -> Set()),215 hubDrop::relay::wKind: Map(0 -> Other, 1 -> Chunks, 2 -> Eof),216 hubDrop::relay::wLen: 3,217 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")218}219220[State 7]221{222 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set("c")),223 hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),224 hubDrop::relay::hLen: 0,225 hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),226 hubDrop::relay::have: Set("b"),227 hubDrop::relay::hubComputing: Set(),228 hubDrop::relay::hubErr: false,229 hubDrop::relay::hubFirstNeed: false,230 hubDrop::relay::hubOutbox: Set(),231 hubDrop::relay::hubSent: Set("a", "b", "c"),232 hubDrop::relay::imported: Set(),233 hubDrop::relay::inline: Set("b", "c"),234 hubDrop::relay::outstanding: 1,235 hubDrop::relay::pending: Set("a", "c"),236 hubDrop::relay::phase: Staging,237 hubDrop::relay::qHashes:238 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),239 hubDrop::relay::qLen: 0,240 hubDrop::relay::recipes: Set("c"),241 hubDrop::relay::rounds: 0,242 hubDrop::relay::store: Set(),243 hubDrop::relay::wChunks: Map(0 -> Set(3), 1 -> Set(), 2 -> Set()),244 hubDrop::relay::wKind: Map(0 -> Chunks, 1 -> Eof, 2 -> Nil),245 hubDrop::relay::wLen: 2,246 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")247}248249[State 8]250{251 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),252 hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),253 hubDrop::relay::hLen: 0,254 hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),255 hubDrop::relay::have: Set("b"),256 hubDrop::relay::hubComputing: Set(),257 hubDrop::relay::hubErr: false,258 hubDrop::relay::hubFirstNeed: false,259 hubDrop::relay::hubOutbox: Set(),260 hubDrop::relay::hubSent: Set("a", "b", "c"),261 hubDrop::relay::imported: Set("c"),262 hubDrop::relay::inline: Set("b", "c"),263 hubDrop::relay::outstanding: 1,264 hubDrop::relay::pending: Set("a"),265 hubDrop::relay::phase: Staging,266 hubDrop::relay::qHashes:267 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),268 hubDrop::relay::qLen: 0,269 hubDrop::relay::recipes: Set("c"),270 hubDrop::relay::rounds: 0,271 hubDrop::relay::store: Set(3),272 hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),273 hubDrop::relay::wKind: Map(0 -> Eof, 1 -> Nil, 2 -> Nil),274 hubDrop::relay::wLen: 1,275 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")276}277278[State 9]279{280 hubDrop::relay::awaiting: Map(1 -> Set(), 2 -> Set(), 3 -> Set()),281 hubDrop::relay::hHashes: Map(0 -> Set(), 1 -> Set()),282 hubDrop::relay::hLen: 0,283 hubDrop::relay::hPaths: Map(0 -> Set(), 1 -> Set()),284 hubDrop::relay::have: Set("b"),285 hubDrop::relay::hubComputing: Set(),286 hubDrop::relay::hubErr: false,287 hubDrop::relay::hubFirstNeed: false,288 hubDrop::relay::hubOutbox: Set(),289 hubDrop::relay::hubSent: Set("a", "b", "c"),290 hubDrop::relay::imported: Set("c"),291 hubDrop::relay::inline: Set("b", "c"),292 hubDrop::relay::outstanding: 0,293 hubDrop::relay::pending: Set("a"),294 hubDrop::relay::phase: Staging,295 hubDrop::relay::qHashes:296 Map(0 -> Set(), 1 -> Set(), 2 -> Set(), 3 -> Set(), 4 -> Set(), 5 -> Set()),297 hubDrop::relay::qLen: 0,298 hubDrop::relay::recipes: Set("c"),299 hubDrop::relay::rounds: 0,300 hubDrop::relay::store: Set(3),301 hubDrop::relay::wChunks: Map(0 -> Set(), 1 -> Set(), 2 -> Set()),302 hubDrop::relay::wKind: Map(0 -> Nil, 1 -> Nil, 2 -> Nil),303 hubDrop::relay::wLen: 0,304 hubDrop::relay::wPath: Map(0 -> "a", 1 -> "a", 2 -> "a")305}306307[violation] Found an issue (2581ms at 64 traces/second).308Use --verbosity=3 to show executions.309Use --seed=0xe7b193ae3b3c5b4e --backend=rust to reproduce.310error: Invariant violated