|
| | | NBAC Invocation and options |
Type nbacg -help, and get:
Usage: nbac <list of options> <filename>
List of options and suboptions:
-----------------------------------------------------------------
-gc "..." : Memory Options
Suboptions are
-space <n> : sets Gc.space_overhead, default is 42
-max <n> : sets Gc.max_overhead, default is max_int
-cudd <n> : sets the BDDs ratio used/max to 1/2^n, default is n=20
-polka <n> : sets the polyhedra ratio used/max to size/<n>Meg, default is 256Meg
-----------------------------------------------------------------
-cudd "..." : CUDD Options
Suboptions are
-maxmem <n> : sets the max. number of MB usable by CUDD
-siftswap <n> : set the CUDD parameter SiftMaxSwap (default max_int)
-----------------------------------------------------------------
-num "..." : Abstract numeric domain Options
Suboptions are
(+/-)strict : enable/disable strict inequalities (default: enabled)
-lib <str> : numerical abstract domain
"polka": Polka (convex polyhedra) (default)
"oct": Oct (octagons)
-----------------------------------------------------------------
-polka "..." : Polka numeric domain Options
Suboptions are
(+/-)widening_affine : affine/linear mode for widening (default: affine)
-----------------------------------------------------------------
-bdd "..." : BDDs Options
Suboptions are
-group <n> : separating or mixing
Boolean variables and non-Boolean constraints ?
0: mixing (default)
1: separating (useful if many Boolean vars and few constraints)
(+/-)parallel : group parallel constraints ? (default: no)
(+/-)reorder : enable/disable reordering after parsing (default: enable)
(+/-)reorder2 : enable/disable reordering after Boolean analysis (default: enable)
(+/-)autoreorder
: enable/disable autoreordering (default: disable)
-----------------------------------------------------------------
-widening "..." : Widening Options
Suboptions are
-depth <n> : depth of recursive iterations (default 2, maybe only more)
(+/-)param : Parametrized by constraint ? (default no)
(+/-)first : enable/disable heuristic `widening first' (default: enable)
-start <n> : first widening step (default 1)
-freq <n> : widening every <n> steps (default 1)
-descend <n> : number of narrowing steps (default 1)
-----------------------------------------------------------------
-postpre "..." : Postpre Options
Suboptions are
-drelation : maximum depth of relational computations (higher means more relational) (default: 0)
-dassert <n> : maximal depth of assert operators (default infinity)
-dite <n> : maximal depth of ite operators (default infinity)
-dselect <n> : function selection parameter (default 1)
-dtimed <n> : maximal depth of ite operators in timed transitions (default infinity)
-gencof (0|1) : generalized cofactors, 0 means classical, 1 top-down
-----------------------------------------------------------------
-dot "<filename> .." : DOT Output
Suboptions are
(+/-)trans : display the transition functions ? (default: yes)
(+/-)cont : display the derivatives constraints ? (default: yes)
(+/-)all : output all control structures, or only the one (default: final)
-margin <n> : margin used for pretty-printing BDDs/MTBDDs
-bdd <n> : maximum size of BDDs/MTBDDs to be displayed
-----------------------------------------------------------------
-partition "..." : Partition Options
Suboptions are
(+/-)source : allow/forbid refinement of source locations (default: forbid)
(+/-)sink : allow/forbid refinement of sink locations (default: forbid)
(+/-)init : allow/forbid refinement of initial locations (default: forbid)
(+/-)final : allow/forbid refinement of final locations (default: forbid)
-ratio <n> : minimum size growth between two analysis (default 50 -maxloc <n> : maximum number of locations (default infinity)
-maxtime <n> : maximum time in secs (default infinity))
-heuristic <n>
: refinement heuristic (default 0).
0: CFC ("Composante Fortement Connexes")
1: SCFC ("Sous-Composante Fortement Connexes")
2: MAXCUT
-----------------------------------------------------------------
-print "..." : Printing Options
Suboptions are
(+/-)d : database
(+/-)p : partition
(+/-)a : analysis
(+/-)t : analysis step
(+/-)s : analysis state
(+/-)pp : postpre
(+/-)h : refinement heuristics
(+/-)r : refinement
-auto <n> : maximum size of partition to be print
-bdd <n> : maximum size of BDDs/MTBDDs to be print
-----------------------------------------------------------------
-o "<filename> .." : NBAC Output
Suboptions are
(+/-)red : simplify formulae in the output ? (default: yes)
(+/-)bdd : use BDD or DNF form for formulae in the output ? (default: BDD)
(+/-)prec
: use precise mode for guards in the output ? (default: false)
(+/-)all : output at each step (in the same file ? (default: false)
-----------------------------------------------------------------
-laure "<filename> .."
: Laure Gonnord's output
Suboptions are
(+/-)all : output at each step (in numbered files) ? (default: false)
(+/-)eliminput
: remove input ? (default: false)
-----------------------------------------------------------------
-analysis <n> : type of analysis
0: reachability (forward) analysis
1: coreachability (backward) analysis
2: slice (both) analysis (default)
(+/-)boolonly : Performs only discrete analysis (default: no)
(+/-)success : stops the analysis as soon as the property is proved ?
(default: yes)
(+/-)valid : if property is proved, stops in a valid state
for the automaton (default: no)
-rc <filename> : parse option file
(+/-)printrc : Print used options in option file format
-help : Display this list of options
--help : Display this list of options
If the requested analysis is reachability, the tool compute an overapproximation of the states reachable from the initial condition. If it is coreachability, it will compute an overapproximation of the states coreachable from the final condition (or the negation from the invariant condition). If it is slice, it will alternate both analysis and keep only states which are both reachable and coreachable. It is the more efficient analysis if the ultimate goal is to verify a property.
If the -o option is given, and if the resulting state-space after analysis is not empty, then the result of the analysis is outputed to the file.
-analysis <n> : type of analysis 0: reachability (forward) analysis 1: coreachability (backward) analysis 2: slice (both) analysis (default) (+/-)boolonly : Performs only discrete analysis (default: no) (+/-)success : stops the analysis as soon as the property is proved ? (default: yes) (+/-)valid : if property is proved, stops in a valid state for the automaton (default: no) -rc <filename> : parse option file (+/-)printrc : Print used options in option file format
These options are related to partition refinement.
-partition "..." : Partition Options
Suboptions are
(+/-)source : allow/forbid refinement of source locations (default: forbid)
(+/-)sink : allow/forbid refinement of sink locations (default: forbid)
(+/-)init : allow/forbid refinement of initial locations (default: forbid)
(+/-)final : allow/forbid refinement of final locations (default: forbid)
-ratio <n> : minimum size growth between two analysis (default 50 -maxloc <n> : maximum number of locations (default infinity)
-maxtime <n> : maximum time in secs (default infinity))
-heuristic <n>
: refinement heuristic (default 0).
0: CFC ("Composante Fortement Connexes")
1: SCFC ("Sous-Composante Fortement Connexes")
2: MAXCUT
-dot "<filename> .." : DOT Output
Suboptions are
(+/-)trans : display the transition functions ? (default: yes)
(+/-)cont : display the derivatives constraints ? (default: yes)
(+/-)all : output all control structures, or only the one (default: final)
-margin <n> : margin used for pretty-printing BDDs/MTBDDs
-bdd <n> : maximum size of BDDs/MTBDDs to be displayed
These options are related to the method used for computing (approximated) post- and pre- conditions. They allow to tune the tradeoff between efficiency and precision. Their meaning is explained in [8].
For medium/big examples, use
-postpre "-dassert 4 -dite 4 -dtimed 3"4 can be replaced by 3, 5, .... The worst-case complexity is exponential in this number.
You can also use -postpre "-dselect 2" to improve the precision.
-postpre "..." : Postpre Options
Suboptions are
-drelation : maximum depth of relational computations (higher means more relational) (default: 0)
-dassert <n> : maximal depth of assert operators (default infinity)
-dite <n> : maximal depth of ite operators (default infinity)
-dselect <n> : function selection parameter (default 1)
-dtimed <n> : maximal depth of ite operators in timed transitions (default infinity)
These also influence the precision/efficiency tradeoff.
-widening "..." : Widening Options
Suboptions are
-depth <n> : depth of recursive iterations (default 2, maybe only more)
(+/-)param : Parametrized by constraint ? (default no)
(+/-)first : enable/disable heuristic `widening first' (default: enable)
-start <n> : first widening step (default 1)
-freq <n> : widening every <n> steps (default 1)
-descend <n> : number of narrowing steps (default 1)
-polka "..." : Polka numeric domain Options
Suboptions are
(+/-)widening_affine : affine/linear mode for widening (default: affine)
-bdd "..." : BDDs Options
Suboptions are
-group <n> : separating or mixing
Boolean variables and non-Boolean constraints ?
0: mixing (default)
1: separating (useful if many Boolean vars and few constraints)
(+/-)parallel : group parallel constraints ? (default: no)
(+/-)reorder : enable/disable reordering after parsing (default: enable)
(+/-)reorder2 : enable/disable reordering after Boolean analysis (default: enable)
(+/-)autoreorder
: enable/disable autoreordering (default: disable)
-print "..." : Printing Options
Suboptions are
+d : database
-d :
+p : partition
-p :
+a : analysis
-a :
+t : analysis step
-t :
+s : analysis state
-s :
+pp : postpre
-pp :
+r : refinement
-r :
-auto <n> : maximum size of partition to be print
-bdd <n> : maximum size of BDDs/MTBDDs to be print
-gc "..." : Memory Options
Suboptions are
-space <n> : sets Gc.space_overhead, default is 42
-max <n> : sets Gc.max_overhead, default is max_int
-cudd <n> : sets the BDDs ratio used/max to 1/2^n, default is 2^20
-polka <n> : sets the polyhedra ratio used/max to size/<n>Meg, default is 256Meg
-cudd "..." : CUDD Options
Suboptions are
-maxmem <n> : sets the max. number of MB usable by CUDD
-siftswap <n> : set the CUDD parameter SiftMaxSwap (default max_int)
|
| | | NBAC Invocation and options |