\* TLC configuration for the ParallelSort fork/join model.
\* N=4, Threshold=1 gives a full recursion tree of 7 nodes (root -> 2 -> 4
\* leaves), enough to exercise siblings, cousins, and multi-level joins. Integer
\* constants can be assigned directly in a .cfg.
CONSTANT N = 4
CONSTANT Threshold = 1

SPECIFICATION Spec

INVARIANT TypeOK
INVARIANT NoDataRace

PROPERTY Terminates