Try merging robots2 again, previous merge was squash #6
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
Use values stored in Prism rather than caching locally. Also make GUI simulator default to previous constants too.
Strategy interface: - main purpose clarified: represents a strategy with respect to a specific, constructed model and, by default, defines choices by action (as an Object) - can also provide getChoiceIndex() but this is not to be relied upon (mainly because model choice ordering varies across engines) - by default, queries take both s (state index) and m (memory index); the interface (formerly subclass) MDStrategy (memoryless deterministic) adds methods that just take the state index s - getNumStates() method moved to this interface - strategies can implement whyUndefined() to explain missing choices - other utility methods: isChoiceDefined(), getChoiceActionString() - new methods for info about memory: getInitialMemory(), getUpdatedMemory() - "interactive" methods, which track the current state of the strategy (i.e., initialise, update) are removed - implementations (MDStrategy*) are updated accordingly - new subclass StrategyExplicit added for implementations of Strategy attached to explicit engine models StrategyGenerator: new interface supporting provision of interfaces at the State (not state index) level, and in an interactive fashion (states are supplied sequentially and the strategy keeps track of its current state, memory, etc.). Not yet used. StrategyInfo: common super-interface for Strategy and StrategyGenerator supplying basic info (e.g., class of strategy) StrategyWithStates: base class for implementations of Strategy, which implements the StrategyGenerator interface, given a state-to-index look-up mechanism. Support for randomised strategies also added: - for randomised strategies, getActionChoice() returns an instance of DistributionOver<Object> rather than just Object - for convenience, Strategy has getChoiceActionProbability(), isActionChosen() and sampleChoiceAction(); StrategyGenerator has comparable methods getCurrentChoiceActionProbability(), isActionChosenCurrently() and sampleCurrentChoiceAction() - both have default implementations based on utility methods included within StrategyInfo
prism.Prism now retains a Strategy if generated/returned during model checking, accessible via getStrategy(). There is a new method loadStrategyIntoSimulator() to pass the current strategy to the simulator. SimulatorEngine has a new mechanism for loading a strategy, as a StrategyGenerator, which takes care of providing a strategy and mapping it to the State view of a model. It is also optional whether it is enforced or not, during automatic path generation, via method setStrategyEnforced(). The state/decision of the strategy can be queried for the current state: isTransitionEnabledByStrategy(), getStrategyDecisionString(). Path classes (optionally) store strategy info (current decision and memory) in states.
…in the simulator.
- Create BigIntegers from int/long directly without String conversion - Use BigInteger#valueOf instead of invoking constructor directly
Both -exportmodel and -exportlabels have an option to export labels from a model and properties file to the same file. The default behaviour only exports labels defined in the model. Note: This changes the default from the previous version which always exported labels from a properties file if present. Fixes prismmodelchecker#179
As raised in prismmodelchecker#211. And generally make more use of statesOfInterest in explicit engine model checking. In particular: respect this for operators handled by passing to apply methods within StateValues.
Specifically: if unsupported (notably explicit engine transition rewards), an empty rewards file is not erroneously created.
Notably these methods are used to handle models with initial states.
Not a problem for parsed expressions, but it was problematic for programatically created ones.
…ive. Previously: RESULT: Error:String would fail because the error message was converted to lower case before testing, but not the test word(s).
… power. Also improve error reporting here slightly.
For parsing, operator precedence is immediatey below * and /, and ^ is right associative (a^b^c = a^(b^c)). This is implemented as another case of ExpressionBinaryOp.
Via getTransitionsMappedIterator() methods.
Skip needless computation for trivial intervals ([1,1]). Also fixes a bug for minimising expected reward to reach a target in IMDPs, where the max is infinite, but the min is finite. Infinite-valued choices should have value +Inf during value iteration, but multiplying +Inf by totP=0.0 gives NaN instead. A regression test is added to check this.
In particular, this means allowing some tolerance for distributions where probabilities are doubles (1e-12 relative, by default). This also allows bisimulation minimisation to factor in double imprecision too.
Now passes all PRISM regressions tests.
…max - still not supported on the prism side
heuristicus
force-pushed
the
robots2
branch
from
ffff48f
to
429c630
Compare
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.
No description provided.