tribuchet: building on jamie An 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: 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 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: 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 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: 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 4] { 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: Done, res: RUnavailable, 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: 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: Done, res: RUnavailable, 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: 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 11] { 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 12] { 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 13] { 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 14] { 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 15] { 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 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: 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: 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: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, 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: 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 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: 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 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: 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 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: 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 22] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 } ) } [State 23] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 } ) } [State 24] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 } ) } [State 25] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 1 } ) } [State 26] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 } ) } [State 27] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 1 } ) } [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: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 } ) } [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: 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: 1 } ) } [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: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 } ) } [ok] No violation found (318ms at 62893 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=0x75d1301874924b6 --backend=rust to reproduce. An 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: 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 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: 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 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: 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 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: Pending, res: RNone, slot: true, 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: 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 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: 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 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: 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 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: 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 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: 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 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: 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 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: 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 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: 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 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: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 14] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 } ) } [State 15] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Building, res: RNone, slot: true, srv: SNone, token: 1 } ) } [State 16] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SNeed, token: 1 } ) } [State 17] { 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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 } ) } [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: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 19] { 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: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 20] { 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: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 21] { 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: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 22] { nextToken: 3, present: false, rowStale: false, rowToken: 2, touched: false, ws: Map( "w1" -> { conn: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(2), token: 2 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 23] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 2 }, "w2" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 24] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 2 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 25] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 2 }, "w2" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 26] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 2 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 27] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 2 }, "w2" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 28] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 2 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 29] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 2 }, "w2" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [State 30] { nextToken: 3, present: false, rowStale: false, rowToken: 0, touched: false, ws: Map( "w1" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 2 }, "w2" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 }, "w3" -> { conn: false, outputs: false, phase: Done, res: RFailed, slot: false, srv: SNone, token: 1 } ) } [ok] No violation found (303ms at 66007 traces/second). Trace length statistics: max=31, min=9, average=19.16 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0xcde816ba570a077a --backend=rust to reproduce.