tribuchet: building on eliza 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: 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 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: 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 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: 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 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: 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 9] { 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: 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 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: 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 14] { 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: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 15] { nextToken: 2, present: false, rowStale: false, rowToken: 1, 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: true, outputs: false, phase: Building, res: RNone, slot: true, srv: SHolder(1), token: 1 } ) } [State 16] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 } ) } [State 17] { 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 } ) } [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: 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 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: 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: 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: 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 21] { 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: 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 22] { nextToken: 3, present: false, rowStale: true, 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: 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 23] { nextToken: 3, present: false, rowStale: true, 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: 2 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 24] { nextToken: 3, present: false, rowStale: true, 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: 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 25] { nextToken: 3, present: false, rowStale: true, rowToken: 2, 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 26] { nextToken: 4, present: false, rowStale: false, rowToken: 3, 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(3), token: 3 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 27] { nextToken: 4, 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: 3 }, "w3" -> { conn: false, outputs: false, phase: Idle, res: RNone, slot: false, srv: SNone, token: 0 } ) } [State 28] { nextToken: 4, 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: 3 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [State 29] { nextToken: 4, 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: 3 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, token: 0 } ) } [State 30] { nextToken: 4, 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 } ) } [ok] No violation found (498ms at 40161 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=0xd44067200ec46775 --backend=rust to reproduce. An 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("in"), 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") } [State 2] { hookFixed::hook::cache: Set("in"), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set()), hookFixed::hook::phase: Upload, hookFixed::hook::restarts: 1, hookFixed::hook::retries: 1, hookFixed::hook::toUpload: Set("drv") } [State 3] { hookFixed::hook::cache: Set("in"), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("in"), "w2" -> Set("drv")), hookFixed::hook::phase: Upload, hookFixed::hook::restarts: 2, hookFixed::hook::retries: 2, hookFixed::hook::toUpload: Set("drv") } [State 4] { hookFixed::hook::cache: Set("drv", "in"), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("drv", "in"), "w2" -> Set("drv")), hookFixed::hook::phase: Build, hookFixed::hook::restarts: 2, hookFixed::hook::retries: 2, hookFixed::hook::toUpload: Set("drv") } [State 5] { hookFixed::hook::cache: Set("drv", "in", "out"), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("drv", "in"), "w2" -> Set("drv", "in", "out")), hookFixed::hook::phase: Fetch, hookFixed::hook::restarts: 2, hookFixed::hook::retries: 2, hookFixed::hook::toUpload: Set("drv") } [State 6] { hookFixed::hook::cache: Set("drv", "in", "out"), hookFixed::hook::drvUploaded: false, hookFixed::hook::local: Map("w1" -> Set("drv", "in"), "w2" -> Set("drv", "in", "out")), hookFixed::hook::phase: Done, hookFixed::hook::restarts: 2, hookFixed::hook::retries: 2, hookFixed::hook::toUpload: Set("drv") } [ok] No violation found (111ms at 180180 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=0x136369ae0b3fba3e --backend=rust to reproduce. An 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 (67ms at 22164 traces/second). Use --verbosity=3 to show executions. Use --seed=0x130e35162a30c779 --backend=rust to reproduce. error: Invariant violated An 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: Failed, hookNoSubstituteDrv::hook::restarts: 0, hookNoSubstituteDrv::hook::retries: 0, hookNoSubstituteDrv::hook::toUpload: Set("drv", "in") } [violation] Found an issue (85ms at 22482 traces/second). Use --verbosity=3 to show executions. Use --seed=0x8c31480bd064c82 --backend=rust to reproduce. error: Invariant violated An 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" -> 1, "b" -> 1), pushFixed::push::inflight: Set((1, "a"), (1, "b")), pushFixed::push::left: Map(1 -> 2), pushFixed::push::sent: Map(1 -> Set("a", "b")) } [State 2] { pushFixed::push::byPath: Map("a" -> 1, "b" -> 1), pushFixed::push::inflight: Set((1, "a")), pushFixed::push::left: Map(1 -> 1), pushFixed::push::sent: Map(1 -> Set("a", "b")) } [State 3] { pushFixed::push::byPath: Map("a" -> 2, "b" -> 2), pushFixed::push::inflight: Set((1, "a"), (2, "a"), (2, "b")), pushFixed::push::left: Map(1 -> 1, 2 -> 2), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b")) } [State 4] { pushFixed::push::byPath: Map("a" -> 2, "b" -> 2), pushFixed::push::inflight: Set((2, "a"), (2, "b")), pushFixed::push::left: Map(1 -> 0, 2 -> 2), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b")) } [State 5] { pushFixed::push::byPath: Map("a" -> 2, "b" -> 2), pushFixed::push::inflight: Set((2, "b")), pushFixed::push::left: Map(1 -> 0, 2 -> 1), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b")) } [State 6] { pushFixed::push::byPath: Map("a" -> 3, "b" -> 3), pushFixed::push::inflight: Set((2, "b"), (3, "a"), (3, "b")), pushFixed::push::left: Map(1 -> 0, 2 -> 1, 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" -> 3, "b" -> 3), pushFixed::push::inflight: Set((2, "b"), (3, "a")), pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 1), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 8] { pushFixed::push::byPath: Map("a" -> 3, "b" -> 3), pushFixed::push::inflight: Set((2, "b")), pushFixed::push::left: Map(1 -> 0, 2 -> 1, 3 -> 0), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 9] { pushFixed::push::byPath: Map("a" -> 3, "b" -> 3), 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 (115ms at 173913 traces/second). Trace length statistics: max=10, min=7, average=7.93 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0x180e43fdadf691a2 --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: 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: 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 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: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, 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: false, outputs: false, phase: Pending, res: RNone, slot: true, 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: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, 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: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, 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: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, 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: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, 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: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, 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: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, 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: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, 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: false, outputs: false, phase: Pending, res: RNone, slot: true, 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: 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 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: 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 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: 1 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, 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: 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 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: 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 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: 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 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: 1 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, 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: 1 }, "w3" -> { conn: false, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNone, 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: 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 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: 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 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: Done, res: RUnavailable, slot: false, srv: SNone, token: 1 }, "w3" -> { conn: true, outputs: false, phase: Pending, res: RNone, slot: true, srv: SNeed, token: 0 } ) } [ok] No violation found (362ms at 55249 traces/second). Trace length statistics: max=31, min=10, average=18.26 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0xfd36ccc650258871 --backend=rust to reproduce.