Model export + import improvements/refactoring #260
Merged
Conversation
This file contains hidden or 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
Global export options (matlab/rows) were being ignored in command line after recent refactoring.
Push handling of export destination (null file being treated as the log) from Prism into explicit.StateModelChecker. This will help: - align explicit/symbolic model checkers (native code still takes File) - adding export to binary files (where PrismLog does not make sense)
This now matches the code for the explicit engine more closely.
Export of transition matrix (MTB)DD to a Dot file (-exportdot) moved to an instance of exportBuiltModelTransitions (DD_DOT format). Export of transition matrix to a spy file (-exportspy) removed from command line, but code kept in StateModelChecker.
…initions. ModelExportTask stores the entity to be exported (model, states, rewards, etc.), the destination and the export options. Tasks that export the whole model (e.g. Dot, DRN) use entity "model", representing the core part of the model, and can also have other entities added as annotations.
This allows multiple -exportmodel with independent options to be used.
This means the deprecated Prism.exportXXX methods are no longer used.
* Add some some alternatives that just take the format * Don't throw FileNotFoundException * Tidy up order of methods in Prism
Use new ModelExportFormat/ModelExportOptions to specify format. The probabilities can also be accessed via computeSteadyStateProbabilities.
Use new ModelExportFormat/ModelExportOptions to specify format. The probabilities can also be accessed via computeTransientProbabilities.
Push some logic (type checks, range handling) into Prism. This means that the GUI can compute multiple transient probabilities. Also fix a memory leak (vectors not clear()ed in multi-time transient).
Also make all exporter classes implement exportModel().
In the same (non-ideal) way currently ued for model checking. We also change the export workflow in the command-line. We no longer force a build initially, and instead bail out when the first export fails, if any.
Also, allow any or no filename extension. E.g.: prism model.prism -exportmodel model.txt:format=explicit prism model.prism -exportmodel stdout:format=drn
All models support getActions(), providing a list of all action labels used, including null for unlabelled choices/transitions. For now, inefficient defaults are available that recompute this information by checking all choices/transitions. explicit.DTMC provides getActionsIterator(s) to get the actions for all transitions from states s. Previously, these were only available in combination with the transitions. The indices of actions (into getActions()) can also be queried: getActionIndex(s, i) for NondetModel and its subclasses and getActionIndicesIterator(s) for DTMC and its subclasses. For now, explicit engine model storage continues to store actions directly as objects and this is looked up as needed.
New method findActionsUsed() in prism.Model interface, used in default implementation of getActions(). The execution of this can be optimised by implementing onlyNullActionUsed() and when all actions are null. New class ActionList to encapsulate info about action names. This is stored in model base classes, notably ModelExplicit, meaning that looking up action indices is much faster. For now, the usage of ActionList is that it is initialised to be empty, and the actual list is computed lazily when needed. Changes to the model that affect actions should call the method markNeedsRecomputing() in case the list has been computed.
C-based version already exists for the purposes of model export.
Works by first converting to an explicit engine model.
Would allow inclusion of variable/observable info in the export.
Temporary storage for info needed by ModelInfo interface. Better than creating a new anonymous class each time and can be re-used by other importers.
Temporary storage for info needed by RewardInfo interface. Better than creating a new anonymous class each time and can be re-used by other importers. Also fixes a bug in model import: rewardStructHasTransitionRewards(). PrismExplicitImporter was wrongly reporting that the model had no transition rewards. This didn't actually prevent transition rewards being used because ConstructRewards does not check the results of rewardStructHasTransitionRewards() for the case of imported rewards. An additional check that state/transition reward files for the same reward structure have matching names is also added.
The interface to PrismExplicitImporter is also changed, so that rewards files can be added one by one.
For Markov chains, the importer is now responsible for providing transition rewards indexed either by the transition's offset within the state or by the successor state. The former is used by the explicit engine, the latter by the symbolic engine. The user calls setTransitionRewardIndexing to specify which indexing is required. There is also a new method setModel in ExplicitModelImporter which can be used to provide access to the model in case needed during transition reward processing. Notably this is used when extracting rewards from a .trew file for use in the explicit engine (which requires conversion of state->offset indexing). This logic is now moved into PrismExplicitImporter.
We assume (s,i) not (s,i,s') for now, since that is what is currently supported by the underlying storage/engines. So the handling of PRISM .trew files, which do technically support (s,i,s') rewards, is pushed into PrismExplicitImporter. And ExplicitModelImporter is adapted to expect (s,i) rewards. ExplicitFiles2MTBDD is also adapted accordingly.
For now, the format is just assumed to be "explicit" (the only option).
Because we now sometimes import to immutable models. This is disabled for import to symbolic models, where this is not an issue.
Plus commenting of related methods in ExplicitModelImporter.
I.e., it imports info about states that were deadlocks, even if they have now been fixed (replaced with self-loops).
For importing from explicit files with the explicit engine,
Markov chain transition rewards often need to be converted
to expected state rewards before model checking, as is done
when constructing rewards from a PRISM model / generator.
Not currently testable with regression tests but:
prism -importmodel ../prism-tests/functionality/import/lec3.all -pf 'R{"r"}=?[C<=10]' -ex
should return 4.552734375 not 2.6640625.
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
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.
No description provided.