blob: b60c298744ad1f8bdb3c7befca8f834ff9e4c67a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
\* 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
|
