diff --git a/src/ReachSets/DiscretePost/ConcreteDiscretePost.jl b/src/ReachSets/DiscretePost/ConcreteDiscretePost.jl index 5a10d265..133f592e 100644 --- a/src/ReachSets/DiscretePost/ConcreteDiscretePost.jl +++ b/src/ReachSets/DiscretePost/ConcreteDiscretePost.jl @@ -110,9 +110,8 @@ function post(𝒫::ConcreteDiscretePost, target_loc_id = target(HS, trans) target_loc = HS.modes[target(HS, trans)] target_invariant = target_loc.X - trans_annot = HS.resetmaps[symbol(HS, trans)] - guard = trans_annot.X - assignment = trans_annot.A + constrained_map = resetmap(HS, trans) + guard = stateset(constrained_map) # perform jumps post_jump = Vector{ReachSet{LazySet{N}, N}}() @@ -125,8 +124,7 @@ function post(𝒫::ConcreteDiscretePost, end # apply assignment - # TODO converting to HPolytope ?? handle automatically ?? - A⌜Rβ‹‚G⌟ = convert(HPolytope, linear_map(assignment, Rβ‹‚G)) + A⌜Rβ‹‚G⌟ = apply_assignment(𝒫, constrained_map, Rβ‹‚G) # intersect with target invariant A⌜Rβ‹‚GβŒŸβ‹‚I = intersection(target_invariant, A⌜Rβ‹‚G⌟) @@ -144,3 +142,12 @@ function post(𝒫::ConcreteDiscretePost, target_loc_id, jumps) end end + +# --- handling assignments --- + +function apply_assignment(𝒫::ConcreteDiscretePost, + constrained_map::ConstrainedLinearMap, + Rβ‹‚G::LazySet; + kwargs...) + return linear_map(constrained_map.A, Rβ‹‚G) +end diff --git a/src/ReachSets/DiscretePost/DiscretePost.jl b/src/ReachSets/DiscretePost/DiscretePost.jl index 9e44be47..fdc7a57e 100644 --- a/src/ReachSets/DiscretePost/DiscretePost.jl +++ b/src/ReachSets/DiscretePost/DiscretePost.jl @@ -10,13 +10,13 @@ Abstract supertype of all discrete post operators. All discrete post operators should provide the following method, in addition to those provided for general post operators: ```julia -tubeβ‹‚inv!(op::DiscretePost, reach_tube::Vector{<:ReachSet{<:LazySet{N}}}, +tubeβ‹‚inv!(𝒫::DiscretePost, reach_tube::Vector{<:ReachSet{<:LazySet{N}}}, invariant, Rsets, start_interval)::Vector{ReachSet{LazySet{N}, N}} ``` """ abstract type DiscretePost <: PostOperator end -function postprocess(op, +function postprocess(𝒫, HS, post_jump, options, @@ -29,7 +29,7 @@ function postprocess(op, if fixpoint_strategy == :eager # eager fixpoint checking post_jump_filtered = - filter(x -> !isfixpoint(op, x, passed_list, target_loc_id), + filter(x -> !isfixpoint(𝒫, x, passed_list, target_loc_id), post_jump) else post_jump_filtered = post_jump @@ -41,13 +41,13 @@ function postprocess(op, end # apply clustering - clustered = cluster(op, post_jump_filtered, options) + clustered = cluster(𝒫, post_jump_filtered, options) # push new sets after jump (unless a fixpoint is detected) for reach_set in clustered if fixpoint_strategy != :none if fixpoint_strategy == :lazy && - isfixpoint(op, reach_set, passed_list, target_loc_id) + isfixpoint(𝒫, reach_set, passed_list, target_loc_id) continue end push!(passed_list[target_loc_id], reach_set) @@ -56,11 +56,11 @@ function postprocess(op, end end -function cluster(op::DiscretePost, +function cluster(𝒫::DiscretePost, reach_sets::Vector{ReachSet{LazySet{N}, N}}, options::Options) where N<:Real clustering_strategy = options[:clustering] - dirs = op.options[:overapproximation] + dirs = 𝒫.options[:overapproximation] if clustering_strategy == :none # no clustering return reach_sets @@ -76,7 +76,7 @@ function cluster(op::DiscretePost, end end -function isfixpoint(op::DiscretePost, +function isfixpoint(𝒫::DiscretePost, reach_set::ReachSet{LazySet{N}, N}, passed_list, loc_id @@ -97,13 +97,13 @@ function isfixpoint(op::DiscretePost, end # default: always apply line search -function use_precise_ρ(op::DiscretePost, +function use_precise_ρ(𝒫::DiscretePost, cap::Intersection{N})::Bool where N<:Real return true end -function get_overapproximation_option(op::DiscretePost, n::Int) - oa = op.options.dict[:overapproximation] +function get_overapproximation_option(𝒫::DiscretePost, n::Int) + oa = 𝒫.options.dict[:overapproximation] if oa isa Symbol dirs = Utils.interpret_template_direction_symbol(oa) return dirs(n) @@ -113,3 +113,12 @@ function get_overapproximation_option(op::DiscretePost, n::Int) error("received unknown :overapproximation option $oa") end end + +# --- default methods for handling assignments --- + +function apply_assignment(𝒫::DiscretePost, + constrained_map::AbstractMap, + Rβ‹‚G::LazySet; + kwargs...) + return apply(constrained_map, Rβ‹‚G) +end diff --git a/src/ReachSets/DiscretePost/LazyDiscretePost.jl b/src/ReachSets/DiscretePost/LazyDiscretePost.jl index b1290761..1e0db587 100644 --- a/src/ReachSets/DiscretePost/LazyDiscretePost.jl +++ b/src/ReachSets/DiscretePost/LazyDiscretePost.jl @@ -116,8 +116,8 @@ function post(𝒫::LazyDiscretePost, options ) where {N} jumps += 1 - # TODO? dirs = 𝒫.options[:overapproximation] - dirs = get_overapproximation_option(𝒫, options[:n]) + # TODO? oa = 𝒫.options[:overapproximation] + oa = get_overapproximation_option(𝒫, options[:n]) source_invariant = HS.modes[source_loc_id].X inv_isa_Hrep, inv_isa_H_polytope = get_Hrep_info(source_invariant) @@ -126,9 +126,8 @@ function post(𝒫::LazyDiscretePost, target_loc_id = target(HS, trans) target_loc = HS.modes[target(HS, trans)] target_invariant = target_loc.X - trans_annot = HS.resetmaps[symbol(HS, trans)] - guard = trans_annot.X - assignment = trans_annot.A + constrained_map = resetmap(HS, trans) + guard = stateset(constrained_map) if inv_isa_Hrep guard_isa_Hrep, guard_isa_H_polytope = get_Hrep_info(guard) @@ -159,9 +158,9 @@ function post(𝒫::LazyDiscretePost, end # apply assignment - A⌜Rβ‹‚G⌟ = LinearMap(assignment, Rβ‹‚G) + A⌜Rβ‹‚G⌟ = apply_assignment(𝒫, constrained_map, Rβ‹‚G) if !𝒫.options[:lazy_Rβ‹‚G] - A⌜Rβ‹‚G⌟ = overapproximate(A⌜Rβ‹‚G⌟, dirs) + A⌜Rβ‹‚G⌟ = overapproximate(A⌜Rβ‹‚G⌟, oa) end # intersect with target invariant @@ -174,7 +173,7 @@ function post(𝒫::LazyDiscretePost, # overapproximate final set once more if !𝒫.options[:lazy_A⌜Rβ‹‚GβŒŸβ‹‚I] - res = overapproximate(A⌜Rβ‹‚GβŒŸβ‹‚I, dirs) + res = overapproximate(A⌜Rβ‹‚GβŒŸβ‹‚I, oa) else res = A⌜Rβ‹‚GβŒŸβ‹‚I end @@ -202,7 +201,7 @@ function get_Hrep_info(set::HPolyhedron) return (true, false) end -# --- line search policies --- +# --- line-search policies --- # usually do not use line search function use_precise_ρ(𝒫::LazyDiscretePost, diff --git a/test/Reachability/models/bouncing_ball.jl b/test/Reachability/models/bouncing_ball.jl index 66b982d2..523f591d 100644 --- a/test/Reachability/models/bouncing_ball.jl +++ b/test/Reachability/models/bouncing_ball.jl @@ -27,8 +27,7 @@ function bouncing_ball() guard = HPolyhedron([HalfSpace([0.0, 1.0], 0.0), # v ≀ 0 HalfSpace([-1.0, 0.0], 0.0), # x β‰₯ 0 HalfSpace([1.0, 0.0], 0.0)]) # x ≀ 0 - t1 = ConstrainedLinearDiscreteSystem(A, guard) # old interface - # t1 = ConstrainedLinearMap(A, guard) # new interface + t1 = ConstrainedLinearMap(A, guard) # transition annotations resetmaps = [t1] diff --git a/test/Reachability/models/thermostat.jl b/test/Reachability/models/thermostat.jl index ee1627dd..786e7772 100644 --- a/test/Reachability/models/thermostat.jl +++ b/test/Reachability/models/thermostat.jl @@ -35,14 +35,12 @@ function thermostat() # transition from on to off add_transition!(automaton, 1, 2, 1) guard = HalfSpace([-1.0], -21.0) # x β‰₯ 21 - t_on2off = ConstrainedLinearDiscreteSystem(hcat(1.0), guard) # old interface - # t_on2off = ConstrainedIdentityMap(2, guard) # new interface + t_on2off = ConstrainedIdentityMap(2, guard) # transition from off to on add_transition!(automaton, 2, 1, 2) guard = HalfSpace([1.0], 19.0) # x ≀ 19 - t_off2on = ConstrainedLinearDiscreteSystem(hcat(1.0), guard) # old interface - # t_off2on = ConstrainedIdentityMap(2, guard) # new interface + t_off2on = ConstrainedIdentityMap(2, guard) # transition annotations resetmaps = [t_on2off, t_off2on]