Fix bugs in IMDP comparison

Author: Zinoex

examples/compare_imdp_approaches.jl

@@ -173,14 +173,20 @@ function benchmark_direct(problem::ComparisonProblem)
             reach = []
         else
             reach_lines = split(chomp(reach), '\n')
-            reach = map(line -> parse(Int32, line), reach_lines) # Parse each line as an integer
+            reach = map(reach_lines) do line
+                line_match = match(r"CartesianIndex\(([0-9]+),\)", line)
+                return parse(Int32, line_match.captures[1])
+            end
             reach = reach .- 1 # Subtract 1 to match 1-based indexing without the avoid state
             reach = map(x -> cartesian_indices[x], reach) # Convert from a linear index to a CartesianIndex
         end
 
         # Read avoid states
         avoid_lines = split(chomp(avoid), '\n') 
-        avoid = map(line -> parse(Int32, line), avoid_lines) # Parse each line as an integer
+        avoid = map(avoid_lines) do line
+            line_match = match(r"CartesianIndex\(([0-9]+),\)", line)
+            return parse(Int32, line_match.captures[1])
+        end
         avoid = filter(x -> x != 1, avoid) # Remove the absorbing avoid state (we remove this manually later)
         avoid = avoid .- 1 # Subtract 1 to match 1-based indexing without the avoid state
         avoid = map(x -> cartesian_indices[x], avoid) # Convert from a linear index to a CartesianIndex
@@ -280,6 +286,7 @@ function benchmark_decoupled(problem::ComparisonProblem)
         else
             reach_lines = split(chomp(reach), '\n')
             reach = map(reach_lines) do line # Parse each line as a tuple of indices
+                line = replace(line, "CartesianIndex" => "")
                 indices = split(line[2:end - 1], ",")
                 indices = map(index -> parse(Int32, index), indices)
                 return Tuple(indices)
@@ -290,6 +297,7 @@ function benchmark_decoupled(problem::ComparisonProblem)
         # Read avoid states
         avoid_lines = split(chomp(avoid), '\n')
         avoid = map(avoid_lines) do line # Parse each line as a tuple of indices
+            line = replace(line, "CartesianIndex" => "")
             indices = split(line[2:end - 1], ",")
             indices = map(index -> parse(Int32, index), indices)
             return Tuple(indices)

examples/isolated_compare_imdp_approaches.jl

@@ -119,27 +119,33 @@ end
 function measure_abstraction_time(problem::IntervalSySCoReComparisonProblem, constructor)
     BenchmarkTools.gcscrub()
     start_time = time_ns()
-    mdp, spec, upper_bound_spec = constructor(problem.state_split, problem.input_split)
+    mdp, spec, upper_bound_spec = constructor(problem.state_split, problem.input_split, problem.time_horizon)
     end_time = time_ns()
     abstraction_time = (end_time - start_time) / 1e9
 
     return abstraction_time, mdp, spec, upper_bound_spec
 end
 
-function warmup_certification(prob)
-    value_iteration(prob)
+function warmup_certification(prob, upper_bound_spec)
+    strategy, _ = control_synthesis(prob)
 
-    return nothing
+    upper_bound_prob = Problem(IntervalMDP.system(prob), upper_bound_spec, strategy)
+    value_iteration(upper_bound_prob)
+
+    return upper_bound_prob
 end
 
-function measure_certification_time(prob)
+function measure_certification_time(prob, upper_bound_prob)
     BenchmarkTools.gcscrub()
     start_time = time_ns()
-    strategy, V, k, res = control_synthesis(prob)
+    
+    _, V_lower, _ = control_synthesis(prob)
+    V_upper, _ = value_iteration(upper_bound_prob)
+
     end_time = time_ns()
     certification_time = (end_time - start_time) / 1e9
 
-    return certification_time, V, strategy
+    return certification_time, V_lower, V_upper
 end
 
 function benchmark_intervalsyscore(name::String, direct=true)
@@ -165,19 +171,15 @@ function benchmark_intervalsyscore(name::String, direct=true)
     prob = Problem(mdp, spec)
 
     # Warmup
-    warmup_certification(prob)
+    upper_bound_prob = warmup_certification(prob, upper_bound_spec)
 
     # Measure certification time
-    certification_time, V_lower, strategy = measure_certification_time(prob)
+    certification_time, V_lower, V_upper = measure_certification_time(prob, upper_bound_prob)
     println(("Certification time", certification_time))
 
-    # Compute upper bound probabilities
-    prob = Problem(mdp, upper_bound_spec, strategy)
-    V_upper, _, _ = value_iteration(prob)
-
     println("reach")
     reach_set = if system_property(spec) isa AbstractReachability
-        reach(system_property(spec))
+        IntervalMDP.reach(system_property(spec))
     else
         []
     end
@@ -186,7 +188,7 @@ function benchmark_intervalsyscore(name::String, direct=true)
     end
 
     println("avoid")
-    for a in avoid(system_property(spec))
+    for a in IntervalMDP.avoid(system_property(spec))
         println(a)
     end
 

examples/systems/almost_identity.jl

@@ -46,7 +46,7 @@ function almost_identity_decoupled(num_dims::Int, time_horizon=10; sparse=false,
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -69,7 +69,7 @@ function almost_identity_direct(num_dims::Int, time_horizon=10; sparse=false, st
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end

examples/systems/bas_4d.jl

@@ -54,7 +54,7 @@ function building_automation_system_4d_decoupled(time_horizon=10; sparse=false,
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -78,7 +78,7 @@ function building_automation_system_4d_direct(time_horizon=10; sparse=false, sta
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end

examples/systems/bas_7d.jl

@@ -48,7 +48,7 @@ function building_automation_system_7d_decoupled(time_horizon=10; sparse=false,
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -71,7 +71,7 @@ function building_automation_system_7d_direct(time_horizon=10; sparse=false, sta
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end

examples/systems/integrator_chain.jl

@@ -52,7 +52,7 @@ function integrator_chain_decoupled(num_dims::Int, time_horizon=5; sparse=false,
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end

examples/systems/nndm.jl

@@ -280,7 +280,7 @@ function action_cartpole_decoupled(time_horizon=10; sparse=false)
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -304,7 +304,7 @@ function action_cartpole_direct(time_horizon=10; sparse=false)
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end

examples/systems/robot_2d.jl

@@ -80,7 +80,7 @@ function robot_2d_decoupled(time_horizon=10; sparse=true, spec=:reachavoid, stat
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -104,7 +104,7 @@ function robot_2d_direct(time_horizon=10; sparse=true, spec=:reachavoid, state_s
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end

examples/systems/running_example.jl

@@ -46,7 +46,7 @@ function running_example_decoupled(time_horizon=10; sparse=false, range_vs_grid=
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -76,7 +76,7 @@ function running_example_direct(time_horizon=10; sparse=false, range_vs_grid=:gr
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end

examples/systems/van_der_pol.jl

@@ -39,7 +39,7 @@ function van_der_pol_decoupled(time_horizon=10; sparse=false, state_split=(50, 5
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end
@@ -59,7 +59,7 @@ function van_der_pol_direct(time_horizon=10; state_split=(50, 50), input_split=1
     mdp, abstract_spec = abstraction(prob, state_abs, input_abs, target_model)
 
     upper_bound_spec = Specification(system_property(spec), !satisfaction_mode(spec))
-    upper_bound_spec = convert_specification(upper_bound_spec, state_abs, target_model)
+    upper_bound_spec = IntervalSySCoRe.convert_specification(upper_bound_spec, state_abs, target_model)
 
     return mdp, abstract_spec, upper_bound_spec
 end