Sapo Output Formats

The Sapo stand-alone application, sapo, always prints the output as list of objects. These objects vary depending on the performed analysis: if sapo was requested to compute a reachability set, the list contains one single flowpipe; if, otherwise, the synthesis was requested, sapo prints a list of pairs parameter set-flowpipe. This is due to the ability of splitting parameter set into subsets and processing them independently whenever the original parameter domain cannot be refined without reducing it to the empty set. The result of this procedure is a distinct flowpipe for each subset and, as a consequence, the synthesis outcome is a list of pairs. In order to have an uniform output for any kind of input, Sapo presents a list also when plain reachability analysis is performed.

sapo has two kind of output format: the text-based format and the JSON format.

Text-based Output Format

The text-based output format is the standard one.

Lists

Each of the elements in a non-empty output list consists in either a flowpipe alone, when the reachability analysis has been performed, or a pair parameter set-flowpipe, in the case of synthesis.

The elements are separated by a line containing twenty =.

Whenever the list is empty sapo outputs a line with the string empty list.

Parameter sets

Each parameter set section begins with a line exclusively containing the string PARAMETER SET. Then the parameter set is reported as a union of convex polyhedra.

Flowpipes

Flowpipes are introduced by the string FLOWPIPE. They are printed as
unions of convex polyhedra, one per time stamp, separated by output lines exclusively containing twenty -.

Convex Polyhedra

They are represented as linear systems of the kind A x <= b where A is an n x m-matrix of real values and b is a m-dimensional vector.

An example of convex polyhedron representation is reported in the following:

1 0 0 0 <= 5
0 1 0 0 <= -3.4
0 0 1 0 <= 0.01
0 0 0 1 <= 0.4
-1 0 0 0 <= -3
0 -1 0 0 <= 2.1
0 0 -1 0 <= 0
0 0 0 -1 <= 0.3

Unions of Convex Polyhedra

The non-empty unions of convex polyhedra are printed as the convex polyhedra contained in it separated by empty lines.

If the union of convex polyhedra is the empty set, sapo reports a line containing the string empty set.

You can found a full example here.

JSON Output Format

Sapo can also print the output in JSON format by using the command line option -j.

Lists

They are represented as in the JSON standard.

The list elements consist in objects having either the only member flowpipe, in the case of reachability analysis, or the members flowpipe and parameter set for the synthesis.

Parameter sets

They are unions of convex polyhedra.

Flowpipes

Every flowpipe is represented as a list of unions of convex polyhedra. The i-th element in the list is the set of points reachable at time i.

Convex Polyhedra

They are represented as linear systems of the kind A x <= b where A is an n x m-matrix of real values and b is a m-dimensional vector.

The JSON output format describes them as objects having the members A and b. Vectors and matrices are represented as lists and row-based lists of lists, respectively.

The polyhedron described in above section will be printed as

{
 'A':[[1,0,0,0],
      [0,1,0,0],
      [0,0,1,0],
      [0,0,0,1],
      [-1,0,0,0],
      [0,-1,0,0],
      [0,0,-1,0],
      [0,0,0,-1]],
 'b':[5,-3.4,0.01,0.4,2.1,0,0.3]
}

Please, notice that indentations and new lines have been included for clarity reasons and may be not present in the sapo output.

Unions of Convex Polyhedra

They are described as lists of convex polyhedra.