Merge pull request #88 from Zinoex/fm/commonsolve

Use CommonSolve standardized interface

Author: Zinoex

Project.toml

@@ -1,9 +1,10 @@
 name = "IntervalMDP"
 uuid = "051c988a-e73c-45a4-90ec-875cac0402c7"
 authors = ["Frederik Baymler Mathiesen <frederik@baymler.com> and contributors"]
-version = "0.5.0"
+version = "0.6.0"
 
 [deps]
+CommonSolve = "38540f10-b2f7-11e9-35d8-d573e4eb0ff2"
 JSON = "682c06a0-de6a-54ab-a142-c8b1cf79cde6"
 LinearAlgebra = "37e2e46d-f89d-539d-b4ee-838fcccc9c8e"
 NCDatasets = "85f8d34a-cbdd-5861-8df4-14fed0d494ab"
@@ -21,6 +22,7 @@ IntervalMDPCudaExt = ["Adapt", "CUDA", "GPUArrays", "LLVM"]
 [compat]
 Adapt = "4"
 CUDA = "5.1"
+CommonSolve = "0.2.4"
 GPUArrays = "10, 11"
 JSON = "0.21.4"
 LLVM = "7, 8, 9"

README.md

@@ -63,10 +63,10 @@ imc = IntervalMarkovChain(prob, initial_states)
 target_set = [3]
 prop = FiniteTimeReachability(target_set, 10)  # Time steps
 spec = Specification(prop, Pessimistic, Maximize)
-problem = Problem(imc, spec)
+problem = VerificationProblem(imc, spec)
 
 # Solve
-V, k, residual = value_iteration(problem)
+V, k, residual = solve(problem)
 ```
 
 See [Usage](https://www.baymler.com/IntervalMDP.jl/dev/usage/) for more information about different specifications, using sparse matrices, and CUDA.

docs/make.jl

@@ -23,7 +23,7 @@ makedocs(;
         "Reference" => Any[
             "Systems" => "reference/systems.md",
             "Specifications" => "reference/specifications.md",
-            "Value Iteration" => "reference/value_iteration.md",
+            "Solve Interface" => "reference/solve.md",
             "Data Storage" => "reference/data.md",
         ],
         "Index" => "api.md",

docs/src/reference/solve.md

@@ -0,0 +1,16 @@
+# Solve Interface
+
+```@docs
+solve
+residual
+num_iterations
+value_function
+StationaryStrategy
+TimeVaryingStrategy
+```
+
+## VI-like Algorithms
+
+```@docs
+RobustValueIteration
+```

docs/src/reference/specifications.md

@@ -1,7 +1,8 @@
 # Problem
 
 ```@docs
-Problem
+VerificationProblem
+ControlSynthesisProblem
 system
 specification
 strategy
@@ -19,8 +20,6 @@ StrategyMode
 ## DFA Reachability
 
 ```@docs
-AbstractDFAReachability
-
 FiniteTimeDFAReachability
 isfinitetime(prop::FiniteTimeDFAReachability)
 terminal_states(prop::FiniteTimeDFAReachability)
@@ -37,8 +36,6 @@ convergence_eps(prop::InfiniteTimeDFAReachability)
 ## Reachability
 
 ```@docs
-AbstractReachability
-
 FiniteTimeReachability
 isfinitetime(prop::FiniteTimeReachability)
 terminal_states(prop::FiniteTimeReachability)
@@ -61,8 +58,6 @@ time_horizon(prop::ExactTimeReachability)
 ## Reach-avoid
 
 ```@docs
-AbstractReachAvoid
-
 FiniteTimeReachAvoid
 isfinitetime(prop::FiniteTimeReachAvoid)
 terminal_states(prop::FiniteTimeReachAvoid)
@@ -88,8 +83,6 @@ time_horizon(prop::ExactTimeReachAvoid)
 ## Safety
 
 ```@docs
-AbstractSafety
-
 FiniteTimeSafety
 isfinitetime(prop::FiniteTimeSafety)
 terminal_states(prop::FiniteTimeSafety)
@@ -106,8 +99,6 @@ convergence_eps(prop::InfiniteTimeSafety)
 ## Reward specification
 
 ```@docs
-AbstractReward
-
 FiniteTimeReward
 isfinitetime(prop::FiniteTimeReward)
 reward(prop::FiniteTimeReward)
@@ -124,8 +115,6 @@ convergence_eps(prop::InfiniteTimeReward)
 ## Hitting time
 
 ```@docs
-AbstractHittingTime
-
 ExpectedExitTime
 isfinitetime(prop::ExpectedExitTime)
 terminal_states(prop::ExpectedExitTime)

docs/src/reference/value_iteration.md

@@ -114,14 +114,19 @@ spec = Specification(prop, Optimistic, Maximize)
 spec = Specification(prop, Optimistic, Minimize)
 
 ## Combine system and specification in a Problem
-problem = Problem(imdp_or_imc, spec)
+problem = VerificationProblem(imdp_or_imc, spec)
 ```
 
-Finally, we call `value_iteration` to solve the specification. `value_iteration` returns the value function for all states in addition to the number of iterations performed and the last Bellman residual.
+Finally, we call [`solve`](@ref) to solve the specification. `solve` returns the value function for all states in addition to the number of iterations performed and the last Bellman residual, wrapped in a solution object.
 
 ```julia
-V, k, residual = value_iteration(problem)
+sol = solve(problem) # or solve(problem, RobustValueIteration())
+V, k, res = sol
+
+# or alternatively
+V, k, res = value_function(sol), num_iterations(sol), residual(sol)
 ```
+For now, only [`RobustValueIteration`](@ref) is supported, but more algorithms are planned.
 
 !!! note
     To use multi-threading for parallelization, you need to either start julia with `julia --threads <n|auto>` where `n` is a positive integer or to set the environment variable `JULIA_NUM_THREADS` to the number of threads you want to use. For more information, see [Multi-threading](https://docs.julialang.org/en/v1/manual/multi-threading/).

docs/src/usage.md

@@ -121,7 +121,7 @@ IntervalMDP.arrayfactory(
     ::MR,
     T,
     num_states,
-) where {R, MR <: Union{CuSparseMatrixCSC{R}, CuMatrix{R}}} = CUDA.zeros(T, num_states)
+) where {R, MR <: Union{CuSparseMatrixCSC{R}, CuArray{R}}} = CUDA.zeros(T, num_states)
 
 include("cuda/utils.jl")
 include("cuda/array.jl")

ext/IntervalMDPCudaExt.jl

@@ -2,4 +2,5 @@
 Adapt.@adapt_structure FiniteTimeReward
 Adapt.@adapt_structure InfiniteTimeReward
 Adapt.@adapt_structure Specification
-Adapt.@adapt_structure Problem
+Adapt.@adapt_structure VerificationProblem
+Adapt.@adapt_structure ControlSynthesisProblem

ext/cuda/specification.jl

@@ -110,15 +110,15 @@ function read_bmdp_tool_file(path)
 end
 
 """
-    write_bmdp_tool_file(path, problem::Problem)
+    write_bmdp_tool_file(path, problem::IntervalMDP.AbstractIntervalMDPProblem)
 
 Write a bmdp-tool transition probability file for the given an IMDP and a reachability specification.
 The file will not contain enough information to specify a reachability specification. The remaining
 parameters are rather command line arguments.
 
 See [Data storage formats](@ref) for more information on the file format.
 """
-write_bmdp_tool_file(path, problem::Problem) =
+write_bmdp_tool_file(path, problem::IntervalMDP.AbstractIntervalMDPProblem) =
     write_bmdp_tool_file(path, system(problem), specification(problem))
 
 """
@@ -130,8 +130,11 @@ write_bmdp_tool_file(path, mdp::IntervalMarkovProcess, spec::Specification) =
 """
     write_bmdp_tool_file(path, mdp::IntervalMarkovProcess, prop::AbstractReachability)
 """
-write_bmdp_tool_file(path, mdp::IntervalMarkovProcess, prop::AbstractReachability) =
-    write_bmdp_tool_file(path, mdp, reach(prop))
+write_bmdp_tool_file(
+    path,
+    mdp::IntervalMarkovProcess,
+    prop::IntervalMDP.AbstractReachability,
+) = write_bmdp_tool_file(path, mdp, reach(prop))
 
 """
     write_bmdp_tool_file(path, mdp::IntervalMarkovProcess, terminal_states::Vector{T})