JsWorkerPool.cfg

\* SPDX-License-Identifier: MPL-2.0
\* Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
\* TLC config for the JsWorkerPool model.
\* Run: java -cp /path/to/tla2tools.jar tlc2.TLC JsWorkerPool.tla
\*
\* Two workers, three requests.
\* Route maps r1 and r3 to w0, r2 to w1.
\* This captures the key topology: two requests sharing one slot (so a
\* single crash at w0 terminates both r1 and r3, while r2 at w1 is
\* unaffected — the CRASH-ISOLATION scenario).
CONSTANTS
  Requests = {r1, r2, r3}
  Workers  = {w0, w1}
  Route    = [r1 |-> w0, r2 |-> w1, r3 |-> w0]

SPECIFICATION Spec

INVARIANTS
  TypeOK
  ReplyOnce
  Consistent
  NoPendingWhileDown
  RouteConsistency

PROPERTIES
  EventuallyReplied