Usage

The command line program for Axelerator allows the use of different precision and interval options to be applied to a given file or list of files during processing. If multiple numeric formats are selected, files will be processed for each available.

There is a header line with special parameters to set the conditions of the problem. The following parameters can be set:

-ld
Long double arithmetic. Uses standard C++ long doubles for all operations (precision is machine dependent as per c++ specifications). This is the fastest performance. Results are unsound.

-ldi
Long double intervals. Soundness is achieved through the use of interval arithmetic at the cost of around 4x slower speed.

-mp #
Multiple precision arithmetic. # identifies the number of bits in the mantissa. If not given, the system will default to 256-bit mantissas.

-mpi #
Multiple precision intervals. Same as mp but soundness is achieved through the use of interval arithmetic at the cost of around 4x slower speed.

-ii
Ignore intervals. This switch instructs the software to output results as central values without their interval ranges.

-u
Process unsound results. When this option is selected, unsound results are processed and tagged in the result as 'not enough precision'. Otherwise the software will throw an error.

-norm
results are given using normalized template directions.

-vert
Results are given as polyhedral vertices as opposed to inequalities.

-inc
Use incremental search. Ordering can be one of the following:

cosine
minimum distance between vectors. Normally gives best results.

min
order vectors by minimum value left to right.

max
order vectors by maximum value left to right.

-params ["params"]
Specifies the properties of the model as a comma separated param=value list (eg "p=2,q=1"). The model parameters may be specified as a header in legacy files and is therefore not required for these. The following parameters can be set:

p
Dimension of the state space. This parameter is always required.

q
Dimension of the parametric inputs. If not present, the problem is assumed to have no inputs. Parametric inputs are not deterministic but assumed to have the same value throughout the progression.

v
Dimension of the control inputs. This parameter will override q if present. Control inputs can take any non-deterministic value at each iteration. Overapproximations of control inputs are in general less precise. If a colon is used (eg v=1:1), the input values are calculated separately. This results in a coarser, faster over-approximation

s
Number of steps (if missing, the problem is assumed unbounded)

l
Logahedral order for the abstract matrix directions. The number of faces of the abstract matrix will be 2^l*p². The higher the order the more precise the abstraction (also the slower the performance) If not present, the default value is 2.

t
Logahedral order for the template directions of the reach tube. The number of faces of the reach tube will be approximately 4*t*p² If not present, the default value is 0 which corresponds to a hypercube.

-sguard [poly]
Specifies a safety invariant as a polyhedral set. When specified, the reach tube is calculated along the directions of sguard. Additionally, the solution will be automatically refined to remove over-approximations that do not meet the specification. The poly argument will have the following format: "c₁₁x₁ , c₁₂x₂ , ... , c_1px_p < d₁; c₂₁x₁ , c₂₂x₂ , ... , c_2px_p < d₂; ...; c_m1x₁ , c_m2x₂ , ... , c_mpx_p < d_m", where 0 coefficients can be omitted (eg "x10<4.1;3x1 , 2x3 , -5x10 < 3.2").

'filename'
Filename to include in the processing stage. All files included will be processed according to their data and program options. Results will be placed in files with extensions corresponding to the numeric options given (i.e. '.ld','.mp#','.ldi','.mpi#'). Multiple files will be processed sequentially but independently of each other.

-spaceex 'filename'
This option will parse the dynamics from a pair of files (one xml file and one cfg file) in spaceEx Format. The parser is currently limited and parameters such as the problem dimensions must be set using the -params options.

back