Skip terminal states of DFA properties in bellman!

src/bellman.jl

@@ -78,6 +78,7 @@ function bellman(
     alg::BellmanAlgorithm = default_bellman_algorithm(model);
     upper_bound = false,
     maximize = true,
+    prop = nothing,
 )
     Vres = similar(V, source_shape(model))
 
@@ -89,6 +90,7 @@ function bellman(
         alg;
         upper_bound = upper_bound,
         maximize = maximize,
+        prop = prop,
     )
 end
 
@@ -179,6 +181,7 @@ function bellman!(
     alg::BellmanAlgorithm = default_bellman_algorithm(model);
     upper_bound = false,
     maximize = true,
+    prop = nothing,
 )
     workspace = construct_workspace(model, alg)
     strategy_cache = construct_strategy_cache(model)
@@ -192,6 +195,7 @@ function bellman!(
         avail_act;
         upper_bound = upper_bound,
         maximize = maximize,
+        prop = prop,
     )
 end
 
@@ -204,6 +208,7 @@ function bellman!(
     avail_act::AbstractAvailableActions = available_actions(model);
     upper_bound = false,
     maximize = true,
+    prop = nothing,
 )
     return _bellman_helper!(
         workspace,
@@ -226,6 +231,7 @@ function bellman!(
     avail_act::AbstractAvailableActions = available_actions(model);
     upper_bound = false,
     maximize = true,
+    prop = nothing,
 )
     mp = markov_process(model)
     lf = labelling_function(model)
@@ -242,6 +248,7 @@ function bellman!(
         avail_act;
         upper_bound = upper_bound,
         maximize = maximize,
+        prop = prop,
     )
 end
 
@@ -256,10 +263,16 @@ function _bellman_helper!(
     avail_act;
     upper_bound = false,
     maximize = true,
+    prop = nothing,
 )
     W = workspace.intermediate_values
 
     @inbounds for state in dfa
+        # If a DFA property is given, skip terminal states
+        if !isnothing(prop) && state ∈ terminal(prop)
+            continue
+        end
+
         local_strategy_cache = localize_strategy_cache(strategy_cache, state)
 
         # Select the value function for the current DFA state
@@ -296,10 +309,16 @@ function _bellman_helper!(
     avail_act;
     upper_bound = false,
     maximize = true,
+    prop = nothing,
 ) where {R}
     W = workspace.intermediate_values
 
     @inbounds for state in dfa
+        # If a DFA property is given, skip terminal states
+        if !isnothing(prop) && state ∈ terminal(prop)
+            continue
+        end
+
         local_strategy_cache = localize_strategy_cache(strategy_cache, state)
 
         # Select the value function for the current DFA state

src/problem.jl

@@ -31,7 +31,7 @@ struct VerificationProblem{
         strategy::C,
     ) where {S <: StochasticProcess, F <: Specification, C <: AbstractStrategy}
         checkspecification(spec, system, strategy)
-        checkstrategy(strategy, system)
+        checkstrategy(strategy, system, system_property(spec))
         return new{S, F, C}(system, spec, strategy)
     end
 end

src/robust_value_iteration.jl

@@ -190,6 +190,7 @@ function _value_iteration!(problem::AbstractIntervalMDPProblem, alg; callback =
         mp;
         upper_bound = upper_bound,
         maximize = maximize,
+        prop = system_property(spec),
     )
     step_postprocess_value_function!(value_function, spec)
     step_postprocess_strategy_cache!(strategy_cache)
@@ -210,6 +211,7 @@ function _value_iteration!(problem::AbstractIntervalMDPProblem, alg; callback =
             mp;
             upper_bound = upper_bound,
             maximize = maximize,
+            prop = system_property(spec),
         )
         step_postprocess_value_function!(value_function, spec)
         step_postprocess_strategy_cache!(strategy_cache)
@@ -255,7 +257,16 @@ function nextiteration!(V)
     return V
 end
 
-function step!(workspace, strategy_cache, value_function, k, mp; upper_bound, maximize)
+function step!(
+    workspace,
+    strategy_cache,
+    value_function,
+    k,
+    mp;
+    upper_bound,
+    maximize,
+    prop,
+)
     bellman!(
         workspace,
         select_strategy_cache(strategy_cache, k),
@@ -265,6 +276,7 @@ function step!(workspace, strategy_cache, value_function, k, mp; upper_bound, ma
         select_available_actions(available_actions(mp), k);
         upper_bound = upper_bound,
         maximize = maximize,
+        prop = prop,
     )
 end
 

src/specification.jl

@@ -144,6 +144,7 @@ time_horizon(prop::FiniteTimeDFAReachability) = prop.time_horizon
 Return the set of DFA states with respect to which to compute reachbility for a finite time DFA reachability property.
 """
 reach(prop::FiniteTimeDFAReachability) = prop.reach
+terminal(prop::FiniteTimeDFAReachability) = reach(prop)
 
 function showproperty(io::IO, first_prefix, prefix, prop::FiniteTimeDFAReachability)
     println(io, first_prefix, styled"{code:FiniteTimeDFAReachability}")
@@ -193,6 +194,7 @@ convergence_eps(prop::InfiniteTimeDFAReachability) = prop.convergence_eps
 Return the set of DFA states with respect to which to compute reachbility for a infinite time DFA reachability property.
 """
 reach(prop::InfiniteTimeDFAReachability) = prop.reach
+terminal(prop::InfiniteTimeDFAReachability) = reach(prop)
 
 function showproperty(io::IO, first_prefix, prefix, prop::InfiniteTimeDFAReachability)
     println(io, first_prefix, styled"{code:InfiniteTimeDFAReachability}")
@@ -277,6 +279,7 @@ time_horizon(prop::FiniteTimeDFASafety) = prop.time_horizon
 Return the set of DFA states with respect to which to compute safety for a finite time DFA safety property.
 """
 avoid(prop::FiniteTimeDFASafety) = prop.avoid
+terminal(prop::FiniteTimeDFASafety) = avoid(prop)
 
 function showproperty(io::IO, first_prefix, prefix, prop::FiniteTimeDFASafety)
     println(io, first_prefix, styled"{code:FiniteTimeDFASafety}")
@@ -325,6 +328,7 @@ convergence_eps(prop::InfiniteTimeDFASafety) = prop.convergence_eps
 Return the set of DFA states with respect to which to compute safety for a infinite time DFA safety property.
 """
 avoid(prop::InfiniteTimeDFASafety) = prop.avoid
+terminal(prop::InfiniteTimeDFASafety) = avoid(prop)
 
 function showproperty(io::IO, first_prefix, prefix, prop::InfiniteTimeDFASafety)
     println(io, first_prefix, styled"{code:InfiniteTimeDFASafety}")

src/strategy.jl

@@ -1,7 +1,7 @@
 abstract type AbstractStrategy end
 
 struct NoStrategy <: AbstractStrategy end
-checkstrategy(::NoStrategy, system) = nothing
+checkstrategy(::NoStrategy, system, prop = nothing) = nothing
 
 """
     StationaryStrategy
@@ -14,20 +14,25 @@ end
 Base.getindex(strategy::StationaryStrategy, k) = strategy.strategy
 time_length(::StationaryStrategy) = typemax(Int64)
 
-function checkstrategy(strategy::StationaryStrategy, system)
-    checkstrategy(strategy.strategy, system)
+function checkstrategy(strategy::StationaryStrategy, system, prop = nothing)
+    checkstrategy(strategy.strategy, system, prop)
 end
 
-function checkstrategy(strategy::AbstractArray, system::ProductProcess)
+function checkstrategy(strategy::AbstractArray, system::ProductProcess, prop = nothing)
     mp = markov_process(system)
     dfa = automaton(system)
 
     for state in dfa
-        checkstrategy(selectdim(strategy, ndims(strategy), state), mp)
+        # If a DFA property is given, skip terminal states
+        if !isnothing(prop) && state ∈ terminal(prop)
+            continue
+        end
+
+        checkstrategy(selectdim(strategy, ndims(strategy), state), mp, prop)
     end
 end
 
-function checkstrategy(strategy::AbstractArray, system::FactoredRMDP)
+function checkstrategy(strategy::AbstractArray, system::FactoredRMDP, prop = nothing)
     if size(strategy) != source_shape(system)
         throw(
             DimensionMismatch(
@@ -77,9 +82,9 @@ end
 Base.getindex(strategy::TimeVaryingStrategy, k) = strategy.strategy[k]
 time_length(strategy::TimeVaryingStrategy) = length(strategy.strategy)
 
-function checkstrategy(strategy::TimeVaryingStrategy, system)
+function checkstrategy(strategy::TimeVaryingStrategy, system, prop = nothing)
     for strategy_step in strategy.strategy
-        checkstrategy(strategy_step, system)
+        checkstrategy(strategy_step, system, prop)
     end
 end