A Analysis options
Several options can be set:

communication and migration analysis:

there are several level of accuracy for describing markers:

uniform: markers are just abstracted away,
 low: the first component of each label pairs are abstracted away,
 high: markers are fully described;
 grammars shape can be simplified:

none: no simplifications are performed,
 collision: grammar are simplified by collapsing similar states, without losing any information;
 Content analysis:

several numerical domains are available:

disabled: content analysis is disabled,
 intervals: we use the nonrelational domain of intervals[2],
 affine equality and intervals: we use a product between affine equality domain[7] and the intervals[2],
 octagons: we use the octagonal domain[8],
 abstract multiset: we use a disjunctive completion based domain, named abstract multiset.
 the number of numerical variable can be set:

one: only one variable,
 linear: as many variables as program points,
 twice: twice variables as program points,
 quadratic: the number of variables is quadratic with respect with the number of program points.
 Global occurrence analysis:

several numerical domains are available:

disabled: content analysis is disabled,
 intervals: we use the nonrelational domain of intervals[2],
 affine equality and intervals: we use a product between affine equality domain[7] and the intervals[2],
 octagons: we use the octagonal domain[8],
 abstract multiset: we use a dijunctive completion based domain, named abstract multiset.
 the number of numerical variable can be set:

one: only one variable,
 linear: as many variables as program points,
 twice: twice variables as program points,
 quadratic: the number of variables is quadratic with respect with the number of program points.