| --args <arg-list> |
(required) comma separated list of finitization parameters, ordered as in
corresponding finitization method. |
| --class <fullClassName> |
(required) name of the class that contains finitization |
| --config <fileName> |
name of the config file to be used |
| --cvDelta |
use delta file format when storing candidate vectors to disk |
| --cvEnd <num> |
set the end candidate vector to <num>-th vector from cvFile |
| --cvExpected <num> |
expected number of total explored vectors |
| --cvFile <filename> |
name of the candidate-vectors file |
| --cvFullFormatRatio <num> |
the ratio of full format vectors (if delta file format is used) |
| --cvStart <num> |
set the start candidate vector to <num>-th vector from cvFile |
| --cvWrite |
write all explored candidate vectors to file |
| --cvWriteNum <num> |
write only <num> equi-distant vectors to disk |
| --excludePackages <packages> |
comma separated list of packages to be excluded from instrumentation |
| --finitization <finMethodName> |
set the name of finitization method. If omitted, default name
fin<ClassName> is used. |
| --help |
print help message. |
| --listeners <listenerClasses> |
comma separated list of full class names that implement
ITestCaseListener interface. |
| --maxStructs <num> |
stop execution after finding <num> invariant-passing
structures |
| --predicate <predMethodName> |
set the name of predicate method. If omitted, default name "repOK"
will be used |
| --print |
print the generated structure to the console |
| --printCandVects |
print candidate vector and accessed field list during the search. |
| --progress <threshold> |
print status of the search after exploration of <threshold>
candidates |
| --serialize <filename> |
seralize the invariant-passing test cases to the specified file. If
filename contains absolute path, use quotes. |
| --visualize |
visualize the generated data structures |