Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Use abs in convergence check #72

Merged
merged 2 commits into from
Nov 26, 2024
Merged

Use abs in convergence check #72

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
3ad8992
Use `abs` in convergence check
bkraske Nov 24, 2024
b182859
Add tests and format
Zinoex Nov 26, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
5 changes: 3 additions & 2 deletions src/synthesis.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ If the specification is infinite time, then the strategy is stationary and only
It is possible to provide a callback function that will be called at each iteration with the current value function and
iteration count. The callback function should have the signature `callback(V::AbstractArray, k::Int)`.
"""
function control_synthesis(problem::Problem; callback=nothing)
function control_synthesis(problem::Problem; callback = nothing)
spec = specification(problem)
prop = system_property(spec)

Expand All @@ -18,7 +18,8 @@ function control_synthesis(problem::Problem; callback=nothing)

strategy_config =
isfinitetime(prop) ? TimeVaryingStrategyConfig() : StationaryStrategyConfig()
V, k, res, strategy_cache = _value_iteration!(strategy_config, problem; callback=callback)
V, k, res, strategy_cache =
_value_iteration!(strategy_config, problem; callback = callback)

return cachetostrategy(strategy_cache), V, k, res
end
12 changes: 8 additions & 4 deletions src/value_iteration.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@ termination_criteria(prop, finitetime::Val{true}) =
struct CovergenceCriteria{T <: AbstractFloat} <: TerminationCriteria
tol::T
end
(f::CovergenceCriteria)(V, k, u) = maximum(u) < f.tol
(f::CovergenceCriteria)(V, k, u) = maximum(abs, u) < f.tol
termination_criteria(prop, finitetime::Val{false}) =
CovergenceCriteria(convergence_eps(prop))

Expand Down Expand Up @@ -73,17 +73,21 @@ V, k, residual = value_iteration(problem)
```

"""
function value_iteration(problem::Problem; callback=nothing)
function value_iteration(problem::Problem; callback = nothing)
strategy_config = whichstrategyconfig(problem)
V, k, res, _ = _value_iteration!(strategy_config, problem; callback=callback)
V, k, res, _ = _value_iteration!(strategy_config, problem; callback = callback)

return V, k, res
end
whichstrategyconfig(::Problem{S, F, <:NoStrategy}) where {S, F} = NoStrategyConfig()
whichstrategyconfig(::Problem{S, F, <:AbstractStrategy}) where {S, F} =
GivenStrategyConfig()

function _value_iteration!(strategy_config::AbstractStrategyConfig, problem::Problem; callback=nothing)
function _value_iteration!(
strategy_config::AbstractStrategyConfig,
problem::Problem;
callback = nothing,
)
mp = system(problem)
spec = specification(problem)
term_criteria = termination_criteria(spec)
Expand Down
30 changes: 27 additions & 3 deletions test/base/vi.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,14 @@ V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeReachAvoid([3], [2], 11)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 11
@test all(V_fixed_it2 .>= 0.0)
@test all(V_fixed_it .<= V_fixed_it2)

prop = InfiniteTimeReachAvoid([3], [2], 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
Expand Down Expand Up @@ -83,6 +91,22 @@ V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

# problem = Problem(mc, InfiniteTimeReward([2.0, 1.0, 0.0], 0.9, 1e-6))
# V_conv, _, u = value_iteration(problem)
# @test maximum(u) <= 1e-6
prop = FiniteTimeReward([2.0, 1.0, -1.0], 0.9, 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it2 .<= V_fixed_it)

prop = InfiniteTimeReward([2.0, 1.0, 0.0], 0.9, 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = InfiniteTimeReward([2.0, 1.0, -1.0], 0.9, 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
58 changes: 55 additions & 3 deletions test/cuda/dense/vi.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,38 +21,90 @@ spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeReachability([3], 11)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 11
@test all(V_fixed_it2 .>= 0.0)
@test all(V_fixed_it .<= V_fixed_it2)

prop = InfiniteTimeReachability([3], 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = FiniteTimeReachAvoid([3], [2], 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeReachAvoid([3], [2], 11)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 11
@test all(V_fixed_it2 .>= 0.0)
@test all(V_fixed_it .<= V_fixed_it2)

prop = InfiniteTimeReachAvoid([3], [2], 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = FiniteTimeSafety([3], 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeSafety([3], 11)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 11
@test all(V_fixed_it2 .>= 0.0)
@test all(V_fixed_it2 .<= V_fixed_it)

prop = InfiniteTimeSafety([3], 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = IntervalMDP.cu(FiniteTimeReward([2.0, 1.0, 0.0], 0.9, 10))
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

# problem = Problem(mc, InfiniteTimeReward([2.0, 1.0, 0.0], 0.9, 1e-6))
# V_conv, _, u = value_iteration(problem)
# @test maximum(u) <= 1e-6
prop = IntervalMDP.cu(FiniteTimeReward([2.0, 1.0, -1.0], 0.9, 10))
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it2 .<= V_fixed_it)

prop = IntervalMDP.cu(InfiniteTimeReward([2.0, 1.0, 0.0], 0.9, 1e-6))
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = IntervalMDP.cu(InfiniteTimeReward([2.0, 1.0, -1.0], 0.9, 1e-6))
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
58 changes: 56 additions & 2 deletions test/cuda/sparse/vi.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,40 +15,94 @@ prob = IntervalProbabilities(;
)

mc = IntervalMDP.cu(IntervalMarkovChain(prob, [1]))

prop = FiniteTimeReachability([3], 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeReachability([3], 11)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 11
@test all(V_fixed_it2 .>= 0.0)
@test all(V_fixed_it .<= V_fixed_it2)

prop = InfiniteTimeReachability([3], 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = FiniteTimeReachAvoid([3], [2], 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeReachAvoid([3], [2], 11)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 11
@test all(V_fixed_it2 .>= 0.0)
@test all(V_fixed_it .<= V_fixed_it2)

prop = InfiniteTimeReachAvoid([3], [2], 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = FiniteTimeReward(IntervalMDP.cu([2.0, 1.0, 0.0]), 0.9, 10)
prop = FiniteTimeSafety([3], 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeSafety([3], 11)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 11
@test all(V_fixed_it2 .>= 0.0)
@test all(V_fixed_it2 .<= V_fixed_it)

prop = InfiniteTimeSafety([3], 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = IntervalMDP.cu(FiniteTimeReward([2.0, 1.0, 0.0], 0.9, 10))
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = IntervalMDP.cu(FiniteTimeReward([2.0, 1.0, -1.0], 0.9, 10))
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10

prop = IntervalMDP.cu(InfiniteTimeReward([2.0, 1.0, 0.0], 0.9, 1e-6))
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = IntervalMDP.cu(InfiniteTimeReward([2.0, 1.0, -1.0], 0.9, 1e-6))
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
55 changes: 55 additions & 0 deletions test/sparse/vi.jl
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,7 @@ spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeReachability([3], 11)
spec = Specification(prop, Pessimistic)
Expand All @@ -34,21 +35,75 @@ spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = FiniteTimeReachAvoid([3], [2], 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeReachAvoid([3], [2], 11)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 11
@test all(V_fixed_it2 .>= 0.0)
@test all(V_fixed_it .<= V_fixed_it2)

prop = InfiniteTimeReachAvoid([3], [2], 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = FiniteTimeSafety([3], 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeSafety([3], 11)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 11
@test all(V_fixed_it2 .>= 0.0)
@test all(V_fixed_it2 .<= V_fixed_it)

prop = InfiniteTimeSafety([3], 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = FiniteTimeReward([2.0, 1.0, 0.0], 0.9, 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it .>= 0.0)

prop = FiniteTimeReward([2.0, 1.0, -1.0], 0.9, 10)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_fixed_it2, k, _ = value_iteration(problem)
@test k == 10
@test all(V_fixed_it2 .<= V_fixed_it)

prop = InfiniteTimeReward([2.0, 1.0, 0.0], 0.9, 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
@test all(V_conv .>= 0.0)

prop = InfiniteTimeReward([2.0, 1.0, -1.0], 0.9, 1e-6)
spec = Specification(prop, Pessimistic)
problem = Problem(mc, spec)
V_conv, _, u = value_iteration(problem)
@test maximum(u) <= 1e-6
Loading