tribuchet: building on eliza
An example execution:

[State 0]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 1]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 2]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 3]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 4]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 5]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 6]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 7]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 8]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 9]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 10]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 11]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 12]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 13]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 14]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 15]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 16]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 17]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 18]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 19]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 20]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 21]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 22]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 23]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 24]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 25]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 26]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 27]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 28]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 29]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 30]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

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

[State 0]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        }
    )
}

[State 1]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 2]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 3]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 4]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 5]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 6]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 7]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 8]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 9]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 10]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        }
    )
}

[State 11]
{
  nextToken: 1,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        }
    )
}

[State 12]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 1,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: true,
          outputs: false,
          phase: Building,
          res: RNone,
          slot: true,
          srv: SHolder(1),
          token: 1
        }
    )
}

[State 13]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 14]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 15]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 16]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 17]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 18]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 19]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 20]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 21]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 22]
{
  nextToken: 2,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 23]
{
  nextToken: 3,
  present: false,
  rowStale: false,
  rowToken: 2,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Building,
          res: RNone,
          slot: true,
          srv: SHolder(2),
          token: 2
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 24]
{
  nextToken: 3,
  present: false,
  rowStale: false,
  rowToken: 2,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Building,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 2
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 25]
{
  nextToken: 3,
  present: false,
  rowStale: false,
  rowToken: 2,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: true,
          outputs: false,
          phase: Building,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 2
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 26]
{
  nextToken: 3,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Idle,
          res: RNone,
          slot: false,
          srv: SNone,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RFailed,
          slot: false,
          srv: SNone,
          token: 2
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 27]
{
  nextToken: 3,
  present: false,
  rowStale: false,
  rowToken: 0,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: true,
          outputs: false,
          phase: Pending,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 0
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RFailed,
          slot: false,
          srv: SNone,
          token: 2
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 28]
{
  nextToken: 4,
  present: false,
  rowStale: false,
  rowToken: 3,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: true,
          outputs: false,
          phase: Building,
          res: RNone,
          slot: true,
          srv: SHolder(3),
          token: 3
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RFailed,
          slot: false,
          srv: SNone,
          token: 2
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 29]
{
  nextToken: 4,
  present: false,
  rowStale: false,
  rowToken: 3,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: false,
          outputs: false,
          phase: Building,
          res: RNone,
          slot: true,
          srv: SNone,
          token: 3
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RFailed,
          slot: false,
          srv: SNone,
          token: 2
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[State 30]
{
  nextToken: 4,
  present: false,
  rowStale: false,
  rowToken: 3,
  touched: false,
  ws:
    Map(
      "w1" ->
        {
          conn: true,
          outputs: false,
          phase: Building,
          res: RNone,
          slot: true,
          srv: SNeed,
          token: 3
        },
      "w2" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RFailed,
          slot: false,
          srv: SNone,
          token: 2
        },
      "w3" ->
        {
          conn: false,
          outputs: false,
          phase: Done,
          res: RUnavailable,
          slot: false,
          srv: SNone,
          token: 1
        }
    )
}

[ok] No violation found (356ms at 56180 traces/second).
Trace length statistics: max=31, min=9, average=18.42
You may increase --max-samples and --max-steps.
Use --verbosity to produce more (or less) output.
Use --seed=0xc4f3492c7b5ba278 --backend=rust to reproduce.