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::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 1]
{
  schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  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::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 2]
{
  schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 0,
  schedFixed::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 3]
{
  schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 1,
  schedFixed::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 4]
{
  schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 5]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 6]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 7]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1", "c2"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 8]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1", "c2"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 9]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1", "c2"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 10]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c2"),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 11]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(("c2", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c2"),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 12]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "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(("c2", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c1", "c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 13]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c1", "w2")),
  schedFixed::scheduler::mBuild: Set(("c2", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 14]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(("c2", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 15]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(("c1", "w2"), ("c2", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 16]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(("c1", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c2"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 17]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(("c1", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 18]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1"),
  schedFixed::scheduler::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 19]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c1", "c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 20]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c1", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 21]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(("c1", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 22]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(("c1", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 23]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(("c1", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[State 24]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set("c1"),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[State 25]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(("c2", "w2")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set("c1"),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[State 26]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(("c2", "w2")),
  schedFixed::scheduler::mDone: Set("w2"),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set("c1"),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w2"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 27]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set("w2"),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set("c1", "c2"),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w2"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 28]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  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("c1", "c2"),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w2"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 29]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CDone),
  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("c1"),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w2"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 30]
{
  schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),
  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::mSchedule: Set(),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w2"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[ok] No violation found (12236ms at 2452 traces/second).
Trace length statistics: max=26, min=15, average=18.29
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0x93730797bcb27edb --backend=rust to reproduce.
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::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 1]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "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::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 2]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedFixed::scheduler::crashes: 0,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1"), 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"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 3]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedFixed::scheduler::crashes: 1,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1"), 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(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 4]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedFixed::scheduler::crashes: 1,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c1", "w1")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 5]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 1,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c1", "w1")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1"),
  schedFixed::scheduler::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 6]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  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::mSchedule: Set("c1", "c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 7]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 1,
  schedFixed::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 8]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 1,
  schedFixed::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w2"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 9]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 10]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c2"),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 11]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c1", "w1"), ("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w1"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c2"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 12]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(("c1", "w1")),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w1"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c2"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 13]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(("c2", "w2")),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set("w1"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1", "c2"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 14]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1"), 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"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1"),
  schedFixed::scheduler::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 15]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), 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"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 16]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), 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"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 17]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), 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"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 18]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), 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"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          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"), 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"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          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"), 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"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c2"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 21]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), 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"),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c1", "c2"),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 22]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), 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::mSchedule: Set(),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 23]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), 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("c2"),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 0,
  schedFixed::scheduler::publishedBy: Set(),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 24]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],
  schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set("w1"),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("c2"),
  schedFixed::scheduler::mSchedule: Set("c1"),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w1"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 25]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],
  schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set("w1"),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c1", "c2"),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w1"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 26]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],
  schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set("w1"),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set("c1"),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w1"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 27]
{
  schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],
  schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set("w1"),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set("c2"),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w1"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 28]
{
  schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w1" }],
  schedFixed::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set("w1"),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set("c2"),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w1"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 29]
{
  schedFixed::scheduler::cl: Map("c1" -> CDone, "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("c2"),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::mSchedule: Set(),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w1"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 30]
{
  schedFixed::scheduler::cl: Map("c1" -> CDone, "c2" -> CDone),
  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::mSchedule: Set(),
  schedFixed::scheduler::published: 1,
  schedFixed::scheduler::publishedBy: Set("w1"),
  schedFixed::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[ok] No violation found (2369ms at 12664 traces/second).
Trace length statistics: max=29, min=16, average=18.88
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0xc4bfa423c5a8decb --backend=rust to reproduce.
An example execution:

[State 0]
{
  schedNoFence::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),
  schedNoFence::scheduler::crashes: 0,
  schedNoFence::scheduler::entry: [],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 1]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedNoFence::scheduler::crashes: 0,
  schedNoFence::scheduler::entry: [],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set("c1"),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 2]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedNoFence::scheduler::crashes: 0,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w1"),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 3]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedNoFence::scheduler::crashes: 1,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w1"),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 4]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedNoFence::scheduler::crashes: 1,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedNoFence::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(("c1", "w1")),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 5]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry: [],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set("c1"),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 6]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry: [],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set("c1"),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 7]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry: [],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set("c1", "c2"),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 8]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry: [],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set("c1", "c2"),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 9]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w2"),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set("c1"),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 10]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoFence::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w2"),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 0,
  schedNoFence::scheduler::publishedBy: Set(),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 11]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoFence::scheduler::mAssigned: Set(("c1", "w2"), ("c2", "w2")),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w2"),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w1"),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 12]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoFence::scheduler::mBuild: Set(("c1", "w2")),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w2"),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w1"),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 13]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoFence::scheduler::mBuild: Set(("c1", "w2")),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w1"),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[State 14]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoFence::scheduler::mBuild: Set(("c1", "w2")),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w1"),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[State 15]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CQueued),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry:
    [{ followers: Set("c1", "c2"), leased: true, worker: "w2" }],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoFence::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoFence::scheduler::mBuild: Set(("c1", "w2")),
  schedNoFence::scheduler::mDone: Set("w2"),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 2,
  schedNoFence::scheduler::publishedBy: Set("w1", "w2"),
  schedNoFence::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[violation] Found an issue (2723ms at 10773 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x7c72004316cdd456 --backend=rust to reproduce.
error: Invariant violated
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::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          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::mSchedule: Set("c1"),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          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"), 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::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          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"), 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::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          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::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: true
        }
    )
}

[State 5]
{
  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::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 6]
{
  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(),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set(),
  schedNoPush::scheduler::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set("c1"),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[violation] Found an issue (2829ms at 4143 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0xe47575b278ac461d --backend=rust to reproduce.
error: Invariant violated
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::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 1]
{
  schedNoPush::scheduler::cl: Map("c1" -> CIdle, "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(),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set(),
  schedNoPush::scheduler::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 2]
{
  schedNoPush::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoPush::scheduler::crashes: 1,
  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::mSchedule: Set("c2"),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 3]
{
  schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedNoPush::scheduler::crashes: 1,
  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::mSchedule: Set("c1", "c2"),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 4]
{
  schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedNoPush::scheduler::crashes: 1,
  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::mSchedule: Set("c1", "c2"),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 5]
{
  schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedNoPush::scheduler::crashes: 1,
  schedNoPush::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoPush::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoPush::scheduler::mBuild: Set(),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set(),
  schedNoPush::scheduler::mSchedule: Set("c1"),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 6]
{
  schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedNoPush::scheduler::crashes: 2,
  schedNoPush::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoPush::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoPush::scheduler::mBuild: Set(),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set(),
  schedNoPush::scheduler::mSchedule: Set("c1"),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 7]
{
  schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  schedNoPush::scheduler::crashes: 2,
  schedNoPush::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoPush::scheduler::mAssigned: Set(),
  schedNoPush::scheduler::mBuild: Set(("c2", "w2")),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set(),
  schedNoPush::scheduler::mSchedule: Set("c1"),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 8]
{
  schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  schedNoPush::scheduler::crashes: 2,
  schedNoPush::scheduler::entry: [],
  schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoPush::scheduler::mAssigned: Set(),
  schedNoPush::scheduler::mBuild: Set(("c2", "w2")),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set("c2"),
  schedNoPush::scheduler::mSchedule: Set("c1"),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 9]
{
  schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  schedNoPush::scheduler::crashes: 2,
  schedNoPush::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedNoPush::scheduler::mAssigned: Set(("c1", "w1")),
  schedNoPush::scheduler::mBuild: Set(("c2", "w2")),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set("c2"),
  schedNoPush::scheduler::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 10]
{
  schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w2")),
  schedNoPush::scheduler::crashes: 2,
  schedNoPush::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedNoPush::scheduler::mAssigned: Set(),
  schedNoPush::scheduler::mBuild: Set(("c1", "w1"), ("c2", "w2")),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set("c2"),
  schedNoPush::scheduler::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 11]
{
  schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w2")),
  schedNoPush::scheduler::crashes: 2,
  schedNoPush::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedNoPush::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedNoPush::scheduler::mAssigned: Set(),
  schedNoPush::scheduler::mBuild: Set(("c2", "w2")),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set("c2"),
  schedNoPush::scheduler::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set("c1"),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 12]
{
  schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w2")),
  schedNoPush::scheduler::crashes: 2,
  schedNoPush::scheduler::entry:
    [{ followers: Set("c1"), leased: true, worker: "w1" }],
  schedNoPush::scheduler::free: Map("w1" -> 0, "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("c2"),
  schedNoPush::scheduler::mSchedule: Set(),
  schedNoPush::scheduler::published: 0,
  schedNoPush::scheduler::publishedBy: Set(),
  schedNoPush::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set("c1"),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set("c2"),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[violation] Found an issue (2159ms at 4895 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0xbc4c2afdf3942c87 --backend=rust to reproduce.
error: Invariant violated
An example execution:

[State 0]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CIdle),
  schedNoReport::scheduler::crashes: 0,
  schedNoReport::scheduler::entry: [],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoReport::scheduler::mAssigned: Set(),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set(),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 1]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 0,
  schedNoReport::scheduler::entry: [],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoReport::scheduler::mAssigned: Set(),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set(),
  schedNoReport::scheduler::mSchedule: Set("c2"),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 2]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 0,
  schedNoReport::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w1" }],
  schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set("w1"),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set(),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 3]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 0,
  schedNoReport::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w1" }],
  schedNoReport::scheduler::free: Map("w1" -> 0, "w2" -> 1),
  schedNoReport::scheduler::mAssigned: Set(("c2", "w1")),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set(),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 4]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 1,
  schedNoReport::scheduler::entry: [],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoReport::scheduler::mAssigned: Set(),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set("c2"),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: true
        }
    )
}

[State 5]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 2,
  schedNoReport::scheduler::entry: [],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoReport::scheduler::mAssigned: Set(),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set("c2"),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: false
        }
    )
}

[State 6]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 2,
  schedNoReport::scheduler::entry: [],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoReport::scheduler::mAssigned: Set(),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set("c2"),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 7]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 2,
  schedNoReport::scheduler::entry: [],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoReport::scheduler::mAssigned: Set(),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set("c2"),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 8]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 2,
  schedNoReport::scheduler::entry: [],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoReport::scheduler::mAssigned: Set(),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set(),
  schedNoReport::scheduler::mSchedule: Set("c2"),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 9]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 2,
  schedNoReport::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set(),
  schedNoReport::scheduler::mExpect: Set("w2"),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set(),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 0,
  schedNoReport::scheduler::publishedBy: Set(),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 10]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 2,
  schedNoReport::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set("w1"),
  schedNoReport::scheduler::mExpect: Set("w2"),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set(),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 1,
  schedNoReport::scheduler::publishedBy: Set("w1"),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 11]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 2,
  schedNoReport::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set("w1"),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set(),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 1,
  schedNoReport::scheduler::publishedBy: Set("w1"),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[State 12]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 2,
  schedNoReport::scheduler::entry:
    [{ followers: Set("c2"), leased: true, worker: "w2" }],
  schedNoReport::scheduler::free: Map("w1" -> 1, "w2" -> 0),
  schedNoReport::scheduler::mAssigned: Set(("c2", "w2")),
  schedNoReport::scheduler::mBuild: Set(),
  schedNoReport::scheduler::mDone: Set("w1", "w2"),
  schedNoReport::scheduler::mExpect: Set(),
  schedNoReport::scheduler::mResult: Set(),
  schedNoReport::scheduler::mRetry: Set(),
  schedNoReport::scheduler::mSchedule: Set(),
  schedNoReport::scheduler::published: 2,
  schedNoReport::scheduler::publishedBy: Set("w1", "w2"),
  schedNoReport::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: true,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[violation] Found an issue (7816ms at 3262 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x7c5f98c8532919cf --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::mSchedule: Set(),
  schedTerminal::scheduler::published: 0,
  schedTerminal::scheduler::publishedBy: Set(),
  schedTerminal::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          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::mSchedule: Set(),
  schedTerminal::scheduler::published: 0,
  schedTerminal::scheduler::publishedBy: Set(),
  schedTerminal::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: true
        }
    )
}

[State 2]
{
  schedTerminal::scheduler::cl: Map("c1" -> CQueued, "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::mSchedule: Set("c1"),
  schedTerminal::scheduler::published: 0,
  schedTerminal::scheduler::publishedBy: Set(),
  schedTerminal::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: true
        }
    )
}

[State 3]
{
  schedTerminal::scheduler::cl: Map("c1" -> CFailed, "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::mSchedule: Set(),
  schedTerminal::scheduler::published: 0,
  schedTerminal::scheduler::publishedBy: Set(),
  schedTerminal::scheduler::ws:
    Map(
      "w1" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: false,
          up: true
        }
    )
}

[violation] Found an issue (6689ms at 173 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x192c54be4f64b039 --backend=rust to reproduce.
error: Invariant violated
An example execution:

[State 0]
{
  hookFixed::hook::cache: Set(),
  hookFixed::hook::drvUploaded: false,
  hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set()),
  hookFixed::hook::phase: Query,
  hookFixed::hook::restarts: 0,
  hookFixed::hook::retries: 0,
  hookFixed::hook::toUpload: Set()
}

[State 1]
{
  hookFixed::hook::cache: Set(),
  hookFixed::hook::drvUploaded: false,
  hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set()),
  hookFixed::hook::phase: Query,
  hookFixed::hook::restarts: 1,
  hookFixed::hook::retries: 1,
  hookFixed::hook::toUpload: Set()
}

[State 2]
{
  hookFixed::hook::cache: Set(),
  hookFixed::hook::drvUploaded: false,
  hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set()),
  hookFixed::hook::phase: Upload,
  hookFixed::hook::restarts: 1,
  hookFixed::hook::retries: 1,
  hookFixed::hook::toUpload: Set("drv", "in")
}

[State 3]
{
  hookFixed::hook::cache: Set(),
  hookFixed::hook::drvUploaded: false,
  hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set("drv", "in")),
  hookFixed::hook::phase: Upload,
  hookFixed::hook::restarts: 2,
  hookFixed::hook::retries: 2,
  hookFixed::hook::toUpload: Set("drv", "in")
}

[State 4]
{
  hookFixed::hook::cache: Set("drv", "in"),
  hookFixed::hook::drvUploaded: false,
  hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set("drv", "in")),
  hookFixed::hook::phase: Build,
  hookFixed::hook::restarts: 2,
  hookFixed::hook::retries: 2,
  hookFixed::hook::toUpload: Set("drv", "in")
}

[State 5]
{
  hookFixed::hook::cache: Set("drv", "in", "out"),
  hookFixed::hook::drvUploaded: false,
  hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set("drv", "in", "out")),
  hookFixed::hook::phase: Fetch,
  hookFixed::hook::restarts: 2,
  hookFixed::hook::retries: 2,
  hookFixed::hook::toUpload: Set("drv", "in")
}

[State 6]
{
  hookFixed::hook::cache: Set("drv", "in", "out"),
  hookFixed::hook::drvUploaded: false,
  hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set("drv", "in", "out")),
  hookFixed::hook::phase: Done,
  hookFixed::hook::restarts: 2,
  hookFixed::hook::retries: 2,
  hookFixed::hook::toUpload: Set("drv", "in")
}

[ok] No violation found (3241ms at 6171 traces/second).
Trace length statistics: max=7, min=5, average=6.76
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0x42633deb93d0ee63 --backend=rust to reproduce.
An example execution:

[State 0]
{
  hookNoSubstituteRefs::hook::cache: Set(),
  hookNoSubstituteRefs::hook::drvUploaded: false,
  hookNoSubstituteRefs::hook::local: Map("w1" -> Set(), "w2" -> Set("in")),
  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(), "w2" -> Set("in")),
  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(), "w2" -> Set("in")),
  hookNoSubstituteRefs::hook::phase: Failed,
  hookNoSubstituteRefs::hook::restarts: 0,
  hookNoSubstituteRefs::hook::retries: 0,
  hookNoSubstituteRefs::hook::toUpload: Set("drv")
}

[violation] Found an issue (3286ms at 449 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x6d13988895a649ea --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("in"), "w2" -> Set()),
  hookNoSubstituteDrv::hook::phase: Query,
  hookNoSubstituteDrv::hook::restarts: 0,
  hookNoSubstituteDrv::hook::retries: 0,
  hookNoSubstituteDrv::hook::toUpload: Set()
}

[State 1]
{
  hookNoSubstituteDrv::hook::cache: Set("in"),
  hookNoSubstituteDrv::hook::drvUploaded: false,
  hookNoSubstituteDrv::hook::local: Map("w1" -> Set("in"), "w2" -> Set()),
  hookNoSubstituteDrv::hook::phase: Upload,
  hookNoSubstituteDrv::hook::restarts: 0,
  hookNoSubstituteDrv::hook::retries: 0,
  hookNoSubstituteDrv::hook::toUpload: Set("drv")
}

[State 2]
{
  hookNoSubstituteDrv::hook::cache: Set("drv", "in"),
  hookNoSubstituteDrv::hook::drvUploaded: false,
  hookNoSubstituteDrv::hook::local:
    Map("w1" -> Set("drv", "in"), "w2" -> Set()),
  hookNoSubstituteDrv::hook::phase: Build,
  hookNoSubstituteDrv::hook::restarts: 0,
  hookNoSubstituteDrv::hook::retries: 0,
  hookNoSubstituteDrv::hook::toUpload: Set("drv")
}

[State 3]
{
  hookNoSubstituteDrv::hook::cache: Set("drv", "in"),
  hookNoSubstituteDrv::hook::drvUploaded: false,
  hookNoSubstituteDrv::hook::local:
    Map("w1" -> Set("drv", "in"), "w2" -> Set()),
  hookNoSubstituteDrv::hook::phase: UploadDrv,
  hookNoSubstituteDrv::hook::restarts: 0,
  hookNoSubstituteDrv::hook::retries: 0,
  hookNoSubstituteDrv::hook::toUpload: Set("drv")
}

[State 4]
{
  hookNoSubstituteDrv::hook::cache: Set("drv", "in"),
  hookNoSubstituteDrv::hook::drvUploaded: true,
  hookNoSubstituteDrv::hook::local:
    Map("w1" -> Set("drv", "in"), "w2" -> Set()),
  hookNoSubstituteDrv::hook::phase: Build,
  hookNoSubstituteDrv::hook::restarts: 0,
  hookNoSubstituteDrv::hook::retries: 0,
  hookNoSubstituteDrv::hook::toUpload: Set("drv")
}

[State 5]
{
  hookNoSubstituteDrv::hook::cache: Set("drv", "in"),
  hookNoSubstituteDrv::hook::drvUploaded: true,
  hookNoSubstituteDrv::hook::local:
    Map("w1" -> Set("drv", "in"), "w2" -> Set()),
  hookNoSubstituteDrv::hook::phase: Failed,
  hookNoSubstituteDrv::hook::restarts: 0,
  hookNoSubstituteDrv::hook::retries: 0,
  hookNoSubstituteDrv::hook::toUpload: Set("drv")
}

[violation] Found an issue (1028ms at 1999 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x78b0e4585f1d6def --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" -> 2, "b" -> 2),
  pushFixed::push::inflight: Set((2, "a"), (2, "b")),
  pushFixed::push::left: Map(2 -> 2),
  pushFixed::push::sent: Map(2 -> Set("a", "b"))
}

[State 2]
{
  pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),
  pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a"), (2, "b")),
  pushFixed::push::left: Map(1 -> 2, 2 -> 2),
  pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))
}

[State 3]
{
  pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),
  pushFixed::push::inflight: Set((1, "a"), (1, "b"), (2, "a")),
  pushFixed::push::left: Map(1 -> 2, 2 -> 1),
  pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))
}

[State 4]
{
  pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),
  pushFixed::push::inflight: Set((1, "a"), (2, "a")),
  pushFixed::push::left: Map(1 -> 1, 2 -> 1),
  pushFixed::push::sent: Map(1 -> Set("a", "b"), 2 -> Set("a", "b"))
}

[State 5]
{
  pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),
  pushFixed::push::inflight: Set((1, "a"), (2, "a"), (3, "a"), (3, "b")),
  pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 2),
  pushFixed::push::sent:
    Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))
}

[State 6]
{
  pushFixed::push::byPath: Map("a" -> 3, "b" -> 3),
  pushFixed::push::inflight: Set((1, "a"), (2, "a"), (3, "b")),
  pushFixed::push::left: Map(1 -> 1, 2 -> 1, 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" -> 3, "b" -> 3),
  pushFixed::push::inflight: Set((1, "a"), (2, "a")),
  pushFixed::push::left: Map(1 -> 1, 2 -> 1, 3 -> 0),
  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, "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" -> 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 (138ms at 144928 traces/second).
Trace length statistics: max=10, min=7, average=7.98
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0x94b0f8ffa4f3cd94 --backend=rust to reproduce.