The Armoise language is used to describe sets of numerical vectors. The syntax allows high-level notations that permits succinct descriptions. The next section presents main syntactic rules the language; then several examples are given.
Armoise at a glance
An Armoise file is a sequence of sets of vectors. Each set description is terminated with a semi-colon (;).
Set 1 ; Set 2 ; ... Set n ;
A set can be described in several ways:
- it can be a predefined set or a set of constants;
- it can be defined with a formula specifying a relation over a set of variables;
- or it can be defined using operations on existing sets.
Since some sets can be quite complex (especially those generated by a tool like a model-checker), Armoise allows to declare local sets. A context is associated with each set and the user can add local definitions to this context. Local definitions are placed between the let and in keywords:
let
S1 := Definition of S1;
S2 := Definition of S2;
...
Sn := Definition of Sn;
in
Definition of the main set;
Each Si can be used in the definition of the main set. Furthermore, each Si has its own context.
Basic sets
Pre-defined set the following:
- nat is the set of natural number (i.e. positive integers)
- int is the set of integers
- posi is the set of positive or null real numbers
- real is the set of real numbers
A set can also be defined by an enumeration of constants:
- { 3, 14, 15 }, { 1/2, 12 }, { (1,2), (3,2/3) }, …
Direct values are shortcuts for singletons:
- 4 is a shortcut for { 4 }
- (1,2) is a shortcut for { (1, 2) }
Ranges are defined as follows:
- [ min ... max ] defines the range of real number between min and max (included); here the ellipsis (...) is actually a lexeme of the language.
- [ min , max ] defines the range of integral numbers between min and max (included).
Formulas
A set described using a formula is simply written { v in Dom | F }; where
- v is a vector of variables: a, (x, y, z) or (a, b, (c, d))
- Dom defines the domain of v. The type of variables appearing in v is inferred from Dom. For instance, if Dom is (nat, real, (real, nat)) then:
- a in Dom means that a is a vector with three components and the third one is itself a couple:
- (x, y, z) in Dom means that x is a positive integer, y is real number and z is a couple whose first component is a natural number and the second one is a real.
- (a, b, (c, d)) in Dom means that a and d are natural numbers and b and c are reals.
- F is a first-order formula that describes the relation between variables listed in v. If a variable is a vector its components can be referenced using the classical square-bracket notation ([]); the first component has the index 0 and the last one the width of the variable minus one.
The formula F is built using:
- Boolean constants: true and false
- Boolean operations:
- disjunction F1 | F2, F1 or F2
- conjunction F1 & F2, F1 and F2
- equivalence F1 <=> F2
- implication F1 => F2
- negation ! F, not F
- Comparison of terms: T1 < T2, T1 <= T2, T1 > T2, T1 >= T2, T1 = T2 and T1 != T2
- Quantifications:
- exists x1 , ..., xn ( ( x1 , ..., xn ) in Dom and G )
- forall x1 , ..., xn ( ( x1 , ..., xn ) in Dom and G ) The type of quantified variables x~i~ is inferred from the set Dom.
Terms are built using:
- Positive integer constants: 3, 14, 15, …
- Vectors of terms: ( t1 , t2 , ..., tn )
- Elements of a vector: v [ i1 ]...[ ik ] where i~j~ are integer constant.
- Arithmetic operators:
- addition t1 + t2. The domain of the term is the coarsest of its operands.
- subtraction t1 - t2. The domain of the term is the coarsest of its operands.
- multiplication t1 * t2. The domain of the term is the coarsest of its operands.
- division t1 / t2. The domain of this term is the one of t1.
- modulo t1 % t2. The domain of this term is the one of t1.
- opposite - t. The domain of this term is the one of t extended to negative numbers.
One should note that arithmetic operators can be applied to vectors. For instance:
- 2 * ( (1,2 * t ) + ( x , y ) ) is the vector (2 * x + 2, 2 * y + 4 * t)
Operations on sets
Sets can be composed using several operations. These operations are essentially extensions of arithmetic or Boolean connectives to sets of vectors.
Boolean operations:
- Union S1 || S2;
- Intersection S1 && S2;
- Difference S1 \ S2;
- Symmetric difference S1 ^ S2 (a shortcut for ( S1 \ S2 ) || ( S2 \ S1 ));
- Complement into real numbers ! S (a shortcut for real \ S).
Numerical operations extended to sets:
- S1 op S2 is semantically equivalent to { x | exist x1 , x2 (( x1 , x2 ) in ( S1 , S2 ) and x = x1 op x2 ) } where op belong to { +, -, *, /, % }.
Of course the type of operands, S1 and S2, must have a sense with the operation op. For instance if S1 is a set of vectors then S1 * S2 have a sense only if S2 is a set of scalar values.
Cartesian product:
- ( S1 , ..., Sn ) is the Cartesian product of sets defined by S~i~ s for i = 1 … n.
Examples
In this section we give small examples of sets specified with the Armoise language.
Linear system with large coefficients
This example defines a set of integer vectors of size 4. The set is defined by 3 linear inequalities. Even if such set is easily handled using binary automata, the presence of large coefficients yields to the construction of a quiet large automaton with 147378 states.
{ x in (nat,nat,nat,nat) | 31 * x[0] - 13 * x[1] >= 0 and
45 * x[0] - 4 * x[1] - 11 * x[2] >= 0 and
27 * x[1] - 11 * x[3] >= 0 };''
Despite the size of the automaton, the Armoise formula synthesized by distiller is quiet small and reveals that there is no redundancy between the three linear constraints.
let
SynForm :=
let
G := int * (1, 0, 0, 0) + int * (0, 1, 0, 0) + int * (0, 0, 1, 0) +
int * (0, 0, 0, 1);
P0 := G;
V := (int, int, int, int);
H2_leq := { (x_0, x_1, x_2, x_3) in (nat, nat, nat, nat) | -45 * x_0 + 4 * x_1 + 11 * x_2 <= 0 };
VH2 := H2_leq && V;
H1_leq := { (x_0, x_1, x_2, x_3) in (nat, nat, nat, nat) | -27 * x_1 + 11 * x_3 <= 0 };
VH1 := H1_leq && V;
H0_leq := { (x_0, x_1, x_2, x_3) in (nat, nat, nat, nat) | -31 * x_0 + 13 * x_1 <= 0 };
VH0 := H0_leq && V;
in
(P0 || VH2 || VH1 || VH0) && VH2 && VH1 && VH0;
in
{ (x_0, x_1, x_2, x_3) | (x_0, x_1, x_2, x_3) in (nat, nat, nat, nat) && SynForm };
A linear inequality with a large number of variables
This example is a simple inequality but with 37 integer variables.
{ x in
(nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat,
nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat,
nat, nat, nat, nat, nat) |
4*x[0] -2*x[ 1]+1*x[ 2]+1*x[ 3]-3*x[ 4]-2*x[5] +1*x[ 6]-4*x[ 7]-3*x[ 8]+1*x[ 9]
+1*x[10]-3*x[11]+2*x[12]+3*x[13]-1*x[14]+1*x[15]+3*x[16]-2*x[17]-1*x[18]+4*x[19]
-3*x[20]-2*x[21]+1*x[22]+4*x[23]-2*x[24]+1*x[25]+1*x[26]-3*x[27]+2*x[28]+1*x[29]
-4*x[30]-3*x[31]+1*x[32]-1*x[33]-3*x[34]+2*x[35]+1*x[36] < 4 };
The automaton computed with PresTAF has 4320 states and the formula synthesizer returns a similar formula:
let
SynForm :=
let
rho_w := (0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0,
0, 0, 0, 0, 0, 0, 0, 0, 0, 1, 0);
V := (int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int,
int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int, int);
H0_leq := { (x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_17,
x_18, x_19, x_20, x_21, x_22, x_23, x_24, x_25, x_26, x_27, x_28, x_29, x_30, x_31, x_32, x_33,
x_34, x_35, x_36) in (nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat,
nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat,
nat, nat, nat, nat) |
4 * x_0 - 2 * x_1 + x_2 + x_3 - 3 * x_4 - 2 * x_5 + x_6 - 4 * x_7 - 3 * x_8 + x_9 + x_10 -
3 * x_11 + 2 * x_12 + 3 * x_13 - x_14 + x_15 + 3 * x_16 - 2 * x_17 - x_18 + 4 * x_19 - 3 * x_20 -
2 * x_21 + x_22 + 4 * x_23 - 2 * x_24 + x_25 + x_26 - 3 * x_27 +
2 * x_28 + x_29 - 4 * x_30 - 3 * x_31 + x_32 - x_33 - 3 * x_34 + 2 * x_35 + x_36 <= 3 };
VH0 := H0_leq && (rho_w + V);
in
VH0;
in
{ (x_0, x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11, x_12, x_13, x_14, x_15, x_16, x_17,
x_18, x_19, x_20, x_21, x_22, x_23, x_24, x_25, x_26, x_27, x_28, x_29, x_30, x_31, x_32, x_33, x_34,
x_35, x_36)
in
(nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat,
nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat, nat,
nat, nat) | SynForm };
Specifications with explicit modulo constraints
Here the example is a Cartesian product of four modulo constraints: multiples of 11, multiples of 7, multiples of 5 and multiples of 3.
(11 * nat, 7 * nat, 5 * nat , 3 * nat);
The automaton computed with the PresTAF plugin has 4620 states and we extract from it the following formula:
let
SynForm :=
let
G := int * (11, 0, 0, 0) + int * (0, 7, 0, 0) + int * (0, 0, 5, 0) + int * (0, 0, 0, 3);
P0 := G;
in
P0;
in
{ (x0, x1, x2, x3) in (nat, nat, nat, nat) | SynForm };
Redundancy elimination
In this example some linear constraints have been deliberately duplicated in the formula.
{ (x0,x1,x2,x3,x4) in (nat,nat,nat,nat,nat) |
( 7*x0 - 4*x1 - 1*x2 + 9*x3 + 10*x4 < 0 and
- 9*x0 + 5*x1 + 2*x2 - 10*x3 + 7*x4 < 0 and
7*x0 - 4*x1 - 1*x2 + 9*x3 + 6*x4 < 0 and
- 9*x0 + 5*x1 - 2*x2 - 11*x3 + 7*x4 < 0 and
-10*x0 - 7*x1 + 3*x2 + x3 - 8*x4 < 0 )
or
(- 9*x0 + 5*x1 - 2*x2 - 11*x3 + 7*x4 < 0 and
8*x0 - 4*x1 + x2 + 9*x3 - 6*x4 < 0 and
9*x0 + 6*x1 - 2*x2 + 11*x3 + 7*x4 < 0 and
-10*x0 + 7*x1 + 4*x2 - x3 + 9*x4 < 0) };
Due to the normalization process induced by the minimization of automata in PresTAF, redundant constraints are eliminated in the formula generated by distiller, in fact only two constraints are actually relevant in this formula:
let
SynForm :=
let
G := int * (1, 0, 0, 0, 0) + int * (0, 1, 0, 0, 0) + int * (0, 0, 1, 0, 0) + int * (0, 0, 0, 1, 0) +
int * (0, 0, 0, 0, 1);
rho_w := (16, 28, 1, 0, 0);
P0 := rho_w + G;
V := (int, int, int, int, int);
H1_geq := { (x0, x1, x2, x3, x4) in (nat, nat, nat, nat, nat) | 7 * x0 - 4 * x1 - x2 + 9 * x3 + 10 * x4 >= 0 };
VH1 := H1_geq && (rho_w + V);
H0_geq := { (x0, x1, x2, x3, x4) in (nat, nat, nat, nat, nat) | -9 * x0 + 5 * x1 + 2 * x2 - 10 * x3 + 7 * x4 >= 0 };
VH0 := H0_geq && (rho_w + V);
in
(P0 \ VH0 \ VH1);
in
{ (x0, x1, x2, x3, x4) in (nat, nat, nat, nat, nat) | SynForm };