Test GP abstraction

src/abstractions/gaussian_process.jl

@@ -19,13 +19,13 @@ function transition_prob(
                          collect(enumerate(regions(state_abstraction)))
         for (j, input) in enumerate(inputs(input_abstraction))
             srcact_idx = (i - 1) * ninputs + j
-            gp_bounds = bounds(dyn, source_region, input)
+            bounds = gp_bounds(dyn, source_region, input)
 
             source_action_transition_prob(
                 dyn,
                 state_abstraction,
                 target_model,
-                gp_bounds,
+                bounds,
                 prob_lower,
                 prob_upper,
                 srcact_idx,

test/abstractions/abstractions.jl

@@ -1,5 +1,4 @@
 
-test_files = ["additive_noise/additive_noise.jl", "mixture.jl"]
-for f in test_files
-    @testset "abstractions/$f" include(f)
-end
+@testset verbose=true "abstractions/additive_noise" include("additive_noise/additive_noise.jl")
+@testset verbose=true "abstractions/gaussian_process.jl" include("gaussian_process.jl")
+@testset verbose=true "abstractions/mixture.jl" include("mixture.jl")

test/abstractions/additive_noise/decoupled.jl

@@ -27,7 +27,8 @@ include("example_systems.jl")
     # Dense
     mdp_dense, spec_dense = simple_1d_decoupled()
     @test num_states(mdp_dense) == 11
-    @test stateptr(mdp_dense)[end] == 11
+    @test length(stateptr(mdp_dense)) == 11  # 10 non-sink states
+    @test stateptr(mdp_dense)[end] == 11  # No control actions
 
     prob_dense = Problem(mdp_dense, spec_dense)
 
@@ -37,7 +38,8 @@ include("example_systems.jl")
     # Sparse
     mdp_sparse, spec_sparse = simple_1d_decoupled(; sparse = true)
     @test num_states(mdp_sparse) == 11
-    @test stateptr(mdp_sparse)[end] == 11
+    @test length(stateptr(mdp_sparse)) == 11  # 10 non-sink states
+    @test stateptr(mdp_sparse)[end] == 11  # No control actions
 
     prob_sparse = Problem(mdp_sparse, spec_sparse)
 
@@ -86,6 +88,7 @@ end
         # Dense, input grid
         mdp_dense, spec_dense = modified_running_example_decoupled()
         @test num_states(mdp_dense) == 121  # 11 * 11 total states
+        @test length(stateptr(mdp_dense)) == 10 * 10 + 1  # 10 * 10 non-sink states
         @test stateptr(mdp_dense)[end] == 10 * 10 * 9 + 1  # 10 * 10 non-sink states, 9 actions
 
         prob_dense = Problem(mdp_dense, spec_dense)
@@ -96,6 +99,7 @@ end
         # Sparse, input grid
         mdp_sparse, spec_sparse = modified_running_example_decoupled(; sparse = true)
         @test num_states(mdp_sparse) == 121  # 11 * 11 total states
+        @test length(stateptr(mdp_sparse)) == 10 * 10 + 1  # 10 * 10 non-sink states
         @test stateptr(mdp_sparse)[end] == 10 * 10 * 9 + 1  # 10 * 10 non-sink states, 9 actions
 
         prob_sparse = Problem(mdp_sparse, spec_sparse)

test/abstractions/additive_noise/direct.jl

@@ -28,7 +28,8 @@ include("example_systems.jl")
     # Dense
     mdp_dense, spec_dense = simple_1d_direct()
     @test num_states(mdp_dense) == 11
-    @test stateptr(mdp_dense)[end] == 11
+    @test length(stateptr(mdp_dense)) == 11  # 10 non-sink states
+    @test stateptr(mdp_dense)[end] == 11  # No control actions
 
     prob_dense = Problem(mdp_dense, spec_dense)
 
@@ -38,7 +39,8 @@ include("example_systems.jl")
     # Sparse
     mdp_sparse, spec_sparse = simple_1d_direct(; sparse = true)
     @test num_states(mdp_sparse) == 11
-    @test stateptr(mdp_sparse)[end] == 11
+    @test length(stateptr(mdp_sparse)) == 11  # 10 non-sink states
+    @test stateptr(mdp_sparse)[end] == 11  # No control actions
 
     prob_sparse = Problem(mdp_sparse, spec_sparse)
 
@@ -87,7 +89,8 @@ end
         # Dense, input grid
         mdp_dense, spec_dense = modified_running_example_direct()
         @test num_states(mdp_dense) == 101
-        @test stateptr(mdp_dense)[end] == 10 * 10 * 9 + 1
+        @test length(stateptr(mdp_dense)) == 10 * 10 + 1  # 10 * 10 non-sink states
+        @test stateptr(mdp_dense)[end] == 10 * 10 * 9 + 1  # 10 * 10 non-sink states, 9 actions
 
         prob_dense = Problem(mdp_dense, spec_dense)
 
@@ -97,7 +100,8 @@ end
         # Sparse, input grid
         mdp_sparse, spec_sparse = modified_running_example_direct(; sparse = true)
         @test num_states(mdp_sparse) == 101
-        @test stateptr(mdp_sparse)[end] == 10 * 10 * 9 + 1
+        @test length(stateptr(mdp_sparse)) == 10 * 10 + 1  # 10 non-sink states
+        @test stateptr(mdp_sparse)[end] == 10 * 10 * 9 + 1  # 10 * 10 non-sink states, 9 actions
 
         prob_sparse = Problem(mdp_sparse, spec_sparse)
 

test/abstractions/gaussian_process.jl

@@ -0,0 +1,120 @@
+using Revise, Test
+using LinearAlgebra, LazySets
+using IntervalMDP, IntervalMDPAbstractions
+
+# System definition
+
+# Action 1
+gp_region1_action1 = AbstractedGaussianProcessRegion(
+    Hyperrectangle(low = [-0.5, -0.5], high = [0.0, 0.0]),
+    [-0.5, 0.5],
+    [0.0, 0.6],
+    [0.1, 0.3],
+    [0.2, 0.4],
+)
+gp_region2_action1 = AbstractedGaussianProcessRegion(
+    Hyperrectangle(low = [0.0, -0.5], high = [0.5, 0.0]),
+    [-0.5, 0.5],
+    [0.0, 0.6],
+    [0.1, 0.3],
+    [0.2, 0.4],
+)
+gp_region3_action1 = AbstractedGaussianProcessRegion(
+    Hyperrectangle(low = [-0.5, 0.0], high = [0.0, 0.5]),
+    [-0.5, 0.5],
+    [0.0, 0.6],
+    [0.1, 0.3],
+    [0.2, 0.4],
+)
+gp_region4_action1 = AbstractedGaussianProcessRegion(
+    Hyperrectangle(low = [0.0, 0.0], high = [0.5, 0.5]),
+    [-0.5, 0.5],
+    [0.0, 0.6],
+    [0.1, 0.3],
+    [0.2, 0.4],
+)
+
+gp_action1 = [gp_region1_action1, gp_region2_action1, gp_region3_action1, gp_region4_action1]
+
+# Action 2
+gp_region1_action2 = AbstractedGaussianProcessRegion(
+    Hyperrectangle(low = [-0.5, -0.5], high = [0.0, 0.0]),
+    [-0.5, 0.5],
+    [0.0, 0.6],
+    [0.1, 0.3],
+    [0.2, 0.4],
+)
+gp_region2_action2 = AbstractedGaussianProcessRegion(
+    Hyperrectangle(low = [0.0, -0.5], high = [0.5, 0.0]),
+    [-0.5, 0.5],
+    [0.0, 0.6],
+    [0.1, 0.3],
+    [0.2, 0.4],
+)
+gp_region3_action2 = AbstractedGaussianProcessRegion(
+    Hyperrectangle(low = [-0.5, 0.0], high = [0.0, 0.5]),
+    [-0.5, 0.5],
+    [0.0, 0.6],
+    [0.1, 0.3],
+    [0.2, 0.4],
+)
+gp_region4_action2 = AbstractedGaussianProcessRegion(
+    Hyperrectangle(low = [0.0, 0.0], high = [0.5, 0.5]),
+    [-0.5, 0.5],
+    [0.0, 0.6],
+    [0.1, 0.3],
+    [0.2, 0.4],
+)
+
+gp_action2 = [gp_region1_action2, gp_region2_action2, gp_region3_action2, gp_region4_action2]
+
+# Noise
+w_variance = [0.2, 0.2]
+w_stddev = sqrt.(w_variance)
+w = AdditiveDiagonalGaussianNoise(w_stddev)
+
+dyn = AbstractedGaussianProcess([gp_action1, gp_action2])
+initial_region = Hyperrectangle(low = [-0.1, -0.1], high = [0.1, 0.1])
+sys = System(dyn, initial_region)
+
+horizon = 10
+avoid_region = EmptySet(2)
+prop = FiniteTimeRegionSafety(avoid_region, horizon)
+spec = Specification(prop, Pessimistic, Maximize)
+
+prob = AbstractionProblem(sys, spec)
+
+X = Hyperrectangle(; low = [-0.5, -0.5], high = [0.5, 0.5])
+state_abs = StateUniformGridSplit(X, (2, 2))
+input_abs = InputDiscrete([1, 2])
+
+
+@testset "direct vs decoupled" begin
+    # Decoupled
+    target_model = OrthogonalIMDPTarget()
+    mdp_decoupled, abstract_spec_decoupled = abstraction(prob, state_abs, input_abs, target_model)
+
+    @test num_states(mdp_decoupled) == 3 * 3
+    @test length(stateptr(mdp_decoupled)) == 5  # 4 non-sink states
+    @test stateptr(mdp_decoupled)[end] == 4 * 2 + 1  # 4 non-sink states, 2 control actions
+
+    prob_decoupled = Problem(mdp_decoupled, abstract_spec_decoupled)
+
+    V_decoupled, k, res = value_iteration(prob_decoupled)
+    @test k == 10
+
+    # Direct
+    target_model = IMDPTarget()
+    mdp_direct, abstract_spec_direct = abstraction(prob, state_abs, input_abs, target_model)
+
+    @test num_states(mdp_direct) == 2 * 2 + 1
+    @test length(stateptr(mdp_direct)) == 5  # 4 non-sink states
+    @test stateptr(mdp_direct)[end] == 4 * 2 + 1  # 4 non-sink states, 2 control actions
+
+    prob_direct = Problem(mdp_direct, abstract_spec_direct)
+
+    V_direct, k, res = value_iteration(prob_direct)
+    @test k == 10
+
+    @test all(V_decoupled[1:end-1, 1:end-1] .≥ reshape(V_direct[1:end-1], 2, 2))
+end

test/dynamics/stochastical_switched.jl

@@ -1,3 +1,6 @@
+using Revise, Test
+using IntervalMDPAbstractions, LazySets
+
 A1 = [
     0.1 0.9
     0.8 0.2

test/specifications.jl

@@ -35,8 +35,8 @@ end
 
     target_model = IMDPTarget()
 
-    time_horizon = 10
-    prop = FiniteTimeRegionReachAvoid(reach_region, avoid_region, time_horizon)
+    horizon = 10
+    prop = FiniteTimeRegionReachAvoid(reach_region, avoid_region, horizon)
     spec = Specification(prop, Pessimistic, Maximize)
 
     prob = AbstractionProblem(sys, spec)