Use CommonSolve standardized interface

[Zinoex]

Replace value_iteration and control_synthesis with the standardized solve(prob, alg) from CommonSolve (with VerificationProblem and ControlSynthesisProblem) to prepare for more algorithmic options and given control to the user.

[Copilot]

Pull Request Overview

This PR standardizes the solve interface by replacing the legacy Problem, value_iteration, and control_synthesis APIs with a unified solve function from CommonSolve, backed by VerificationProblem and ControlSynthesisProblem.

• Introduce VerificationProblem and ControlSynthesisProblem types and deprecate the old Problem type.
• Replace all calls to value_iteration and control_synthesis with solve in tests and core modules.
• Refactor module exports and documentation to align with the CommonSolve solve interface.

Reviewed Changes

Copilot reviewed 41 out of 42 changed files in this pull request and generated 1 comment.

Show a summary per file

File	Description
test/sparse/vi.jl	Updated tests to use VerificationProblem and solve.
test/sparse/synthesis.jl	Updated tests to use ControlSynthesisProblem and solve.
test/sparse/orthogonal.jl	Refactored workspace and strategy cache construction calls.
test/sparse/imdp.jl	Switched from value_iteration to solve with VerificationProblem.
test/sparse/bellman.jl	Updated construct_strategy_cache calls to use the new API.
test/runtests.jl	Commented out CUDA tests; updated test suite inclusion.
test/data/prism.jl	Changed Problem to VerificationProblem.
test/data/bmdp_tool.jl	Changed Problem to VerificationProblem.
test/cuda/dense/vi.jl	Updated CUDA tests to use solve with VerificationProblem.
test/cuda/dense/synthesis.jl	Updated CUDA synthesis tests to use solve.
test/cuda/dense/imdp.jl	Converted CUDA IMDP tests to new solve interface.
test/cuda/dense/bellman.jl	Updated CUDA Bellman tests to use construct_strategy_cache.
test/base/vi.jl	Switched base tests from value_iteration to solve.
test/base/synthesis.jl	Updated base synthesis tests to use ControlSynthesisProblem.
test/base/specification.jl	Replaced Problem with VerificationProblem in spec tests.
test/base/product.jl	Updated product tests to use unified solve and new problem types.
test/base/orthogonal.jl	Refactored orthogonal tests for workspace and strategy cache.
test/base/mixture.jl	Updated mixture tests to new cache construction API.
test/base/imdp.jl	Converted base IMDP tests to solve API.
test/base/bellman.jl	Updated base Bellman tests to use construct_strategy_cache.
src/utils.jl	Added arrayfactory and valuetype methods for new API.
src/stategy_cache.jl	New strategy cache file supporting solve interface.
src/robust_value_iteration.jl	Replaced value_iteration with solve overloads; updated docs.
src/problem.jl	Defined VerificationProblem and ControlSynthesisProblem.
src/algorithms.jl	Introduced AbstractIntervalMDPAlgorithm and default solve.
src/IntervalMDP.jl	Integrated CommonSolve interface and reorganized exports.
src/bellman.jl	Updated bellman calls to use construct_strategy_cache.
src/specification.jl	Expanded checkproperty methods for new problem types.
src/Data/prism.jl	Adjusted PRISM I/O to return ControlSynthesisProblem.
src/Data/intervalmdp.jl	Updated read/write to use new problem types.
src/Data/bmdp-tool.jl	Adjusted BMDP tool I/O to accept AbstractIntervalMDPProblem.
ext/cuda/specification.jl	Adapted CUDA spec to VerificationProblem and ControlSynthesisProblem.
docs/src/usage.md	Updated usage examples to use solve instead of value_iteration.
docs/src/reference/value_iteration.md	Removed outdated value_iteration docs (needs replacement).
docs/src/reference/specifications.md	Updated reference to VerificationProblem and ControlSynthesisProblem.

Comments suppressed due to low confidence (3)

src/utils.jl:23

• The where clause references R without declaring it. Update to valuetype(::MR) where {R, MR <: AbstractMatrix{R}} = R to correctly bind both type parameters.

valuetype(::MR) where {R, MR <: AbstractMatrix{R}} = R

src/stategy_cache.jl:1

• The filename stategy_cache.jl is misspelled; it should be strategy_cache.jl to match the module name and improve discoverability.

abstract type AbstractStrategyCache end

src/IntervalMDP.jl:40

• The module still exports a Problem type, but Problem has been removed in favor of VerificationProblem and ControlSynthesisProblem. Consider removing this export to avoid confusion.

export Specification, Problem