Skip to content

Commit c0754ce

Browse files
ZinoexZinoex
committed
Update tests to match new API
1 parent d1c42cb commit c0754ce

File tree

4 files changed

+269
-210
lines changed

4 files changed

+269
-210
lines changed

‎test/abstractions/compare_abstractions.jl

+9-18
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,8 @@ using IntervalMDP, IntervalMDPAbstractions
55
include("example_systems.jl")
66

77
function modified_running_example_compare()
8-
sys = modified_running_example_sys()
8+
sys, spec = modified_running_example_sys()
9+
prob = AbstractionProblem(sys, spec)
910

1011
X = Hyperrectangle(; low = [-10.0, -10.0], high = [10.0, 10.0])
1112
state_abs = StateUniformGridSplit(X, (10, 10))
@@ -14,36 +15,26 @@ function modified_running_example_compare()
1415
input_abs = InputGridSplit(U, [3, 3])
1516

1617
target_model_direct = IMDPTarget()
17-
mdp_direct, reach_direct, avoid_direct =
18-
abstraction(sys, state_abs, input_abs, target_model_direct)
18+
mdp_direct, abstract_spec_direct = abstraction(prob, state_abs, input_abs, target_model_direct)
1919

2020
target_model_decoupled = OrthogonalIMDPTarget()
21-
mdp_decoupled, reach_decoupled, avoid_decoupled =
22-
abstraction(sys, state_abs, input_abs, target_model_decoupled)
23-
24-
return mdp_direct,
25-
reach_direct,
26-
avoid_direct,
27-
mdp_decoupled,
28-
reach_decoupled,
29-
avoid_decoupled
21+
mdp_decoupled, abstract_spec_decoupled = abstraction(prob, state_abs, input_abs, target_model_decoupled)
22+
23+
return mdp_direct, abstract_spec_direct,
24+
mdp_decoupled, abstract_spec_decoupled
3025
end
3126

32-
mdp_direct, reach_direct, avoid_direct, mdp_decoupled, reach_decoupled, avoid_decoupled =
27+
mdp_direct, spec_direct, mdp_decoupled, spec_decoupled =
3328
modified_running_example_compare()
3429

3530
# Value iteration
36-
prop_direct = FiniteTimeReachAvoid(reach_direct, avoid_direct, 10)
37-
spec_direct = Specification(prop_direct, Pessimistic, Maximize)
3831
prob_direct = Problem(mdp_direct, spec_direct)
3932

4033
V_direct, k, res = value_iteration(prob_direct)
4134
@test k == 10
4235

43-
prop_decoupled = FiniteTimeReachAvoid(reach_decoupled, avoid_decoupled, 10)
44-
spec_decoupled = Specification(prop_decoupled, Pessimistic, Maximize)
4536
prob_decoupled = Problem(mdp_decoupled, spec_decoupled)
4637

4738
V_decoupled, k, res = value_iteration(prob_decoupled)
4839
@test k == 10
49-
@test all(V_decoupled[2:end, 2:end] .≥ reshape(V_direct[2:end], 10, 10))
40+
@test all(V_decoupled[1:end-1, 1:end-1] .≥ reshape(V_direct[1:end-1], 10, 10))

‎test/abstractions/decoupled.jl

+123-95
Original file line numberDiff line numberDiff line change
@@ -4,111 +4,139 @@ using IntervalMDP, IntervalMDPAbstractions
44

55
include("example_systems.jl")
66

7-
function simple_1d_decoupled(; sparse = false)
8-
sys = simple_1d_sys()
9-
10-
X = Hyperrectangle(; low = [-2.5], high = [2.5])
11-
state_abs = StateUniformGridSplit(X, (10,))
12-
input_abs = InputDiscrete([Singleton([0.0])])
13-
14-
if sparse
15-
target_model = SparseOrthogonalIMDPTarget()
16-
else
17-
target_model = OrthogonalIMDPTarget()
7+
@testset "1d dense vs sparse" begin
8+
function simple_1d_decoupled(; sparse = false)
9+
sys, spec = simple_1d_sys()
10+
11+
X = Hyperrectangle(; low = [-2.5], high = [2.5])
12+
state_abs = StateUniformGridSplit(X, (10,))
13+
input_abs = InputDiscrete([Singleton([0.0])])
14+
15+
if sparse
16+
target_model = SparseOrthogonalIMDPTarget()
17+
else
18+
target_model = OrthogonalIMDPTarget()
19+
end
20+
21+
prob = AbstractionProblem(sys, spec)
22+
mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
23+
24+
return mdp, abstract_spec
1825
end
1926

20-
mdp, reach, avoid = abstraction(sys, state_abs, input_abs, target_model)
21-
22-
return mdp, reach, avoid
27+
# Dense
28+
mdp_dense, spec_dense = simple_1d_decoupled()
29+
@test num_states(mdp_dense) == 11
30+
@test stateptr(mdp_dense)[end] == 11
31+
32+
prob_dense = Problem(mdp_dense, spec_dense)
33+
34+
V_dense, k, res = value_iteration(prob_dense)
35+
@test k == 10
36+
37+
# Sparse
38+
mdp_sparse, spec_sparse = simple_1d_decoupled(; sparse = true)
39+
@test num_states(mdp_sparse) == 11
40+
@test stateptr(mdp_sparse)[end] == 11
41+
42+
prob_sparse = Problem(mdp_sparse, spec_sparse)
43+
44+
V_sparse, k, res = value_iteration(prob_sparse)
45+
@test k == 10
46+
@test all(V_dense .≥ V_sparse)
47+
48+
@test satisfaction_mode(spec_dense) == satisfaction_mode(spec_sparse)
49+
@test strategy_mode(spec_dense) == strategy_mode(spec_sparse)
50+
51+
prop_dense = system_property(spec_dense)
52+
prop_sparse = system_property(spec_sparse)
53+
@test all(IntervalMDP.reach(prop_dense) .== IntervalMDP.reach(prop_sparse))
54+
@test all(IntervalMDP.avoid(prop_dense) .== IntervalMDP.avoid(prop_sparse))
2355
end
2456

25-
# Dense
26-
mdp_decoupled, reach_decoupled, avoid_decoupled = simple_1d_decoupled()
27-
@test num_states(mdp_decoupled) == 11
28-
@test stateptr(mdp_decoupled)[end] == 12
29-
30-
prop_decoupled = FiniteTimeReachAvoid(reach_decoupled, avoid_decoupled, 10)
31-
spec_decoupled = Specification(prop_decoupled, Pessimistic, Maximize)
32-
prob_decoupled = Problem(mdp_decoupled, spec_decoupled)
33-
34-
V_dense_grid, k, res = value_iteration(prob_decoupled)
35-
@test k == 10
57+
@testset "2d" begin
58+
function modified_running_example_decoupled(; sparse = false, range_vs_grid = :grid)
59+
sys, spec = modified_running_example_sys()
3660

37-
# Sparse
38-
mdp_decoupled, reach_decoupled, avoid_decoupled = simple_1d_decoupled(; sparse = true)
39-
@test num_states(mdp_decoupled) == 11
40-
@test stateptr(mdp_decoupled)[end] == 12
61+
X = Hyperrectangle(; low = [-10.0, -10.0], high = [10.0, 10.0])
62+
state_abs = StateUniformGridSplit(X, (10, 10))
4163

42-
prop_decoupled = FiniteTimeReachAvoid(reach_decoupled, avoid_decoupled, 10)
43-
spec_decoupled = Specification(prop_decoupled, Pessimistic, Maximize)
44-
prob_decoupled = Problem(mdp_decoupled, spec_decoupled)
64+
U = Hyperrectangle(; low = [-1.0, -1.0], high = [1.0, 1.0])
65+
if range_vs_grid == :range
66+
input_abs = InputLinRange(U, [3, 3])
67+
elseif range_vs_grid == :grid
68+
input_abs = InputGridSplit(U, [3, 3])
69+
else
70+
throw(ArgumentError("Invalid range_vs_grid argument"))
71+
end
4572

46-
V_sparse_grid, k, res = value_iteration(prob_decoupled)
47-
@test k == 10
48-
@test all(V_dense_grid .≥ V_sparse_grid)
73+
if sparse
74+
target_model = SparseOrthogonalIMDPTarget()
75+
else
76+
target_model = OrthogonalIMDPTarget()
77+
end
4978

50-
function modified_running_example_decoupled(; sparse = false, range_vs_grid = :grid)
51-
sys = modified_running_example_sys()
79+
prob = AbstractionProblem(sys, spec)
80+
mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
5281

53-
X = Hyperrectangle(; low = [-10.0, -10.0], high = [10.0, 10.0])
54-
state_abs = StateUniformGridSplit(X, (10, 10))
55-
56-
U = Hyperrectangle(; low = [-1.0, -1.0], high = [1.0, 1.0])
57-
if range_vs_grid == :range
58-
input_abs = InputLinRange(U, [3, 3])
59-
elseif range_vs_grid == :grid
60-
input_abs = InputGridSplit(U, [3, 3])
61-
else
62-
throw(ArgumentError("Invalid range_vs_grid argument"))
82+
return mdp, abstract_spec
6383
end
6484

65-
if sparse
66-
target_model = SparseOrthogonalIMDPTarget()
67-
else
68-
target_model = OrthogonalIMDPTarget()
85+
@testset "dense vs sparse" begin
86+
# Dense, input grid
87+
mdp_dense, spec_dense = modified_running_example_decoupled()
88+
@test num_states(mdp_dense) == 121 # 11 * 11 total states
89+
@test stateptr(mdp_dense)[end] == 10 * 10 * 9 + 1 # 10 * 10 non-sink states, 9 actions
90+
91+
prob_dense = Problem(mdp_dense, spec_dense)
92+
93+
V_dense, k, res = value_iteration(prob_dense)
94+
@test k == 10
95+
96+
# Sparse, input grid
97+
mdp_sparse, spec_sparse = modified_running_example_decoupled(; sparse = true)
98+
@test num_states(mdp_sparse) == 121 # 11 * 11 total states
99+
@test stateptr(mdp_sparse)[end] == 10 * 10 * 9 + 1 # 10 * 10 non-sink states, 9 actions
100+
101+
prob_sparse = Problem(mdp_sparse, spec_sparse)
102+
103+
V_sparse, k, res = value_iteration(prob_sparse)
104+
@test k == 10
105+
@test all(V_dense .≥ V_sparse)
106+
107+
@test satisfaction_mode(spec_dense) == satisfaction_mode(spec_sparse)
108+
@test strategy_mode(spec_dense) == strategy_mode(spec_sparse)
109+
110+
prop_dense = system_property(spec_dense)
111+
prop_sparse = system_property(spec_sparse)
112+
@test all(IntervalMDP.reach(prop_dense) .== IntervalMDP.reach(prop_sparse))
113+
@test all(IntervalMDP.avoid(prop_dense) .== IntervalMDP.avoid(prop_sparse))
69114
end
70115

71-
mdp, reach, avoid = abstraction(sys, state_abs, input_abs, target_model)
72-
73-
return mdp, reach, avoid
74-
end
75-
76-
# Dense, input grid
77-
mdp_decoupled, reach_decoupled, avoid_decoupled = modified_running_example_decoupled()
78-
@test num_states(mdp_decoupled) == 121
79-
@test stateptr(mdp_decoupled)[end] == 11 * 11 + 10 * 10 * 8 + 1
80-
81-
prop_decoupled = FiniteTimeReachAvoid(reach_decoupled, avoid_decoupled, 10)
82-
spec_decoupled = Specification(prop_decoupled, Pessimistic, Maximize)
83-
prob_decoupled = Problem(mdp_decoupled, spec_decoupled)
84-
85-
V_dense_grid, k, res = value_iteration(prob_decoupled)
86-
@test k == 10
87-
88-
# Sparse, input grid
89-
mdp_decoupled, reach_decoupled, avoid_decoupled =
90-
modified_running_example_decoupled(; sparse = true)
91-
@test num_states(mdp_decoupled) == 121
92-
@test stateptr(mdp_decoupled)[end] == 11 * 11 + 10 * 10 * 8 + 1
93-
94-
prop_decoupled = FiniteTimeReachAvoid(reach_decoupled, avoid_decoupled, 10)
95-
spec_decoupled = Specification(prop_decoupled, Pessimistic, Maximize)
96-
prob_decoupled = Problem(mdp_decoupled, spec_decoupled)
97-
98-
V_sparse_grid, k, res = value_iteration(prob_decoupled)
99-
@test k == 10
100-
@test all(V_dense_grid .≥ V_sparse_grid)
101-
102-
# Dense, input range
103-
mdp_decoupled, reach_decoupled, avoid_decoupled =
104-
modified_running_example_decoupled(; range_vs_grid = :range)
105-
@test num_states(mdp_decoupled) == 121
106-
@test stateptr(mdp_decoupled)[end] == 11 * 11 + 10 * 10 * 8 + 1
107-
108-
prop_decoupled = FiniteTimeReachAvoid(reach_decoupled, avoid_decoupled, 10)
109-
spec_decoupled = Specification(prop_decoupled, Pessimistic, Maximize)
110-
prob_decoupled = Problem(mdp_decoupled, spec_decoupled)
111-
112-
V_range, k, res = value_iteration(prob_decoupled)
113-
@test k == 10
114-
@test all(V_range .≥ V_dense_grid)
116+
@testset "dense grid vs range" begin
117+
# Dense, input grid
118+
mdp_grid, spec_grid = modified_running_example_decoupled(; range_vs_grid = :grid)
119+
120+
prob_grid = Problem(mdp_grid, spec_grid)
121+
V_grid, k, res = value_iteration(prob_grid)
122+
123+
# Dense, input range
124+
mdp_range, spec_range = modified_running_example_decoupled(; range_vs_grid = :range)
125+
@test num_states(mdp_range) == 121 # 11 * 11 total states
126+
@test stateptr(mdp_range)[end] == 10 * 10 * 9 + 1 # 10 * 10 non-sink states, 9 actions
127+
128+
prob_range = Problem(mdp_range, spec_range)
129+
V_range, k, res = value_iteration(prob_range)
130+
131+
@test k == 10
132+
@test all(V_range .≥ V_grid)
133+
134+
@test satisfaction_mode(spec_grid) == satisfaction_mode(spec_range)
135+
@test strategy_mode(spec_grid) == strategy_mode(spec_range)
136+
137+
prop_grid = system_property(spec_grid)
138+
prop_range = system_property(spec_range)
139+
@test all(IntervalMDP.reach(prop_grid) .== IntervalMDP.reach(prop_range))
140+
@test all(IntervalMDP.avoid(prop_grid) .== IntervalMDP.avoid(prop_range))
141+
end
142+
end

0 commit comments

Comments
 (0)