irafhy
Interval arithmetic based Reachability Analysis Framework for Hybrid Automaton
Getting Started

This section will show you the dependencies of the framework, and how to modify the compilation or installation.

Dependencies

The framework depends on the following three-party libraries:

Library URL Version
Eigen http://eigen.tuxfamily.org/index.php?title=Main_Page 3.3.4
CMake https://cmake.org/ latest
GLPK https://www.gnu.org/software/glpk/ 4.65-2
FILIB++ http://www2.math.uni-wuppertal.de/wrswt/software/filib.html 3.0.2
boost https://www.boost.org/ 1.67.0.0
Doxygen http://www.doxygen.nl/ 1.8.13
Grapviz https://www.graphviz.org/ 2.40.1-5
Google Test https://github.com/google/googletest 1.8.1
Qhull https://github.com/qhull/qhull 7.2.1
FLANN https://www.cs.ubc.ca/research/flann/ 1.9.1
Antlr https://www.antlr.org/ 4.7.2
libigl https://github.com/libigl/libigl.git latest
OpenMP https://www.openmp.org/ latest

:point_up:   It is recommended to install the latest version of these libraries.

Installation

It is recommended build the library out of source, e.g. build in a separate folder named build. we will under the assumption that the folder build has been created under the root directory to illustrate the configuration options and installation. So we recommend you run the following command under the root directory of the source code before compilation

$ mkdir build && cd build

Configuration

The IraFhy provides such following configuration options:

  • ENABLE EXAMPLES enable generating examples
  • ENABLE TESTING enable Unit Testing
  • ENABLE DOC enable generating documents

Building

You may specify the building procedure with different options as following: e.g. under the build directory, if someone want to enable generating examples, unit testing and documents generating, simply runs the following command:

$ cmake . . −DENABLE EXAMPLES=1 −DENABLE TESTING=1 −DENABLE DOC=1

Once the cmake configuration and generation procedure done, the example 0 can be compiled and runs as following:

$ make example

Documents can be generated by running the command:

$ make doc

Unit testing can be turned on by running the following command:

$ make test