FIG: Tutorial

The most basic invocation of FIG requires three mandatory options: <model>, <termination> and <strategy>. Their syntax and semantics can be briefly described as follows:

  • <model>: The path to the file with the IOSA (or JANI ) model description and property queries.
  • <termination>: The stopping criterion (or criteria). It can be:
    • --stop-conf <value> <value> to simulate until the specified confidence coefficient and relative precision are achieved. Those values must be numbers in the open interval (0, 1);
    • --stop-time <digits>[<s/m/h/d>] to simulate for the specified amount of (wall-clock) time . Options 's', 'm', 'h' and 'd' can be used to denote, respectively, 'seconds',' minutes', 'hours' and 'days'. The default option is 's'.
  • <strategy>: The strategy used to simulate. It must be one of:
    • --flat to perform standard Monte Carlo simulations;
    • --amono to perform RESTART simulations using an automatic monolithic importance function, built using the approach in [Chapter 3, Budde17]
    • --acomp to perform RESTART simulations using an automatic compositional importance function, built using the approach from [Chapter 4, Budde17] and a composition operand (or strategy) given as mandatory parameter (see below);
    • --adhoc to perform RESTART simulations using an ad hoc importance function specified by the user as mandatory parameter (see below).

The order of the options is arbitrary. For instance the line

~$ fig model_and_queries.sa --flat --stop-conf .9 .4

invokes the tool to perform standard Monte Carlo simulations on the IOSA file model_and_queries.sa. For each of the property queries specified within the file, simulations will run until a confidence interval of 90% confidence level and 40% relative precision (i.e. a 20% relative error) is built around the estimated value of the property.

Both <model> and <strategy> are simple options, whereas <termination> is a multi-option. This means several stopping criteria can be specified, and independent estimations are run to meet each of them. For instance

~$ fig model.sa --amono --stop-time 5m --stop-conf .9 .4

launches, for each property query specified in model.sa: first an estimation lasting 5 minutes of (wall-time) execution, for which typical confidence intervals around the estimate are reported; and then an estimation which will run until an interval of 90% confidence level and 40% relative precision is built around the estimate.

Syntax and Semantics of FIG

USAGE:

fig  {--flat/--adhoc <adhoc_fun>/--amono/--acomp <composition_fun>/--from-jani/--to-jani} 
     [-c] [-f] [--rng-seed <random/<digit>+>] 
     [-r <mt64/pcg32/pcg64>] [-s <comma-separated-split-values>] [--timeout <<digit>+[<s/m/h/d>]>]
     [--post-process <shift/exp> <value>]...  
     [--stop-time <<digit>+[<s/m/h/d>]>] ...  
     [--stop-conf <confCo ∈ (0,1)> <relPrec ∈ (0,1)>]...  
     [-t <fix/ams/smc/hyb>] [-e <nosplit/restart>] [-v] [--] [--version] [-h] 
     <modelFile>
     <propertiesFile>

Options surrounded by square braces, i.e. [...], are optional.
Options surrounded by curly braces, i.e. {...}, are always required but at least (or exactly) one of them is needed, depending on whether the separator is '|' or '/' respectively.

Where:

--flat
(XOR required) Use a flat importance function, i.e. consider all states in the model equally important. Information is kept symbolically as an algebraic expression, thus using very little memory. Notice the flat function is only compatible with the no-split simulation engine.
--adhoc <adhoc_fun>
(XOR required) Use an ad hoc importance function, i.e. assign importance to the states using an user-provided algebraic function on them. Information is kept symbolically as an algebraic expression, thus using very little memory.
--amono
(XOR required) Use an automatically computed "monolithic" importance function, i.e. store information for the global, parallely composed model. This stores in memory a vector the size of the global model's concrete state space, which may be huge.
--acomp <composition_fun>
(XOR required) Use an automatically computed "compositional" importance function, i.e. store information separately for each module. This stores in memory one vector per module, and then uses the algebraic expression provided to "compose" the global importance from these.
--from-jani
(XOR required) Don't estimate; create IOSA model file from JANI-spec model file.
--to-jani
(XOR required) Don't estimate; create JANI-spec model file from IOSA model file.
-c, --confluence
Run algorithm to check confluence of committed actions.
-f, --force
Force FIG operation disregarding any warning of the model not being IOSA-compliant. Depending on the user command, this may force estimation of the properties values, or translation to the JANI Specification format.
--rng-seed <random/<digits>>
Specify the (numeric) seed of the RNG; may also specify "random" to use randomized seeding in all simulation runs
-r <mt64/pcg32/pcg64>, --rng <mt64/pcg32/pcg64>
Specify the pseudo Random Number Generator (aka RNG) to use for sampling the time values of clocks.
-s <comma-separated-split-values>, --splitting <comma-separated-split-values>
Define splitting values to try out with RESTART-like simulation engines, specified as a comma-separated list of integral values greater than '1'
--timeout <<digit>+[<s/m/h/d>]>
Running time limit: if set, any simulation will be soft-interrupted after running for this (wall clock) time. If the stopping condition for a simulation is also time based, the lowest of the two values will apply.
[--post-process <shift/exp> <value>]...
Specify a post-processing to apply to the importance computed, e.g. "--post-process exp 2.0" to exponentiate all values using '2' as the base. Only applicable to --amono and --acomp importance functions.
--stop-time <<digit>+[<s/m/h/d>]>(accepted multiple times)
Add a stopping condition for estimations based on a (wall clock) execution time length, e.g. "45m". Can specify seconds (s), minutes (m), hours (h) or days (d). Default is seconds, i.e. 's' is assumed if no suffix is specified. This is a multi-argument, meaning you can define as many of them as you wish, e.g. "--stop-time 30 --stop-time 10m"
[--stop-conf <confCo ∈ (0,1)> <relPrec ∈ (0,1)>]...
Add a stopping condition for estimations based on a confidence criterion, i.e. a "confidence coefficient" and a "precision" (relative to the estimate) to reach. This is a multi-argument, meaning you can define as many of them as you wish, e.g. "--stop-conf 0.8 0.4 --stop-conf 0.95 0.1"
-t <fix/ams/smc/hyb>, --thresholds <fix/ams/smc/hyb>
Technique to use for building the importance thresholds. Default is "hyb".
-e <nosplit/restart>, --engine <nosplit/restart>
Name of the simulation engine to use for estimations. Default is "restart".
-v, --version-full
Displays full version information and exits.
--, --ignore_rest
Ignores the rest of the labeled arguments following this flag.
--version
Displays version information and exits.
-h, --help
Displays usage information and exits.
<modelFile>
(required) Path to the file with the IOSA/JANI model
<propertiesFile>
Path to the file with the properties to estimate

Sample usage:

~$ fig models/tandem.{sa,pp} --amono --stop-time 5m

Use an automatically computed "monolithic" importance function built on the global state space of the model, performing a 5 minutes estimation which will employ the RESTART simulation engine (default) for splitting 2 (default) and the hybrid thresholds building technique, i.e. "hyb" (default)

~$ fig models/tandem.{sa,pp} --flat -e nosplit --stop-conf 0.8 0.4 --timeout 1h

Use a flat importance function to perform a standard Monte Carlo simulation (i.e. no splitting), which will run until either the relative precision achieved for an 80% confidence interval equals 40% of the value estimated for each property, or 1 hour of wall clock time has passed, whichever happens first.

~$ fig models/tandem.{sa,pp} --adhoc "10*q2+q1" -t ams --stop-conf 0.9 0.2

Use the importance function "10*q2+q1" defined ad hoc by the user, with the RESTART simulation engine (default) for splitting 2 (default), employing the Adaptive Multilevel Splitting thresholds building technique, i.e. "ams", estimating until the relative precision achieved for a 90% confidence interval equals 20% of the value estimated for each property.

~$ fig models/tandem.{sa,pp} --acomp "+" -t hyb --stop-conf .8 .4 --stop-time 1h --stop-conf .95 .1 --splitting 2,3,5,9,15 -e restart --timeout 30m

Use an automatically computed "compositional" importance function, built modularly on every module's state space, simulating with the RESTART engine for the splitting values explicitly specified, using the hybrid thresholds building technique, i.e. "hyb", estimating the value of each property for this configuration and for each one of the three stopping conditions, or until the wall-clock timeout is reached in each case.

Powered by Drupal