Command-Line Options » History » Revision 2
Revision 1 (Andrei Tatarnikov, 05/23/2015 09:20 AM) → Revision 2/24 (Andrei Tatarnikov, 05/23/2015 09:38 AM)
h1. MicroTESK Command-Line Options MicroTESK works in two modes: specification translation and test generation, which are enabled with the @--translate@ (used by default) and @--generate@ keys correspondingly. In addition, the @--help@ key prints information on the command-line format. The @--translate@ and @--generate@ keys are inserted into the command-line by @compile.sh/compile.bat@ and @generate.sh/generate.bat@ scripts correspondingly. Other options should be specified explicitly to customize the behavior of MicroTESK. *Options:* | Full name | Short name | Description Descritpion | | --output-dir <arg> | -d | Sets where to place generated files [works with -t] | | --generate | -g | Generates test programs | | --help | -h | Shows this message | | --include <arg> | -i | Sets include files directories [works with -t] | | --branch-exec-limit <arg> | -l | Sets the limit on control transfers to detect endless loops [works with -g] | | --random-seed <arg> | -r | Sets seed for randomizer [works with -g] | | --solver <arg> | -s | Sets constraint solver engine to be used [works with -g] | | --translate | -t | Translates formal specifications | | --verbose | -v | Enables printing diagnostic messages |