Run either quail script (Linux) or quail.bat (Windows) in a command line console.
quail [options] program.quail
Alternatively it is possible to run directly the JAR package Quail.jar in the directory dist.
Options:
quail [options] program.quail
Options:
-c | --clean
Delete the temporary preprocessed file.
--config=<filename>
Alternative location for the configuration file.
-h | -? | --help
Print this help and terminate.
-v <level>
Verbose mode between 0 (minimum) and 4 (maximum).
Default value if not specified is 2.
-th <number>
Sets the number of parallel threads QUAIL should use. Default is the number returned by Runtime.getRuntime().availableProcessors(), minimum 1
-p <value>
Define computation precision as a number of digits. Default value if not specified is 15.
--const:<cname>:=<cvalue>
Replace the value of a constant cname in the model by the value cvalue
--preprocess
Run only the preprocessor and terminate.
--simulate
Run the simulator instead of the analyzer. If this option is chosen, the following additional options are available:
-i <iterations>
Sets the number of simulations. Default: 50000
-l <threshold>
Sets the sufficient probability threshold after which exploration of the probability space can be terminated.
Default: 1 (meaning 100% of the probability space)
-t <time_limit> Sets the time limit (in milliseconds) for the simulation. A value of 0 means no time limit. Default: 0 (meaning no time limit)
--fullmc
Runs the QUAIl version 1 algorithm constructing the full Markov chain (slow). If this option is chosen, the following additional options are available:
--no_hiding
Do not run the hiding algorithm.
-mc [values]
Print the Markov chains:
0 program Markov chain
1 hiding non observable states
2 observer’s quotient
3 secret’s quotient
4 joint quotient
e.g. -mc 0 1 2 3 4 will print all Markov chains.
By default, if no value is given, print the program Markov chain.
The output format can be any format supported by Graphviz,
Use option -Tgif,-Tfig,-Tpdf,-Tps,-Tsvg or -Tpng for the most common.
By default if no format is provided it prints in dot format.
-o <filename>
File name for Markov chains. Suffixes are added automatically.
