Sapo Input Language - sapotools/sapo GitHub Wiki

Sapo Input Language (SIL) is a language designed to provide an input model for Sapo. Any SIL file is divided in

• Header
• Symbol definitions
• Matrices definition
• Footer

It consists in

problem: reachability | synthesis;

variable_mode: boxes (default) | parallelotopes | polytopes;

parameter_mode: boxes (default) | parallelotopes;

iterations: num;

max_parameter_splits: num;

When parameter synthesis returns an empty set, the result may be due to over-approximation. Since the approximation also directly depends on the size of the parameter set, in order to decrease it, the initial parameter set can be split in subsets and the computation can be repeated for each them. The max_parameter_splits option declares the maximum number of splits that Sapo can perform searching for a non-empty set satisfying the specification.

In this section, we define variables with dynamics, parameters, constants and the specification (if required). Each symbol must be defined before it is used.

If the variable modality is boxes, they are defined with the initial values

var v in [a,b];

Otherwise, just the name is provided. Multiple variables can be defined in the same command.

var v1, v2;

Variable names follow the C++ rule for identifiers.

They follow the syntax of variable definition. If parameter modality is boxes, they require the initial interval.

param p1, p2 in [0.01, 0.02];

Otherwise, no interval must be provided

param p1;

They define a map between identifiers and numerical values. The usual rules hold for constant names, and the corresponding expression must be numeric only.

const c1 = 1.2;
const c2 = 34 * 0.78;

They represent the evolution of variables with resect to time.

dynamic(v1) = v1 + p * (v2 - c + v3);

where

• v1 is a name of an already defined variable
• all symbols occurring in the expression must be already defined
• the expression must be linear with regard to parameters
• the expression must be polynomial with respect to the variables

Each variable must have a corresponding dynamic defined.

If problem is synthesis, a STL specification must be provided.

• An atomic formula is of the form

   ex1 ~ ex2

  where

  • ex1 and ex2 are expression involving numbers, variables and constants
  • ~ is one of <, <=, >, >= or =

• Negation is written

   ! f

• Conjunction is written

   f1 && f2

• Disjunction is written

   f1 || f2

• Until is written

   f1 U[a,b] f2

  This formula holds at time t if there exists a time point t' in [t+a, t+b] such that f2 hlds at time t' and f1 hold in all time points from t to t'.

• Eventually is written

   F[a,b] f

  This means that there exists a point in [t+a, t+b] where f holds.

• Globally is written

   G[a,b] f

  This means that at all time points in '[t+a, t+b]the formulaf` holds

Finally, the specification is provided as

spec: STLformula;

In this section, we provide the definition of the polytopes used to approximate reachable sets and parameters.

If variable modality is boxes, no matrix must be defined. If variable modality is parallelotopes, then we must define the direction matrix. That is, for each direction we write

direction <num_1, ..., num_n> in [a, b];

We have as many elements in a direction as the number of variables. The meaning is

a <= num_1*v_1 + ... + num_n * v_n <= b

We must provide as many directions as the number ov variables, paying attention to defined a bounded set.

If variable modality is polytopes, then we must define a set of directions as described above. This time we can provide a number of directions which is higher than the number of variables. Then, we define the template matrix in which each row represents a parallelotope.

template = {
	{num_1, ..., num_n},
	.
	.
	.
	{num_1, ..., num_n}
}

where each row has as many elements as the number of variables, and each value corresponds to a direction. For example, number 0 is the first direction (in order of definition), 1 is the second and so on. The template matrix can have any number of rows (at least one).

They work similarly to the variables. If parameter modality is boxes, no matrix is required. Otherwise, we must provide the directions for parameter parallelotope.

parameter_direction <num_1, ..., num_m> in [a, b];

where there is a number for each parameter, and the meaning is

a <= num_1 * p_1 + ... + num_n * p_m <= b

We recall that parameter modality cannot be polytopes.

In this section, we can provide some options to tune the behavior of Sapo. All them are optional, so this section can be empty.

We can define

• how we compute the image of a polytope (optional)

  option transformation AFO (default) | OFO; In general, AFO gives more accurate results but OFO is faster.

• whether or not to perform an optional decomposition phase after computing set images.

  option decomposition;

• set a weigth alpha in [0,1] used in decomposition, to define the importance given to polytope volume over maximum side length in the cost function

  option sapo_alpha num;

SIL understands C/C++ like comments, both sigle and multi-line

...
// single line comment
...
/*
multi-line
comment
*/
...