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