Running... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 11400s | 1/30000 samples | 3 samples/sRunning... [                                        ] 0% | ETA: 11400s | 1/30000 samples | 3 samples/sRunning... [■■                                      ] 4% | ETA: 11s | 1471/30000 samples | 2704 samples/sRunning... [■■■                                     ] 8% | ETA: 8s | 2545/30000 samples | 3903 samples/sRunning... [■■■■                                    ] 10% | ETA: 7s | 3284/30000 samples | 4338 samples/sRunning... [■■■■                                    ] 10% | ETA: 7s | 3284/30000 samples | 4338 samples/sRunning... [■■■■■■                                  ] 15% | ETA: 6s | 4657/30000 samples | 4856 samples/sRunning... [■■■■■■                                  ] 15% | ETA: 6s | 4657/30000 samples | 4856 samples/sRunning... [■■■■■■■■                                ] 20% | ETA: 5s | 6273/30000 samples | 5417 samples/sRunning... [■■■■■■■■                                ] 20% | ETA: 5s | 6273/30000 samples | 5417 samples/sRunning... [■■■■■■■■■■■                             ] 27% | ETA: 4s | 8312/30000 samples | 6006 samples/sRunning... [■■■■■■■■■■■■                            ] 30% | ETA: 4s | 9226/30000 samples | 6167 samples/sRunning... [■■■■■■■■■■■■                            ] 30% | ETA: 4s | 9226/30000 samples | 6167 samples/sRunning... [■■■■■■■■■■■■                            ] 30% | ETA: 4s | 9226/30000 samples | 6167 samples/sRunning... [■■■■■■■■■■■■■■■                         ] 37% | ETA: 3s | 11353/30000 samples | 6532 samples/sRunning... [■■■■■■■■■■■■■■■                         ] 37% | ETA: 3s | 11353/30000 samples | 6532 samples/sRunning... [■■■■■■■■■■■■■■■■■■                      ] 45% | ETA: 2s | 13661/30000 samples | 6893 samples/sRunning... [■■■■■■■■■■■■■■■■■■                      ] 45% | ETA: 2s | 13661/30000 samples | 6893 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■                   ] 51% | ETA: 2s | 15588/30000 samples | 7134 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■                  ] 55% | ETA: 2s | 16674/30000 samples | 7243 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■                  ] 55% | ETA: 2s | 16674/30000 samples | 7243 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■                  ] 55% | ETA: 2s | 16674/30000 samples | 7243 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■               ] 63% | ETA: 2s | 19034/30000 samples | 7458 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■             ] 68% | ETA: 2s | 20493/30000 samples | 7551 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■             ] 68% | ETA: 2s | 20493/30000 samples | 7551 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■             ] 68% | ETA: 2s | 20493/30000 samples | 7551 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■          ] 75% | ETA: 1s | 22718/30000 samples | 7665 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■        ] 79% | ETA: 1s | 23729/30000 samples | 7714 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■        ] 79% | ETA: 1s | 23729/30000 samples | 7714 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■       ] 82% | ETA: 1s | 24630/30000 samples | 7553 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■       ] 82% | ETA: 1s | 24630/30000 samples | 7553 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■      ] 85% | ETA: 1s | 25628/30000 samples | 7318 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■      ] 85% | ETA: 1s | 25628/30000 samples | 7318 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■    ] 88% | ETA: 1s | 26631/30000 samples | 7266 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■   ] 92% | ETA: 1s | 27863/30000 samples | 7226 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■   ] 92% | ETA: 1s | 27863/30000 samples | 7226 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 96% | ETA: 1s | 28881/30000 samples | 7183 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 96% | ETA: 1s | 28881/30000 samples | 7183 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 29812/30000 samples | 7061 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 100% | ETA: 0s | 30000/30000 samples | 6932 samples/sAn 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" -> CIdle),
  schedFixed::scheduler::crashes: 1,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set(),
  schedFixed::scheduler::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: false,
          up: false
        }
    )
}

[State 2]
{
  schedFixed::scheduler::cl: Map("c1" -> CIdle, "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("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: false,
          up: false
        }
    )
}

[State 3]
{
  schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 1,
  schedFixed::scheduler::entry:
    [{ followers: Set("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(),
  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 4]
{
  schedFixed::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(),
  schedFixed::scheduler::mDone: Set(),
  schedFixed::scheduler::mExpect: Set(),
  schedFixed::scheduler::mResult: Set(),
  schedFixed::scheduler::mRetry: Set("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: false,
          up: false
        }
    )
}

[State 5]
{
  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(),
  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: false,
          up: false
        }
    )
}

[State 6]
{
  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(),
  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: 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(),
  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: true,
          up: true
        },
      "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: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("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 9]
{
  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 10]
{
  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 11]
{
  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 12]
{
  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(("c2", "w1")),
  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 13]
{
  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(("c2", "w1")),
  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 14]
{
  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 15]
{
  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 16]
{
  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(("c2", "w1")),
  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 17]
{
  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 18]
{
  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 19]
{
  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(),
  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: true,
          running: true,
          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: "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(),
  schedFixed::scheduler::mSchedule: Set("c1", "c2"),
  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 21]
{
  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(),
  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: true,
          running: true,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 22]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CQueued),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry:
    [{ followers: Set("c1", "c2"), 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(),
  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: 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(("c1", "w1")),
  schedFixed::scheduler::mBuild: Set(("c2", "w1")),
  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: 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(("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("c2"),
          built: false,
          expecting: true,
          running: true,
          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" -> 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(),
  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 26]
{
  schedFixed::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w1")),
  schedFixed::scheduler::crashes: 2,
  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("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 27]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),
  schedFixed::scheduler::crashes: 2,
  schedFixed::scheduler::entry: [],
  schedFixed::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedFixed::scheduler::mAssigned: Set(),
  schedFixed::scheduler::mBuild: Set(("c1", "w1")),
  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 28]
{
  schedFixed::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CSent("w1")),
  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("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" -> CSent("w1"), "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("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 (4365ms at 6873 traces/second).
Trace length statistics: max=31, min=14, average=17.61
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0xba92937ec6d7bd29 --backend=rust to reproduce.
Running... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [■■                                      ] 4% | ETA: 8s | 1234/30000 samples | 4073 samples/sRunning... [■■                                      ] 4% | ETA: 8s | 1234/30000 samples | 4073 samples/sRunning... [■■                                      ] 4% | ETA: 8s | 1234/30000 samples | 4073 samples/sRunning... [■■                                      ] 5% | ETA: 9s | 1655/30000 samples | 3251 samples/sRunning... [■■■                                     ] 6% | ETA: 10s | 1923/30000 samples | 3092 samples/sRunning... [■■■                                     ] 7% | ETA: 10s | 2178/30000 samples | 2984 samples/sRunning... [■■■                                     ] 8% | ETA: 10s | 2427/30000 samples | 2859 samples/sRunning... [■■■■                                    ] 8% | ETA: 10s | 2646/30000 samples | 2782 samples/sRunning... [■■■■                                    ] 8% | ETA: 10s | 2646/30000 samples | 2782 samples/sRunning... [■■■■                                    ] 10% | ETA: 10s | 3251/30000 samples | 2707 samples/sRunning... [■■■■■                                   ] 11% | ETA: 10s | 3517/30000 samples | 2693 samples/sRunning... [■■■■■                                   ] 12% | ETA: 10s | 3801/30000 samples | 2690 samples/sRunning... [■■■■■                                   ] 12% | ETA: 10s | 3801/30000 samples | 2690 samples/sRunning... [■■■■■■                                  ] 13% | ETA: 12s | 4142/30000 samples | 2662 samples/sRunning... [■■■■■■                                  ] 14% | ETA: 11s | 4475/30000 samples | 2665 samples/sRunning... [■■■■■■                                  ] 14% | ETA: 11s | 4475/30000 samples | 2665 samples/sRunning... [■■■■■■■                                 ] 16% | ETA: 11s | 4893/30000 samples | 2643 samples/sRunning... [■■■■■■■                                 ] 17% | ETA: 11s | 5215/30000 samples | 2622 samples/sRunning... [■■■■■■■                                 ] 18% | ETA: 10s | 5584/30000 samples | 2617 samples/sRunning... [■■■■■■■■                                ] 19% | ETA: 10s | 5844/30000 samples | 2612 samples/sRunning... [■■■■■■■■                                ] 20% | ETA: 10s | 6060/30000 samples | 2593 samples/sRunning... [■■■■■■■■                                ] 20% | ETA: 10s | 6060/30000 samples | 2593 samples/sRunning... [■■■■■■■■                                ] 21% | ETA: 10s | 6308/30000 samples | 2584 samples/sRunning... [■■■■■■■■■                               ] 22% | ETA: 10s | 6759/30000 samples | 2580 samples/sRunning... [■■■■■■■■■                               ] 22% | ETA: 10s | 6759/30000 samples | 2580 samples/sRunning... [■■■■■■■■■                               ] 23% | ETA: 10s | 7105/30000 samples | 2586 samples/sRunning... [■■■■■■■■■■                              ] 25% | ETA: 10s | 7568/30000 samples | 2568 samples/sRunning... [■■■■■■■■■■                              ] 26% | ETA: 9s | 7847/30000 samples | 2574 samples/sRunning... [■■■■■■■■■■                              ] 26% | ETA: 9s | 7847/30000 samples | 2574 samples/sRunning... [■■■■■■■■■■                              ] 26% | ETA: 9s | 7847/30000 samples | 2574 samples/sRunning... [■■■■■■■■■■■                             ] 27% | ETA: 9s | 8314/30000 samples | 2554 samples/sRunning... [■■■■■■■■■■■                             ] 27% | ETA: 9s | 8314/30000 samples | 2554 samples/sRunning... [■■■■■■■■■■■■                            ] 29% | ETA: 9s | 8942/30000 samples | 2551 samples/sRunning... [■■■■■■■■■■■■                            ] 30% | ETA: 9s | 9183/30000 samples | 2547 samples/sRunning... [■■■■■■■■■■■■                            ] 30% | ETA: 9s | 9183/30000 samples | 2547 samples/sRunning... [■■■■■■■■■■■■■                           ] 32% | ETA: 9s | 9783/30000 samples | 2552 samples/sRunning... [■■■■■■■■■■■■■                           ] 32% | ETA: 9s | 9783/30000 samples | 2552 samples/sRunning... [■■■■■■■■■■■■■■                          ] 34% | ETA: 8s | 10291/30000 samples | 2553 samples/sRunning... [■■■■■■■■■■■■■■                          ] 34% | ETA: 8s | 10291/30000 samples | 2553 samples/sRunning... [■■■■■■■■■■■■■■                          ] 34% | ETA: 8s | 10291/30000 samples | 2553 samples/sRunning... [■■■■■■■■■■■■■■■                         ] 36% | ETA: 8s | 10951/30000 samples | 2557 samples/sRunning... [■■■■■■■■■■■■■■■                         ] 37% | ETA: 8s | 11356/30000 samples | 2558 samples/sRunning... [■■■■■■■■■■■■■■■                         ] 37% | ETA: 8s | 11356/30000 samples | 2558 samples/sRunning... [■■■■■■■■■■■■■■■■                        ] 38% | ETA: 8s | 11679/30000 samples | 2552 samples/sRunning... [■■■■■■■■■■■■■■■■                        ] 38% | ETA: 8s | 11679/30000 samples | 2552 samples/sRunning... [■■■■■■■■■■■■■■■■                        ] 40% | ETA: 8s | 12283/30000 samples | 2555 samples/sRunning... [■■■■■■■■■■■■■■■■                        ] 40% | ETA: 8s | 12283/30000 samples | 2555 samples/sRunning... [■■■■■■■■■■■■■■■■■                       ] 42% | ETA: 7s | 12857/30000 samples | 2555 samples/sRunning... [■■■■■■■■■■■■■■■■■■                      ] 43% | ETA: 7s | 13152/30000 samples | 2559 samples/sRunning... [■■■■■■■■■■■■■■■■■■                      ] 44% | ETA: 7s | 13410/30000 samples | 2557 samples/sRunning... [■■■■■■■■■■■■■■■■■■                      ] 44% | ETA: 7s | 13410/30000 samples | 2557 samples/sRunning... [■■■■■■■■■■■■■■■■■■                      ] 44% | ETA: 7s | 13410/30000 samples | 2557 samples/sRunning... [■■■■■■■■■■■■■■■■■■■                     ] 46% | ETA: 7s | 14016/30000 samples | 2553 samples/sRunning... [■■■■■■■■■■■■■■■■■■■                     ] 47% | ETA: 7s | 14270/30000 samples | 2552 samples/sRunning... [■■■■■■■■■■■■■■■■■■■                     ] 47% | ETA: 7s | 14270/30000 samples | 2552 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■                    ] 49% | ETA: 6s | 14937/30000 samples | 2565 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■                    ] 49% | ETA: 6s | 14937/30000 samples | 2565 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■                   ] 51% | ETA: 6s | 15375/30000 samples | 2563 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■                   ] 52% | ETA: 6s | 15889/30000 samples | 2569 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■                   ] 52% | ETA: 6s | 15889/30000 samples | 2569 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■                   ] 52% | ETA: 6s | 15889/30000 samples | 2569 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■                  ] 55% | ETA: 6s | 16570/30000 samples | 2575 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■                  ] 56% | ETA: 6s | 16814/30000 samples | 2572 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■                  ] 56% | ETA: 6s | 16814/30000 samples | 2572 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■                 ] 58% | ETA: 5s | 17547/30000 samples | 2586 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■                 ] 58% | ETA: 5s | 17547/30000 samples | 2586 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■                 ] 58% | ETA: 5s | 17547/30000 samples | 2586 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■                ] 60% | ETA: 5s | 18286/30000 samples | 2599 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■                ] 60% | ETA: 5s | 18286/30000 samples | 2599 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■               ] 62% | ETA: 5s | 18859/30000 samples | 2606 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■              ] 64% | ETA: 4s | 19241/30000 samples | 2605 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■              ] 64% | ETA: 4s | 19241/30000 samples | 2605 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■             ] 66% | ETA: 4s | 19879/30000 samples | 2607 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■             ] 66% | ETA: 4s | 19879/30000 samples | 2607 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■             ] 67% | ETA: 4s | 20257/30000 samples | 2596 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■             ] 67% | ETA: 4s | 20257/30000 samples | 2596 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■             ] 68% | ETA: 4s | 20420/30000 samples | 2570 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■             ] 68% | ETA: 4s | 20420/30000 samples | 2570 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■            ] 69% | ETA: 4s | 20953/30000 samples | 2570 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■           ] 71% | ETA: 4s | 21399/30000 samples | 2571 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■           ] 71% | ETA: 4s | 21399/30000 samples | 2571 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■           ] 72% | ETA: 4s | 21712/30000 samples | 2565 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■           ] 72% | ETA: 4s | 21712/30000 samples | 2565 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■          ] 74% | ETA: 4s | 22207/30000 samples | 2564 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■          ] 74% | ETA: 4s | 22207/30000 samples | 2564 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■          ] 75% | ETA: 4s | 22674/30000 samples | 2555 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■         ] 76% | ETA: 4s | 22955/30000 samples | 2551 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■         ] 77% | ETA: 4s | 23208/30000 samples | 2551 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■         ] 77% | ETA: 4s | 23208/30000 samples | 2551 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■         ] 78% | ETA: 3s | 23585/30000 samples | 2549 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■         ] 78% | ETA: 3s | 23585/30000 samples | 2549 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■        ] 80% | ETA: 3s | 24142/30000 samples | 2546 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■        ] 81% | ETA: 3s | 24357/30000 samples | 2541 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■       ] 81% | ETA: 3s | 24567/30000 samples | 2535 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■       ] 82% | ETA: 3s | 24891/30000 samples | 2533 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■      ] 83% | ETA: 3s | 25125/30000 samples | 2530 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■      ] 83% | ETA: 3s | 25125/30000 samples | 2530 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■      ] 85% | ETA: 2s | 25773/30000 samples | 2535 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■      ] 85% | ETA: 2s | 25773/30000 samples | 2535 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■     ] 87% | ETA: 2s | 26262/30000 samples | 2540 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■     ] 87% | ETA: 2s | 26262/30000 samples | 2540 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■     ] 88% | ETA: 2s | 26624/30000 samples | 2535 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■    ] 90% | ETA: 2s | 27264/30000 samples | 2569 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■   ] 92% | ETA: 1s | 27797/30000 samples | 2593 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■   ] 92% | ETA: 1s | 27833/30000 samples | 2571 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■   ] 93% | ETA: 1s | 27942/30000 samples | 2557 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■  ] 94% | ETA: 1s | 28204/30000 samples | 2557 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■  ] 94% | ETA: 1s | 28204/30000 samples | 2557 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■  ] 95% | ETA: 1s | 28669/30000 samples | 2552 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 96% | ETA: 1s | 28981/30000 samples | 2547 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 97% | ETA: 1s | 29296/30000 samples | 2548 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 97% | ETA: 1s | 29296/30000 samples | 2548 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 98% | ETA: 1s | 29535/30000 samples | 2544 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 98% | ETA: 1s | 29535/30000 samples | 2544 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 29791/30000 samples | 2523 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 29865/30000 samples | 2507 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 29937/30000 samples | 2492 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 100% | ETA: 0s | 30000/30000 samples | 2463 samples/sAn 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: 1,
  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: false,
          up: false
        }
    )
}

[State 3]
{
  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: 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" -> 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("c1"),
  schedNoFence::scheduler::mSchedule: Set("c2"),
  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 5]
{
  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("c1"),
  schedNoFence::scheduler::mSchedule: Set("c2"),
  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 6]
{
  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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 7]
{
  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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 8]
{
  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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 9]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  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")),
  schedNoFence::scheduler::mBuild: Set(("c2", "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: 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 10]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(("c1", "w2"), ("c2", "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: 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 11]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(("c2", "w2")),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w2"),
  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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 12]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(("c2", "w2")),
  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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 13]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w2"),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set("c2"),
  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 14]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  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")),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w2"),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set("c2"),
  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 15]
{
  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")),
  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("c2"),
  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 16]
{
  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(),
  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("c2"),
  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 17]
{
  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(),
  schedNoFence::scheduler::mBuild: Set(),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w2"),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set("c1"),
  schedNoFence::scheduler::mSchedule: Set("c2"),
  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 18]
{
  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(),
  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", "c2"),
  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 19]
{
  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")),
  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("c2"),
  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 20]
{
  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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 21]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  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")),
  schedNoFence::scheduler::mBuild: Set(("c2", "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: 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 22]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(("c1", "w2"), ("c2", "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: 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 23]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(("c2", "w2")),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set("w2"),
  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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: false,
          running: false,
          session: true,
          up: true
        }
    )
}

[State 24]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(("c2", "w2")),
  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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[State 25]
{
  schedNoFence::scheduler::cl: Map("c1" -> CSent("w2"), "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(("c2", "w2")),
  schedNoFence::scheduler::mDone: Set("w2"),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set("c1"),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w2"),
  schedNoFence::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 26]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(("c2", "w2")),
  schedNoFence::scheduler::mDone: Set("w2"),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set(),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set("c1"),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w2"),
  schedNoFence::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]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  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(),
  schedNoFence::scheduler::mBuild: Set(("c2", "w2")),
  schedNoFence::scheduler::mDone: Set("w2"),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set("c1"),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w2"),
  schedNoFence::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]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  schedNoFence::scheduler::crashes: 2,
  schedNoFence::scheduler::entry: [],
  schedNoFence::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoFence::scheduler::mAssigned: Set(),
  schedNoFence::scheduler::mBuild: Set(("c2", "w2")),
  schedNoFence::scheduler::mDone: Set(),
  schedNoFence::scheduler::mExpect: Set(),
  schedNoFence::scheduler::mResult: Set("c1"),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w2"),
  schedNoFence::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]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CSent("w2")),
  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("c1", "c2"),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w2"),
  schedNoFence::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]
{
  schedNoFence::scheduler::cl: Map("c1" -> CQueued, "c2" -> CDone),
  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("c1"),
  schedNoFence::scheduler::mRetry: Set(),
  schedNoFence::scheduler::mSchedule: Set(),
  schedNoFence::scheduler::published: 1,
  schedNoFence::scheduler::publishedBy: Set("w2"),
  schedNoFence::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 (12248ms at 2449 traces/second).
Trace length statistics: max=31, min=13, average=17.57
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0x87683464076efdc5 --backend=rust to reproduce.
Running... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sAn 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: true,
          up: true
        }
    )
}

[State 2]
{
  schedNoPush::scheduler::cl: Map("c1" -> CQueued, "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("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 3]
{
  schedNoPush::scheduler::cl: Map("c1" -> CQueued, "c2" -> CIdle),
  schedNoPush::scheduler::crashes: 1,
  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(),
  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("w1"), "c2" -> CIdle),
  schedNoPush::scheduler::crashes: 1,
  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")),
  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 5]
{
  schedNoPush::scheduler::cl: Map("c1" -> CSent("w1"), "c2" -> CIdle),
  schedNoPush::scheduler::crashes: 2,
  schedNoPush::scheduler::entry: [],
  schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoPush::scheduler::mAssigned: Set(),
  schedNoPush::scheduler::mBuild: Set(("c1", "w1")),
  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("w1"), "c2" -> CIdle),
  schedNoPush::scheduler::crashes: 2,
  schedNoPush::scheduler::entry: [],
  schedNoPush::scheduler::free: Map("w1" -> 1, "w2" -> 1),
  schedNoPush::scheduler::mAssigned: Set(),
  schedNoPush::scheduler::mBuild: Set(),
  schedNoPush::scheduler::mDone: Set(),
  schedNoPush::scheduler::mExpect: Set(),
  schedNoPush::scheduler::mResult: Set(),
  schedNoPush::scheduler::mRetry: Set(),
  schedNoPush::scheduler::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
        }
    )
}

[violation] Found an issue (491ms at 731 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0xd1b3523c4c71915d --backend=rust to reproduce.
error: Invariant violated
Running... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/30000 samples | 0 samples/sRunning... [■                                       ] 1% | ETA: 15s | 417/30000 samples | 1986 samples/sRunning... [■                                       ] 1% | ETA: 20s | 493/30000 samples | 1508 samples/sRunning... [■                                       ] 1% | ETA: 20s | 493/30000 samples | 1508 samples/sRunning... [■                                       ] 2% | ETA: 21s | 670/30000 samples | 1429 samples/sRunning... [■■                                      ] 3% | ETA: 18s | 1153/30000 samples | 1676 samples/sRunning... [■■                                      ] 3% | ETA: 18s | 1153/30000 samples | 1676 samples/sRunning... [■■                                      ] 3% | ETA: 18s | 1153/30000 samples | 1676 samples/sRunning... [■■                                      ] 4% | ETA: 20s | 1338/30000 samples | 1453 samples/sRunning... [■■                                      ] 4% | ETA: 20s | 1338/30000 samples | 1453 samples/sRunning... [■■                                      ] 4% | ETA: 22s | 1444/30000 samples | 1312 samples/sRunning... [■■                                      ] 5% | ETA: 23s | 1505/30000 samples | 1250 samples/sRunning... [■■                                      ] 5% | ETA: 23s | 1666/30000 samples | 1237 samples/sRunning... [■■                                      ] 5% | ETA: 23s | 1666/30000 samples | 1237 samples/sRunning... [■■                                      ] 6% | ETA: 27s | 1853/30000 samples | 1182 samples/sRunning... [■■                                      ] 6% | ETA: 28s | 1873/30000 samples | 1121 samples/sRunning... [■■■                                     ] 6% | ETA: 31s | 1892/30000 samples | 1053 samples/sRunning... [■■■                                     ] 6% | ETA: 29s | 1984/30000 samples | 1040 samples/sRunning... [■■■                                     ] 6% | ETA: 29s | 1984/30000 samples | 1040 samples/sRunning... [■■■                                     ] 6% | ETA: 44s | 2065/30000 samples | 984 samples/sRunning... [■■■                                     ] 6% | ETA: 44s | 2065/30000 samples | 984 samples/sRunning... [■■■                                     ] 7% | ETA: 48s | 2121/30000 samples | 940 samples/sRunning... [■■■                                     ] 7% | ETA: 54s | 2125/30000 samples | 885 samples/sRunning... [■■■                                     ] 7% | ETA: 54s | 2125/30000 samples | 885 samples/sRunning... [■■■                                     ] 7% | ETA: 59s | 2147/30000 samples | 845 samples/sRunning... [■■■                                     ] 7% | ETA: 73s | 2168/30000 samples | 817 samples/sAn 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: "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: 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: "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(),
  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: true,
          running: true,
          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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          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: false,
          running: false,
          session: false,
          up: false
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[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: false,
          running: false,
          session: true,
          up: true
        },
      "w2" ->
        {
          attached: Set(),
          built: false,
          expecting: true,
          running: true,
          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(),
  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: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[State 8]
{
  schedNoReport::scheduler::cl: Map("c1" -> CIdle, "c2" -> CQueued),
  schedNoReport::scheduler::crashes: 2,
  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: true,
          running: true,
          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: "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: true,
          running: true,
          session: true,
          up: true
        }
    )
}

[violation] Found an issue (2911ms at 745 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0xa02dfb098039cf9c --backend=rust to reproduce.
error: Invariant violated
Running... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [■■■■■■■                                 ] 17% | ETA: 3s | 3483/20000 samples | 6911 samples/sRunning... [■■■■■■■                                 ] 17% | ETA: 3s | 3483/20000 samples | 6911 samples/sRunning... [■■■■■■■■■■                              ] 25% | ETA: 2s | 5194/20000 samples | 7549 samples/sRunning... [■■■■■■■■■■                              ] 25% | ETA: 2s | 5194/20000 samples | 7549 samples/sRunning... [■■■■■■■■■■■■■                           ] 32% | ETA: 2s | 6427/20000 samples | 7197 samples/sRunning... [■■■■■■■■■■■■■                           ] 32% | ETA: 2s | 6427/20000 samples | 7197 samples/sRunning... [■■■■■■■■■■■■■■■                         ] 37% | ETA: 2s | 7585/20000 samples | 6772 samples/sRunning... [■■■■■■■■■■■■■■■■■                       ] 43% | ETA: 2s | 8661/20000 samples | 6793 samples/sRunning... [■■■■■■■■■■■■■■■■■■                      ] 44% | ETA: 2s | 8894/20000 samples | 6459 samples/sRunning... [■■■■■■■■■■■■■■■■■■                      ] 44% | ETA: 2s | 8894/20000 samples | 6459 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■                    ] 49% | ETA: 2s | 9847/20000 samples | 6308 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■                    ] 49% | ETA: 2s | 9847/20000 samples | 6308 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■                  ] 55% | ETA: 2s | 11103/20000 samples | 6352 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■                  ] 55% | ETA: 2s | 11103/20000 samples | 6352 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■               ] 62% | ETA: 2s | 12535/20000 samples | 6340 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■           ] 72% | ETA: 1s | 14595/20000 samples | 7013 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■          ] 74% | ETA: 1s | 14811/20000 samples | 6785 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■         ] 76% | ETA: 1s | 15291/20000 samples | 6692 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■         ] 76% | ETA: 1s | 15291/20000 samples | 6692 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■       ] 82% | ETA: 1s | 16434/20000 samples | 6822 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■     ] 88% | ETA: 1s | 17681/20000 samples | 6969 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■    ] 89% | ETA: 1s | 17986/20000 samples | 6795 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■    ] 89% | ETA: 1s | 17986/20000 samples | 6795 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 97% | ETA: 1s | 19474/20000 samples | 6755 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19815/20000 samples | 6636 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19909/20000 samples | 6449 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19956/20000 samples | 6252 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19956/20000 samples | 6252 samples/sAn 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: Query,
  hookFixed::hook::restarts: 2,
  hookFixed::hook::retries: 2,
  hookFixed::hook::toUpload: Set()
}

[State 3]
{
  hookFixed::hook::cache: Set(),
  hookFixed::hook::drvUploaded: false,
  hookFixed::hook::local: Map("w1" -> Set(), "w2" -> Set()),
  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 (3304ms at 6053 traces/second).
Trace length statistics: max=7, min=5, average=6.75
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0xe449f7919c7fb461 --backend=rust to reproduce.
Running... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sAn 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 (177ms at 418 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x5db5ed8be129893b --backend=rust to reproduce.
error: Invariant violated
Running... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sAn example execution:

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

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

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

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

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

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

[violation] Found an issue (209ms at 488 traces/second).
Use --verbosity=3 to show executions.
Use --seed=0x5b252d83e7e3e4e8 --backend=rust to reproduce.
error: Invariant violated
Running... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [                                        ] 0% | ETA: 0s | 0/20000 samples | 0 samples/sRunning... [■■■■■■■■■■■                             ] 28% | ETA: 1s | 5649/20000 samples | 30048 samples/sRunning... [■■■■■■■■■■■                             ] 28% | ETA: 1s | 5649/20000 samples | 30048 samples/sRunning... [■■■■■■■■■■■                             ] 28% | ETA: 1s | 5649/20000 samples | 30048 samples/sRunning... [■■■■■■■■■■■■■■■■■■■                     ] 47% | ETA: 1s | 9494/20000 samples | 21725 samples/sRunning... [■■■■■■■■■■■■■■■■■■■                     ] 47% | ETA: 1s | 9494/20000 samples | 21725 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■               ] 61% | ETA: 1s | 12367/20000 samples | 20109 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■            ] 68% | ETA: 1s | 13779/20000 samples | 19191 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■            ] 68% | ETA: 1s | 13779/20000 samples | 19191 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■    ] 89% | ETA: 1s | 17946/20000 samples | 18597 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 96% | ETA: 1s | 19317/20000 samples | 17804 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■ ] 96% | ETA: 1s | 19317/20000 samples | 17804 samples/sRunning... [■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■■] 99% | ETA: 1s | 19957/20000 samples | 16107 samples/sAn 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" -> 2, "b" -> 2),
  pushFixed::push::inflight: Set((2, "a")),
  pushFixed::push::left: Map(2 -> 1),
  pushFixed::push::sent: Map(2 -> Set("a", "b"))
}

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

[State 4]
{
  pushFixed::push::byPath: Map("a" -> 1, "b" -> 1),
  pushFixed::push::inflight: Set((1, "a"), (1, "b")),
  pushFixed::push::left: Map(1 -> 2, 2 -> 0),
  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"), (1, "b"), (3, "a"), (3, "b")),
  pushFixed::push::left: Map(1 -> 2, 2 -> 0, 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"), (1, "b"), (3, "b")),
  pushFixed::push::left: Map(1 -> 2, 2 -> 0, 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, "b"), (3, "b")),
  pushFixed::push::left: Map(1 -> 1, 2 -> 0, 3 -> 1),
  pushFixed::push::sent:
    Map(1 -> Set("a", "b"), 2 -> Set("a", "b"), 3 -> Set("a", "b"))
}

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