Failure when computing Lie derivative of a disjunction of predicates

[lgeretti]

After introducing support for conjunction of predicates, I tried to enrich one invariant in the hybrid evolution tutorial:

automaton.new_invariant(rising,height<=hmax+delta and height>=0,must_close);

where the evolution is such that height is always very far from zero.

While computing evolution we get the following error (I attach the full trace of the log here):

[:3]    initial_set=HybridBoundedConstraintSet( { (controller|rising,valve|opened):[(height,{6.9:7});] } )
[:3]    initial_enclosure=HybridEnclosure( variables = [x0],
   events=[],
   location=(controller|rising,valve|opened),
   state_space=[height],
   range=[{6.8999999:7.0000001}],
   domain=[{6.900:7.000}],
   reduced_domain=[{6.900:7.000}],
   is_(reduced_domain_)empty=false,
   state=VectorFunctionPatch(result_size=1,dom=[{6.900:7.000}], rng=[{6.8999999:7.0000001}])[ { 1.000*x0 -0.0000000000000004441+/-0.0000000954} ],
   constraints=    
[ ],
   time=FunctionPatch(dom=[{6.900:7.000}]){0})
[:2]   
HybridEvolverBase::orbit(...): verbosity=8
[:3]    HybridEvolverBase::_evolution_in_mode(...)
[:4]     initial_set=HybridEnclosure( variables = [x0],
   events=[],
   location=(controller|rising,valve|opened),
   state_space=[height],
   range=[{6.8999999:7.0000001}],
   domain=[{6.900:7.000}],
   reduced_domain=[{6.900:7.000}],
   is_(reduced_domain_)empty=false,
   state=VectorFunctionPatch(result_size=1,dom=[{6.900:7.000}], rng=[{6.8999999:7.0000001}])[ { 1.000*x0 -0.0000000000000004441+/-0.0000000954} ],
   constraints=    
[ ],
   time=FunctionPatch(dom=[{6.900:7.000}]){0})

[:3]    HybridEvolverBase::_extract_transitions(...)
[:5]      event=can_close, kind=permissive
[:5]      constraint_function=x0-sub(7.75,0.02)
[:5]      event=must_close, kind=invariant
[:5]      constraint_function=min(x0-add(7.75,0.02),0-x0)
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/function.cpp:708: Ariadne::EffectiveScalarMultivariateFunction Ariadne::lie_derivative(const Ariadne::EffectiveScalarMultivariateFunction &, const Ariadne::EffectiveVectorMultivariateFunction &): ErrorTag Failed to compute Lie derivative of min(x0-add(7.75,0.02),0-x0) under vector field [0.3*1-0.02*x0]

Can we work around this @pietercollins ?

[lgeretti]

By allowing derivative(min/max(f1,f2)) to be min/max(derivative(f1),derivative(f2)) it is possible to work around this. However, by applying disjunction with a guard in the hybrid evolution tutorial, it seems this introduces excessive overapproximation even if the guard is trivially satisfied. This should be investigated.