Run either quail script (Linux) or quail.bat (Windows) in a command line console.<\/p>\n
Alternatively it is possible to run directly the JAR package Quail.jar in the directory dist.<\/p>\n quail [options] program.quail<\/p>\n Options:<\/p>\n <\/p>","protected":false},"excerpt":{"rendered":" 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 | -? | … <\/p>\nquail [options] program.quail<\/code><\/p>\nOptions:<\/h3>\n
-c | --clean<\/code>
\nDelete the temporary preprocessed file.<\/p>\n--config=<filename><\/code>
\nAlternative location for the configuration file.<\/p>\n-h | -? | --help<\/code>
\nPrint this help and terminate.<\/p>\n-v <level><\/code>
\nVerbose mode between 0 (minimum) and 4 (maximum).
\nDefault value if not specified is 2.<\/p>\n-th <number><\/code>
\nSets the number of parallel threads QUAIL should use. Default is the number returned by Runtime.getRuntime().availableProcessors(), minimum 1<\/p>\n-p <value><\/code>
\nDefine computation precision as a number of digits. Default value if not specified is 15.<\/p>\n--const:<cname>:=<cvalue><\/code>
\nReplace the value of a constant cname in the model by the value cvalue<\/p>\n--preprocess<\/code>
\nRun only the preprocessor and terminate.<\/p>\n--simulate<\/code>
\nRun the simulator instead of the analyzer. If this option is chosen, the following additional options are available:<\/p>\n-i <iterations><\/code>
\nSets the number of simulations. Default: 50000<\/p>\n-l <threshold><\/code>
\nSets the sufficient probability threshold after which exploration of the probability space can be terminated.
\nDefault: 1 (meaning 100% of the probability space)<\/p>\n-t <time_limit><\/code> Sets the time limit (in milliseconds) for the simulation. A value of 0 means no time limit. Default: 0 (meaning no time limit)<\/p>\n--fullmc<\/code>
\nRuns the QUAIl version 1 algorithm constructing the full Markov chain (slow). If this option is chosen, the following additional options are available:<\/p>\n--no_hiding<\/code>
\nDo not run the hiding algorithm.<\/p>\n-mc [values]<\/code>
\nPrint the Markov chains:<\/p>\n0<\/code> program Markov chain<\/p>\n1<\/code> hiding non observable states<\/p>\n2<\/code> observer’s quotient<\/p>\n3<\/code> secret’s quotient<\/p>\n4<\/code> joint quotient
\ne.g. -mc 0 1 2 3 4<\/code> will print all Markov chains.
\nBy default, if no value is given, print the program Markov chain.
\nThe output format can be any format supported by Graphviz,
\nUse option -Tgif,-Tfig,-Tpdf,-Tps,-Tsvg<\/code> or -Tpng<\/code> for the most common.
\nBy default if no format is provided it prints in dot format.<\/p>\n-o <filename><\/code>
\nFile name for Markov chains. Suffixes are added automatically.<\/p>\n