Bellman operator for ProductProcess

[Zinoex]

No description provided.

[Copilot]

Pull Request Overview

This PR introduces first-class support for ProductProcess—the product of an interval Markov process and a DFA—and refactors related workspace construction, Bellman updates, strategy checking, and exports across the codebase. It also cleans up legacy product‐IMDP types and brings labelling and transition functions in line with the new product API.

• Added ProductProcess, ProductWorkspace, and dispatch in the Bellman operator and value_iteration to handle product models.
• Refactored TransitionFunction and LabellingFunction (exports, indexing, naming) and updated docs/tests accordingly.
• Extended strategy and specification modules to validate ProductProcess compatibility and improved test coverage for product models.

Reviewed Changes

Copilot reviewed 31 out of 31 changed files in this pull request and generated 2 comments.

Show a summary per file

File	Description
src/models/ProductProcess.jl	Defines ProductProcess, validity checks, and accessors
src/bellman.jl	Adds bellman! for ProductProcess using preallocated workspace
src/strategy.jl	Extends checkstrategy to support slicing strategies by DFA state
src/workspace.jl	Introduces ProductWorkspace and constructor for ProductProcess
test/base/product.jl	Tests for product construction, Bellman operator, and value iteration

Comments suppressed due to low confidence (3)

src/workspace.jl:19

• The new construct_workspace method for ProductProcess is not covered by existing tests. Add unit tests to ensure ProductWorkspace fields (underlying_workspace and intermediate_values) are correctly initialized and reusable across Bellman iterations.

function construct_workspace(proc::ProductProcess)

src/specification.jl:10

• This new compatibility check function lacks a docstring describing its purpose, parameters, and error conditions. Add a short docstring above the function to maintain consistency with the rest of the API.

function checkmodelpropertycompatibility(prop, system)

src/IntervalMDP.jl:22

• The exports for LTLFormula, LTLfFormula, and PCTLFormula have been removed, which is a breaking change. Consider providing deprecation stubs or updating downstream code/documentation to avoid unexpected failures.

export Property, BasicProperty, ProductProperty