Giter Site home page Giter Site logo

ariadne-cps / ariadne Goto Github PK

View Code? Open in Web Editor NEW
26.0 9.0 9.0 19.57 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 Issues

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.

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.

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.

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.

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.

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.

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.

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.

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?

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.

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;
                                         ^

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.