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:

stopconf <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); 
stoptime <digits>[<s/m/h/d>]
to simulate for the specified amount of (wallclock) 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 stopconf .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 multioption. This means several stopping criteria can be specified, and independent estimations are run to meet each of them. For instance
~$ fig model.sa amono stoptime 5m stopconf .9 .4
launches, for each property query specified in model.sa: first an estimation lasting 5 minutes of (walltime) 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>/fromjani/tojani} [c] [f] [rngseed <random/<digit>+>] [r <mt64/pcg32/pcg64>] [s <commaseparatedsplitvalues>] [timeout <<digit>+[<s/m/h/d>]>] [postprocess <shift/exp> <value>]... [stoptime <<digit>+[<s/m/h/d>]>] ... [stopconf <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 nosplit simulation engine.
adhoc <adhoc_fun>

(XOR required) Use an ad hoc importance function, i.e. assign importance to the states using an userprovided 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.
fromjani

(XOR required) Don't estimate; create IOSA model file from JANIspec model file.
tojani

(XOR required) Don't estimate; create JANIspec 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 IOSAcompliant. Depending on the user command, this may force estimation of the properties values, or translation to the JANI Specification format.
rngseed <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 <commaseparatedsplitvalues>, splitting <commaseparatedsplitvalues>

Define splitting values to try out with RESTARTlike simulation engines, specified as a commaseparated list of integral values greater than '1'
timeout <<digit>+[<s/m/h/d>]>

Running time limit: if set, any simulation will be softinterrupted 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.
[postprocess <shift/exp> <value>]...

Specify a postprocessing to apply to the importance computed, e.g. "
postprocess exp 2.0
" to exponentiate all values using '2' as the base. Only applicable toamono
andacomp
importance functions. stoptime <<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 multiargument, meaning you can define as many of them as you wish, e.g. "
stoptime 30 stoptime 10m
" [stopconf <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 multiargument, meaning you can define as many of them as you wish, e.g. "
stopconf 0.8 0.4 stopconf 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, versionfull

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 stoptime 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 stopconf 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 stopconf 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 stopconf .8 .4 stoptime 1h stopconf .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 wallclock timeout is reached in each case.