Running... [ ] 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: [State 0] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 1] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 2] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 3] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 4] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 5] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 6] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 7] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 8] { nextToken: 2, present: false, rowStale: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 9] { nextToken: 2, present: false, rowStale: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 10] { nextToken: 2, present: false, rowStale: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 11] { nextToken: 2, present: false, rowStale: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 12] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 13] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 14] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 15] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 16] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 17] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 18] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 19] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 20] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 21] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 22] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 23] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 24] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 25] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 26] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 27] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 28] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 29] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 } ) } [State 30] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [ok] No violation found (12031ms at 1662 traces/second). Trace length statistics: max=31, min=31, average=31.00 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0x52fe5b3db5ac6187 --backend=rust to reproduce. Running... [ ] 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: [State 0] { hookFixed::hook::cache: Set(), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set()), hookFixed::hook::phase: Query, hookFixed::hook::restarts: 0, hookFixed::hook::retries: 0, hookFixed::hook::toUpload: Set() } [State 1] { hookFixed::hook::cache: Set(), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set()), hookFixed::hook::phase: Upload, hookFixed::hook::restarts: 0, hookFixed::hook::retries: 0, hookFixed::hook::toUpload: Set("drv", "in") } [State 2] { hookFixed::hook::cache: Set(), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("drv", "in"), "w2" -> Set()), hookFixed::hook::phase: Upload, hookFixed::hook::restarts: 1, hookFixed::hook::retries: 1, hookFixed::hook::toUpload: Set("drv", "in") } [State 3] { hookFixed::hook::cache: Set(), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("drv", "in"), "w2" -> Set()), hookFixed::hook::phase: Upload, hookFixed::hook::restarts: 2, hookFixed::hook::retries: 2, hookFixed::hook::toUpload: Set("drv", "in") } [State 4] { hookFixed::hook::cache: Set("drv", "in"), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("drv", "in"), "w2" -> Set("drv", "in")), hookFixed::hook::phase: Build, hookFixed::hook::restarts: 2, hookFixed::hook::retries: 2, hookFixed::hook::toUpload: Set("drv", "in") } [State 5] { hookFixed::hook::cache: Set("drv", "in", "out"), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("drv", "in", "out"), "w2" -> Set("drv", "in")), hookFixed::hook::phase: Fetch, hookFixed::hook::restarts: 2, hookFixed::hook::retries: 2, hookFixed::hook::toUpload: Set("drv", "in") } [State 6] { hookFixed::hook::cache: Set("drv", "in", "out"), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("drv", "in", "out"), "w2" -> Set("drv", "in")), hookFixed::hook::phase: Done, hookFixed::hook::restarts: 2, hookFixed::hook::retries: 2, hookFixed::hook::toUpload: Set("drv", "in") } [ok] No violation found (1114ms at 17953 traces/second). Trace length statistics: max=7, min=5, average=6.75 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0xb9be42e6f736a061 --backend=rust to reproduce. Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sAn example execution: [State 0] { hookNoSubstituteRefs::hook::cache: Set(), hookNoSubstituteRefs::hook::drvUploaded: false, hookNoSubstituteRefs::hook::local: Map("w1" -> Set("in"), "w2" -> Set()), hookNoSubstituteRefs::hook::phase: Query, hookNoSubstituteRefs::hook::restarts: 0, hookNoSubstituteRefs::hook::retries: 0, hookNoSubstituteRefs::hook::toUpload: Set() } [State 1] { hookNoSubstituteRefs::hook::cache: Set("in"), hookNoSubstituteRefs::hook::drvUploaded: false, hookNoSubstituteRefs::hook::local: Map("w1" -> Set("in"), "w2" -> Set()), hookNoSubstituteRefs::hook::phase: Upload, hookNoSubstituteRefs::hook::restarts: 0, hookNoSubstituteRefs::hook::retries: 0, hookNoSubstituteRefs::hook::toUpload: Set("drv") } [State 2] { hookNoSubstituteRefs::hook::cache: Set("in"), hookNoSubstituteRefs::hook::drvUploaded: false, hookNoSubstituteRefs::hook::local: Map("w1" -> Set("in"), "w2" -> Set()), hookNoSubstituteRefs::hook::phase: Failed, hookNoSubstituteRefs::hook::restarts: 0, hookNoSubstituteRefs::hook::retries: 0, hookNoSubstituteRefs::hook::toUpload: Set("drv") } [violation] Found an issue (380ms at 205 traces/second). Use --verbosity=3 to show executions. Use --seed=0x5f8bc60f54b5deda --backend=rust to reproduce. error: Invariant violated Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sAn example execution: [State 0] { hookNoSubstituteDrv::hook::cache: Set(), hookNoSubstituteDrv::hook::drvUploaded: false, hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set()), hookNoSubstituteDrv::hook::phase: Query, hookNoSubstituteDrv::hook::restarts: 0, hookNoSubstituteDrv::hook::retries: 0, hookNoSubstituteDrv::hook::toUpload: Set() } [State 1] { hookNoSubstituteDrv::hook::cache: Set(), hookNoSubstituteDrv::hook::drvUploaded: false, hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set()), hookNoSubstituteDrv::hook::phase: Upload, hookNoSubstituteDrv::hook::restarts: 0, hookNoSubstituteDrv::hook::retries: 0, hookNoSubstituteDrv::hook::toUpload: Set("drv", "in") } [State 2] { hookNoSubstituteDrv::hook::cache: Set("drv", "in"), hookNoSubstituteDrv::hook::drvUploaded: false, hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set("drv", "in")), hookNoSubstituteDrv::hook::phase: Build, hookNoSubstituteDrv::hook::restarts: 0, hookNoSubstituteDrv::hook::retries: 0, hookNoSubstituteDrv::hook::toUpload: Set("drv", "in") } [State 3] { hookNoSubstituteDrv::hook::cache: Set("drv", "in"), hookNoSubstituteDrv::hook::drvUploaded: false, hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set("drv", "in")), hookNoSubstituteDrv::hook::phase: UploadDrv, hookNoSubstituteDrv::hook::restarts: 0, hookNoSubstituteDrv::hook::retries: 0, hookNoSubstituteDrv::hook::toUpload: Set("drv", "in") } [State 4] { hookNoSubstituteDrv::hook::cache: Set("drv", "in"), hookNoSubstituteDrv::hook::drvUploaded: true, hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set("drv", "in")), hookNoSubstituteDrv::hook::phase: Build, hookNoSubstituteDrv::hook::restarts: 0, hookNoSubstituteDrv::hook::retries: 0, hookNoSubstituteDrv::hook::toUpload: Set("drv", "in") } [State 5] { hookNoSubstituteDrv::hook::cache: Set("drv", "in"), hookNoSubstituteDrv::hook::drvUploaded: true, hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set("drv", "in")), hookNoSubstituteDrv::hook::phase: Build, hookNoSubstituteDrv::hook::restarts: 1, hookNoSubstituteDrv::hook::retries: 1, hookNoSubstituteDrv::hook::toUpload: Set("drv", "in") } [State 6] { hookNoSubstituteDrv::hook::cache: Set("drv", "in"), hookNoSubstituteDrv::hook::drvUploaded: true, hookNoSubstituteDrv::hook::local: Map("w1" -> Set(), "w2" -> Set("drv", "in")), hookNoSubstituteDrv::hook::phase: Failed, hookNoSubstituteDrv::hook::restarts: 1, hookNoSubstituteDrv::hook::retries: 1, hookNoSubstituteDrv::hook::toUpload: Set("drv", "in") } [violation] Found an issue (167ms at 599 traces/second). Use --verbosity=3 to show executions. Use --seed=0xc4a8bbaa51c21692 --backend=rust to reproduce. error: Invariant violated Running... [ ] 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: [State 0] { pushFixed::push::byPath: Map(), pushFixed::push::inflight: Set(), pushFixed::push::left: Map(), pushFixed::push::sent: Map() } [State 1] { pushFixed::push::byPath: Map("a" -> 3, "b" -> 3), pushFixed::push::inflight: Set((3, "a"), (3, "b")), pushFixed::push::left: Map(3 -> 2), pushFixed::push::sent: Map(3 -> Set("a", "b")) } [State 2] { pushFixed::push::byPath: Map("a" -> 2, "b" -> 2), pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "a"), (3, "b")), pushFixed::push::left: Map(2 -> 2, 3 -> 2), pushFixed::push::sent: Map(2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 3] { pushFixed::push::byPath: Map("a" -> 1, "b" -> 1), pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")), pushFixed::push::left: Map(1 -> 2, 2 -> 2, 3 -> 2), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 4] { pushFixed::push::byPath: Map("a" -> 1, "b" -> 1), pushFixed::push::inflight: Set((1, "b"), (2, "a"), (2, "b"), (3, "a"), (3, "b")), pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 2), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 5] { pushFixed::push::byPath: Map("a" -> 1, "b" -> 1), pushFixed::push::inflight: Set((1, "b"), (2, "b"), (3, "a"), (3, "b")), pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 2), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 6] { pushFixed::push::byPath: Map("a" -> 1, "b" -> 1), pushFixed::push::inflight: Set((1, "b"), (3, "a"), (3, "b")), pushFixed::push::left: Map(1 -> 1, 2 -> 0, 3 -> 2), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 7] { pushFixed::push::byPath: Map("a" -> 1, "b" -> 1), pushFixed::push::inflight: Set((3, "a"), (3, "b")), pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 2), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 8] { pushFixed::push::byPath: Map("a" -> 1, "b" -> 1), pushFixed::push::inflight: Set((3, "b")), pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 1), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 9] { pushFixed::push::byPath: Map("a" -> 1, "b" -> 1), pushFixed::push::inflight: Set(), pushFixed::push::left: Map(1 -> 0, 2 -> 0, 3 -> 0), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [ok] No violation found (1508ms at 13263 traces/second). Trace length statistics: max=10, min=7, average=8.00 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0x47e7fd81622e254a --backend=rust to reproduce. Running... [ ] 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: [State 0] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 1] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 2] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 3] { nextToken: 1, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 4] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 5] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 6] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 7] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 8] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 9] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 10] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 11] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 12] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 } ) } [State 13] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 14] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 } ) } [State 15] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 16] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 } ) } [State 17] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 18] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 } ) } [State 19] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 20] { nextToken: 3, present: false, rowStale: false, rowToken: 2, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(2), token: 2 } ) } [State 21] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [State 22] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [State 23] { nextToken: 4, present: false, rowStale: false, rowToken: 3, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(3), token: 3 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [State 24] { nextToken: 4, present: false, rowStale: false, rowToken: 3, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 3 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [State 25] { nextToken: 4, present: false, rowStale: false, rowToken: 3, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 3 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [State 26] { nextToken: 4, present: false, rowStale: false, rowToken: 3, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 3 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [State 27] { nextToken: 4, present: false, rowStale: false, rowToken: 3, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 3 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [State 28] { nextToken: 4, present: false, rowStale: false, rowToken: 3, touched: false, ws: Map( "w1" -> { conn: true, outputs: true, phase: Publishing, res: RNone, slot: true, srv: SNeed, token: 3 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [State 29] { nextToken: 4, present: false, rowStale: false, rowToken: 3, touched: false, ws: Map( "w1" -> { conn: true, outputs: true, phase: Publishing, res: RNone, slot: true, srv: SHolder(3), token: 3 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [State 30] { nextToken: 4, present: true, rowStale: false, rowToken: 0, touched: true, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RBuilt, slot: false, srv: SNone, token: 3 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 2 } ) } [ok] No violation found (7409ms at 2699 traces/second). Trace length statistics: max=31, min=9, average=18.59 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0x515f12ed2468f1a0 --backend=rust to reproduce.