From 3ad899219d176aabaf52236e88c16c1fe2325d2c Mon Sep 17 00:00:00 2001 From: bkraske Date: Sun, 24 Nov 2024 16:47:58 -0700 Subject: [PATCH 1/2] Use `abs` in convergence check --- src/value_iteration.jl | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/value_iteration.jl b/src/value_iteration.jl index fc64365..46cf153 100644 --- a/src/value_iteration.jl +++ b/src/value_iteration.jl @@ -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)) From b182859f5ed3e95281fa9c93b50bd65f22b48594 Mon Sep 17 00:00:00 2001 From: Frederik Baymler Mathiesen Date: Tue, 26 Nov 2024 12:29:42 +0100 Subject: [PATCH 2/2] Add tests and format --- src/synthesis.jl | 5 ++-- src/value_iteration.jl | 12 ++++++--- test/base/vi.jl | 30 +++++++++++++++++++--- test/cuda/dense/vi.jl | 58 +++++++++++++++++++++++++++++++++++++++--- test/cuda/sparse/vi.jl | 58 ++++++++++++++++++++++++++++++++++++++++-- test/sparse/vi.jl | 55 +++++++++++++++++++++++++++++++++++++++ 6 files changed, 204 insertions(+), 14 deletions(-) diff --git a/src/synthesis.jl b/src/synthesis.jl index 7fa57d9..971b423 100644 --- a/src/synthesis.jl +++ b/src/synthesis.jl @@ -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) @@ -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 diff --git a/src/value_iteration.jl b/src/value_iteration.jl index 46cf153..2fa1e0c 100644 --- a/src/value_iteration.jl +++ b/src/value_iteration.jl @@ -14,7 +14,7 @@ termination_criteria(prop, finitetime::Val{true}) = struct CovergenceCriteria{T <: AbstractFloat} <: TerminationCriteria tol::T end -(f::CovergenceCriteria)(V, k, u) = maximum(abs,u) < f.tol +(f::CovergenceCriteria)(V, k, u) = maximum(abs, u) < f.tol termination_criteria(prop, finitetime::Val{false}) = CovergenceCriteria(convergence_eps(prop)) @@ -73,9 +73,9 @@ 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 @@ -83,7 +83,11 @@ whichstrategyconfig(::Problem{S, F, <:NoStrategy}) where {S, F} = NoStrategyConf 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) diff --git a/test/base/vi.jl b/test/base/vi.jl index 7882ec7..5552b35 100644 --- a/test/base/vi.jl +++ b/test/base/vi.jl @@ -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) @@ -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 diff --git a/test/cuda/dense/vi.jl b/test/cuda/dense/vi.jl index b7bfdc4..36ae914 100644 --- a/test/cuda/dense/vi.jl +++ b/test/cuda/dense/vi.jl @@ -21,12 +21,14 @@ 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) @@ -34,25 +36,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 = 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 diff --git a/test/cuda/sparse/vi.jl b/test/cuda/sparse/vi.jl index ecbb28d..c804fd5 100644 --- a/test/cuda/sparse/vi.jl +++ b/test/cuda/sparse/vi.jl @@ -15,18 +15,19 @@ 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) @@ -34,21 +35,74 @@ 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 diff --git a/test/sparse/vi.jl b/test/sparse/vi.jl index 0065bc8..8544a20 100644 --- a/test/sparse/vi.jl +++ b/test/sparse/vi.jl @@ -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) @@ -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