MicroTESK

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 |

| --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 |