Merge pull request #439 from JuliaReach/schillic/436

#436 - Use AbstractMap interface in hybrid models

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

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

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,

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]

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]