Format

Zinoex · Jan 28, 2025 · 4e66612 · 4e66612
1 parent 29fda66
commit 4e66612
Show file tree

Hide file tree

Showing 30 changed files with 442 additions and 201 deletions.
diff --git a/docs/make.jl b/docs/make.jl
@@ -21,13 +21,13 @@ makedocs(;
     pages = [
         "Home" => "index.md"
         "Reference" => Any[
-            "Dynamics" => "reference/dynamics.md",
-            "Specifications" => "reference/specifications.md",
-            "Abstractions" => "reference/abstractions.md",
+            "Dynamics"=>"reference/dynamics.md",
+            "Specifications"=>"reference/specifications.md",
+            "Abstractions"=>"reference/abstractions.md",
         ]
     ],
     doctest = true,
-    checkdocs = :exports
+    checkdocs = :exports,
 )
 
 deploydocs(; repo = "github.com/Zinoex/IntervalMDPAbstractions.jl", devbranch = "main")
diff --git a/examples/systems/almost_identity.jl b/examples/systems/almost_identity.jl
@@ -51,8 +51,11 @@ function almost_identity_decoupled(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -80,8 +83,11 @@ function almost_identity_direct(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end

diff --git a/examples/systems/bas_4d.jl b/examples/systems/bas_4d.jl
@@ -62,8 +62,11 @@ function building_automation_system_4d_decoupled(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -95,8 +98,11 @@ function building_automation_system_4d_direct(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end

diff --git a/examples/systems/big.jl b/examples/systems/big.jl
@@ -48,8 +48,11 @@ function big_decoupled(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -77,8 +80,11 @@ function big_direct(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -104,11 +110,7 @@ function small_sys(time_horizon)
     return sys, spec
 end
 
-function small_direct(
-    time_horizon = 10;
-    sparse = false,
-    state_split_per_dim = 2,
-)
+function small_direct(time_horizon = 10; sparse = false, state_split_per_dim = 2)
     sys, spec = small_sys(time_horizon)
 
     X = Hyperrectangle(; low = [-1.0], high = [1.0])
@@ -126,8 +128,11 @@ function small_direct(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end

diff --git a/examples/systems/car_parking.jl b/examples/systems/car_parking.jl
@@ -52,8 +52,11 @@ function car_parking_decoupled(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -89,8 +92,11 @@ function car_parking_direct(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end

diff --git a/examples/systems/gp_dkl.jl b/examples/systems/gp_dkl.jl
@@ -98,8 +98,11 @@ function dubins_car_decoupled(time_horizon = 10; sparse = false)
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -123,8 +126,11 @@ function dubins_car_direct(time_horizon = 10; sparse = true)
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
diff --git a/examples/systems/linear_stochastically_switched.jl b/examples/systems/linear_stochastically_switched.jl
@@ -61,8 +61,11 @@ function linear_stochastically_switched_direct(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -89,8 +92,11 @@ function linear_stochastically_switched_mixture(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end

diff --git a/examples/systems/nndm.jl b/examples/systems/nndm.jl
@@ -321,8 +321,11 @@ function action_cartpole_decoupled(time_horizon = 10; sparse = false)
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -349,8 +352,11 @@ function action_cartpole_direct(time_horizon = 10; sparse = false)
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
diff --git a/examples/systems/robot_2d.jl b/examples/systems/robot_2d.jl
@@ -86,8 +86,11 @@ function robot_2d_decoupled(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -117,8 +120,11 @@ function robot_2d_direct(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end

diff --git a/examples/systems/van_der_pol.jl b/examples/systems/van_der_pol.jl
@@ -47,8 +47,11 @@ function van_der_pol_decoupled(
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -68,8 +71,11 @@ function van_der_pol_direct(time_horizon = 10; state_split = (50, 50), input_spl
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec =
-        IntervalMDPAbstractions.convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalMDPAbstractions.convert_specification(
+        upper_bound_spec,
+        state_abs,
+        target_model,
+    )
 
     return mdp, abstract_spec, upper_bound_spec
 end

diff --git a/src/abstractions/abstraction.jl b/src/abstractions/abstraction.jl
@@ -145,16 +145,28 @@ end
 
 function initprob(::SparseIMDPTarget, nregions, ninputs)
     nchoices = nregions * ninputs
-    prob_lower = AtomicSparseMatrixCOO{Float64, Int32}(undef, nregions + 1, nchoices)
-    prob_upper = AtomicSparseMatrixCOO{Float64, Int32}(undef, nregions + 1, nchoices)
+    prob_lower = AtomicSparseMatrixCOO{Float64,Int32}(undef, nregions + 1, nchoices)
+    prob_upper = AtomicSparseMatrixCOO{Float64,Int32}(undef, nregions + 1, nchoices)
 
     return prob_lower, prob_upper
 end
 
 function postprocessprob(::SparseIMDPTarget, prob_lower, prob_upper)
-    prob_lower = sparse(prob_lower.rows, prob_lower.cols, prob_lower.values, prob_lower.m, prob_lower.n)
-    prob_upper = sparse(prob_upper.rows, prob_upper.cols, prob_upper.values, prob_upper.m, prob_upper.n)
-
+    prob_lower = sparse(
+        prob_lower.rows,
+        prob_lower.cols,
+        prob_lower.values,
+        prob_lower.m,
+        prob_lower.n,
+    )
+    prob_upper = sparse(
+        prob_upper.rows,
+        prob_upper.cols,
+        prob_upper.values,
+        prob_upper.m,
+        prob_upper.n,
+    )
+
     return prob_lower, prob_upper
 end
 
@@ -166,7 +178,7 @@ function convert_property(
     prop = system_property(spec)
 
     reach_states = Int32[]
-    avoid_states = Int32[numregions(state_abstraction) + 1]  # Absorbing state
+    avoid_states = Int32[numregions(state_abstraction)+1]  # Absorbing state
 
     for (i, source_region) in enumerate(regions(state_abstraction))
         if ispessimistic(spec) && source_region ⊆ reach(prop)
@@ -187,7 +199,7 @@ function convert_property(
     prop = system_property(spec)
 
     reach_states = Int32[]
-    avoid_states = Int32[numregions(state_abstraction) + 1]  # Absorbing state
+    avoid_states = Int32[numregions(state_abstraction)+1]  # Absorbing state
 
     for (i, source_region) in enumerate(regions(state_abstraction))
         if ispessimistic(spec) && !iszeromeasure(avoid(prop), source_region)
@@ -211,7 +223,7 @@ function convert_property(
 )
     prop = system_property(spec)
 
-    avoid_states = Int32[numregions(state_abstraction) + 1]  # Absorbing state
+    avoid_states = Int32[numregions(state_abstraction)+1]  # Absorbing state
 
     for (i, source_region) in enumerate(regions(state_abstraction))
         if ispessimistic(spec) && !iszeromeasure(avoid(prop), source_region)
@@ -313,14 +325,16 @@ function initprob(
     state_abstraction::StateUniformGridSplit,
     ninputs,
 )
-    prob_lower = AtomicSparseMatrixCOO{Float64, Int32}[]
-    prob_upper = AtomicSparseMatrixCOO{Float64, Int32}[]
+    prob_lower = AtomicSparseMatrixCOO{Float64,Int32}[]
+    prob_upper = AtomicSparseMatrixCOO{Float64,Int32}[]
 
     nchoices = numregions(state_abstraction) * ninputs
 
     for axisregions in splits(state_abstraction)
-        local_prob_lower = AtomicSparseMatrixCOO{Float64, Int32}(undef, axisregions + 1, nchoices)
-        local_prob_upper = AtomicSparseMatrixCOO{Float64, Int32}(undef, axisregions + 1, nchoices)
+        local_prob_lower =
+            AtomicSparseMatrixCOO{Float64,Int32}(undef, axisregions + 1, nchoices)
+        local_prob_upper =
+            AtomicSparseMatrixCOO{Float64,Int32}(undef, axisregions + 1, nchoices)
 
         push!(prob_lower, local_prob_lower)
         push!(prob_upper, local_prob_upper)