Use new sink state encoding in IntervalMDP

Author: Zinoex

examples/systems/almost_identity.jl

@@ -96,7 +96,7 @@ function main(n)
     @time "value iteration" V, k, res = value_iteration(prob)
 
     # Remove the first state from each axis (the avoid state, whose value is always 0).
-    V = V[(2:d for d in size(V))...]
+    V = V[(1:d-1 for d in size(V))...]
 
     return V
 end

examples/systems/bas_4d.jl

@@ -111,7 +111,7 @@ function main()
     @time "value iteration" V_safety, k, res = value_iteration(prob)
 
     # Remove the first state from each axis (the avoid state, whose value is always 0).
-    V_safety = V_safety[(2:d for d in size(V_safety))...]
+    V_safety = V_safety[(1:d-1 for d in size(V_safety))...]
 
     return V_safety
 end

examples/systems/big.jl

@@ -133,7 +133,7 @@ function small_direct(
 end
 
 function main(n)
-    @time "abstraction" mdp, spec, _ = small_direct(; sparse = false)
+    @time "abstraction" mdp, spec, _ = big_decoupled(n; sparse = false)
 
     println("Memory usage: $(Base.summarysize(mdp) / 1000^2) MB")
 
@@ -142,7 +142,7 @@ function main(n)
     @time "value iteration" V, k, res = value_iteration(prob)
 
     # Remove the first state from each axis (the avoid state, whose value is always 0).
-    V = V[(2:d for d in size(V))...]
+    V = V[(1:d-1 for d in size(V))...]
 
     return V
 end

examples/systems/car_parking.jl

@@ -110,7 +110,7 @@ function main()
     @time "value iteration decoupled" V_decoupled, k_decoupled, res_decoupled =
         value_iteration(prob_decoupled)
 
-    V_diff = V_decoupled[2:end, 2:end] - reshape(V_direct[2:end], 20, 20)
+    V_diff = V_decoupled[1:end-1, 1:end-1] - reshape(V_direct[1:end-1], 20, 20)
 
-    return V_diff, V_decoupled[2:end, 2:end], reshape(V_direct[2:end], 20, 20)
+    return V_diff, V_decoupled[1:end-1, 1:end-1], reshape(V_direct[1:end-1], 20, 20)
 end

examples/systems/linear_stochastically_switched.jl

@@ -106,8 +106,8 @@ function main()
     @time "upper bound" V_upper, _, _ = value_iteration(upper_bound_prob)
 
     # Remove the first state from each axis (the avoid state, whose value is always 0).
-    V_lower = V_lower[(2:d for d in size(V_lower))...]
-    V_upper = V_upper[(2:d for d in size(V_upper))...]
+    V_lower = V_lower[(1:d-1 for d in size(V_lower))...]
+    V_upper = V_upper[(1:d-1 for d in size(V_upper))...]
 
     return V_lower, V_upper
 end

examples/systems/robot_2d.jl

@@ -134,7 +134,7 @@ function main()
 
     @time "value-iteration reach-avoid" V_reachavoid, k_reachavoid, res_reachavoid =
         value_iteration(prob_reachavoid)
-    V_reachavoid = V_reachavoid[2:end, 2:end]
+    V_reachavoid = V_reachavoid[1:d-1, 1:d-1]
 
     @time "abstraction reachability" mdp_reachability, spec_reachability, _ =
         robot_2d_decoupled(;
@@ -146,7 +146,7 @@ function main()
 
     @time "value-iteration reachability" V_reachability, k_reachability, res_reachability =
         value_iteration(prob_reachability)
-    V_reachability = V_reachability[2:end, 2:end]
+    V_reachability = V_reachability[1:d-1, 1:d-1]
 
     return V_reachavoid, V_reachability
 end

examples/systems/van_der_pol.jl

@@ -117,5 +117,5 @@ function main()
     prob = Problem(mdp, spec)
 
     @time "value iteration" V, k, res = value_iteration(prob)
-    return V[2:end, 2:end]
+    return V[1:d-1, 1:d-1]
 end

src/abstractions/abstraction.jl

@@ -91,8 +91,8 @@ function abstraction(
 
     # State pointer
     stateptr = Int32[
-        [1, 2]
-        (1:numregions(state_abstraction)) .* numinputs(input_abstraction) .+ 2
+        [1]
+        (1:numregions(state_abstraction)) .* numinputs(input_abstraction) .+ 1
     ]
 
     # Transition probabilities
@@ -108,7 +108,7 @@ function abstraction(
     initial_states = Int32[]
     for (i, source_region) in enumerate(regions(state_abstraction))
         if !isdisjoint(initial(sys), source_region)
-            push!(initial_states, i + 1)
+            push!(initial_states, i)
         end
     end
 
@@ -121,15 +121,17 @@ function abstraction(
 end
 
 function initprob(::IMDPTarget, nregions, ninputs)
-    prob_lower = [zeros(Float64, nregions) for _ = 1:((nregions-1)*ninputs+1)]
-    prob_upper = [zeros(Float64, nregions) for _ = 1:((nregions-1)*ninputs+1)]
+    nchoices = nregions * ninputs
+    prob_lower = zeros(Float64, nregions + 1, nchoices)
+    prob_upper = zeros(Float64, nregions + 1, nchoices)
 
     return prob_lower, prob_upper
 end
 
 function initprob(::SparseIMDPTarget, nregions, ninputs)
-    prob_lower = [spzeros(Float64, nregions) for _ = 1:((nregions-1)*ninputs+1)]
-    prob_upper = [spzeros(Float64, nregions) for _ = 1:((nregions-1)*ninputs+1)]
+    nchoices = nregions * ninputs
+    prob_lower = spzeros(Float64, nregions + 1, nchoices)
+    prob_upper = spzeros(Float64, nregions + 1, nchoices)
 
     return prob_lower, prob_upper
 end
@@ -142,13 +144,13 @@ function convert_property(
     prop = system_property(spec)
 
     reach_states = Int32[]
-    avoid_states = Int32[1]  # Absorbing state
+    avoid_states = Int32[numregions(state_abstraction)]  # Absorbing state
 
     for (i, source_region) in enumerate(regions(state_abstraction))
         if ispessimistic(spec) && source_region ⊆ reach(prop)
-            push!(reach_states, i + 1)
+            push!(reach_states, i)
         elseif isoptimistic(spec) && !iszeromeasure(reach(prop), source_region)
-            push!(reach_states, i + 1)
+            push!(reach_states, i)
         end
     end
 
@@ -163,17 +165,17 @@ function convert_property(
     prop = system_property(spec)
 
     reach_states = Int32[]
-    avoid_states = Int32[1]  # Absorbing state
+    avoid_states = Int32[numregions(state_abstraction)]  # Absorbing state
 
     for (i, source_region) in enumerate(regions(state_abstraction))
         if ispessimistic(spec) && !iszeromeasure(avoid(prop), source_region)
-            push!(avoid_states, i + 1)
+            push!(avoid_states, i)
         elseif isoptimistic(spec) && source_region ⊆ avoid(prop)
-            push!(avoid_states, i + 1)
+            push!(avoid_states, i)
         elseif ispessimistic(spec) && source_region ⊆ reach(prop)
-            push!(reach_states, i + 1)
+            push!(reach_states, i)
         elseif isoptimistic(spec) && !iszeromeasure(reach(prop), source_region)
-            push!(reach_states, i + 1)
+            push!(reach_states, i)
         end
     end
 
@@ -187,13 +189,13 @@ function convert_property(
 )
     prop = system_property(spec)
 
-    avoid_states = Int32[1]  # Absorbing state
+    avoid_states = Int32[numregions(state_abstraction)]  # Absorbing state
 
     for (i, source_region) in enumerate(regions(state_abstraction))
         if ispessimistic(spec) && !iszeromeasure(avoid(prop), source_region)
-            push!(avoid_states, i + 1)
+            push!(avoid_states, i)
         elseif isoptimistic(spec) && source_region ⊆ avoid(prop)
-            push!(avoid_states, i + 1)
+            push!(avoid_states, i)
         end
     end
 
@@ -220,14 +222,10 @@ function abstraction(
 
     # State pointer
     stateptr = Int32[1]
-    sizehint!(stateptr, prod(splits(state_abstraction) .+ 1))
+    sizehint!(stateptr, prod(splits(state_abstraction)) + 1)
 
-    for I in CartesianIndices(splits(state_abstraction) .+ 1)
-        if any(Tuple(I) .== 1)
-            push!(stateptr, stateptr[end] + 1)
-        else
-            push!(stateptr, stateptr[end] + numinputs(input_abstraction))
-        end
+    for I in CartesianIndices(splits(state_abstraction))
+        push!(stateptr, stateptr[end] + numinputs(input_abstraction))
     end
 
     interval_prob = transition_prob(
@@ -239,11 +237,11 @@ function abstraction(
     )
 
     # Initial states
-    initial_states = NTuple{dimstate(sys),Int32}[]
+    initial_states = CartesianIndex{dimstate(sys)}[]
     for (I, source_region) in
         zip(CartesianIndices(splits(state_abstraction)), regions(state_abstraction))
         if !isdisjoint(initial(sys), source_region)
-            push!(initial_states, Tuple(I) .+ 1)
+            push!(initial_states, I)
         end
     end
 
@@ -259,9 +257,7 @@ function initprob(::OrthogonalIMDPTarget, state_abstraction::StateUniformGridSpl
     prob_lower = Matrix{Float64}[]
     prob_upper = Matrix{Float64}[]
 
-    # One action for non-absorbing states is already included in the first term.
-    nchoices =
-        prod(splits(state_abstraction) .+ 1) + numregions(state_abstraction) * (ninputs - 1)
+    nchoices = numregions(state_abstraction) * ninputs
 
     for axisregions in splits(state_abstraction)
         local_prob_lower = zeros(Float64, axisregions + 1, nchoices)
@@ -282,9 +278,7 @@ function initprob(
     prob_lower = SparseMatrixCSC{Float64, Int32}[]
     prob_upper = SparseMatrixCSC{Float64, Int32}[]
 
-    # One action for non-absorbing states is already included in the first term.
-    nchoices =
-        prod(splits(state_abstraction) .+ 1) + numregions(state_abstraction) * (ninputs - 1)
+    nchoices = numregions(state_abstraction) * ninputs
 
     for axisregions in splits(state_abstraction)
         local_prob_lower = spzeros(Float64, Int32, axisregions + 1, nchoices)
@@ -304,22 +298,23 @@ function convert_property(
 )
     prop = system_property(spec)
 
-    reach_states = NTuple{dim(prop),Int32}[]
-    avoid_states = NTuple{dim(prop),Int32}[]
+    reach_states = CartesianIndex{dim(prop)}[]
+    avoid_states = CartesianIndex{dim(prop)}[]
 
     # Absorbing states
-    for I in CartesianIndices(splits(state_abstraction) .+ 1)
-        if any(Tuple(I) .== 1)
-            push!(avoid_states, Tuple(I))
+    extended_states = splits(state_abstraction) .+ 1
+    for I in CartesianIndices(extended_states)
+        if any(Tuple(I) .== extended_states)
+            push!(avoid_states, I)
         end
     end
 
     for (I, source_region) in
         zip(CartesianIndices(splits(state_abstraction)), regions(state_abstraction))
         if ispessimistic(spec) && source_region ⊆ reach(prop)
-            push!(reach_states, Tuple(I) .+ 1)
+            push!(reach_states, I)
         elseif isoptimistic(spec) && !iszeromeasure(reach(prop), source_region)
-            push!(reach_states, Tuple(I) .+ 1)
+            push!(reach_states, I)
         end
     end
 
@@ -333,26 +328,27 @@ function convert_property(
 )
     prop = system_property(spec)
 
-    reach_states = NTuple{dim(prop),Int32}[]
-    avoid_states = NTuple{dim(prop),Int32}[]
+    reach_states = CartesianIndex{dim(prop)}[]
+    avoid_states = CartesianIndex{dim(prop)}[]
 
     # Absorbing states
-    for I in CartesianIndices(splits(state_abstraction) .+ 1)
-        if any(Tuple(I) .== 1)
-            push!(avoid_states, Tuple(I))
+    extended_states = splits(state_abstraction) .+ 1
+    for I in CartesianIndices(extended_states)
+        if any(Tuple(I) .== extended_states)
+            push!(avoid_states, I)
         end
     end
 
     for (I, source_region) in
         zip(CartesianIndices(splits(state_abstraction)), regions(state_abstraction))
         if ispessimistic(spec) && !iszeromeasure(avoid(prop), source_region)
-            push!(avoid_states, Tuple(I) .+ 1)
+            push!(avoid_states, I)
         elseif isoptimistic(spec) && source_region ⊆ avoid(prop)
-            push!(avoid_states, Tuple(I) .+ 1)
+            push!(avoid_states, I)
         elseif ispessimistic(spec) && source_region ⊆ reach(prop)
-            push!(reach_states, Tuple(I) .+ 1)
+            push!(reach_states, I)
         elseif isoptimistic(spec) && !iszeromeasure(reach(prop), source_region)
-            push!(reach_states, Tuple(I) .+ 1)
+            push!(reach_states, I)
         end
     end
 
@@ -366,21 +362,22 @@ function convert_property(
 )
     prop = system_property(spec)
 
-    avoid_states = NTuple{dim(prop),Int32}[]
+    avoid_states = CartesianIndex{dim(prop)}[]
 
     # Absorbing states
-    for I in CartesianIndices(splits(state_abstraction) .+ 1)
-        if any(Tuple(I) .== 1)
-            push!(avoid_states, Tuple(I))
+    extended_states = splits(state_abstraction) .+ 1
+    for I in CartesianIndices(extended_states)
+        if any(Tuple(I) .== extended_states)
+            push!(avoid_states, I)
         end
     end
 
     for (I, source_region) in
         zip(CartesianIndices(splits(state_abstraction)), regions(state_abstraction))
         if ispessimistic(spec) && !iszeromeasure(avoid(prop), source_region)
-            push!(avoid_states, Tuple(I) .+ 1)
+            push!(avoid_states, I)
         elseif isoptimistic(spec) && source_region ⊆ avoid(prop)
-            push!(avoid_states, Tuple(I) .+ 1)
+            push!(avoid_states, I)
         end
     end
 
@@ -407,14 +404,10 @@ function abstraction(
 
     # State pointer
     stateptr = Int32[1]
-    sizehint!(stateptr, prod(splits(state_abstraction) .+ 1))
+    sizehint!(stateptr, prod(splits(state_abstraction)) + 1)
 
-    for I in CartesianIndices(splits(state_abstraction) .+ 1)
-        if any(Tuple(I) .== 1)
-            push!(stateptr, stateptr[end] + 1)
-        else
-            push!(stateptr, stateptr[end] + numinputs(input_abstraction))
-        end
+    for I in CartesianIndices(splits(state_abstraction))
+        push!(stateptr, stateptr[end] + numinputs(input_abstraction))
     end
 
     # Transition probabilities
@@ -427,11 +420,11 @@ function abstraction(
     )
 
     # Initial states
-    initial_states = NTuple{dimstate(sys),Int32}[]
+    initial_states = CartesianIndex{dimstate(sys)}[]
     for (I, source_region) in
         zip(CartesianIndices(splits(state_abstraction)), regions(state_abstraction))
         if !isdisjoint(initial(sys), source_region)
-            push!(initial_states, Tuple(I) .+ 1)
+            push!(initial_states, I)
         end
     end