Refactoring: API, parametric/exact, symbolic #249
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Member
davexparker
commented
Aug 8, 2024
davexparker
commented
- prism.Prism API: remove some old deprecated methods
- prism.Prism: refactored storage/access for model info
- prism.Prism: integration of exact model building/checking
- parametric engine refactored to use explicit models/rewards
- symbolic code rearranged (new symbolic package)
- symbolic model storage refactored, simplified, documented
- parametric engine: improved error reporting and formatting
- prism.API: exportprism moved from setting to API call
And rename currentModel to currentModelSymb.
We also add argument buildIfMissing (default true) to getModelGenerator(). This allows us to query if it is null without forcing its construction.
Implemented by symbolic/explicit Model superclasses, including small alignments between the two, e.g.: - getNumStates() returns int, not long - getNum*Initial*States(), not "Start" Stored and made available from prism.Prism via getBuiltModel(), which previously returned the symbolic version. Removes a dependency on symbolic/explicit models in GUI.
Use (new) createFromArrayResult not createFromDoubleArrayResult, which will allow easier migration to non-double results.
Model and reward storage (and creation) in the parametric model checking engine is migrated to the existing generic classes from the explicit package, using Function as Value. ParamModel is converted to Model<Function>, and deleted. * Separate model classes (DTMC, CTMC, MDP) now * Choice indexing now local to each state, not global (and only used for MDPs) * D/CTMC actions are now stored per state, not transition * CTMCs are stored directly (previously it was actually the embedded DTMC) and rate sums for each state are not stored for other models * The FunctionFactory is now stored in the Evaluator ParamRewardStruct is converted to Rewards<Function>, and deleted. * State and transition rewards are now stored separately * No support for D/CTMC transition rewards now * The FunctionFactory is now stored in the Evaluator ModelBuilder is replaced by ConstructModel, and deleted. * Creation of a FunctionFactory, based on PrismSettings, is pushed into a static FunctionFactory.create() method. ParamModelChecker and ValueComputer: * New setModelCheckingInfo(), as for other model checkers * Model passed to check(), not stored, as for others * Policy iteration migrated to DTMCFromMDPMemorylessAdversary * Reward construction is now done by ConstructReward (checks for negative/invalid rewards now differ slightly and this may need to be revisited)
In exact mode, model construction and storage is now handled in prism.Prism in the same way as for other engines. Model checking is now triggered by the usual modelCheck() method and modelCheckExact() is now deprecated. A few changes are made in the parametric model checking code to align the way that results are stored and displayed. Unsupported aspects of model checking are now detected and reported more cleanly. Model export is now also supported for exact mode.
symbolic.model.Model remains the top-level interface, but contains only the read-only access methods for models. Some method implementations are moved there as defaults. New class ModelSymbolic is the (mutable) base implementation, covering features common to all models, e.g., initial states, reachable states, labels. Most of this was in ProbModel previously. The split between Model/ModelSymbolic mirrors the situation in the explicit engine with Model and ModelExplicit. ProbModel (DTMC) and NondetModel (MDP) now separately extend ModelSymbolic and StochModel (CTMC) extends ProbModel. Lots of tidying and commenting. A few unimplemented/deprecated methods are removed.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.