486
C. E. Budde
3 Modelling formalism and input languages
IOSA. FIG models are Input/Output Stochastic Automata with urgency [11].
In iosa, continuous variables called clocks sample random values from arbitrary
distributions (pdfs). As time evolves, all clocks count down at the same rate.
The first to reach zero can trigger events and synchronise with other modules,
broadcasting an output action that synchronises with homonymous input actions
(iosa are input-enabled). Actions can be urgent, where urgent outputs have
module M1
fc,rc
: clock;
inf,brk : [0..2] init 0;
[fl!] brk==0 @ fc -> (inf’=1)
& (brk’=1);
[r??] brk==1 ->(brk’=2) & (rc’=γ);
[up!] brk==2 @ rc -> (inf’=2)
& (brk’=0)
& (fc’=μ);
[f!!] inf==1 -> (inf’=0);
[u!!] inf==2 -> (inf’=0);
endmodule
Code 1: iosa module in FIG 1.2
maximal progress. iosa can thus be nondeterministic: to allow simulation, [23] gives conditions to ensure determinism modulo weak bisimulation. iosa variables are clocks, integers,
or Booleans. Constants can also be floats and
have global scope (variables are module-local).
FIG offers array variables and can get e.g. “arandom/the-smallest value.” Code 1 shows the
guarded command language of FIG models. Decorators ?/! tell an action is input/output, e.g.
fl!. Double decorators (r??) are for urgency. Non-urgent outputs can be sent only
on clock expiration ([fl!]· · · @ fc ->). A clock can sample random values (fc’=μ).
JANI. Besides its native input syntax, FIG 1.2 reads models written in the jani
exchange format [7]. Model types supported are ctmc and a subset of sta that
matches iosa, e.g. with a single pdf per clock and broadcast synchronisation.
FIG also translates iosa to jani as sta, to share models with tools such as the
Modest Toolset [16] and Storm [13]. This is used in Sec. 4 for comparisons.
Properties. FIG estimates the probability with which input properties
P( q2>0 U q2==8 )
S( q2>=8 )
S[9:999]( q2>=8 )
endproperties
Code 2: Property
queries in FIG
models satisfy temporal logic formulæ. A formula is specified
as a (transient or steady-state) property query in the model
file. Transient properties in FIG correspond to the pctl-like
query P=? in prism [19]: e.g. the first property in Code 2
asks the probability of assigning value 8 to variable q2 before
it takes a value 0. Steady-state properties in FIG correspond to the unbounded
csl-like query S=? in prism: e.g. S(q2>=8). For steady-state estimations FIG
implements batch means [9]. The initial (discarded) transient simulation time,
and the batch time, can be heuristically computed by the tool. These values can
also be given by the user—in Code 2, the last property specifies 9 and 999 resp.
4 FIG 1.2 showcase
The Finite Improbability Generator is written in C++14 and is available at https:
//git.snt.utwente.nl/buddece/fig under the gnu gplv3. FIG is built in modules
across three categories: simulation engines, importance functions, and thresholds
builders. Engines are nosplit, restart, and sfe, which resp. run cmc, restart
(rst [31]), and Fixed Effort (fe [14]) simulations. The latter two are isplit
algorithms: fe was described in Sec. 2, and works for transient properties; rst
also works for steady-state analysis (steady-state via fe requires regeneration
C. E. Budde
3 Modelling formalism and input languages
IOSA. FIG models are Input/Output Stochastic Automata with urgency [11].
In iosa, continuous variables called clocks sample random values from arbitrary
distributions (pdfs). As time evolves, all clocks count down at the same rate.
The first to reach zero can trigger events and synchronise with other modules,
broadcasting an output action that synchronises with homonymous input actions
(iosa are input-enabled). Actions can be urgent, where urgent outputs have
module M1
fc,rc
: clock;
inf,brk : [0..2] init 0;
[fl!] brk==0 @ fc -> (inf’=1)
& (brk’=1);
[r??] brk==1 ->(brk’=2) & (rc’=γ);
[up!] brk==2 @ rc -> (inf’=2)
& (brk’=0)
& (fc’=μ);
[f!!] inf==1 -> (inf’=0);
[u!!] inf==2 -> (inf’=0);
endmodule
Code 1: iosa module in FIG 1.2
maximal progress. iosa can thus be nondeterministic: to allow simulation, [23] gives conditions to ensure determinism modulo weak bisimulation. iosa variables are clocks, integers,
or Booleans. Constants can also be floats and
have global scope (variables are module-local).
FIG offers array variables and can get e.g. “arandom/the-smallest value.” Code 1 shows the
guarded command language of FIG models. Decorators ?/! tell an action is input/output, e.g.
fl!. Double decorators (r??) are for urgency. Non-urgent outputs can be sent only
on clock expiration ([fl!]· · · @ fc ->). A clock can sample random values (fc’=μ).
JANI. Besides its native input syntax, FIG 1.2 reads models written in the jani
exchange format [7]. Model types supported are ctmc and a subset of sta that
matches iosa, e.g. with a single pdf per clock and broadcast synchronisation.
FIG also translates iosa to jani as sta, to share models with tools such as the
Modest Toolset [16] and Storm [13]. This is used in Sec. 4 for comparisons.
Properties. FIG estimates the probability with which input properties
P( q2>0 U q2==8 )
S( q2>=8 )
S[9:999]( q2>=8 )
endproperties
Code 2: Property
queries in FIG
models satisfy temporal logic formulæ. A formula is specified
as a (transient or steady-state) property query in the model
file. Transient properties in FIG correspond to the pctl-like
query P=? in prism [19]: e.g. the first property in Code 2
asks the probability of assigning value 8 to variable q2 before
it takes a value 0. Steady-state properties in FIG correspond to the unbounded
csl-like query S=? in prism: e.g. S(q2>=8). For steady-state estimations FIG
implements batch means [9]. The initial (discarded) transient simulation time,
and the batch time, can be heuristically computed by the tool. These values can
also be given by the user—in Code 2, the last property specifies 9 and 999 resp.
4 FIG 1.2 showcase
The Finite Improbability Generator is written in C++14 and is available at https:
//git.snt.utwente.nl/buddece/fig under the gnu gplv3. FIG is built in modules
across three categories: simulation engines, importance functions, and thresholds
builders. Engines are nosplit, restart, and sfe, which resp. run cmc, restart
(rst [31]), and Fixed Effort (fe [14]) simulations. The latter two are isplit
algorithms: fe was described in Sec. 2, and works for transient properties; rst
also works for steady-state analysis (steady-state via fe requires regeneration