tribuchet: building on eliza An example execution: [State 0] { schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle), schedFixed::scheduler::crashes: 0, schedFixed::scheduler::entry: [], schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 0, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 1] { schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle), schedFixed::scheduler::crashes: 1, schedFixed::scheduler::entry: [], schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 0, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true } ) } [State 2] { schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [], schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 0, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true } ) } [State 3] { schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [], schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 0, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true } ) } [State 4] { schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [], schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 0, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 5] { schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [], schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c2"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 0, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 6] { schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c2", "w1")), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 7] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c2", "w1")), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c1"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 8] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 9] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c1", "w1")), schedFixed::scheduler::mBuild: Set(("c2", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 10] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 11] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(("c2", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c1"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 12] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(("c2", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c1"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 13] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c2"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c1"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 14] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c1", "w1")), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c2"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 15] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c1", "w1")), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c2"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 16] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(("c1", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c2"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 17] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c2", "w1")), schedFixed::scheduler::mBuild: Set(("c1", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 18] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c2", "w1")), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c1"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 19] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(("c2", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c1"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 20] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c1", "c2"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 21] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c2"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c1"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 22] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c1", "c2"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 23] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c2", "w1")), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c1"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 24] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w1")), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 25] { schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(("c1", "w1")), schedFixed::scheduler::mBuild: Set(("c2", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 26] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set(), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 27] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(("c1", "w1")), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c2"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 28] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(("w1", 1)), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c1", "c2"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 29] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c1", "c2"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set(), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: true, lease: 1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 30] { schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued), schedFixed::scheduler::crashes: 2, schedFixed::scheduler::entry: [{ followers: Set("c1", "c2"), lease: 1, leased: true, worker: "w1" }], schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1), schedFixed::scheduler::mAssigned: Set(), schedFixed::scheduler::mBuild: Set(), schedFixed::scheduler::mDone: Set(), schedFixed::scheduler::mExpect: Set(), schedFixed::scheduler::mResult: Set(), schedFixed::scheduler::mRetry: Set("c1"), schedFixed::scheduler::mRevoke: Set(), schedFixed::scheduler::mSchedule: Set("c2"), schedFixed::scheduler::published: 0, schedFixed::scheduler::publishedBy: Set(), schedFixed::scheduler::seq: 1, schedFixed::scheduler::stolen: false, schedFixed::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: true, lease: 1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [ok] No violation found (18137ms at 1654 traces/second). Trace length statistics: max=31, min=16, average=28.96 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0xb35b1cba65cd8e68 --backend=rust to reproduce. An example execution: [State 0] { schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle), schedNoPush::scheduler::crashes: 0, schedNoPush::scheduler::entry: [], schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedNoPush::scheduler::mAssigned: Set(), schedNoPush::scheduler::mBuild: Set(), schedNoPush::scheduler::mDone: Set(), schedNoPush::scheduler::mExpect: Set(), schedNoPush::scheduler::mResult: Set(), schedNoPush::scheduler::mRetry: Set(), schedNoPush::scheduler::mRevoke: Set(), schedNoPush::scheduler::mSchedule: Set(), schedNoPush::scheduler::published: 0, schedNoPush::scheduler::publishedBy: Set(), schedNoPush::scheduler::seq: 0, schedNoPush::scheduler::stolen: false, schedNoPush::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 1] { schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle), schedNoPush::scheduler::crashes: 0, schedNoPush::scheduler::entry: [], schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedNoPush::scheduler::mAssigned: Set(), schedNoPush::scheduler::mBuild: Set(), schedNoPush::scheduler::mDone: Set(), schedNoPush::scheduler::mExpect: Set(), schedNoPush::scheduler::mResult: Set(), schedNoPush::scheduler::mRetry: Set(), schedNoPush::scheduler::mRevoke: Set(), schedNoPush::scheduler::mSchedule: Set("c1"), schedNoPush::scheduler::published: 0, schedNoPush::scheduler::publishedBy: Set(), schedNoPush::scheduler::seq: 0, schedNoPush::scheduler::stolen: false, schedNoPush::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 2] { schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle), schedNoPush::scheduler::crashes: 0, schedNoPush::scheduler::entry: [{ followers: Set("c1"), lease: 1, leased: true, worker: "w2" }], schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0), schedNoPush::scheduler::mAssigned: Set(("c1", "w2")), schedNoPush::scheduler::mBuild: Set(), schedNoPush::scheduler::mDone: Set(), schedNoPush::scheduler::mExpect: Set(), schedNoPush::scheduler::mResult: Set(), schedNoPush::scheduler::mRetry: Set(), schedNoPush::scheduler::mRevoke: Set(), schedNoPush::scheduler::mSchedule: Set(), schedNoPush::scheduler::published: 0, schedNoPush::scheduler::publishedBy: Set(), schedNoPush::scheduler::seq: 1, schedNoPush::scheduler::stolen: false, schedNoPush::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 3] { schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle), schedNoPush::scheduler::crashes: 0, schedNoPush::scheduler::entry: [{ followers: Set("c1"), lease: 1, leased: true, worker: "w2" }], schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0), schedNoPush::scheduler::mAssigned: Set(), schedNoPush::scheduler::mBuild: Set(("c1", "w2")), schedNoPush::scheduler::mDone: Set(), schedNoPush::scheduler::mExpect: Set(), schedNoPush::scheduler::mResult: Set(), schedNoPush::scheduler::mRetry: Set(), schedNoPush::scheduler::mRevoke: Set(), schedNoPush::scheduler::mSchedule: Set(), schedNoPush::scheduler::published: 0, schedNoPush::scheduler::publishedBy: Set(), schedNoPush::scheduler::seq: 1, schedNoPush::scheduler::stolen: false, schedNoPush::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 4] { schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle), schedNoPush::scheduler::crashes: 1, schedNoPush::scheduler::entry: [], schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedNoPush::scheduler::mAssigned: Set(), schedNoPush::scheduler::mBuild: Set(("c1", "w2")), schedNoPush::scheduler::mDone: Set(), schedNoPush::scheduler::mExpect: Set(), schedNoPush::scheduler::mResult: Set(), schedNoPush::scheduler::mRetry: Set(), schedNoPush::scheduler::mRevoke: Set(), schedNoPush::scheduler::mSchedule: Set(), schedNoPush::scheduler::published: 0, schedNoPush::scheduler::publishedBy: Set(), schedNoPush::scheduler::seq: 1, schedNoPush::scheduler::stolen: false, schedNoPush::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true } ) } [State 5] { schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle), schedNoPush::scheduler::crashes: 2, schedNoPush::scheduler::entry: [], schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedNoPush::scheduler::mAssigned: Set(), schedNoPush::scheduler::mBuild: Set(("c1", "w2")), schedNoPush::scheduler::mDone: Set(), schedNoPush::scheduler::mExpect: Set(), schedNoPush::scheduler::mResult: Set(), schedNoPush::scheduler::mRetry: Set(), schedNoPush::scheduler::mRevoke: Set(), schedNoPush::scheduler::mSchedule: Set(), schedNoPush::scheduler::published: 0, schedNoPush::scheduler::publishedBy: Set(), schedNoPush::scheduler::seq: 1, schedNoPush::scheduler::stolen: false, schedNoPush::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true } ) } [State 6] { schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle), schedNoPush::scheduler::crashes: 2, schedNoPush::scheduler::entry: [], schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedNoPush::scheduler::mAssigned: Set(), schedNoPush::scheduler::mBuild: Set(("c1", "w2")), schedNoPush::scheduler::mDone: Set(), schedNoPush::scheduler::mExpect: Set(), schedNoPush::scheduler::mResult: Set(), schedNoPush::scheduler::mRetry: Set(), schedNoPush::scheduler::mRevoke: Set(), schedNoPush::scheduler::mSchedule: Set(), schedNoPush::scheduler::published: 0, schedNoPush::scheduler::publishedBy: Set(), schedNoPush::scheduler::seq: 1, schedNoPush::scheduler::stolen: false, schedNoPush::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 7] { schedNoPush::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CIdle), schedNoPush::scheduler::crashes: 2, schedNoPush::scheduler::entry: [], schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedNoPush::scheduler::mAssigned: Set(), schedNoPush::scheduler::mBuild: Set(), schedNoPush::scheduler::mDone: Set(), schedNoPush::scheduler::mExpect: Set(), schedNoPush::scheduler::mResult: Set(), schedNoPush::scheduler::mRetry: Set(), schedNoPush::scheduler::mRevoke: Set(), schedNoPush::scheduler::mSchedule: Set(), schedNoPush::scheduler::published: 0, schedNoPush::scheduler::publishedBy: Set(), schedNoPush::scheduler::seq: 1, schedNoPush::scheduler::stolen: false, schedNoPush::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true }, "w2" -> { attached: Set("c1"), built: false, expecting: false, lease: -1, running: true, session: true, up: true } ) } [violation] Found an issue (10955ms at 1152 traces/second). Use --verbosity=3 to show executions. Use --seed=0xb123203dd9d96548 --backend=rust to reproduce. error: Invariant violated An example execution: [State 0] { schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle), schedTerminal::scheduler::crashes: 0, schedTerminal::scheduler::entry: [], schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedTerminal::scheduler::mAssigned: Set(), schedTerminal::scheduler::mBuild: Set(), schedTerminal::scheduler::mDone: Set(), schedTerminal::scheduler::mExpect: Set(), schedTerminal::scheduler::mResult: Set(), schedTerminal::scheduler::mRetry: Set(), schedTerminal::scheduler::mRevoke: Set(), schedTerminal::scheduler::mSchedule: Set(), schedTerminal::scheduler::published: 0, schedTerminal::scheduler::publishedBy: Set(), schedTerminal::scheduler::seq: 0, schedTerminal::scheduler::stolen: false, schedTerminal::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: true, up: true } ) } [State 1] { schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle), schedTerminal::scheduler::crashes: 1, schedTerminal::scheduler::entry: [], schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedTerminal::scheduler::mAssigned: Set(), schedTerminal::scheduler::mBuild: Set(), schedTerminal::scheduler::mDone: Set(), schedTerminal::scheduler::mExpect: Set(), schedTerminal::scheduler::mResult: Set(), schedTerminal::scheduler::mRetry: Set(), schedTerminal::scheduler::mRevoke: Set(), schedTerminal::scheduler::mSchedule: Set(), schedTerminal::scheduler::published: 0, schedTerminal::scheduler::publishedBy: Set(), schedTerminal::scheduler::seq: 0, schedTerminal::scheduler::stolen: false, schedTerminal::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true } ) } [State 2] { schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued), schedTerminal::scheduler::crashes: 1, schedTerminal::scheduler::entry: [], schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedTerminal::scheduler::mAssigned: Set(), schedTerminal::scheduler::mBuild: Set(), schedTerminal::scheduler::mDone: Set(), schedTerminal::scheduler::mExpect: Set(), schedTerminal::scheduler::mResult: Set(), schedTerminal::scheduler::mRetry: Set(), schedTerminal::scheduler::mRevoke: Set(), schedTerminal::scheduler::mSchedule: Set("c2"), schedTerminal::scheduler::published: 0, schedTerminal::scheduler::publishedBy: Set(), schedTerminal::scheduler::seq: 0, schedTerminal::scheduler::stolen: false, schedTerminal::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true } ) } [State 3] { schedTerminal::scheduler::cl: Map("c1" -> CIdle, "c2" -> CFailed), schedTerminal::scheduler::crashes: 1, schedTerminal::scheduler::entry: [], schedTerminal::scheduler::free: Map("w1" -> 1, "w2" -> 1), schedTerminal::scheduler::mAssigned: Set(), schedTerminal::scheduler::mBuild: Set(), schedTerminal::scheduler::mDone: Set(), schedTerminal::scheduler::mExpect: Set(), schedTerminal::scheduler::mResult: Set(), schedTerminal::scheduler::mRetry: Set(), schedTerminal::scheduler::mRevoke: Set(), schedTerminal::scheduler::mSchedule: Set(), schedTerminal::scheduler::published: 0, schedTerminal::scheduler::publishedBy: Set(), schedTerminal::scheduler::seq: 0, schedTerminal::scheduler::stolen: false, schedTerminal::scheduler::ws: Map( "w1" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true }, "w2" -> { attached: Set(), built: false, expecting: false, lease: -1, running: false, session: false, up: true } ) } [violation] Found an issue (19123ms at 52 traces/second). Use --verbosity=3 to show executions. Use --seed=0x21550218a3554eae --backend=rust to reproduce. error: Invariant violated schedFixed ok schedFixed::scheduler::dupBuildTest passed 100 test(s) ok schedFixed::scheduler::helloStealTest passed 100 test(s) ok schedFixed::scheduler::staleDoneTest passed 100 test(s) 3 passing (853ms) schedNoRevoke ok schedNoRevoke::scheduler::dupBuildTest passed 100 test(s) 1 passing (643ms) schedNoFence ok schedNoFence::scheduler::dupBuildTest passed 100 test(s) 1 passing (7289ms) schedNoReport ok schedNoReport::scheduler::dupBuildTest passed 100 test(s) 1 passing (6020ms) schedHelloSteal ok schedHelloSteal::scheduler::helloStealTest passed 100 test(s) 1 passing (2799ms) schedNoLease ok schedNoLease::scheduler::staleDoneTest passed 100 test(s) 1 passing (6972ms) 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, "b")), pushFixed::push::left: Map(1 -> 1), pushFixed::push::sent: Map(1 -> Set("a", "b")) } [State 3] { pushFixed::push::byPath: Map("a" -> 3, "b" -> 3), pushFixed::push::inflight: Set((1, "b"), (3, "a"), (3, "b")), pushFixed::push::left: Map(1 -> 1, 3 -> 2), pushFixed::push::sent: Map(1 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 4] { pushFixed::push::byPath: Map("a" -> 2, "b" -> 2), 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" -> 2, "b" -> 2), pushFixed::push::inflight: Set((1, "b"), (2, "a"), (2, "b"), (3, "b")), pushFixed::push::left: Map(1 -> 1, 2 -> 2, 3 -> 1), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 6] { pushFixed::push::byPath: Map("a" -> 2, "b" -> 2), pushFixed::push::inflight: Set((2, "a"), (2, "b"), (3, "b")), pushFixed::push::left: Map(1 -> 0, 2 -> 2, 3 -> 1), pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b")) } [State 7] { pushFixed::push::byPath: Map("a" -> 2, "b" -> 2), pushFixed::push::inflight: Set((2, "a"), (3, "b")), 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" -> 2, "b" -> 2), pushFixed::push::inflight: Set((2, "a")), 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" -> 2, "b" -> 2), 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 (16759ms at 1193 traces/second). Trace length statistics: max=10, min=7, average=7.97 You may increase --max-samples and --max-steps. Use --verbosity to produce more (or less) output. Use --seed=0x8f63f37137df847b --backend=rust to reproduce.