\* Passing config (complete search, 69872 states / 5772 distinct, depth 15).
\* Sessions are independent in the design (own address, own ledger) and
\* the spec is parametric in Sessions; a two-session run at these bounds
\* exceeds the hosted checker's budget, so the alternate
\*   Sessions = {s1, s2}, MaxCtr = 1, MaxIssued = 1
\* (214497 / 17144 distinct, depth 15) covers cross-session isolation and
\* this one covers two-receipt sequences across restarts.  MaxReorg = 2 = K
\* exercises un-credit and negative balances (SolventUnderFinality is
\* vacuous there); MaxReorg = 1 (6272 / 997, depth 12) checks it for real.
\* PersistOnWrite = FALSE (lazy snapshots) violates IssuedMonotone and
\* ReplaySafe within 3 steps: refuse -> crash -> restart -> same counter
\* accepted, receipt seq 1 emitted twice.
CONSTANTS
  Sessions = {s1}
  OutputIds = {o1, o2}
  K = 2
  MaxHeight = 3
  MaxReorg = 2
  MaxAmt = 1
  MaxCost = 1
  MaxCtr = 2
  MaxInflight = 1
  MaxIssued = 2
  PersistOnWrite = TRUE
  NULL = NULL

SPECIFICATION Spec
INVARIANT TypeOK
INVARIANT ChainWellFormed
INVARIANT SpentWithinConfirmed
INVARIANT SolventUnderFinality
INVARIANT NoDoubleCredit
INVARIANT CreditedWasConfirmed
INVARIANT ReservedMatchesInflight
INVARIANT IssuedMonotone
INVARIANT ReceiptsConsistent
INVARIANT ReceiptsDurable
INVARIANT ReplaySafe
PROPERTY NoOverdraftAdmission
CHECK_DEADLOCK FALSE