\* TLC configuration for the SleepSort model.
\* Input is a small multiset with a duplicate (the two 1s) and out-of-order
\* values -- enough to exercise ordering, ties, and termination exhaustively.
\* It is defined as InputValue in the module (a .cfg cannot hold a <<..>>).
CONSTANT Input <- InputValue

SPECIFICATION Spec

INVARIANT TypeOK
INVARIANT OutputSorted
INVARIANT PermutationWhenDone

PROPERTY Terminates