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 *S*_{i} can be used in the definition of the main set. Furthermore, each *S*_{i} 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

- disjunction
- 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.

- addition

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 };