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