Merge pull request #72 from bkraske/main

Use `abs` in convergence check

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

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))
 
@@ -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)

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

test/cuda/dense/vi.jl

@@ -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

test/cuda/sparse/vi.jl

@@ -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

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