diff --git a/src/solve.jl b/src/solve.jl index 3760b9bb..c1bcd4e1 100644 --- a/src/solve.jl +++ b/src/solve.jl @@ -173,6 +173,26 @@ function solve!(system::InitialValueProblem{<:HybridSystem, property_loc = property isa Dict ? get(property, loc_id, nothing) : property + + # add the very first initial approximation + if passed_list != nothing && + (!isassigned(passed_list, loc_id) || isempty(passed_list[loc_id])) + reach_set = reach_tube.Xk[1] + # TODO For lazy X0 the fixpoint check is likely to fail, so we + # currently ignore that. In general, we want to add an + # *underapproximation*, which we currently do not support. + X = set(reach_set) + if !(X isa CartesianProductArray) || !(array(X)[1] isa CH) + Xoa = overapproximate(X) + ti, tf = time_start(reach_set), time_end(reach_set) + passed_list[loc_id] = [ReachSet{LazySet{N}}(Xoa, ti, tf)] + end + end + + # count_Rsets counts the number of new reach sets added to Rsets + count_Rsets = tube⋂inv!(opD, reach_tube.Xk, loc.X, Rsets, + [time_start(X0), time_end(X0)]) + if property_loc != nothing if opD isa DecomposedDiscretePost temp_vars = opD.options[:temp_vars] @@ -190,7 +210,7 @@ function solve!(system::InitialValueProblem{<:HybridSystem, end end else - for (i, reach_set) in enumerate(reach_tube.Xk) + for (i, reach_set) in enumerate(Rsets[length(Rsets) - count_Rsets + 1 : end]) if !check(property_loc, set(reach_set)) return CheckSolution(false, i, options) end @@ -198,25 +218,6 @@ function solve!(system::InitialValueProblem{<:HybridSystem, end end - # add the very first initial approximation - if passed_list != nothing && - (!isassigned(passed_list, loc_id) || isempty(passed_list[loc_id])) - reach_set = reach_tube.Xk[1] - # TODO For lazy X0 the fixpoint check is likely to fail, so we - # currently ignore that. In general, we want to add an - # *underapproximation*, which we currently do not support. - X = set(reach_set) - if !(X isa CartesianProductArray) || !(array(X)[1] isa CH) - Xoa = overapproximate(X) - ti, tf = time_start(reach_set), time_end(reach_set) - passed_list[loc_id] = [ReachSet{LazySet{N}}(Xoa, ti, tf)] - end - end - - # count_Rsets counts the number of new reach sets added to Rsets - count_Rsets = tube⋂inv!(opD, reach_tube.Xk, loc.X, Rsets, - [time_start(X0), time_end(X0)]) - if jumps == max_jumps continue end