Usage

Mercury binary is a command-line program. A normal execution is performed by giving the optional flags followed by a valid input file. As input, it accepts only textual Petri Net models written using the .net format (the same that is used by Tina/LAAS-CNRS). The exploration of a system will normally generate a textual output. A second group of options can be used to define some initial parameters of the algorithm. They are useful when the user can provide an approximate value for the size of the state space and/or a formula to be verified.

You will find below some usage examples of model checking using Mercury.

Common modes:

Exhaustive Reachability Analysis:

Command:   mercury -v -th 16 -Hts 22 -sc 1 example.net
Explanation: Mercury running with 16 threads (-th 16), initial global hash table set to 4 million  states (-Hts 22) and with Huffman compression enabled (-sc 1). Mercury is able to resize the local hash tables automatically If the initial hash table size is not enough to store all states.

Local Sub-CTL Model Checking:

Command:   mercury -v -th 16 -Hts 22 -sc 1 -f “A <> dead” example.net
Explanation: Exhaustive CTL model checking of the formula “A <> dead”.
Command:   mercury -v -th 16 -bls 22 -aprox 0 -f “A [] – dead” example.net
Explanation: Probabilistic reachability analysis of the formula “A [] – dead”.

Probabilistic Reachability Analysis:

Command:   mercury -v -th 16 -bls 22 -sc 1 -aprox 0 example.net
Explanation: Mercury running with 16 threads (-th 16), initial Bloom Table (-aprox 0) set to hold 2 millions states symbolically (-bls 22), an overflow table set for 100000 states and Huffman compression enabled (-sc 1). The flag -aprox 0 instruments Mercury to perform a probabilistic experiment with the Bloom Table data structure.

NEW: Disc Based State Space Exploration:

Command:  mercury -disc -th 4 -bls 22 example.net
Explanation: Disc based exploration (-disc) set for 2 millions states (-bls 22).  It uses in average 4-8 times less memory but takes twice of the time of a normal RAM based memory algorithm.

Help option: -h

Ex: mercury -h

Textual options:

Verbose: -v
Statistics: -stats
Ex: mercury -v -stats example.net

State marking options: -b n

-b 0    marking is a vector of bits  (max 1 token)
-b 1    marking is a vector of chars (max 125 tokens) (default)
-b 2    marking is a linked list of integers (temporarily disabled)
Ex: mercury -b 1 example.net

Compression options: -sc n

-sc 0 no compression (default)
-sc 1 :Huffman
-sc 2 :RLE
Ex: mercury -sc 1 example.net

Parallel options:

Number of threads: -th n
Ex: mercury -th 16 example.net

Localization Table Configurations:

Common usage: mercury -Hts size example.net

Global Hash Table configuration: -Hts n (default n is 22)
Ex: mercury -Hts 24 example.net

Model Checking: -f “non-nested CTL formula”

Ex: mercury -f “A <> dead” example.net
Obs: See Ph.D. Thesis (Chapter 4, section 2) for a complete list of supported formulas.

Probabilistic Bloom Table: -bls bloom_table_size -aprox 0

Ex: mercury -bls 24 -aprox 0 example.net

Disc Based State Space Exploration:

EX:  mercury -disc -disc_factor 4 -th 4 -bls 22 example.net
Options:
  • -disc : enables the disc based exploration mode.
  • -disc_async: enables the disc based exploration mode but solves the collisions asynchronously. It is helpful when there is not enough space available at the local storage (hard disc).
  • -disc_factor N : Memory factor supplied by the user, default is 2. Note that the runtime is sensible to this parameter.