Overview
 

Input Language


1. Specifying Input Hybrid Automata
2. Specifying Computation Parameters


 
 
 
 

1. Specifying Input Hybrid Automata

The input hybrid automaton and the safety property are specified in a model file (.hyb).  Here we present the grammar and illustrate it with an example. See the manual for more details.
 

1.1 Grammar
The input hybrid automaton is described using the following grammar.

 
HybAuto  ::=  dim ';' Constants ';' SpecDecl LocationList ';' Limits

dim  ::=  'dimension :' Integer ';'

SpecDecl  := InitSet Safeset Badset Targetset

Constants  ::=  'constants :' ConstantList
                    | None

ConstantList  ::=  ConstantList ','  ConstantDecl
                           | ConstantDecl

ConstantDecl  ::=  Name '=' Double

InitSet  ::=  'initset :' SymbolicState ';'
                  | None

SafeSet  ::=  'safeset :' SymbolicState ';'
                    | None

BadSet  ::=  'badset :' SymbolicState ';'
                   | None

TargetSet  ::=  'targetset :' SymbolicState ';'
                       | None

LocationList  ::=  LocationList  LocationDecl
                      | LocationDecl

LocationDecl  ::=  'location :'  Integer  ';' Dynamics  StaySet  OutTransitions

Dynamics  ::=  'matrixA :'  Matrix  ';'  InputSet

InputSet  ::=  'inputset :' Polyhedron ';'
                      | None

StaySet  ::=  'stayset :' Polyhedron ';'
                    | None

OutTransitions  ::=  'transition :' TransitionList
                                 | None

TransitionList  ::=  TransitionList Transition
                              | None

Transition  ::=  'label' Name ': if in' Polyhedron 'goto' Integer ';'

Limits  ::=  'limits :' Polyhedron
                 | 'limits :' InequalityList

SymbolicState  ::=  'loc_id :' Integer ';' PolyhedronList

PolyhedronList  ::=  PolyhedronList 'or' Polyhedron
                                | Polyhedron

Polyhedron  ::=  PolyType Matrix
                             | None

PolyType  ::=  'convex_vert'
                    | 'convex_constr'
                    | 'rectangle'
                    | 'griddy'

InequalityList  ::=  InequalityList 'and' Inequality
                             | Inequality

Inequality  ::=  Variable InequalityType ArithmExpr
                        | None

InequalityType  ::=  '<='
                               | '>='

Variable  ::=  Name '[' Integer ']'

Matrix  ::=  Matrix ',' Vector
                   | Vector

Vector  ::=  Vector ArithmExpr
                    | ArithmExpr

ArithmExpr  ::=  Name
                          | Double
                          | ArithmExpr '+' ArithmExpr
                          | ArithmExpr '-' ArithmExpr
                          | ArithmExpr '*' ArithmExpr
                          | ArithmExpr '/' ArithmExpr
                          | '-' ArithmExpr
                          | ArithmExpr 'pow ('ArithmExpr')'
                          | '(' ArithmExpr ')'
                          | Fct '(' ArithmExpr ')'

Fct  ::=  'cos'
             | 'sin'
             | 'tan'
             | 'acos'
             | 'asin'
             | 'atan'
             | 'cotan'
             | 'sqrt'

Double  ::=  {Integer('.'{Integer})?{Exposant}?

Exposant  ::=  [eE][+-]?{Integer}

Name  ::=  {Lettre('_'|Lettre|Number)*

Integer  ::=  {Number}+

Number  ::=  [0-9]

Letter  ::=  [a-zA-Z]
 
 


1.2 Example
Let us illustrate the syntax through several examples.

A vector is a series of reals or arithmetic expressions (possibly referring to constant parameters) which ends with a comma ",". A matrix consists of several vectors (the ith vector corresponds to the ith line of the matrix). The last vector should end with a semi-colon ";". For example, suppose we have defined two parameters a1=0.1 and a2=0.2, we can now define a 4-dimensional vector
0.5   a1+a2   cos(a1)  1.0 ,
and a 2x2 matrix
0.5    a1 ,
a2   -3.0 ;

A polyhedron is specified as follows.

type [rectangle, convex_constr, convex_vert, griddy]
Matrix
  • convex_const is used for specifying convex polyhedra by their constraints. An example of a 2-dimensional polyhedron is given below.
    • type convex_const
           1.0    2.0  -0.02 ,   /* x[0] + 2x[1] <= -0.02 */
         -1.5    0.8   -1.5 ,    /* -1.5x[0] + 0.8x[1] <= -1.5 */
         -1.0   1.0    1.5 ;     /* -x[0] + x[1] <= 1.5 */
    Geometrically speaking, each constraint defines a halfspace. The first N elements define the outward normal vector, and the last is a signed offset. The offset is the distance from the boundary of the halfspace to the origin if the normal is a unit vector, and it is positive if the origin is inside the halfspace.
     
  • convex_vert is used for defining convex polyhedra by their vertices. Each vector of the matrix corresponds to a vertex and consists of N real coordinates. As an example, a triangle with vertices (0.5, 0.5), (0.5, 1.0), and (1.0, 0.5) can be defined as follows.
    • type convex_vert
        0.5  0.5 ,   /* vertex (0.5, 0.5) */
        0.5  1.0 ,   /* vertex (0.5, 1.0) */
       1.0   0.5 ;   /* vertex (1.0, 0.5) */
  • griddy is used for defining orthogonal polyhedra by their extreme vertices (see [4]).

    •  
  • rectangle is used for specifying hyperrectangles as products of intervals. The ith vector consists of 2 real numbers defining the left and right bounds in the axis i.
    • type rectangle   /* a rectangle specified by intervals */
           0.62  0.67 ,  /* 0.62 <= x[0] <= 0.67 */
         -0.1    0.1 ;    /* -0.1 <= x[1] <= 0.1 */


    A hybrid automaton can be specified as follows.
     

    dimension : Integer;    /* Dimension = # of  continuous variables, e.g.  N */
    constants : /* constant parameters in the system description, should not be confused with computation parameters */
       a_1 = 0.2 ,
       a_2 = 0.5 ;

    initloc : Integer ;                /* loc_id */
    initset : PolyhedronList ;

    safeset : Integer                  /* loc_id */
                   PolyhedronList ;   /* for synthesis purposes*/
    badset : Integer                   /* loc_id */
                  PolyhedronList ;    /* for verification purposes */

    /* Next, the locations are given one after another */
    location : Integer ;        /* id of the location */

    matrixA : Matrix of size NxN
    scalB : Double
    inputset : Polyhedron          /* must be convex, skip it if there is no input */
    stayset : Polyhedron            /* must be convex, skip it if the staying set is the whole continuous state space*/
              /* The outgoing transitions are then given one after another */
               transition : Name               /* transition label */
                      if in guard Polyhedron    /* convex */
                      goto Integer              /* id of the target location */

    limits x_i<=b and x_j>=c            /* the limits define a bounded analysis set */

    Note that a bounded analysis set (limits) must be given; otherwise, d/dt will refuse. No computation is performed outside the analysis set.
     

    2. Specifying Computation Parameters

    By default d/dt reads the computation parameters from a file having the same name as the model file but with .par as extension. If such a file does not exist, default parameters will be used. Some parameters can be specified in the command line. If using the menu bar, during the analysis of a system some computation parameters can be modified online through the Preferences menu.

    There are 4 types of computation parameters: parameters specific to each location, underlying mesh size, polyhedral computation parameters, and interface/visualization parameters. Note that if a parameter is not specified, its default value will be used. However, some important parameters related to precision control should be specified in order to guarantee the desired accuracy.

    We present first the grammar for specifying computation parameters. Then, using a simple example we explain the usage of these parameters.

    2.1 Grammar
    Formally, the computation parameters are specified using the following grammar.

             CompParams  ::=  dim ';' LocationParams ';'  MeshSize ';' PolyCompParams ';'InterfaceParams

             dim  ::= 'dimension :' Integer ';'

             LocationParams :=  LocationParamList
                                         | None

             PolyCompParams := PolyCompParamList
                                           | None

             InterfaceParams := InterfaceParamList
                                          | None

             LocationParamList  ::=   LocationParamList  EachLocationParams
                                               | EachLocationParams

             EachLocationParams  ::=   'location :'  Integer','EachLocParamList

            EachLocParamList ::= EachLocParamList ','LocParamDecl
                                              |  LocParamDecl

             PolyCompParamList  ::=  PolyCompParamList ','PolyCompParamDecl
                                                 | PolyCompParamDecl

             InterfaceParamList  ::=  InterfaceParamList ',' InterfaceParamDecl
                                               |  InterfaceParamDecl

             MeshSize ::= 'mesh_size' Vector

             LocParamDecl ::= 'time_step' Double
                                      | 'bloat' Double
                                       | 'abs_tol' Double
                                     | 'rel_tol' Vector
                                       | 'hull' Boolean
                                       | 'itermax' Integer
                                       | 'grid_method' GridType

             PolyCompParamDecl ::= 'dblmin' Double
                                                  | 'polylib_priority' PolyLibName
                                                  | 'cdd_zero' Double

     
    InterfaceParamDecl ::= 'file_out' OutputType
                                      | 'display' DisplayType
                                      | 'verbose' VerboseType
                                      | 'projection' Integer Integer Integer
                                      | 'view_angle' Double
                                      | 'xmin' Double | 'ymin' Double |  'zmin' Double
                                      | 'xmax' Double | 'ymax' Double |  'zmax' Double
                                    | 'colour' Integer
                                    | 'rotation' Double Double Double
                                      | 'viewing_mode' Integer
                                      | 'refresh'  Boolean
                                      | 'height' Double
                                      | 'width' Double


             Double  ::=  {Integer('.'{Integer})?{Exposant}?

             Exposant  ::=  [eE][+-]?{Integer}

             Integer  ::=  {Number}+

             Boolean  ::= '1' | '0'

             Number  ::=  [0-9]

              PolyLibName ::= 'qhull'  |  'cdd'

              VerboseType ::= 'i' |  's'  |  'q'

              DisplayType ::= 'noview'  |  'ddt_viewer'  |  'geomview'

              OutputType ::= 'nosave'  |  'ddt_format'  |  'oogl_format'
     

    2.2 Example
    We now illustrate the grammar with a 2-dimensional hybrid automaton with only one location.

    /* Dimension = # of  continuous variables */
    dimension : 2 ;

    /* Parameters specific to each location */
    location : 0 ,  /* id of the location*/

    /* Precision control */
    time_step 0.2 /*time step*/
    bloat 0.005 /* bloating amount, positive for over-approximations, negative for under-approximations */
    abs_tol 10 10 /* absolute tolerance for numerical integration*/
    rel_tol 6     /* relative tolerance for numerical integration */
    hull 0         /* No convex hull approximation is performed */
    grid_method bsp/* ``griddization'' method */
    /* Order of exploration */
    itermax 300 /* If after 300 integration steps the continuous reachability computation of the current location has not yet terminated, delay it till next global iteration and explore other locations. If undefined, this option is ignored */
    ;

    /* Mesh size*/
    mesh_size 0.01 0.01 /* granularity of the underlying mesh*/
    ;

    /* Polyhedral error control parameters */
    dblmin 1E-20                /* user-defined DBL_MIN */
    polylib_priority qhull     /* or cdd */
    cdd_zero 1E-12           /* ``almost zero constant'' for the library CDD */
    ;

    /* Interface  and visualization parameters */
    file_out  nosave            /* nosave, ddt_format, oogl_format * /
    display  ddt_viewer     /* set to  noview to skip run-time visualization,  geomview to use the GeomView */
    verbose  s                  /* i (interactive), s (summary), q (quiet) */

    view_angle 60           /* in degree */
    projection 0 1 0         /* viewing projection axes, the default values are 0 1 2 */
    zmin -0.8
    zmax 0.8
    xmin -0.4
    xmax 0.8
    ymin -0.4
    ymax 0.8             /* window coordinates, the default values are the analysis limits given in the model file */
    colour 2              /* ranging from 0 to 16 */
    rotation 0 90 0    /* the default values are 0 0 0 */
    viewing_mode 1 /* 0 for Filled, 1 for Wireframe */
    refresh  1           /* set to 1 to clear the window after each step; it's defautl value is 0 */
    height 900          /* height of the display window, 800 by default */
    width 900           /* (width of the display window, 800 by default */


    2.3 Precision Control

  • time_step: the choice of the time step for each location depends on the desired accuracy and on the continuous dynamics, that is, matrix A. The automatic calculation of these parameters is not yet included in d/dt (see [1-0]).
  • mesh_size: to approximate reachable sets by orthogonal polyhedra, the former are ``discretized'' over a rectangular mesh whose granularity is determined by the desired approximation accuracy (see [1-0]). If you ignore this parameter, the result produced by d/dt can be bad. By reducing the mesh size one can achieve better approximations at the price of more computation time.
  • rel_tol and abs_tol:  the desired integration accuracy is specified by a scalar relative tolerance and an absolute tolerance vector.
  • bloat: this parameter is used to ensure over-approximations for verification problems and under-approximations for synthesis problems (see [1]). If its value is positive, over-approximations are produced, otherwise under-approximations. The value of bloat for a location depends on the time step and the matrix of the continuous dynamics. See [1-0] for the calculation of this parameter.

    •  
    2.4 Additional Options
  • Orthogonal approximation: there are several ``griddization'' methods for orthogonal approximations implemented in d/dt. The parameter grid_method of a location specifies the method to be used for the continuous reachability computations at the location.

    • The default choice is bsp. The stability and efficiency of these methods depend on the geometric form of reachable sets. Note that orthogonal approximations are used because orthogonal polyhedra are in general easier to manipulate than lists of convex polyhedra. However, there are cases where treating reachable sets as lists of convex polyhedra is less expensive than as orthogonal polyhedra. The possible values of grid_method are:
  • bsp: binary-space-partition based method
  • lp: linear programming based method
  • enu: enumeration method
  • sim: skip the orthogonal approximation step and store the reachable set as a list of convex polyhedra.
  • Convex-hull approximation: in order to speed up the continuous reachability computation in a location, the user has an option to over-approximate the initial sets to explore by their convex hull by setting parameter hull to 1. This obviously reduces the approximation accuracy.

    •  
  • Search order: the current version of d/dt performs breadth first search. If after itermax integration steps the computation of continuous-successors has not yet terminated, it will be delayed until next global iteration and other locations are then explored. If unspecified, this option is ignored.

    •  
  • Polyhedral error control parameters:
  • polylib_priority: for convex polyhedral manipulation, the tool combines two libraries QHULL and  CDD, which allows better precision control. The library CDD can handle degenerate cases such as non-full dimensional polyhedra but it is less time-efficient than QHULL. If the value of polylib_priority is qhull, the library QHULL will be used first and if it fails, the library CDD will then be used, and vice versa.
  • cdd_zero: ``almost zero constant'' that the library CDD uses to control error.
  • dblmin: user-defined DBL_MIN used by d/dt for various operations related to membership testing.

    •  
  • Visualization: If you want to set up 3D display by yourself, then specify the visualization parameters. the visualization paramameters in the example above define a perspective window. The angle of its field of view in direction y is 80 degrees. (xmin, ymin, zmin) define the coordinates of the bottom left corner of the display window. ``projection 0 1 2'' means that the object is projected on the first, second, and third coordinate axes. To visualize higher than three dimensional polyhedra, the coordinate axes in which the object will be displayed should be specified. In the above example, ``translation -0.1 -0.1 -0.1'' means that the object is rotated 0 degree about the axis x, 90 about y, and translated by (-0.1,-0.1,-0.1).  See the OpenGL documentation for more details on 3D viewing.

    •  
  • Output: if the parameter file_out is set to ddt_format, the analysis results will be saved in a file having the same as the model file but with .res as extension. The results are stored in form of a sequence of (q,P) where P is the computed set at location q. The data from .res files can be then viewed using the View menu. If file_out is set to oogl_format the results are saved in OOGL format and can be then input to GeomView. The default value of file_out is nosave.

    •