Format

Zinoex · Apr 24, 2024 · 3f95d73 · 3f95d73
1 parent 84a97b3
commit 3f95d73
Show file tree

Hide file tree

Showing 5 changed files with 20 additions and 41 deletions.
diff --git a/ext/cuda/value_iteration.jl b/ext/cuda/value_iteration.jl
@@ -16,13 +16,7 @@ function IntervalMDP.step_imdp!(
     maximize,
     upper_bound,
 ) where {R, VR <: AbstractVector{R}, MR <: CuSparseMatrixCSC{R}}
-    ominmax!(
-        ordering,
-        p,
-        prob,
-        value_function.prev;
-        max = upper_bound,
-    )
+    ominmax!(ordering, p, prob, value_function.prev; max = upper_bound)
 
     value_function.action_values .= Transpose(value_function.prev_transpose * p)
 

diff --git a/src/Data/bmdp-tool.jl b/src/Data/bmdp-tool.jl
@@ -180,7 +180,9 @@ function write_bmdp_tool_file(
     end
 end
 
-function write_bmdp_tool_file(path, mdp::IntervalMarkovChain, 
+function write_bmdp_tool_file(
+    path,
+    mdp::IntervalMarkovChain,
     terminal_states::Vector{T},
 ) where {T <: Integer}
     prob = transition_prob(mdp)

diff --git a/src/specification.jl b/src/specification.jl
@@ -493,8 +493,10 @@ Specification(prop::Property) = Specification(prop, Pessimistic)
 Specification(prop::Property, satisfaction::SatisfactionMode) =
     Specification(prop, satisfaction, Maximize)
 
-initialize!(value_function, spec::Specification) = initialize!(value_function, system_property(spec))
-postprocess!(value_function, spec::Specification) = postprocess!(value_function, system_property(spec))
+initialize!(value_function, spec::Specification) =
+    initialize!(value_function, system_property(spec))
+postprocess!(value_function, spec::Specification) =
+    postprocess!(value_function, system_property(spec))
 
 function checkspecification!(spec::Specification, system)
     return checkproperty!(system_property(spec), system)

diff --git a/src/synthesis.jl b/src/synthesis.jl
@@ -87,13 +87,7 @@ function step_imdp_with_extract!(
 )
     sptr = stateptr(mdp)
 
-    ominmax!(
-        ordering,
-        p,
-        prob,
-        value_function.prev;
-        max = upper_bound,
-    )
+    ominmax!(ordering, p, prob, value_function.prev; max = upper_bound)
 
     optfun = maximize ? argmax : argmin
 
@@ -107,7 +101,7 @@ function step_imdp_with_extract!(
         @inbounds s2 = sptr[j + 1]
 
         @inbounds indices[j] =
-            optfun(view(value_function.action_values, s1:(s2 - 1)))  + s1 - 1
+            optfun(view(value_function.action_values, s1:(s2 - 1))) + s1 - 1
         @inbounds value_function.cur[j] = value_function.action_values[indices[j]]
     end
 

diff --git a/src/value_iteration.jl b/src/value_iteration.jl
@@ -90,14 +90,12 @@ function construct_value_function(::AbstractMatrix{R}, num_states) where {R}
 end
 
 mutable struct IMCValueFunction
-    prev
-    prev_transpose
-    cur
+    prev::Any
+    prev_transpose::Any
+    cur::Any
 end
 
-function IMCValueFunction(
-    problem::Problem{M, S},
-) where {M <: IntervalMarkovChain, S}
+function IMCValueFunction(problem::Problem{M, S}) where {M <: IntervalMarkovChain, S}
     mc = system(problem)
 
     prev = construct_value_function(gap(transition_prob(mc)), num_states(mc))
@@ -238,10 +236,10 @@ function value_iteration(
 end
 
 mutable struct IMDPValueFunction
-    prev
-    prev_transpose
-    cur
-    action_values
+    prev::Any
+    prev_transpose::Any
+    cur::Any
+    action_values::Any
 end
 
 function IMDPValueFunction(
@@ -254,12 +252,7 @@ function IMDPValueFunction(
 
     action_values = similar(prev, num_choices(mdp))
 
-    return IMDPValueFunction(
-        prev,
-        Transpose(prev),
-        cur,
-        action_values
-    )
+    return IMDPValueFunction(prev, Transpose(prev), cur, action_values)
 end
 
 function step_imdp!(
@@ -271,13 +264,7 @@ function step_imdp!(
     maximize,
     upper_bound,
 )
-    ominmax!(
-        ordering,
-        p,
-        prob,
-        value_function.prev;
-        max = upper_bound,
-    )
+    ominmax!(ordering, p, prob, value_function.prev; max = upper_bound)
 
     optfun = maximize ? maximum : minimum