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... [■■■■ ] 8% | ETA: 6s | 1752/20000 samples | 3168 samples/sRunning... [■■■■ ] 8% | ETA: 6s | 1752/20000 samples | 3168 samples/sRunning... [■■■■■■ ] 14% | ETA: 5s | 2968/20000 samples | 4022 samples/sRunning... [■■■■■■■ ] 18% | ETA: 4s | 3727/20000 samples | 4359 samples/sRunning... [■■■■■■■■■ ] 23% | ETA: 4s | 4600/20000 samples | 4632 samples/sRunning... [■■■■■■■■■ ] 23% | ETA: 4s | 4600/20000 samples | 4632 samples/sRunning... [■■■■■■■■■■■■ ] 29% | ETA: 3s | 5973/20000 samples | 5249 samples/sRunning... [■■■■■■■■■■■■■■ ] 35% | ETA: 3s | 7071/20000 samples | 5661 samples/sRunning... [■■■■■■■■■■■■■■■■ ] 41% | ETA: 2s | 8238/20000 samples | 6057 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 50% | ETA: 2s | 10080/20000 samples | 6610 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■ ] 50% | ETA: 2s | 10080/20000 samples | 6610 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 57% | ETA: 2s | 11560/20000 samples | 6935 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 65% | ETA: 1s | 13044/20000 samples | 7203 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 70% | ETA: 1s | 14008/20000 samples | 7311 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 74% | ETA: 1s | 14985/20000 samples | 7411 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 74% | ETA: 1s | 14985/20000 samples | 7411 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 74% | ETA: 1s | 14985/20000 samples | 7411 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 84% | ETA: 1s | 16896/20000 samples | 7536 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 91% | ETA: 1s | 18265/20000 samples | 7678 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 96% | ETA: 1s | 19343/20000 samples | 7793 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 96% | ETA: 1s | 19343/20000 samples | 7793 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: 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 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: 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 7] { 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: 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 8] { 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: 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 9] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 } ) } [State 10] { 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: 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 11] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 } ) } [State 12] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 } ) } [State 13] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 } ) } [State 14] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 } ) } [State 15] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 } ) } [State 16] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 } ) } [State 17] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 } ) } [State 18] { 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 19] { 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 20] { 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 21] { 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: 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 22] { 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: 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: 1, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 }, "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 24] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 }, "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 25] { nextToken: 2, present: false, rowStale: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 }, "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 26] { nextToken: 2, present: false, rowStale: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "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: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "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: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 } ) } [State 29] { nextToken: 2, present: false, rowStale: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "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: true, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "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 (2578ms at 7758 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=0x9f3aff4648c5d80b --backend=rust to reproduce. Running... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [ ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [■■■■■■■ ] 18% | ETA: 1s | 3734/20000 samples | 19448 samples/sRunning... [■■■■■■■ ] 18% | ETA: 1s | 3734/20000 samples | 19448 samples/sRunning... [■■■■■■■ ] 18% | ETA: 1s | 3734/20000 samples | 19448 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 42% | ETA: 1s | 8425/20000 samples | 19548 samples/sRunning... [■■■■■■■■■■■■■■■■■ ] 42% | ETA: 1s | 8425/20000 samples | 19548 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 57% | ETA: 1s | 11532/20000 samples | 18812 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■ ] 57% | ETA: 1s | 11532/20000 samples | 18812 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 79% | ETA: 1s | 15836/20000 samples | 18393 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 79% | ETA: 1s | 15836/20000 samples | 18393 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 94% | ETA: 1s | 18870/20000 samples | 18197 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 94% | ETA: 1s | 18870/20000 samples | 18197 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: 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 4] { 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 5] { 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 6] { 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 7] { 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 8] { 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 9] { 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 10] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 }, "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 11] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 }, "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 12] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 1 }, "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 13] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 }, "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 14] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 1 }, "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 15] { nextToken: 2, present: false, rowStale: false, rowToken: 1, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 }, "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: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "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: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "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 18] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "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 19] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "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: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "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 21] { nextToken: 2, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "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 22] { nextToken: 3, present: false, rowStale: false, rowToken: 2, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(2), token: 2 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 23] { nextToken: 3, present: false, rowStale: false, rowToken: 2, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 2 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 24] { nextToken: 3, present: false, rowStale: false, rowToken: 2, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 2 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 25] { nextToken: 3, present: false, rowStale: false, rowToken: 2, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: true, outputs: true, phase: Publishing, res: RNone, slot: true, srv: SNeed, token: 2 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 26] { nextToken: 3, present: false, rowStale: false, rowToken: 2, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: true, outputs: true, phase: Publishing, res: RNone, slot: true, srv: SHolder(2), token: 2 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 27] { nextToken: 3, present: false, rowStale: false, rowToken: 2, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: false, outputs: true, phase: Publishing, res: RNone, slot: true, srv: SNone, token: 2 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 28] { nextToken: 3, present: true, rowStale: false, rowToken: 0, touched: true, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RBuilt, slot: false, srv: SNone, token: 2 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 29] { nextToken: 3, present: true, rowStale: false, rowToken: 0, touched: true, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RBuilt, slot: false, srv: SNone, token: 2 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 30] { nextToken: 3, present: true, rowStale: false, rowToken: 0, touched: true, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 }, "w2" -> { conn: false, outputs: false, phase: Done, res: RBuilt, slot: false, srv: SNone, token: 2 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RAlreadyValid, slot: false, srv: SNone, token: 0 } ) } [ok] No violation found (1130ms at 17699 traces/second). Trace length statistics: max=31, min=9, average=18.44 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0x77b2d77b33bf6b26 --backend=rust to reproduce.