Merge in new interval model code #19
Closed
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.
This means that the action format in .tra/.dot export changes from e.g. [a1][b2]<2> to [a1,b2,-]. Additional info, storing integer indices, remains in place. addActionLabelledChoice can be provided either with int[], as currently done in model construction, or with a JointAction object. Other info is created accordingly. For consistency with elsewhere, the list of actions in CSG/CSGSimple changes from Vector<String> to List<Object>.
When generating Transition objects during export, we no longer assume that the attached values are of type Value (i.e., the generic type for the accompanying model). Instead, each Transition has an associated evaluator, used to implement isZero and (custom) toString methods. This will allow cleaner handling of exports for interval models.
Since they only require choice/successor methods. And to allow IMDPs etc. to implement them without being MDPs.
The IMDP interface no longer extends MDP<Interval>. This created to many problems due to it extending both Model<Interval<Value>> and Model<Value>, and it did not support many MDP methods anyway. Instead, it extends a (new) UMDP interface, to which most old IMDP methods have been moved. To help reuse old code, IMDP has methods getIntervalTransitionsIterator and getIntervalModel, which provide access to transitions/model over Interval<Value>. There is a new UMDP model type, currently only only used in the UMDP interface (and overwritten by IMDP). This will later be used for other implementations of uncertain MDPs. The IMDPSimple implementation of IMDP also changes. Rather than extend an MDPSimple<Interval>, it uses one for internal storage. In a related change, IMDPSimple<Value>'s evaluator is now also of type <Value> and there is a separate setIntervalEvaluator() method to provide an evaluator for intervals. As before, for the usual case of doubles, everything just works.
But currently IMDPs are the only kind of UMDP that exist.
As done earlier for MDPs.
As done earlier for MDPs.
As done earlier for MDPs.
… function per (s,a); adapted the CSGModelChecker for this
…ategies); "doublised" transitions and choices accessors in CSGModelChecker so it's compatible with Double Intervals
…ting stored values (`prechoices`) in CSGStrategy
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
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.