File Format

The file format follows the nomenclature of the papers
G -> AX + BU

Since A and B are matrices and G,X and U are polyhedral sets (defined as CX < D), they are all represented in matrix format as follows:
For matrices
[ a₁₁ , a₁₂, ... , a_1p
a₂₁ , a₂₂, ... , a_2p
...
a_p1 , a_p2, ... , a_pp ]

For sets
[ c₁₁ , c₁₂ , ... , c_1p < d₁
c₂₁ , c₂₂ , ... , c_2p < d₂
...
c_m1 , c_m2 , ... , c_mp < d_m ]

Note that the < can also be replaced with a > for inequalities that have a minimum instead of a maximum. The software will negate both sides and produce a st will all maximums, thus result files will have no > symbols
c_j1,c_j2, ... ,c_jp > d_j <=> -c_j1,-c_j2, ... ,-c_jp < -d_j
Additionally, when interval arithmetic is selected, result files will be printed using a central value and an error range. Items marked as c_ij+e_ij indicate an interval [c_ij-e_ij c_ij+e_ij]. Note that if there is no error range (e_ij=0) the printed value will be c_ij

There is a header line with special parameters to set the conditions of the problem. 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.

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.

m
Number of bits in the mantissa representation (only valid for mp problems). If not present, the default is either the precision suppliend in the command line or 256 in its absence

e
This header is only present on result files and indicates the eigendecomposition error (used for reference of error sources).

A complete file for a 2 dimensional problem could look like this:
p=2,q=2
[g₁₁ , g₁₂ < h₁
g₂₁ , g₂₂ < h₂ ]
->
[a₁₁ , a₁₂
a₂₁ , a₂₂ ]
[x₁₁ , x₁₂ < y₁
x₂₁ , x₂₂ < y₂
x₃₁ , x₃₂ < y₃ ]
+
[b₁₁ , b₁₂
b₂₁ , b₂₂ ]
[u₁₁ , u₁₂ < v₁
u₂₁ , u₂₂ < v₂
u₃₁ , u₃₂ > v₃ ]

The result file will look like this:
p=2,q=2,s=50,l=2,t=0,e=1.5e-23
[r₁₁ + e₁₁ , r₁₂ + e₁₂ < s₁ + es₁
r₂₁ + e₂₁ , r₂₂ + e₂₂ < s₂ + es₂
r₃₁ + e₃₁ , r₃₂ + e₃₂ < s₃ + es₃
r₄₁ + e₄₁ , r₄₂ + e₄₂ < s₄ + es₄ ]

back