SPECIFICATION Spec

CONSTANTS
    Clients = {c1, c2}
    MaxInc = 3
    GuardedAttach = TRUE

INVARIANT TypeOK
INVARIANT NoAttachWithoutShellSetup
INVARIANT BootIdempotent

\* Bounded model: once inc hits MaxInc no further wakes are enabled, so
\* some states have no successor by design.
CHECK_DEADLOCK FALSE