Giter Site home page Giter Site logo

ariadne-cps / ariadne Goto Github PK

View Code? Open in Web Editor NEW
25.0 9.0 9.0 19.45 MB

C++ framework for rigorous computation on cyber-physical systems

Home Page: http://www.ariadne-cps.org

License: GNU General Public License v3.0

CMake 1.11% C++ 97.04% Python 1.85%
numerical-analysis hybrid-systems formal-verification cyber-physical-systems reachability-analysis interval-arithmetic

ariadne's Introduction

Ariadne Ariadne

License: GPL v3 Release Status Debug Status codecov

Ariadne is a tool for reachability analysis and model checking of hybrid systems. Additionally, it is a framework for rigorous computation featuring arithmetic, linear algebra, calculus, geometry, algebraic and differential equations, and optimization solvers.

Installation

The command-line installation instructions are presented for Debian Linux systems and derivatives (using apt) and macOS systems (using Homebrew). However, openSUSE and Fedora are known to be working when using their own package managers. Windows installations are not supported yet.

Official packages are available for Ubuntu LTS (currently 20.04) and derivatives and macOS 11, but if your architecture or particular setup necessarily requires compilation from sources, instructions are provided. The build system used is CMake. The library is tested for compilation using gcc (minimum required: 10.2) and clang (minimum required: 11.0).

Official packages

Supplied packages are published using the official Launchpad platform for Ubuntu, and a custom Homebrew tap repository for macOS. Packages simply require all the dependencies, namely: MPFR, Cairo, Gnuplot and Python 3.

Ubuntu

In order to install the apt package, first you need to import the ppa repository to the ppa list:

sudo add-apt-repository ppa:ariadne-cps/ariadne

Then you can install Ariadne (along with any missing dependencies):

sudo apt-get install ariadne

which will be updated with the latest release as with other apt packages.

macOS

In order to install the Homebrew package, you just need to

brew install ariadne-cps/tap/ariadne

which in one line both sets up the "tap" for Ariadne and installs the package along with any missing dependencies. The package will be upgraded with any new versions after a brew upgrade is issued. The package currently supports x86-64 architectures on macOS Big Sur. Other configurations trigger an automatic build, therefore you should not need to deal with sources any time.

Dependencies for installation from sources

If installed from sources, the only required library dependency is MPFR. To enable the graphical output you will require either Cairo or Gnuplot in order to save into png files. Finally, the Python bindings require the Python headers (version 3 is only supported, since version 2 is discontinued). In particular for Python, there is an internal Git submodule dependency on the header-only pybind11 library. In order to build the all the submodules of the library, Git must be installed even if Ariadne has been downloaded as an archive. Download of the dependencies is automatic though.

Finally, if you want to build the documentation, you need Doxygen and a working Latex distribution (including the Math packages).

Please note that adding new library dependencies after preparing the build environment requires to re-run the CMake command.

Specific instructions for Ubuntu and macOS follow, starting from installation from pre-compiled packages.

Ubuntu

apt packages: cmake pkg-config git libmpfr-dev libcairo2-dev gnuplot and either clang-11 or g++-10 for the compiler toolchain.

Additional package required for the Python interface: python3-dev.

Additional packages required for documentation: doxygen doxygen-latex

macOS

Homebrew packages: cmake git mpfr cairo gnuplot and gcc@10 if using GCC.

For Cairo support, you may need to set up a permanent variable for the path of pkgconfig by adding the following line in your ~\.bash_profile:

export PKG_CONFIG_PATH=/usr/local/opt/libffi/lib/pkgconfig

To allow building the documentation: brew install --cask mactex-no-gui and brew install doxygen.

Downloading the sources

A pre-packaged source zip/tar.gz archive is always available in the releases section of Ariadne's GitHub space. Still, it is usually preferable to clone the repository using Git, in order to keep the distribution updated as soon as a new release is available. To do that, you shall issue

git clone https://github.com/ariadne-cps/ariadne 

which creates an ariadne directory under the present working directory. Let's switch into that directory.

Building

To build the library from sources in a clean way, it is preferable that you set up a build subdirectory, say:

$ mkdir build && cd build

Then you can prepare the build environment, choosing a Release build for maximum performance:

$ cmake .. -DCMAKE_BUILD_TYPE=Release

At this point, if no error arises, you can build the C++ library and its Python bindings with:

$ cmake --build .

This build does not include the examples, tutorials and tests targets. You can build those by supplying targets with the following:

$ cmake --build . --target <TARGET>

or by using the everything target to include all code targets.

To build the doc target for documentation, explicitly use:

$ cmake --build . --target doc

then you can access the built documentation from the docs/html/index.html file in the build directory.

Installing globally

To install the library globally from built sources, you must do

$ cmake --build . --target install

using sudo if you require administrator privileges for a Linux installation. Please note that the installation will build the whole distribution beforehand, hence it is preferable that you first build the other targets without administrator privileges, build the install target.

To find the installed library under Ubuntu, you may need to set the LD_LIBRARY_PATH in the .bashrc file of your home directory:

export LD_LIBRARY_PATH=/usr/local/lib

Building executables using Ariadne

The tutorials directory contains two CMake projects that rely on a correct installation of Ariadne, either by using a package or by building the sources. You can copy a project directory in any place on your file system and follow the instructions on the README file inside to check that your installation was successful.

Due to limitations of the C++ standard library on macOS since C++11, you won't be able to build an executable with GCC if the Ariadne library has been built using Clang, and viceversa. Hence on macOS you shall use the same compiler for both Ariadne and any projects that depend on it. If Ariadne comes from the Homebrew package, then it has been built using g++ 10.

Contribution guidelines

If you would like to contribute to Ariadne, please contact the developers. We are especially interested to hear how the documentation and user interface could be improved.

ariadne's People

Contributors

albertocasagrande avatar davide-univr avatar fonskuijk avatar ivan-zapreev avatar lgeretti avatar okrima avatar pietercollins avatar

Stargazers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

Watchers

 avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar  avatar

ariadne's Issues

Implicit conversion from Bool to logical classes

Originally reported by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)


It is still not possible to perform an implicit conversion to a logical class from a Bool value, as in

(nonlinear_programming.cc:1383)

#!c++

if(probably(t>0)) {

or

(grid_set.cc:407)

#!c++

pCurrentNode->_isEnabled = theEnabledCells[leaf_counter];

Currently, we rely on explicit conversion of the boolean condition into the proper class. Curiously, this issue appeared only on macOS.


Improve label handling/displaying for locations

Originally reported by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)


I feel that there is little clarity when defining and using locations for HybridAutomata and their composition. In particular, using a combination of StringVariable and StringConstant for a location name feels awkward. See examples/watertank-compositional.cc.

I would rather keep something similar to the following:

  1. A location of an automaton has its own name, possibly duplicate within a system but unique within an automaton
  2. When handling a composition, a location name gains the prefix of the automaton itself.

In other terms, we should not have redundancy both when defining the automaton and when displaying it. In particular, it would also be nice if the displayed composite location name didn't have the location name of any automaton with just one location: this is clearly redundant information, with the only effect of increasing the location name.


Review `Void Enclosure:: uniform_error_recondition()`

Originally reported by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)


The implementation of uniform error reconditioning in geometry/enclosure.cc:1032 seems odd to me. I assume that it should work by collecting all the result indices for which a relatively large error is present in the model, then it modifies the models for those dimensions by creating a new parameter that encloses the error (which is then removed).

My doubts:

  1. The error_domains variable is assigned twice with no particular reason.
  2. The result dimensions chosen for moving the error into a new parameter do not match the dimensions for which the error is relatively large: we should apply the reconditioning to the large_error_indices[i] dimensions.
  3. The second error>MAXIMUM_ERROR seems redundant to me.

Crossing issues

Using the test_crossings_issue in the crossings-issue branch, if we use a step size of 1e-2, we get:

#!c++

[:0] Unexpected error in computing critical time for event comes:
  std::runtime_error in /Users/lgeretti/Public/sources/ariadne-all/ariadne/geometry/enclosure.cc:492: : Assertion `time.argument_size()==this->number_of_parameters()' failed.

If on the other hand we use a step size of 1e-3, for example, we get a segfault.

Changes to Logical classes

Originally reported by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


Currently our Logical classes are templates parametrised by a Paradigm tag, with typedefs to user-level names (Boolean, Sierpinskian, Kleenean). I plan to re-implement so that the user-level names are class names, and make some other changes to the semantics to make the interface slightly cleaner.

  1. Use Boolean, Sierpinskian and Kleenean as top-level class names, with Lower/Upper- modifiers for Kleenean, Negated- for Sierpinskian, and Validated- and Approximate- versions. Here, Kleenean is a completion of Boolean in much the same way as Real is a completion of Rational.

  2. Distinguish Sierpinskian from LowerKleenean. Sierpinskian would be for cases in which there is no possibility for robust falsification (which in our case is essentially for inequality) and LowerKleenean for partial information on a quasidecidable predicate (e.g. testing for positivity of a LowerReal, where positivity of a Real would return Kleenean).

    • One of the main conceptual motivations for this change is on whether 'Sierpinskian' with values 'true' and 'indeterminate' has more or less information (i.e. can be converted to/from) 'Kleenean' with values 'true', 'indeterminate' and 'false'. Conversion by inclusion Sierpinskian -> Kleenean loses the information that 'false' is not a possible value, whereas conversion Kleenean -> Sierpinskian taking 'false' to 'indeterminate' loses the information when the value is false.
    • After the change, there would then be implicit conversions Sierpinskian -> Kleenean -> LowerKleenean.
  3. Fix LowerKleenean to be for Verifyable predicates (currently LowerKleenean is for Falsifyable, but this is incorrect, since a verified lower bound of 'true' means the predicate must be true, but a lower bound of 'false' means no information).

  4. Effective logical classes will not be convertible to Validated/Approximate classes, but can only be checked with some given Effort.

    • Mixed Effective/Validated operations could be supported by storing the effort_used in the Validated class, and using this to check(...) the Effective value (see below).
  5. Add conjunction/disjunction for Sequences of logical types.

  6. Our SetInterface classes also need Effective and Validated versions. Effective (i.e. exactly specified sets) would have predicates returning (Lower)Kleenean, and Validated sets return their Validated logical versions.

  7. Store the effort_used for a Validated/Approximate logical value, to allow mixed Effective/Validated operations (see above).

  8. Store a cached Validated checked value together with the Effort used with any Effective logical predicate. The advantage of this is fast re-checking of predicates.

    • We need to decide on whether to maintain functionality e.g. if p is a Kleeanean and p.check(Effort(1)) yields indeterminate and p.check(Effort(3)) yields true, should a subsequent p.check(Effort(1)) yield true or indeterminate? What about p.check(Effort(2))?
    • I think that maintaining functionality is sufficiently important to do so. This can be accomplished by also storing the largest Effort for which no decision is reached. Recomputation would only be needed for an intermediate Effort.

Additionally:
9. Consider removing possibly(...) and definitely(...) for Approximate and Naive logical values, as these always yield true and false. (However, the usage is consistent, so may be useful in template code.)
10. Deprecate use of decide(...). It currently has two orthogonal uses: check Effective logical types with minimum Effort, and select an appropriate case for Validated (definitely) and Approximate (probably). Maybe rename to something less snappy, like cast_decision.
11. Consider changing probably to is_likely and adding an is_unlikely. Consider changing these to only apply to Approximate logical types.


Hybrid evolutions scheduling and execution

Originally reported by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


Split hybrid evolution code into scheduling and execution parts.

The rationale is to put complex logic of deciding how to perform the step (so as to avoid excess splitting, variables and constraints) from the task of rigorously performing the step. Ideally, the correctness of the schedule (notably, which events are active) should be simple to check.


Force use of let when creating assignment

Originally reported by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


Currently, given a Variable x and an Expression e, writing x=e creates an Assignment object. An alternative syntax is let(x)=e. Since a Variable is also an Expression, if y is also a Variable, then x=y creates an assignment rather than re-assigning Variable. This is a potential source of bugs/confusion.

I propose forcing the let(x)=e (or an alternative set(x)=e) syntax.

Assignment of variables should then either be usual assignment or disallowed; which is preferable?


Laser example hangs at _compute_crossings

Originally reported by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)


With the laser example present in 5d1257bc of the macos_support branch, there are severe issues when computing crossings. The example is quite trivial, the guard is quadratic and should not be such an issue, since on the stable version of Ariadne this system (or more precisely, the full system which is more complicated) is not a problem at all.


Improve methods for simplification / reconditioning of sets

Simplifying enclosures is a critical problem in computing system dynamics, especially for our differential inclusion methods.

For affine enclosures, there are well-known methods of Lohner and Kuhn which are implemented in the now deprecated Zonotope class, and should be moved to AffineSet classes.

For polynomial enclosures, the problem is an open research problem, but maybe we could do something using the Chebyshev basis.

Depends on #308.

Dangling-field issue

Originally reported by Luca Geretti (Bitbucket: lgeretti, GitHub: lgeretti)


On 'function.cc:37', we have the following warning:

#!c++

/Users/lgeretti/Public/sources/ariadne-all/ariadne/function/function_model.h:474:18: warning: binding reference member '_prototype' to a temporary value [-Wdangling-field]
    : _prototype(f.create_zero()) { }
                 ^~~~~~~~~~~~~~~
/Users/lgeretti/Public/sources/ariadne-all/ariadne/function/function_model.h:323:16: note: in instantiation of member function 'Ariadne::FunctionModelBuilder<Ariadne::ValidatedTag, Ariadne::Precision64,
      Ariadne::Precision64>::FunctionModelBuilder' requested here
        return FunctionModelBuilder<P,PR,PRE>(f); }
               ^
/Users/lgeretti/Public/sources/ariadne-all/ariadne/function/function.cc:1061:81: note: in instantiation of member function 'Ariadne::factory' requested here
        ValidatedVectorFunctionModel f1m(f1p); ValidatedVectorFunctionModel f2m=factory(f1m).create(f2); return join(f1m,f2m);
                                                                                ^
/Users/lgeretti/Public/sources/ariadne-all/ariadne/function/function_model.h:52:42: note: reference member declared here
    ScalarFunctionModel<P,PR,PRE> const& _prototype;
                                         ^


Safe operator/expression objects

Originally reported by Pieter Collins (Bitbucket: pietercollins, GitHub: pietercollins)


The current way of handling operators and symbolic expressions is not type-safe and is sensitive to bugs. Need a more type-safe solution.

One possibility would be to use a variant object, but std::variant is not yet available and boost::variant is less powerful and more buggy. A more lightweight alternative would be to use Operator types with restricted Code enumerations.


Recommend Projects

  • React photo React

    A declarative, efficient, and flexible JavaScript library for building user interfaces.

  • Vue.js photo Vue.js

    ๐Ÿ–– Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.

  • Typescript photo Typescript

    TypeScript is a superset of JavaScript that compiles to clean JavaScript output.

  • TensorFlow photo TensorFlow

    An Open Source Machine Learning Framework for Everyone

  • Django photo Django

    The Web framework for perfectionists with deadlines.

  • D3 photo D3

    Bring data to life with SVG, Canvas and HTML. ๐Ÿ“Š๐Ÿ“ˆ๐ŸŽ‰

Recommend Topics

  • javascript

    JavaScript (JS) is a lightweight interpreted programming language with first-class functions.

  • web

    Some thing interesting about web. New door for the world.

  • server

    A server is a program made to process requests and deliver data to clients.

  • Machine learning

    Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.

  • Game

    Some thing interesting about game, make everyone happy.

Recommend Org

  • Facebook photo Facebook

    We are working to build community through open source technology. NB: members must have two-factor auth.

  • Microsoft photo Microsoft

    Open source projects and samples from Microsoft.

  • Google photo Google

    Google โค๏ธ Open Source for everyone.

  • D3 photo D3

    Data-Driven Documents codes.