ariadne-cps / ariadne

C++ framework for rigorous computation on cyber-physical systems
http://www.ariadne-cps.org
GNU General Public License v3.0
28 stars 9 forks source link

Issue with merge of #370 on hybrid evolution #405

Closed lgeretti closed 4 years ago

lgeretti commented 4 years ago

I noticed that after rebasing my "arch" branch (where only examples are modified) with the commits corresponding to the merging of dynamics-named_auxiliary#370, hybrid evolution for one of them failed.

The example is experimental/examples/arch/lotka_volterra_arch.cpp, and if you check the corresponding dynamics-regression#405 branch by running it with verbosity 1 you get an error just after a set is split from a tangential crossing. By using maximum verbosity you get:

   location=(lotkavolterra|outside),
   state_space=[x,y,cnt],
   range=[{0.93548561:0.94668436},{0.85082822:0.85578139},{0.:0.}],
   domain=[{1.296:1.304},{-0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002225:0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002225},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{0.:0.02000}],
   reduced_domain=[{1.296:1.304},{0.:0.},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{0.:0.02000}],
   is_(reduced_domain_)empty=false,
   state=VectorFunctionPatch(result_size=3,dom=[{1.296:1.304},{-0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002225:0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002225},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{0.:0.02000}], rng=[{0.93551802:0.94668311},{0.85086386:0.85578139},{0.:0.}])[ { -0.1229*x9^3 +0.4862*x0*x9^2 -0.4663*x9^2 -0.0003129*x5*x9 +0.00008623*x4*x9 +0.00009859*x3*x9 -0.0002970*x2*x9 +1.078*x0*x9 -0.9902*x9 +0.00000001283*x5 +0.0002064*x4 -0.0001769*x3 -0.00009900*x2 -0.03905*x0^2 -0.1344*x0 +1.178+/-0.000000783}, { 0.4168*x0*x9^2 -0.3637*x9^2 +0.0001768*x4*x9 -0.0001515*x3*x9 -0.00008480*x2*x9 -0.1757*x0*x9 +0.1745*x9 +0.0001103*x5 -0.000000002851*x4 -0.00006081*x3 +0.00009014*x2 -0.4185*x0 +1.398+/-0.000000526}, {0} ],
   constraints=    
[ -inf[:]<=FunctionPatch(dom=[{1.296:1.304},{-0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002225:0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000002225},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{0.:0.02000}]){ 1.000*x9 -0.02000+/-0.00000000000000000223}<=0.0[:]],
   time=FunctionPatch(dom=[{1.296:1.304},{0.:0.},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{0.:0.02000}]){ 1.000*x9 +2.610+/-0.0000000000000156})
[e:8]        event=enter, guard=sqr(0.15)-(sqr(x0-div(1,1))+sqr(x1-div(3,3))), flow_derivative=(0-((x0-div(1,1))*2*(1-0)+(x1-div(3,3))*2*(0-0)))*(3*x0-3*x0*x1)+(0-((x0-div(1,1))*2*(0-0)+(x1-div(3,3))*2*(1-0)))*(1*x0*x1-1*x1)+(0-((x0-div(1,1))*2*(0-0)+(x1-div(3,3))*2*(0-0)))*0
[e:9]         guard_range={-0.0039143240:-0.0011415676}, flow_derivative_range={0.022238527:0.046620301}
[e:7]       HybridEvolverBase::_compute_crossings(...)
[e:4]    crossings={ }
[e:7]       GeneralHybridEvolver::_estimate_timing(...)
[e:7]       starting_time_range={2.6099999:2.6100001} step_size=0.020000000000000000 final_time=3.[6:7]
[e:9]         remaining_time_range={1.0299999:1.0300001}
[e:7]       finishing_kind=BEFORE_FINAL_TIME
[e:7]       temporal_evolution_time=FunctionPatch(dom=[{2.610:2.630}]){ 0.02000}
[e:6]      No creep
[e:7]       evolution_time=FunctionPatch(dom=[{0.9355:0.9384},{0.8519:0.8558},{0.:0.},{2.610:2.630}]){ 0.02000+/-0.00000000000000000445}
[e:7]       finishing_time=FunctionPatch(dom=[{0.9355:0.9384},{0.8519:0.8558},{0.:0.},{2.610:2.630}]){ 1.000*x3 +0.02000+/-0.000000000000000227}
libc++abi.dylib: terminating with uncaught exception of type std::runtime_error: std::runtime_error in /Users/lgeretti/Public/sources/ariadne-cps/ariadne/source/function/scaled_function_patch.tpl.hpp:349: Ariadne::Void Ariadne::VectorScaledFunctionPatch<Ariadne::TaylorModel<Ariadne::ValidatedTag, Ariadne::FloatDP> >::adjoin(const ScaledFunctionPatch<M> &) [M = Ariadne::TaylorModel<Ariadne::ValidatedTag, Ariadne::FloatDP>]: Assertion `sf.domain()==this->domain()' failed.
  sf=FunctionPatch(dom=[{1.296:1.304},{0.:0.},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000},{-1.000:1.000}]){ 2.610+/-0.0000000000000153}

Moreover, if you change the radius of the initial set by setting e = 0, this problem does not surface. Conversely, changing the step size or the order doesn't seem to affect the error.

pietercollins commented 4 years ago

The problem is due to widening of singleton domains in some cases, but not others. I'm not quite sure where the problem arises in this example, but removing widening and/or discarding of singleton domains fixes the problem. There may be other issues arising in examples, but all the tests pass.

lgeretti commented 4 years ago

I'll rebase and check. What changes did you make that end up triggering this issue?