nixbot

builds

succeeded nix-grpc-store-claims-spec checks.aarch64-darwin.claims-spec · build #156 · raw

1Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [■■ ] 5% | ETA: 11s | 1057/20000 samples | 1898 samples/sRunning... [■■ ] 5% | ETA: 11s | 1057/20000 samples | 1898 samples/sRunning... [■■■ ] 7% | ETA: 10s | 1480/20000 samples | 1958 samples/sRunning... [■■■ ] 7% | ETA: 10s | 1480/20000 samples | 1958 samples/sRunning... [■■■■ ] 9% | ETA: 10s | 1840/20000 samples | 1989 samples/sRunning... [■■■■ ] 9% | ETA: 10s | 1840/20000 samples | 1989 samples/sRunning... [■■■■■ ] 11% | ETA: 9s | 2337/20000 samples | 1989 samples/sRunning... [■■■■■ ] 11% | ETA: 9s | 2337/20000 samples | 1989 samples/sRunning... [■■■■■■ ] 14% | ETA: 9s | 2903/20000 samples | 2043 samples/sRunning... [■■■■■■ ] 14% | ETA: 9s | 2903/20000 samples | 2043 samples/sRunning... [■■■■■■ ] 16% | ETA: 9s | 3225/20000 samples | 2059 samples/sRunning... [■■■■■■ ] 16% | ETA: 9s | 3225/20000 samples | 2059 samples/sRunning... [■■■■■■■ ] 18% | ETA: 8s | 3735/20000 samples | 2077 samples/sRunning... [■■■■■■■■ ] 19% | ETA: 8s | 3976/20000 samples | 2083 samples/sRunning... [■■■■■■■■ ] 19% | ETA: 8s | 3976/20000 samples | 2083 samples/sRunning... [■■■■■■■■ ] 19% | ETA: 8s | 3976/20000 samples | 2083 samples/sRunning... [■■■■■■■■■ ] 22% | ETA: 8s | 4514/20000 samples | 2091 samples/sRunning... [■■■■■■■■■ ] 22% | ETA: 8s | 4514/20000 samples | 2091 samples/sRunning... [■■■■■■■■■■ ] 25% | ETA: 7s | 5083/20000 samples | 2117 samples/sRunning... [■■■■■■■■■■ ] 25% | ETA: 7s | 5083/20000 samples | 2117 samples/sRunning... [■■■■■■■■■■■ ] 27% | ETA: 7s | 5460/20000 samples | 2090 samples/sRunning... [■■■■■■■■■■■ ] 28% | ETA: 7s | 5647/20000 samples | 2075 samples/sRunning... [■■■■■■■■■■■ ] 28% | ETA: 7s | 5647/20000 samples | 2075 samples/sRunning... [■■■■■■■■■■■ ] 28% | ETA: 7s | 5647/20000 samples | 2075 samples/sRunning... [■■■■■■■■■■■■ ] 30% | ETA: 7s | 6117/20000 samples | 2066 samples/sRunning... [■■■■■■■■■■■■■ ] 31% | ETA: 7s | 6326/20000 samples | 2065 samples/sRunning... [■■■■■■■■■■■■■ ] 31% | ETA: 7s | 6326/20000 samples | 2065 samples/sRunning... [■■■■■■■■■■■■■ ] 33% | ETA: 7s | 6727/20000 samples | 2060 samples/sRunning... [■■■■■■■■■■■■■ ] 33% | ETA: 7s | 6727/20000 samples | 2060 samples/sRunning... [■■■■■■■■■■■■■■ ] 35% | ETA: 7s | 7176/20000 samples | 2056 samples/sRunning... [■■■■■■■■■■■■■■ ] 35% | ETA: 7s | 7176/20000 samples | 2056 samples/sRunning... [■■■■■■■■■■■■■■■ ] 38% | ETA: 7s | 7665/20000 samples | 2059 samples/sRunning... [■■■■■■■■■■■■■■■ ] 38% | ETA: 7s | 7665/20000 samples | 2059 samples/sRunning... [■■■■■■■■■■■■■■■■ ] 39% | ETA: 7s | 7957/20000 samples | 2027 samples/sRunning... [■■■■■■■■■■■■■■■■ ] 39% | ETA: 7s | 7957/20000 samples | 2027 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 41% | ETA: 7s | 8257/20000 samples | 2000 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 43% | ETA: 6s | 8763/20000 samples | 2079 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 44% | ETA: 6s | 8962/20000 samples | 2076 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 45% | ETA: 6s | 9008/20000 samples | 2034 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 45% | ETA: 6s | 9199/20000 samples | 2028 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 45% | ETA: 6s | 9199/20000 samples | 2028 samples/sRunning... [■■■■■■■■■■■■■■■■■■■ ] 47% | ETA: 6s | 9563/20000 samples | 2002 samples/sRunning... [■■■■■■■■■■■■■■■■■■■ ] 47% | ETA: 6s | 9563/20000 samples | 2002 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 48% | ETA: 6s | 9774/20000 samples | 1987 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 49% | ETA: 6s | 9913/20000 samples | 1974 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 50% | ETA: 6s | 10061/20000 samples | 1964 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 50% | ETA: 6s | 10198/20000 samples | 1951 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■ ] 51% | ETA: 7s | 10380/20000 samples | 1949 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■ ] 52% | ETA: 7s | 10548/20000 samples | 1943 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■ ] 54% | ETA: 7s | 10801/20000 samples | 1919 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■ ] 54% | ETA: 7s | 10801/20000 samples | 1919 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■ ] 55% | ETA: 6s | 11106/20000 samples | 1914 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 56% | ETA: 6s | 11367/20000 samples | 1917 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 56% | ETA: 6s | 11367/20000 samples | 1917 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 58% | ETA: 6s | 11603/20000 samples | 1916 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■ ] 59% | ETA: 6s | 11812/20000 samples | 1909 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■ ] 59% | ETA: 6s | 11812/20000 samples | 1909 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■ ] 60% | ETA: 5s | 12140/20000 samples | 1902 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■ ] 61% | ETA: 5s | 12275/20000 samples | 1890 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■ ] 61% | ETA: 5s | 12395/20000 samples | 1879 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■ ] 62% | ETA: 5s | 12524/20000 samples | 1869 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■ ] 62% | ETA: 5s | 12524/20000 samples | 1869 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 64% | ETA: 5s | 12907/20000 samples | 1857 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 64% | ETA: 5s | 12907/20000 samples | 1857 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 64% | ETA: 5s | 12907/20000 samples | 1857 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 66% | ETA: 5s | 13257/20000 samples | 1846 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 66% | ETA: 5s | 13257/20000 samples | 1846 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 68% | ETA: 5s | 13689/20000 samples | 1842 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 69% | ETA: 4s | 13887/20000 samples | 1841 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 69% | ETA: 4s | 13887/20000 samples | 1841 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 69% | ETA: 4s | 13887/20000 samples | 1841 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 71% | ETA: 4s | 14246/20000 samples | 1829 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 72% | ETA: 4s | 14423/20000 samples | 1823 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 73% | ETA: 4s | 14677/20000 samples | 1816 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 73% | ETA: 4s | 14677/20000 samples | 1816 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 74% | ETA: 4s | 14821/20000 samples | 1809 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 75% | ETA: 4s | 15074/20000 samples | 1802 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 75% | ETA: 4s | 15074/20000 samples | 1802 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 76% | ETA: 3s | 15373/20000 samples | 1801 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 77% | ETA: 3s | 15560/20000 samples | 1800 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 77% | ETA: 3s | 15560/20000 samples | 1800 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 79% | ETA: 3s | 15831/20000 samples | 1787 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 79% | ETA: 3s | 15831/20000 samples | 1787 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 79% | ETA: 3s | 15831/20000 samples | 1787 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 81% | ETA: 3s | 16213/20000 samples | 1781 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 82% | ETA: 3s | 16486/20000 samples | 1784 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 82% | ETA: 3s | 16486/20000 samples | 1784 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 84% | ETA: 3s | 16804/20000 samples | 1775 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 84% | ETA: 3s | 16804/20000 samples | 1775 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 85% | ETA: 2s | 17146/20000 samples | 1766 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 85% | ETA: 2s | 17146/20000 samples | 1766 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 85% | ETA: 2s | 17146/20000 samples | 1766 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 87% | ETA: 2s | 17479/20000 samples | 1755 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 88% | ETA: 2s | 17649/20000 samples | 1754 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 89% | ETA: 2s | 17822/20000 samples | 1752 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 89% | ETA: 2s | 17822/20000 samples | 1752 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 90% | ETA: 2s | 18076/20000 samples | 1751 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 91% | ETA: 2s | 18235/20000 samples | 1748 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 92% | ETA: 1s | 18467/20000 samples | 1749 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 92% | ETA: 1s | 18467/20000 samples | 1749 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 94% | ETA: 1s | 18836/20000 samples | 1746 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 95% | ETA: 1s | 19063/20000 samples | 1747 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 95% | ETA: 1s | 19063/20000 samples | 1747 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 96% | ETA: 1s | 19285/20000 samples | 1745 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 97% | ETA: 1s | 19511/20000 samples | 1736 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 97% | ETA: 1s | 19511/20000 samples | 1736 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 98% | ETA: 1s | 19685/20000 samples | 1732 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 98% | ETA: 1s | 19762/20000 samples | 1723 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19873/20000 samples | 1711 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19919/20000 samples | 1699 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19919/20000 samples | 1699 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19997/20000 samples | 1674 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19997/20000 samples | 1674 samples/sAn example execution:23[State 0]4{5 nextToken: 1,6 present: false,7 rowStale: false,8 rowToken: 0,9 touched: false,10 ws:11 Map(12 "w1" ->13 {14 conn: false,15 outputs: false,16 phase: Idle,17 res: RNone,18 slot: false,19 srv: SNone,20 token: 021 },22 "w2" ->23 {24 conn: false,25 outputs: false,26 phase: Idle,27 res: RNone,28 slot: false,29 srv: SNone,30 token: 031 },32 "w3" ->33 {34 conn: false,35 outputs: false,36 phase: Idle,37 res: RNone,38 slot: false,39 srv: SNone,40 token: 041 }42 )43}4445[State 1]46{47 nextToken: 1,48 present: false,49 rowStale: false,50 rowToken: 0,51 touched: false,52 ws:53 Map(54 "w1" ->55 {56 conn: true,57 outputs: false,58 phase: Pending,59 res: RNone,60 slot: true,61 srv: SNeed,62 token: 063 },64 "w2" ->65 {66 conn: false,67 outputs: false,68 phase: Idle,69 res: RNone,70 slot: false,71 srv: SNone,72 token: 073 },74 "w3" ->75 {76 conn: false,77 outputs: false,78 phase: Idle,79 res: RNone,80 slot: false,81 srv: SNone,82 token: 083 }84 )85}8687[State 2]88{89 nextToken: 1,90 present: false,91 rowStale: false,92 rowToken: 0,93 touched: false,94 ws:95 Map(96 "w1" ->97 {98 conn: false,99 outputs: false,100 phase: Pending,101 res: RNone,102 slot: true,103 srv: SNone,104 token: 0105 },106 "w2" ->107 {108 conn: false,109 outputs: false,110 phase: Idle,111 res: RNone,112 slot: false,113 srv: SNone,114 token: 0115 },116 "w3" ->117 {118 conn: false,119 outputs: false,120 phase: Idle,121 res: RNone,122 slot: false,123 srv: SNone,124 token: 0125 }126 )127}128129[State 3]130{131 nextToken: 1,132 present: false,133 rowStale: false,134 rowToken: 0,135 touched: false,136 ws:137 Map(138 "w1" ->139 {140 conn: false,141 outputs: false,142 phase: Done,143 res: RUnavailable,144 slot: false,145 srv: SNone,146 token: 0147 },148 "w2" ->149 {150 conn: false,151 outputs: false,152 phase: Idle,153 res: RNone,154 slot: false,155 srv: SNone,156 token: 0157 },158 "w3" ->159 {160 conn: false,161 outputs: false,162 phase: Idle,163 res: RNone,164 slot: false,165 srv: SNone,166 token: 0167 }168 )169}170171[State 4]172{173 nextToken: 1,174 present: false,175 rowStale: false,176 rowToken: 0,177 touched: false,178 ws:179 Map(180 "w1" ->181 {182 conn: false,183 outputs: false,184 phase: Idle,185 res: RNone,186 slot: false,187 srv: SNone,188 token: 0189 },190 "w2" ->191 {192 conn: false,193 outputs: false,194 phase: Idle,195 res: RNone,196 slot: false,197 srv: SNone,198 token: 0199 },200 "w3" ->201 {202 conn: false,203 outputs: false,204 phase: Idle,205 res: RNone,206 slot: false,207 srv: SNone,208 token: 0209 }210 )211}212213[State 5]214{215 nextToken: 1,216 present: false,217 rowStale: false,218 rowToken: 0,219 touched: false,220 ws:221 Map(222 "w1" ->223 {224 conn: false,225 outputs: false,226 phase: Idle,227 res: RNone,228 slot: false,229 srv: SNone,230 token: 0231 },232 "w2" ->233 {234 conn: true,235 outputs: false,236 phase: Pending,237 res: RNone,238 slot: true,239 srv: SNeed,240 token: 0241 },242 "w3" ->243 {244 conn: false,245 outputs: false,246 phase: Idle,247 res: RNone,248 slot: false,249 srv: SNone,250 token: 0251 }252 )253}254255[State 6]256{257 nextToken: 2,258 present: false,259 rowStale: false,260 rowToken: 1,261 touched: false,262 ws:263 Map(264 "w1" ->265 {266 conn: false,267 outputs: false,268 phase: Idle,269 res: RNone,270 slot: false,271 srv: SNone,272 token: 0273 },274 "w2" ->275 {276 conn: true,277 outputs: false,278 phase: Building,279 res: RNone,280 slot: true,281 srv: SHolder(1),282 token: 1283 },284 "w3" ->285 {286 conn: false,287 outputs: false,288 phase: Idle,289 res: RNone,290 slot: false,291 srv: SNone,292 token: 0293 }294 )295}296297[State 7]298{299 nextToken: 2,300 present: false,301 rowStale: false,302 rowToken: 1,303 touched: false,304 ws:305 Map(306 "w1" ->307 {308 conn: false,309 outputs: false,310 phase: Idle,311 res: RNone,312 slot: false,313 srv: SNone,314 token: 0315 },316 "w2" ->317 {318 conn: false,319 outputs: false,320 phase: Building,321 res: RNone,322 slot: true,323 srv: SNone,324 token: 1325 },326 "w3" ->327 {328 conn: false,329 outputs: false,330 phase: Idle,331 res: RNone,332 slot: false,333 srv: SNone,334 token: 0335 }336 )337}338339[State 8]340{341 nextToken: 2,342 present: false,343 rowStale: true,344 rowToken: 1,345 touched: false,346 ws:347 Map(348 "w1" ->349 {350 conn: false,351 outputs: false,352 phase: Idle,353 res: RNone,354 slot: false,355 srv: SNone,356 token: 0357 },358 "w2" ->359 {360 conn: false,361 outputs: false,362 phase: Building,363 res: RNone,364 slot: true,365 srv: SNone,366 token: 1367 },368 "w3" ->369 {370 conn: false,371 outputs: false,372 phase: Idle,373 res: RNone,374 slot: false,375 srv: SNone,376 token: 0377 }378 )379}380381[State 9]382{383 nextToken: 2,384 present: false,385 rowStale: true,386 rowToken: 1,387 touched: false,388 ws:389 Map(390 "w1" ->391 {392 conn: false,393 outputs: false,394 phase: Idle,395 res: RNone,396 slot: false,397 srv: SNone,398 token: 0399 },400 "w2" ->401 {402 conn: true,403 outputs: false,404 phase: Building,405 res: RNone,406 slot: true,407 srv: SNeed,408 token: 1409 },410 "w3" ->411 {412 conn: false,413 outputs: false,414 phase: Idle,415 res: RNone,416 slot: false,417 srv: SNone,418 token: 0419 }420 )421}422423[State 10]424{425 nextToken: 2,426 present: false,427 rowStale: true,428 rowToken: 1,429 touched: false,430 ws:431 Map(432 "w1" ->433 {434 conn: false,435 outputs: false,436 phase: Idle,437 res: RNone,438 slot: false,439 srv: SNone,440 token: 0441 },442 "w2" ->443 {444 conn: false,445 outputs: false,446 phase: Building,447 res: RNone,448 slot: true,449 srv: SNone,450 token: 1451 },452 "w3" ->453 {454 conn: false,455 outputs: false,456 phase: Idle,457 res: RNone,458 slot: false,459 srv: SNone,460 token: 0461 }462 )463}464465[State 11]466{467 nextToken: 2,468 present: false,469 rowStale: true,470 rowToken: 1,471 touched: false,472 ws:473 Map(474 "w1" ->475 {476 conn: false,477 outputs: false,478 phase: Idle,479 res: RNone,480 slot: false,481 srv: SNone,482 token: 0483 },484 "w2" ->485 {486 conn: true,487 outputs: false,488 phase: Building,489 res: RNone,490 slot: true,491 srv: SNeed,492 token: 1493 },494 "w3" ->495 {496 conn: false,497 outputs: false,498 phase: Idle,499 res: RNone,500 slot: false,501 srv: SNone,502 token: 0503 }504 )505}506507[State 12]508{509 nextToken: 2,510 present: false,511 rowStale: false,512 rowToken: 0,513 touched: false,514 ws:515 Map(516 "w1" ->517 {518 conn: false,519 outputs: false,520 phase: Idle,521 res: RNone,522 slot: false,523 srv: SNone,524 token: 0525 },526 "w2" ->527 {528 conn: false,529 outputs: false,530 phase: Done,531 res: RUnavailable,532 slot: false,533 srv: SNone,534 token: 1535 },536 "w3" ->537 {538 conn: false,539 outputs: false,540 phase: Idle,541 res: RNone,542 slot: false,543 srv: SNone,544 token: 0545 }546 )547}548549[State 13]550{551 nextToken: 2,552 present: false,553 rowStale: false,554 rowToken: 0,555 touched: false,556 ws:557 Map(558 "w1" ->559 {560 conn: true,561 outputs: false,562 phase: Pending,563 res: RNone,564 slot: true,565 srv: SNeed,566 token: 0567 },568 "w2" ->569 {570 conn: false,571 outputs: false,572 phase: Done,573 res: RUnavailable,574 slot: false,575 srv: SNone,576 token: 1577 },578 "w3" ->579 {580 conn: false,581 outputs: false,582 phase: Idle,583 res: RNone,584 slot: false,585 srv: SNone,586 token: 0587 }588 )589}590591[State 14]592{593 nextToken: 2,594 present: false,595 rowStale: false,596 rowToken: 0,597 touched: false,598 ws:599 Map(600 "w1" ->601 {602 conn: false,603 outputs: false,604 phase: Pending,605 res: RNone,606 slot: true,607 srv: SNone,608 token: 0609 },610 "w2" ->611 {612 conn: false,613 outputs: false,614 phase: Done,615 res: RUnavailable,616 slot: false,617 srv: SNone,618 token: 1619 },620 "w3" ->621 {622 conn: false,623 outputs: false,624 phase: Idle,625 res: RNone,626 slot: false,627 srv: SNone,628 token: 0629 }630 )631}632633[State 15]634{635 nextToken: 2,636 present: false,637 rowStale: false,638 rowToken: 0,639 touched: false,640 ws:641 Map(642 "w1" ->643 {644 conn: false,645 outputs: false,646 phase: Pending,647 res: RNone,648 slot: true,649 srv: SNone,650 token: 0651 },652 "w2" ->653 {654 conn: false,655 outputs: false,656 phase: Idle,657 res: RNone,658 slot: false,659 srv: SNone,660 token: 0661 },662 "w3" ->663 {664 conn: false,665 outputs: false,666 phase: Idle,667 res: RNone,668 slot: false,669 srv: SNone,670 token: 0671 }672 )673}674675[State 16]676{677 nextToken: 2,678 present: false,679 rowStale: false,680 rowToken: 0,681 touched: false,682 ws:683 Map(684 "w1" ->685 {686 conn: true,687 outputs: false,688 phase: Pending,689 res: RNone,690 slot: true,691 srv: SNeed,692 token: 0693 },694 "w2" ->695 {696 conn: false,697 outputs: false,698 phase: Idle,699 res: RNone,700 slot: false,701 srv: SNone,702 token: 0703 },704 "w3" ->705 {706 conn: false,707 outputs: false,708 phase: Idle,709 res: RNone,710 slot: false,711 srv: SNone,712 token: 0713 }714 )715}716717[State 17]718{719 nextToken: 2,720 present: false,721 rowStale: false,722 rowToken: 0,723 touched: false,724 ws:725 Map(726 "w1" ->727 {728 conn: false,729 outputs: false,730 phase: Pending,731 res: RNone,732 slot: true,733 srv: SNone,734 token: 0735 },736 "w2" ->737 {738 conn: false,739 outputs: false,740 phase: Idle,741 res: RNone,742 slot: false,743 srv: SNone,744 token: 0745 },746 "w3" ->747 {748 conn: false,749 outputs: false,750 phase: Idle,751 res: RNone,752 slot: false,753 srv: SNone,754 token: 0755 }756 )757}758759[State 18]760{761 nextToken: 2,762 present: false,763 rowStale: false,764 rowToken: 0,765 touched: false,766 ws:767 Map(768 "w1" ->769 {770 conn: false,771 outputs: false,772 phase: Done,773 res: RUnavailable,774 slot: false,775 srv: SNone,776 token: 0777 },778 "w2" ->779 {780 conn: false,781 outputs: false,782 phase: Idle,783 res: RNone,784 slot: false,785 srv: SNone,786 token: 0787 },788 "w3" ->789 {790 conn: false,791 outputs: false,792 phase: Idle,793 res: RNone,794 slot: false,795 srv: SNone,796 token: 0797 }798 )799}800801[State 19]802{803 nextToken: 2,804 present: false,805 rowStale: false,806 rowToken: 0,807 touched: false,808 ws:809 Map(810 "w1" ->811 {812 conn: false,813 outputs: false,814 phase: Done,815 res: RUnavailable,816 slot: false,817 srv: SNone,818 token: 0819 },820 "w2" ->821 {822 conn: true,823 outputs: false,824 phase: Pending,825 res: RNone,826 slot: true,827 srv: SNeed,828 token: 0829 },830 "w3" ->831 {832 conn: false,833 outputs: false,834 phase: Idle,835 res: RNone,836 slot: false,837 srv: SNone,838 token: 0839 }840 )841}842843[State 20]844{845 nextToken: 2,846 present: false,847 rowStale: false,848 rowToken: 0,849 touched: false,850 ws:851 Map(852 "w1" ->853 {854 conn: false,855 outputs: false,856 phase: Idle,857 res: RNone,858 slot: false,859 srv: SNone,860 token: 0861 },862 "w2" ->863 {864 conn: true,865 outputs: false,866 phase: Pending,867 res: RNone,868 slot: true,869 srv: SNeed,870 token: 0871 },872 "w3" ->873 {874 conn: false,875 outputs: false,876 phase: Idle,877 res: RNone,878 slot: false,879 srv: SNone,880 token: 0881 }882 )883}884885[State 21]886{887 nextToken: 2,888 present: false,889 rowStale: false,890 rowToken: 0,891 touched: false,892 ws:893 Map(894 "w1" ->895 {896 conn: false,897 outputs: false,898 phase: Idle,899 res: RNone,900 slot: false,901 srv: SNone,902 token: 0903 },904 "w2" ->905 {906 conn: false,907 outputs: false,908 phase: Pending,909 res: RNone,910 slot: true,911 srv: SNone,912 token: 0913 },914 "w3" ->915 {916 conn: false,917 outputs: false,918 phase: Idle,919 res: RNone,920 slot: false,921 srv: SNone,922 token: 0923 }924 )925}926927[State 22]928{929 nextToken: 2,930 present: false,931 rowStale: false,932 rowToken: 0,933 touched: false,934 ws:935 Map(936 "w1" ->937 {938 conn: false,939 outputs: false,940 phase: Idle,941 res: RNone,942 slot: false,943 srv: SNone,944 token: 0945 },946 "w2" ->947 {948 conn: false,949 outputs: false,950 phase: Done,951 res: RUnavailable,952 slot: false,953 srv: SNone,954 token: 0955 },956 "w3" ->957 {958 conn: false,959 outputs: false,960 phase: Idle,961 res: RNone,962 slot: false,963 srv: SNone,964 token: 0965 }966 )967}968969[State 23]970{971 nextToken: 2,972 present: false,973 rowStale: false,974 rowToken: 0,975 touched: false,976 ws:977 Map(978 "w1" ->979 {980 conn: false,981 outputs: false,982 phase: Idle,983 res: RNone,984 slot: false,985 srv: SNone,986 token: 0987 },988 "w2" ->989 {990 conn: false,991 outputs: false,992 phase: Idle,993 res: RNone,994 slot: false,995 srv: SNone,996 token: 0997 },998 "w3" ->999 {1000 conn: false,1001 outputs: false,1002 phase: Idle,1003 res: RNone,1004 slot: false,1005 srv: SNone,1006 token: 01007 }1008 )1009}10101011[State 24]1012{1013 nextToken: 2,1014 present: false,1015 rowStale: false,1016 rowToken: 0,1017 touched: false,1018 ws:1019 Map(1020 "w1" ->1021 {1022 conn: false,1023 outputs: false,1024 phase: Idle,1025 res: RNone,1026 slot: false,1027 srv: SNone,1028 token: 01029 },1030 "w2" ->1031 {1032 conn: true,1033 outputs: false,1034 phase: Pending,1035 res: RNone,1036 slot: true,1037 srv: SNeed,1038 token: 01039 },1040 "w3" ->1041 {1042 conn: false,1043 outputs: false,1044 phase: Idle,1045 res: RNone,1046 slot: false,1047 srv: SNone,1048 token: 01049 }1050 )1051}10521053[State 25]1054{1055 nextToken: 2,1056 present: false,1057 rowStale: false,1058 rowToken: 0,1059 touched: false,1060 ws:1061 Map(1062 "w1" ->1063 {1064 conn: false,1065 outputs: false,1066 phase: Idle,1067 res: RNone,1068 slot: false,1069 srv: SNone,1070 token: 01071 },1072 "w2" ->1073 {1074 conn: false,1075 outputs: false,1076 phase: Pending,1077 res: RNone,1078 slot: true,1079 srv: SNone,1080 token: 01081 },1082 "w3" ->1083 {1084 conn: false,1085 outputs: false,1086 phase: Idle,1087 res: RNone,1088 slot: false,1089 srv: SNone,1090 token: 01091 }1092 )1093}10941095[State 26]1096{1097 nextToken: 2,1098 present: false,1099 rowStale: false,1100 rowToken: 0,1101 touched: false,1102 ws:1103 Map(1104 "w1" ->1105 {1106 conn: false,1107 outputs: false,1108 phase: Idle,1109 res: RNone,1110 slot: false,1111 srv: SNone,1112 token: 01113 },1114 "w2" ->1115 {1116 conn: false,1117 outputs: false,1118 phase: Done,1119 res: RUnavailable,1120 slot: false,1121 srv: SNone,1122 token: 01123 },1124 "w3" ->1125 {1126 conn: false,1127 outputs: false,1128 phase: Idle,1129 res: RNone,1130 slot: false,1131 srv: SNone,1132 token: 01133 }1134 )1135}11361137[State 27]1138{1139 nextToken: 2,1140 present: false,1141 rowStale: false,1142 rowToken: 0,1143 touched: false,1144 ws:1145 Map(1146 "w1" ->1147 {1148 conn: false,1149 outputs: false,1150 phase: Idle,1151 res: RNone,1152 slot: false,1153 srv: SNone,1154 token: 01155 },1156 "w2" ->1157 {1158 conn: false,1159 outputs: false,1160 phase: Done,1161 res: RUnavailable,1162 slot: false,1163 srv: SNone,1164 token: 01165 },1166 "w3" ->1167 {1168 conn: true,1169 outputs: false,1170 phase: Pending,1171 res: RNone,1172 slot: true,1173 srv: SNeed,1174 token: 01175 }1176 )1177}11781179[State 28]1180{1181 nextToken: 2,1182 present: false,1183 rowStale: false,1184 rowToken: 0,1185 touched: false,1186 ws:1187 Map(1188 "w1" ->1189 {1190 conn: false,1191 outputs: false,1192 phase: Idle,1193 res: RNone,1194 slot: false,1195 srv: SNone,1196 token: 01197 },1198 "w2" ->1199 {1200 conn: false,1201 outputs: false,1202 phase: Idle,1203 res: RNone,1204 slot: false,1205 srv: SNone,1206 token: 01207 },1208 "w3" ->1209 {1210 conn: true,1211 outputs: false,1212 phase: Pending,1213 res: RNone,1214 slot: true,1215 srv: SNeed,1216 token: 01217 }1218 )1219}12201221[State 29]1222{1223 nextToken: 2,1224 present: false,1225 rowStale: false,1226 rowToken: 0,1227 touched: false,1228 ws:1229 Map(1230 "w1" ->1231 {1232 conn: false,1233 outputs: false,1234 phase: Idle,1235 res: RNone,1236 slot: false,1237 srv: SNone,1238 token: 01239 },1240 "w2" ->1241 {1242 conn: false,1243 outputs: false,1244 phase: Idle,1245 res: RNone,1246 slot: false,1247 srv: SNone,1248 token: 01249 },1250 "w3" ->1251 {1252 conn: false,1253 outputs: false,1254 phase: Pending,1255 res: RNone,1256 slot: true,1257 srv: SNone,1258 token: 01259 }1260 )1261}12621263[State 30]1264{1265 nextToken: 2,1266 present: false,1267 rowStale: false,1268 rowToken: 0,1269 touched: false,1270 ws:1271 Map(1272 "w1" ->1273 {1274 conn: false,1275 outputs: false,1276 phase: Idle,1277 res: RNone,1278 slot: false,1279 srv: SNone,1280 token: 01281 },1282 "w2" ->1283 {1284 conn: false,1285 outputs: false,1286 phase: Idle,1287 res: RNone,1288 slot: false,1289 srv: SNone,1290 token: 01291 },1292 "w3" ->1293 {1294 conn: true,1295 outputs: false,1296 phase: Pending,1297 res: RNone,1298 slot: true,1299 srv: SNeed,1300 token: 01301 }1302 )1303}13041305[ok] No violation found (12031ms at 1662 traces/second).1306Trace length statistics: max=31, min=31, average=31.001307You may increase --max-samples and --max-steps.1308Use --verbosity to produce more (or less) output.1309Use --seed=0x52fe5b3db5ac6187 --backend=rust to reproduce.1310Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 91s | 35/20000 samples | 227 samples/sRunning... [■■■■■■■■■■■■■■■ ] 36% | ETA: 1s | 7305/20000 samples | 27566 samples/sRunning... [■■■■■■■■■■■■■■■ ] 36% | ETA: 1s | 7305/20000 samples | 27566 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■ ] 52% | ETA: 1s | 10422/20000 samples | 23160 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 63% | ETA: 1s | 12753/20000 samples | 22374 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 67% | ETA: 1s | 13430/20000 samples | 19867 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 75% | ETA: 1s | 15040/20000 samples | 19282 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 83% | ETA: 1s | 16702/20000 samples | 17308 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 83% | ETA: 1s | 16702/20000 samples | 17308 samples/sAn example execution:13111312[State 0]1313{1314 hookFixed::hook::cache: Set(),1315 hookFixed::hook::drvUploaded: false,1316 hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1317 hookFixed::hook::phase: Query,1318 hookFixed::hook::restarts: 0,1319 hookFixed::hook::retries: 0,1320 hookFixed::hook::toUpload: Set()1321}13221323[State 1]1324{1325 hookFixed::hook::cache: Set(),1326 hookFixed::hook::drvUploaded: false,1327 hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1328 hookFixed::hook::phase: Upload,1329 hookFixed::hook::restarts: 0,1330 hookFixed::hook::retries: 0,1331 hookFixed::hook::toUpload: Set("drv", "in")1332}13331334[State 2]1335{1336 hookFixed::hook::cache: Set(),1337 hookFixed::hook::drvUploaded: false,1338 hookFixed::hook::local: Map("w1" -> Set("drv", "in"), "w2" -> Set()),1339 hookFixed::hook::phase: Upload,1340 hookFixed::hook::restarts: 1,1341 hookFixed::hook::retries: 1,1342 hookFixed::hook::toUpload: Set("drv", "in")1343}13441345[State 3]1346{1347 hookFixed::hook::cache: Set(),1348 hookFixed::hook::drvUploaded: false,1349 hookFixed::hook::local: Map("w1" -> Set("drv", "in"), "w2" -> Set()),1350 hookFixed::hook::phase: Upload,1351 hookFixed::hook::restarts: 2,1352 hookFixed::hook::retries: 2,1353 hookFixed::hook::toUpload: Set("drv", "in")1354}13551356[State 4]1357{1358 hookFixed::hook::cache: Set("drv", "in"),1359 hookFixed::hook::drvUploaded: false,1360 hookFixed::hook::local:1361 Map("w1" -> Set("drv", "in"), "w2" -> Set("drv", "in")),1362 hookFixed::hook::phase: Build,1363 hookFixed::hook::restarts: 2,1364 hookFixed::hook::retries: 2,1365 hookFixed::hook::toUpload: Set("drv", "in")1366}13671368[State 5]1369{1370 hookFixed::hook::cache: Set("drv", "in", "out"),1371 hookFixed::hook::drvUploaded: false,1372 hookFixed::hook::local:1373 Map("w1" -> Set("drv", "in", "out"), "w2" -> Set("drv", "in")),1374 hookFixed::hook::phase: Fetch,1375 hookFixed::hook::restarts: 2,1376 hookFixed::hook::retries: 2,1377 hookFixed::hook::toUpload: Set("drv", "in")1378}13791380[State 6]1381{1382 hookFixed::hook::cache: Set("drv", "in", "out"),1383 hookFixed::hook::drvUploaded: false,1384 hookFixed::hook::local:1385 Map("w1" -> Set("drv", "in", "out"), "w2" -> Set("drv", "in")),1386 hookFixed::hook::phase: Done,1387 hookFixed::hook::restarts: 2,1388 hookFixed::hook::retries: 2,1389 hookFixed::hook::toUpload: Set("drv", "in")1390}13911392[ok] No violation found (1114ms at 17953 traces/second).1393Trace length statistics: max=7, min=5, average=6.751394You may increase --max-samples and --max-steps.1395Use --verbosity to produce more (or less) output.1396Use --seed=0xb9be42e6f736a061 --backend=rust to reproduce.1397Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sAn example execution:13981399[State 0]1400{1401 hookNoSubstituteRefs::hook::cache: Set(),1402 hookNoSubstituteRefs::hook::drvUploaded: false,1403 hookNoSubstituteRefs::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1404 hookNoSubstituteRefs::hook::phase: Query,1405 hookNoSubstituteRefs::hook::restarts: 0,1406 hookNoSubstituteRefs::hook::retries: 0,1407 hookNoSubstituteRefs::hook::toUpload: Set()1408}14091410[State 1]1411{1412 hookNoSubstituteRefs::hook::cache: Set("in"),1413 hookNoSubstituteRefs::hook::drvUploaded: false,1414 hookNoSubstituteRefs::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1415 hookNoSubstituteRefs::hook::phase: Upload,1416 hookNoSubstituteRefs::hook::restarts: 0,1417 hookNoSubstituteRefs::hook::retries: 0,1418 hookNoSubstituteRefs::hook::toUpload: Set("drv")1419}14201421[State 2]1422{1423 hookNoSubstituteRefs::hook::cache: Set("in"),1424 hookNoSubstituteRefs::hook::drvUploaded: false,1425 hookNoSubstituteRefs::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),1426 hookNoSubstituteRefs::hook::phase: Failed,1427 hookNoSubstituteRefs::hook::restarts: 0,1428 hookNoSubstituteRefs::hook::retries: 0,1429 hookNoSubstituteRefs::hook::toUpload: Set("drv")1430}14311432[violation] Found an issue (380ms at 205 traces/second).1433Use --verbosity=3 to show executions.1434Use --seed=0x5f8bc60f54b5deda --backend=rust to reproduce.1435error: Invariant violated1436Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sAn example execution:14371438[State 0]1439{1440 hookNoSubstituteDrv::hook::cache: Set(),1441 hookNoSubstituteDrv::hook::drvUploaded: false,1442 hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set()),1443 hookNoSubstituteDrv::hook::phase: Query,1444 hookNoSubstituteDrv::hook::restarts: 0,1445 hookNoSubstituteDrv::hook::retries: 0,1446 hookNoSubstituteDrv::hook::toUpload: Set()1447}14481449[State 1]1450{1451 hookNoSubstituteDrv::hook::cache: Set(),1452 hookNoSubstituteDrv::hook::drvUploaded: false,1453 hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set()),1454 hookNoSubstituteDrv::hook::phase: Upload,1455 hookNoSubstituteDrv::hook::restarts: 0,1456 hookNoSubstituteDrv::hook::retries: 0,1457 hookNoSubstituteDrv::hook::toUpload: Set("drv", "in")1458}14591460[State 2]1461{1462 hookNoSubstituteDrv::hook::cache: Set("drv", "in"),1463 hookNoSubstituteDrv::hook::drvUploaded: false,1464 hookNoSubstituteDrv::hook::local:1465 Map("w1" -> Set(), "w2" -> Set("drv", "in")),1466 hookNoSubstituteDrv::hook::phase: Build,1467 hookNoSubstituteDrv::hook::restarts: 0,1468 hookNoSubstituteDrv::hook::retries: 0,1469 hookNoSubstituteDrv::hook::toUpload: Set("drv", "in")1470}14711472[State 3]1473{1474 hookNoSubstituteDrv::hook::cache: Set("drv", "in"),1475 hookNoSubstituteDrv::hook::drvUploaded: false,1476 hookNoSubstituteDrv::hook::local:1477 Map("w1" -> Set(), "w2" -> Set("drv", "in")),1478 hookNoSubstituteDrv::hook::phase: UploadDrv,1479 hookNoSubstituteDrv::hook::restarts: 0,1480 hookNoSubstituteDrv::hook::retries: 0,1481 hookNoSubstituteDrv::hook::toUpload: Set("drv", "in")1482}14831484[State 4]1485{1486 hookNoSubstituteDrv::hook::cache: Set("drv", "in"),1487 hookNoSubstituteDrv::hook::drvUploaded: true,1488 hookNoSubstituteDrv::hook::local:1489 Map("w1" -> Set(), "w2" -> Set("drv", "in")),1490 hookNoSubstituteDrv::hook::phase: Build,1491 hookNoSubstituteDrv::hook::restarts: 0,1492 hookNoSubstituteDrv::hook::retries: 0,1493 hookNoSubstituteDrv::hook::toUpload: Set("drv", "in")1494}14951496[State 5]1497{1498 hookNoSubstituteDrv::hook::cache: Set("drv", "in"),1499 hookNoSubstituteDrv::hook::drvUploaded: true,1500 hookNoSubstituteDrv::hook::local:1501 Map("w1" -> Set(), "w2" -> Set("drv", "in")),1502 hookNoSubstituteDrv::hook::phase: Build,1503 hookNoSubstituteDrv::hook::restarts: 1,1504 hookNoSubstituteDrv::hook::retries: 1,1505 hookNoSubstituteDrv::hook::toUpload: Set("drv", "in")1506}15071508[State 6]1509{1510 hookNoSubstituteDrv::hook::cache: Set("drv", "in"),1511 hookNoSubstituteDrv::hook::drvUploaded: true,1512 hookNoSubstituteDrv::hook::local:1513 Map("w1" -> Set(), "w2" -> Set("drv", "in")),1514 hookNoSubstituteDrv::hook::phase: Failed,1515 hookNoSubstituteDrv::hook::restarts: 1,1516 hookNoSubstituteDrv::hook::retries: 1,1517 hookNoSubstituteDrv::hook::toUpload: Set("drv", "in")1518}15191520[violation] Found an issue (167ms at 599 traces/second).1521Use --verbosity=3 to show executions.1522Use --seed=0xc4a8bbaa51c21692 --backend=rust to reproduce.1523error: Invariant violated1524Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 274s | 3/20000 samples | 73 samples/sRunning... [■■■■■■■■■■■■■ ] 32% | ETA: 1s | 6412/20000 samples | 39826 samples/sRunning... [■■■■■■■■■■■■■■■ ] 37% | ETA: 1s | 7551/20000 samples | 27558 samples/sRunning... [■■■■■■■■■■■■■■■ ] 37% | ETA: 1s | 7551/20000 samples | 27558 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 43% | ETA: 1s | 8646/20000 samples | 18357 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 43% | ETA: 1s | 8646/20000 samples | 18357 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■ ] 54% | ETA: 1s | 10994/20000 samples | 15980 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■ ] 60% | ETA: 1s | 12007/20000 samples | 15141 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■ ] 60% | ETA: 1s | 12007/20000 samples | 15141 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 73% | ETA: 1s | 14704/20000 samples | 14221 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 79% | ETA: 1s | 15949/20000 samples | 13551 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 79% | ETA: 1s | 15949/20000 samples | 13551 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 91% | ETA: 1s | 18300/20000 samples | 13811 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 91% | ETA: 1s | 18300/20000 samples | 13811 samples/sAn example execution:15251526[State 0]1527{1528 pushFixed::push::byPath: Map(),1529 pushFixed::push::inflight: Set(),1530 pushFixed::push::left: Map(),1531 pushFixed::push::sent: Map()1532}15331534[State 1]1535{1536 pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),1537 pushFixed::push::inflight: Set((3, "a"), (3, "b")),1538 pushFixed::push::left: Map(3 -> 2),1539 pushFixed::push::sent: Map(3 -> Set("a", "b"))1540}15411542[State 2]1543{1544 pushFixed::push::byPath: Map("a" -> 2, "b" -> 2),1545 pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "a"), (3, "b")),1546 pushFixed::push::left: Map(2 -> 2, 3 -> 2),1547 pushFixed::push::sent: Map(2 -> Set("a", "b"), 3 -> Set("a", "b"))1548}15491550[State 3]1551{1552 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1553 pushFixed::push::inflight:1554 Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),1555 pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 2),1556 pushFixed::push::sent:1557 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1558}15591560[State 4]1561{1562 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1563 pushFixed::push::inflight:1564 Set((1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")),1565 pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 2),1566 pushFixed::push::sent:1567 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1568}15691570[State 5]1571{1572 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1573 pushFixed::push::inflight: Set((1, "b"), (2, "b"), (3, "a"), (3, "b")),1574 pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 2),1575 pushFixed::push::sent:1576 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1577}15781579[State 6]1580{1581 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1582 pushFixed::push::inflight: Set((1, "b"), (3, "a"), (3, "b")),1583 pushFixed::push::left: Map(1 -> 1, 2 -> 0, 3 -> 2),1584 pushFixed::push::sent:1585 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1586}15871588[State 7]1589{1590 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1591 pushFixed::push::inflight: Set((3, "a"), (3, "b")),1592 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 2),1593 pushFixed::push::sent:1594 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1595}15961597[State 8]1598{1599 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1600 pushFixed::push::inflight: Set((3, "b")),1601 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 1),1602 pushFixed::push::sent:1603 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1604}16051606[State 9]1607{1608 pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),1609 pushFixed::push::inflight: Set(),1610 pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0),1611 pushFixed::push::sent:1612 Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))1613}16141615[ok] No violation found (1508ms at 13263 traces/second).1616Trace length statistics: max=10, min=7, average=8.001617You may increase --max-samples and --max-steps.1618Use --verbosity to produce more (or less) output.1619Use --seed=0x47e7fd81622e254a --backend=rust to reproduce.1620Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [■■ ] 6% | ETA: 4s | 1247/20000 samples | 6053 samples/sRunning... [■■ ] 6% | ETA: 4s | 1247/20000 samples | 6053 samples/sRunning... [■■■■ ] 10% | ETA: 5s | 2018/20000 samples | 4435 samples/sRunning... [■■■■ ] 10% | ETA: 5s | 2018/20000 samples | 4435 samples/sRunning... [■■■■ ] 10% | ETA: 5s | 2018/20000 samples | 4435 samples/sRunning... [■■■■■■ ] 14% | ETA: 5s | 2975/20000 samples | 3696 samples/sRunning... [■■■■■■ ] 14% | ETA: 5s | 2975/20000 samples | 3696 samples/sRunning... [■■■■■■ ] 14% | ETA: 5s | 2975/20000 samples | 3696 samples/sRunning... [■■■■■■■ ] 17% | ETA: 6s | 3467/20000 samples | 3289 samples/sRunning... [■■■■■■■■ ] 19% | ETA: 6s | 3824/20000 samples | 3163 samples/sRunning... [■■■■■■■■ ] 19% | ETA: 6s | 3824/20000 samples | 3163 samples/sRunning... [■■■■■■■■ ] 19% | ETA: 6s | 3824/20000 samples | 3163 samples/sRunning... [■■■■■■■■ ] 21% | ETA: 6s | 4201/20000 samples | 2930 samples/sRunning... [■■■■■■■■ ] 21% | ETA: 6s | 4201/20000 samples | 2930 samples/sRunning... [■■■■■■■■■■ ] 23% | ETA: 6s | 4769/20000 samples | 2837 samples/sRunning... [■■■■■■■■■■ ] 24% | ETA: 6s | 4981/20000 samples | 2789 samples/sRunning... [■■■■■■■■■■ ] 24% | ETA: 6s | 4981/20000 samples | 2789 samples/sRunning... [■■■■■■■■■■■ ] 26% | ETA: 7s | 5330/20000 samples | 2755 samples/sRunning... [■■■■■■■■■■■ ] 26% | ETA: 7s | 5330/20000 samples | 2755 samples/sRunning... [■■■■■■■■■■■■ ] 29% | ETA: 7s | 5888/20000 samples | 2744 samples/sRunning... [■■■■■■■■■■■■ ] 29% | ETA: 7s | 5888/20000 samples | 2744 samples/sRunning... [■■■■■■■■■■■■■ ] 31% | ETA: 6s | 6396/20000 samples | 2732 samples/sRunning... [■■■■■■■■■■■■■ ] 33% | ETA: 6s | 6723/20000 samples | 2736 samples/sRunning... [■■■■■■■■■■■■■■ ] 34% | ETA: 6s | 6940/20000 samples | 2706 samples/sRunning... [■■■■■■■■■■■■■■■ ] 36% | ETA: 6s | 7288/20000 samples | 2693 samples/sRunning... [■■■■■■■■■■■■■■■ ] 36% | ETA: 6s | 7288/20000 samples | 2693 samples/sRunning... [■■■■■■■■■■■■■■■ ] 36% | ETA: 6s | 7288/20000 samples | 2693 samples/sRunning... [■■■■■■■■■■■■■■■■ ] 39% | ETA: 6s | 7882/20000 samples | 2667 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 41% | ETA: 5s | 8284/20000 samples | 2633 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 41% | ETA: 5s | 8284/20000 samples | 2633 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 43% | ETA: 5s | 8775/20000 samples | 2626 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 45% | ETA: 5s | 9021/20000 samples | 2616 samples/sRunning... [■■■■■■■■■■■■■■■■■■ ] 45% | ETA: 5s | 9021/20000 samples | 2616 samples/sRunning... [■■■■■■■■■■■■■■■■■■■ ] 47% | ETA: 5s | 9403/20000 samples | 2617 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 48% | ETA: 5s | 9779/20000 samples | 2638 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 50% | ETA: 4s | 10190/20000 samples | 2667 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 50% | ETA: 4s | 10190/20000 samples | 2667 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■ ] 53% | ETA: 4s | 10754/20000 samples | 2664 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■ ] 53% | ETA: 4s | 10754/20000 samples | 2664 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 56% | ETA: 4s | 11254/20000 samples | 2677 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 56% | ETA: 4s | 11254/20000 samples | 2677 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■ ] 61% | ETA: 3s | 12211/20000 samples | 2742 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■ ] 61% | ETA: 3s | 12211/20000 samples | 2742 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 65% | ETA: 3s | 13114/20000 samples | 2803 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 65% | ETA: 3s | 13114/20000 samples | 2803 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 65% | ETA: 3s | 13114/20000 samples | 2803 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 67% | ETA: 3s | 13495/20000 samples | 2740 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 68% | ETA: 3s | 13751/20000 samples | 2733 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 68% | ETA: 3s | 13751/20000 samples | 2733 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 73% | ETA: 2s | 14661/20000 samples | 2776 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 73% | ETA: 2s | 14661/20000 samples | 2776 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 75% | ETA: 2s | 15105/20000 samples | 2786 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 78% | ETA: 2s | 15764/20000 samples | 2808 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 78% | ETA: 2s | 15764/20000 samples | 2808 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 81% | ETA: 2s | 16249/20000 samples | 2811 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 81% | ETA: 2s | 16249/20000 samples | 2811 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 83% | ETA: 2s | 16623/20000 samples | 2794 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 85% | ETA: 2s | 17020/20000 samples | 2782 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 85% | ETA: 2s | 17020/20000 samples | 2782 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 87% | ETA: 1s | 17423/20000 samples | 2788 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 87% | ETA: 1s | 17423/20000 samples | 2788 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 90% | ETA: 1s | 18168/20000 samples | 2819 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 91% | ETA: 1s | 18360/20000 samples | 2789 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 93% | ETA: 1s | 18757/20000 samples | 2800 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 95% | ETA: 1s | 19156/20000 samples | 2804 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 97% | ETA: 1s | 19500/20000 samples | 2812 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 97% | ETA: 1s | 19500/20000 samples | 2812 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19846/20000 samples | 2792 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19846/20000 samples | 2792 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19846/20000 samples | 2792 samples/sAn example execution:16211622[State 0]1623{1624 nextToken: 1,1625 present: false,1626 rowStale: false,1627 rowToken: 0,1628 touched: false,1629 ws:1630 Map(1631 "w1" ->1632 {1633 conn: false,1634 outputs: false,1635 phase: Idle,1636 res: RNone,1637 slot: false,1638 srv: SNone,1639 token: 01640 },1641 "w2" ->1642 {1643 conn: false,1644 outputs: false,1645 phase: Idle,1646 res: RNone,1647 slot: false,1648 srv: SNone,1649 token: 01650 },1651 "w3" ->1652 {1653 conn: false,1654 outputs: false,1655 phase: Idle,1656 res: RNone,1657 slot: false,1658 srv: SNone,1659 token: 01660 }1661 )1662}16631664[State 1]1665{1666 nextToken: 1,1667 present: false,1668 rowStale: false,1669 rowToken: 0,1670 touched: false,1671 ws:1672 Map(1673 "w1" ->1674 {1675 conn: false,1676 outputs: false,1677 phase: Idle,1678 res: RNone,1679 slot: false,1680 srv: SNone,1681 token: 01682 },1683 "w2" ->1684 {1685 conn: true,1686 outputs: false,1687 phase: Pending,1688 res: RNone,1689 slot: true,1690 srv: SNeed,1691 token: 01692 },1693 "w3" ->1694 {1695 conn: false,1696 outputs: false,1697 phase: Idle,1698 res: RNone,1699 slot: false,1700 srv: SNone,1701 token: 01702 }1703 )1704}17051706[State 2]1707{1708 nextToken: 1,1709 present: false,1710 rowStale: false,1711 rowToken: 0,1712 touched: false,1713 ws:1714 Map(1715 "w1" ->1716 {1717 conn: false,1718 outputs: false,1719 phase: Idle,1720 res: RNone,1721 slot: false,1722 srv: SNone,1723 token: 01724 },1725 "w2" ->1726 {1727 conn: false,1728 outputs: false,1729 phase: Pending,1730 res: RNone,1731 slot: true,1732 srv: SNone,1733 token: 01734 },1735 "w3" ->1736 {1737 conn: false,1738 outputs: false,1739 phase: Idle,1740 res: RNone,1741 slot: false,1742 srv: SNone,1743 token: 01744 }1745 )1746}17471748[State 3]1749{1750 nextToken: 1,1751 present: false,1752 rowStale: false,1753 rowToken: 0,1754 touched: false,1755 ws:1756 Map(1757 "w1" ->1758 {1759 conn: false,1760 outputs: false,1761 phase: Idle,1762 res: RNone,1763 slot: false,1764 srv: SNone,1765 token: 01766 },1767 "w2" ->1768 {1769 conn: true,1770 outputs: false,1771 phase: Pending,1772 res: RNone,1773 slot: true,1774 srv: SNeed,1775 token: 01776 },1777 "w3" ->1778 {1779 conn: false,1780 outputs: false,1781 phase: Idle,1782 res: RNone,1783 slot: false,1784 srv: SNone,1785 token: 01786 }1787 )1788}17891790[State 4]1791{1792 nextToken: 2,1793 present: false,1794 rowStale: false,1795 rowToken: 1,1796 touched: false,1797 ws:1798 Map(1799 "w1" ->1800 {1801 conn: false,1802 outputs: false,1803 phase: Idle,1804 res: RNone,1805 slot: false,1806 srv: SNone,1807 token: 01808 },1809 "w2" ->1810 {1811 conn: true,1812 outputs: false,1813 phase: Building,1814 res: RNone,1815 slot: true,1816 srv: SHolder(1),1817 token: 11818 },1819 "w3" ->1820 {1821 conn: false,1822 outputs: false,1823 phase: Idle,1824 res: RNone,1825 slot: false,1826 srv: SNone,1827 token: 01828 }1829 )1830}18311832[State 5]1833{1834 nextToken: 2,1835 present: false,1836 rowStale: false,1837 rowToken: 1,1838 touched: false,1839 ws:1840 Map(1841 "w1" ->1842 {1843 conn: false,1844 outputs: false,1845 phase: Idle,1846 res: RNone,1847 slot: false,1848 srv: SNone,1849 token: 01850 },1851 "w2" ->1852 {1853 conn: false,1854 outputs: false,1855 phase: Building,1856 res: RNone,1857 slot: true,1858 srv: SNone,1859 token: 11860 },1861 "w3" ->1862 {1863 conn: false,1864 outputs: false,1865 phase: Idle,1866 res: RNone,1867 slot: false,1868 srv: SNone,1869 token: 01870 }1871 )1872}18731874[State 6]1875{1876 nextToken: 2,1877 present: false,1878 rowStale: false,1879 rowToken: 1,1880 touched: false,1881 ws:1882 Map(1883 "w1" ->1884 {1885 conn: false,1886 outputs: false,1887 phase: Idle,1888 res: RNone,1889 slot: false,1890 srv: SNone,1891 token: 01892 },1893 "w2" ->1894 {1895 conn: true,1896 outputs: false,1897 phase: Building,1898 res: RNone,1899 slot: true,1900 srv: SNeed,1901 token: 11902 },1903 "w3" ->1904 {1905 conn: false,1906 outputs: false,1907 phase: Idle,1908 res: RNone,1909 slot: false,1910 srv: SNone,1911 token: 01912 }1913 )1914}19151916[State 7]1917{1918 nextToken: 2,1919 present: false,1920 rowStale: false,1921 rowToken: 1,1922 touched: false,1923 ws:1924 Map(1925 "w1" ->1926 {1927 conn: false,1928 outputs: false,1929 phase: Idle,1930 res: RNone,1931 slot: false,1932 srv: SNone,1933 token: 01934 },1935 "w2" ->1936 {1937 conn: false,1938 outputs: false,1939 phase: Building,1940 res: RNone,1941 slot: true,1942 srv: SNone,1943 token: 11944 },1945 "w3" ->1946 {1947 conn: false,1948 outputs: false,1949 phase: Idle,1950 res: RNone,1951 slot: false,1952 srv: SNone,1953 token: 01954 }1955 )1956}19571958[State 8]1959{1960 nextToken: 2,1961 present: false,1962 rowStale: false,1963 rowToken: 1,1964 touched: false,1965 ws:1966 Map(1967 "w1" ->1968 {1969 conn: false,1970 outputs: false,1971 phase: Idle,1972 res: RNone,1973 slot: false,1974 srv: SNone,1975 token: 01976 },1977 "w2" ->1978 {1979 conn: true,1980 outputs: false,1981 phase: Building,1982 res: RNone,1983 slot: true,1984 srv: SNeed,1985 token: 11986 },1987 "w3" ->1988 {1989 conn: false,1990 outputs: false,1991 phase: Idle,1992 res: RNone,1993 slot: false,1994 srv: SNone,1995 token: 01996 }1997 )1998}19992000[State 9]2001{2002 nextToken: 2,2003 present: false,2004 rowStale: false,2005 rowToken: 1,2006 touched: false,2007 ws:2008 Map(2009 "w1" ->2010 {2011 conn: false,2012 outputs: false,2013 phase: Idle,2014 res: RNone,2015 slot: false,2016 srv: SNone,2017 token: 02018 },2019 "w2" ->2020 {2021 conn: true,2022 outputs: false,2023 phase: Building,2024 res: RNone,2025 slot: true,2026 srv: SHolder(1),2027 token: 12028 },2029 "w3" ->2030 {2031 conn: false,2032 outputs: false,2033 phase: Idle,2034 res: RNone,2035 slot: false,2036 srv: SNone,2037 token: 02038 }2039 )2040}20412042[State 10]2043{2044 nextToken: 2,2045 present: false,2046 rowStale: false,2047 rowToken: 0,2048 touched: false,2049 ws:2050 Map(2051 "w1" ->2052 {2053 conn: false,2054 outputs: false,2055 phase: Idle,2056 res: RNone,2057 slot: false,2058 srv: SNone,2059 token: 02060 },2061 "w2" ->2062 {2063 conn: false,2064 outputs: false,2065 phase: Done,2066 res: RUnavailable,2067 slot: false,2068 srv: SNone,2069 token: 12070 },2071 "w3" ->2072 {2073 conn: false,2074 outputs: false,2075 phase: Idle,2076 res: RNone,2077 slot: false,2078 srv: SNone,2079 token: 02080 }2081 )2082}20832084[State 11]2085{2086 nextToken: 2,2087 present: false,2088 rowStale: false,2089 rowToken: 0,2090 touched: false,2091 ws:2092 Map(2093 "w1" ->2094 {2095 conn: false,2096 outputs: false,2097 phase: Idle,2098 res: RNone,2099 slot: false,2100 srv: SNone,2101 token: 02102 },2103 "w2" ->2104 {2105 conn: false,2106 outputs: false,2107 phase: Done,2108 res: RUnavailable,2109 slot: false,2110 srv: SNone,2111 token: 12112 },2113 "w3" ->2114 {2115 conn: true,2116 outputs: false,2117 phase: Pending,2118 res: RNone,2119 slot: true,2120 srv: SNeed,2121 token: 02122 }2123 )2124}21252126[State 12]2127{2128 nextToken: 2,2129 present: false,2130 rowStale: false,2131 rowToken: 0,2132 touched: false,2133 ws:2134 Map(2135 "w1" ->2136 {2137 conn: false,2138 outputs: false,2139 phase: Idle,2140 res: RNone,2141 slot: false,2142 srv: SNone,2143 token: 02144 },2145 "w2" ->2146 {2147 conn: false,2148 outputs: false,2149 phase: Done,2150 res: RUnavailable,2151 slot: false,2152 srv: SNone,2153 token: 12154 },2155 "w3" ->2156 {2157 conn: false,2158 outputs: false,2159 phase: Pending,2160 res: RNone,2161 slot: true,2162 srv: SNone,2163 token: 02164 }2165 )2166}21672168[State 13]2169{2170 nextToken: 2,2171 present: false,2172 rowStale: false,2173 rowToken: 0,2174 touched: false,2175 ws:2176 Map(2177 "w1" ->2178 {2179 conn: false,2180 outputs: false,2181 phase: Idle,2182 res: RNone,2183 slot: false,2184 srv: SNone,2185 token: 02186 },2187 "w2" ->2188 {2189 conn: false,2190 outputs: false,2191 phase: Done,2192 res: RUnavailable,2193 slot: false,2194 srv: SNone,2195 token: 12196 },2197 "w3" ->2198 {2199 conn: true,2200 outputs: false,2201 phase: Pending,2202 res: RNone,2203 slot: true,2204 srv: SNeed,2205 token: 02206 }2207 )2208}22092210[State 14]2211{2212 nextToken: 2,2213 present: false,2214 rowStale: false,2215 rowToken: 0,2216 touched: false,2217 ws:2218 Map(2219 "w1" ->2220 {2221 conn: false,2222 outputs: false,2223 phase: Idle,2224 res: RNone,2225 slot: false,2226 srv: SNone,2227 token: 02228 },2229 "w2" ->2230 {2231 conn: false,2232 outputs: false,2233 phase: Done,2234 res: RUnavailable,2235 slot: false,2236 srv: SNone,2237 token: 12238 },2239 "w3" ->2240 {2241 conn: false,2242 outputs: false,2243 phase: Pending,2244 res: RNone,2245 slot: true,2246 srv: SNone,2247 token: 02248 }2249 )2250}22512252[State 15]2253{2254 nextToken: 2,2255 present: false,2256 rowStale: false,2257 rowToken: 0,2258 touched: false,2259 ws:2260 Map(2261 "w1" ->2262 {2263 conn: false,2264 outputs: false,2265 phase: Idle,2266 res: RNone,2267 slot: false,2268 srv: SNone,2269 token: 02270 },2271 "w2" ->2272 {2273 conn: false,2274 outputs: false,2275 phase: Done,2276 res: RUnavailable,2277 slot: false,2278 srv: SNone,2279 token: 12280 },2281 "w3" ->2282 {2283 conn: true,2284 outputs: false,2285 phase: Pending,2286 res: RNone,2287 slot: true,2288 srv: SNeed,2289 token: 02290 }2291 )2292}22932294[State 16]2295{2296 nextToken: 2,2297 present: false,2298 rowStale: false,2299 rowToken: 0,2300 touched: false,2301 ws:2302 Map(2303 "w1" ->2304 {2305 conn: false,2306 outputs: false,2307 phase: Idle,2308 res: RNone,2309 slot: false,2310 srv: SNone,2311 token: 02312 },2313 "w2" ->2314 {2315 conn: false,2316 outputs: false,2317 phase: Done,2318 res: RUnavailable,2319 slot: false,2320 srv: SNone,2321 token: 12322 },2323 "w3" ->2324 {2325 conn: false,2326 outputs: false,2327 phase: Pending,2328 res: RNone,2329 slot: true,2330 srv: SNone,2331 token: 02332 }2333 )2334}23352336[State 17]2337{2338 nextToken: 2,2339 present: false,2340 rowStale: false,2341 rowToken: 0,2342 touched: false,2343 ws:2344 Map(2345 "w1" ->2346 {2347 conn: false,2348 outputs: false,2349 phase: Idle,2350 res: RNone,2351 slot: false,2352 srv: SNone,2353 token: 02354 },2355 "w2" ->2356 {2357 conn: false,2358 outputs: false,2359 phase: Done,2360 res: RUnavailable,2361 slot: false,2362 srv: SNone,2363 token: 12364 },2365 "w3" ->2366 {2367 conn: true,2368 outputs: false,2369 phase: Pending,2370 res: RNone,2371 slot: true,2372 srv: SNeed,2373 token: 02374 }2375 )2376}23772378[State 18]2379{2380 nextToken: 2,2381 present: false,2382 rowStale: false,2383 rowToken: 0,2384 touched: false,2385 ws:2386 Map(2387 "w1" ->2388 {2389 conn: false,2390 outputs: false,2391 phase: Idle,2392 res: RNone,2393 slot: false,2394 srv: SNone,2395 token: 02396 },2397 "w2" ->2398 {2399 conn: false,2400 outputs: false,2401 phase: Done,2402 res: RUnavailable,2403 slot: false,2404 srv: SNone,2405 token: 12406 },2407 "w3" ->2408 {2409 conn: false,2410 outputs: false,2411 phase: Pending,2412 res: RNone,2413 slot: true,2414 srv: SNone,2415 token: 02416 }2417 )2418}24192420[State 19]2421{2422 nextToken: 2,2423 present: false,2424 rowStale: false,2425 rowToken: 0,2426 touched: false,2427 ws:2428 Map(2429 "w1" ->2430 {2431 conn: false,2432 outputs: false,2433 phase: Idle,2434 res: RNone,2435 slot: false,2436 srv: SNone,2437 token: 02438 },2439 "w2" ->2440 {2441 conn: false,2442 outputs: false,2443 phase: Done,2444 res: RUnavailable,2445 slot: false,2446 srv: SNone,2447 token: 12448 },2449 "w3" ->2450 {2451 conn: true,2452 outputs: false,2453 phase: Pending,2454 res: RNone,2455 slot: true,2456 srv: SNeed,2457 token: 02458 }2459 )2460}24612462[State 20]2463{2464 nextToken: 3,2465 present: false,2466 rowStale: false,2467 rowToken: 2,2468 touched: false,2469 ws:2470 Map(2471 "w1" ->2472 {2473 conn: false,2474 outputs: false,2475 phase: Idle,2476 res: RNone,2477 slot: false,2478 srv: SNone,2479 token: 02480 },2481 "w2" ->2482 {2483 conn: false,2484 outputs: false,2485 phase: Done,2486 res: RUnavailable,2487 slot: false,2488 srv: SNone,2489 token: 12490 },2491 "w3" ->2492 {2493 conn: true,2494 outputs: false,2495 phase: Building,2496 res: RNone,2497 slot: true,2498 srv: SHolder(2),2499 token: 22500 }2501 )2502}25032504[State 21]2505{2506 nextToken: 3,2507 present: false,2508 rowStale: false,2509 rowToken: 0,2510 touched: false,2511 ws:2512 Map(2513 "w1" ->2514 {2515 conn: false,2516 outputs: false,2517 phase: Idle,2518 res: RNone,2519 slot: false,2520 srv: SNone,2521 token: 02522 },2523 "w2" ->2524 {2525 conn: false,2526 outputs: false,2527 phase: Done,2528 res: RUnavailable,2529 slot: false,2530 srv: SNone,2531 token: 12532 },2533 "w3" ->2534 {2535 conn: false,2536 outputs: false,2537 phase: Done,2538 res: RUnavailable,2539 slot: false,2540 srv: SNone,2541 token: 22542 }2543 )2544}25452546[State 22]2547{2548 nextToken: 3,2549 present: false,2550 rowStale: false,2551 rowToken: 0,2552 touched: false,2553 ws:2554 Map(2555 "w1" ->2556 {2557 conn: true,2558 outputs: false,2559 phase: Pending,2560 res: RNone,2561 slot: true,2562 srv: SNeed,2563 token: 02564 },2565 "w2" ->2566 {2567 conn: false,2568 outputs: false,2569 phase: Done,2570 res: RUnavailable,2571 slot: false,2572 srv: SNone,2573 token: 12574 },2575 "w3" ->2576 {2577 conn: false,2578 outputs: false,2579 phase: Done,2580 res: RUnavailable,2581 slot: false,2582 srv: SNone,2583 token: 22584 }2585 )2586}25872588[State 23]2589{2590 nextToken: 4,2591 present: false,2592 rowStale: false,2593 rowToken: 3,2594 touched: false,2595 ws:2596 Map(2597 "w1" ->2598 {2599 conn: true,2600 outputs: false,2601 phase: Building,2602 res: RNone,2603 slot: true,2604 srv: SHolder(3),2605 token: 32606 },2607 "w2" ->2608 {2609 conn: false,2610 outputs: false,2611 phase: Done,2612 res: RUnavailable,2613 slot: false,2614 srv: SNone,2615 token: 12616 },2617 "w3" ->2618 {2619 conn: false,2620 outputs: false,2621 phase: Done,2622 res: RUnavailable,2623 slot: false,2624 srv: SNone,2625 token: 22626 }2627 )2628}26292630[State 24]2631{2632 nextToken: 4,2633 present: false,2634 rowStale: false,2635 rowToken: 3,2636 touched: false,2637 ws:2638 Map(2639 "w1" ->2640 {2641 conn: false,2642 outputs: false,2643 phase: Building,2644 res: RNone,2645 slot: true,2646 srv: SNone,2647 token: 32648 },2649 "w2" ->2650 {2651 conn: false,2652 outputs: false,2653 phase: Done,2654 res: RUnavailable,2655 slot: false,2656 srv: SNone,2657 token: 12658 },2659 "w3" ->2660 {2661 conn: false,2662 outputs: false,2663 phase: Done,2664 res: RUnavailable,2665 slot: false,2666 srv: SNone,2667 token: 22668 }2669 )2670}26712672[State 25]2673{2674 nextToken: 4,2675 present: false,2676 rowStale: false,2677 rowToken: 3,2678 touched: false,2679 ws:2680 Map(2681 "w1" ->2682 {2683 conn: true,2684 outputs: false,2685 phase: Building,2686 res: RNone,2687 slot: true,2688 srv: SNeed,2689 token: 32690 },2691 "w2" ->2692 {2693 conn: false,2694 outputs: false,2695 phase: Done,2696 res: RUnavailable,2697 slot: false,2698 srv: SNone,2699 token: 12700 },2701 "w3" ->2702 {2703 conn: false,2704 outputs: false,2705 phase: Done,2706 res: RUnavailable,2707 slot: false,2708 srv: SNone,2709 token: 22710 }2711 )2712}27132714[State 26]2715{2716 nextToken: 4,2717 present: false,2718 rowStale: false,2719 rowToken: 3,2720 touched: false,2721 ws:2722 Map(2723 "w1" ->2724 {2725 conn: false,2726 outputs: false,2727 phase: Building,2728 res: RNone,2729 slot: true,2730 srv: SNone,2731 token: 32732 },2733 "w2" ->2734 {2735 conn: false,2736 outputs: false,2737 phase: Done,2738 res: RUnavailable,2739 slot: false,2740 srv: SNone,2741 token: 12742 },2743 "w3" ->2744 {2745 conn: false,2746 outputs: false,2747 phase: Done,2748 res: RUnavailable,2749 slot: false,2750 srv: SNone,2751 token: 22752 }2753 )2754}27552756[State 27]2757{2758 nextToken: 4,2759 present: false,2760 rowStale: false,2761 rowToken: 3,2762 touched: false,2763 ws:2764 Map(2765 "w1" ->2766 {2767 conn: true,2768 outputs: false,2769 phase: Building,2770 res: RNone,2771 slot: true,2772 srv: SNeed,2773 token: 32774 },2775 "w2" ->2776 {2777 conn: false,2778 outputs: false,2779 phase: Done,2780 res: RUnavailable,2781 slot: false,2782 srv: SNone,2783 token: 12784 },2785 "w3" ->2786 {2787 conn: false,2788 outputs: false,2789 phase: Done,2790 res: RUnavailable,2791 slot: false,2792 srv: SNone,2793 token: 22794 }2795 )2796}27972798[State 28]2799{2800 nextToken: 4,2801 present: false,2802 rowStale: false,2803 rowToken: 3,2804 touched: false,2805 ws:2806 Map(2807 "w1" ->2808 {2809 conn: true,2810 outputs: true,2811 phase: Publishing,2812 res: RNone,2813 slot: true,2814 srv: SNeed,2815 token: 32816 },2817 "w2" ->2818 {2819 conn: false,2820 outputs: false,2821 phase: Done,2822 res: RUnavailable,2823 slot: false,2824 srv: SNone,2825 token: 12826 },2827 "w3" ->2828 {2829 conn: false,2830 outputs: false,2831 phase: Done,2832 res: RUnavailable,2833 slot: false,2834 srv: SNone,2835 token: 22836 }2837 )2838}28392840[State 29]2841{2842 nextToken: 4,2843 present: false,2844 rowStale: false,2845 rowToken: 3,2846 touched: false,2847 ws:2848 Map(2849 "w1" ->2850 {2851 conn: true,2852 outputs: true,2853 phase: Publishing,2854 res: RNone,2855 slot: true,2856 srv: SHolder(3),2857 token: 32858 },2859 "w2" ->2860 {2861 conn: false,2862 outputs: false,2863 phase: Done,2864 res: RUnavailable,2865 slot: false,2866 srv: SNone,2867 token: 12868 },2869 "w3" ->2870 {2871 conn: false,2872 outputs: false,2873 phase: Done,2874 res: RUnavailable,2875 slot: false,2876 srv: SNone,2877 token: 22878 }2879 )2880}28812882[State 30]2883{2884 nextToken: 4,2885 present: true,2886 rowStale: false,2887 rowToken: 0,2888 touched: true,2889 ws:2890 Map(2891 "w1" ->2892 {2893 conn: false,2894 outputs: false,2895 phase: Done,2896 res: RBuilt,2897 slot: false,2898 srv: SNone,2899 token: 32900 },2901 "w2" ->2902 {2903 conn: false,2904 outputs: false,2905 phase: Done,2906 res: RUnavailable,2907 slot: false,2908 srv: SNone,2909 token: 12910 },2911 "w3" ->2912 {2913 conn: false,2914 outputs: false,2915 phase: Done,2916 res: RUnavailable,2917 slot: false,2918 srv: SNone,2919 token: 22920 }2921 )2922}29232924[ok] No violation found (7409ms at 2699 traces/second).2925Trace length statistics: max=31, min=9, average=18.592926You may increase --max-samples and --max-steps.2927Use --verbosity to produce more (or less) output.2928Use --seed=0x515f12ed2468f1a0 --backend=rust to reproduce.