Was already enabled for steady-state probabilities in 3cb4f42d,
following addition of no-sparse printing for MTBDD vectors.
Not sure why this was not enabled too.
Was previously being parsed as a PRISM expression as a fallback,
but the parser currently does not handle big integers.
Test case added. And these tests moved to a new "testing" directory.
Calling code should be calling Prism.setPRISMModelConstants now,
after recent changes to the usage of Prism. But the methods
in GUISimulator got missed when this was updated elsewhere.
Introduced in symbolic engines during recent-ish refactoring.
Seems to have been wrong in explicit engines for longer.
Format is 0=0.27109177824020264, not 0:=0.27109177824020264
This allows simulation and statistical model checking to be performed on
a wider range of model sources, not just PRISM language models.
SimulatorEngine and associated files have had their dependencies on
ModulesFile removed, now using ModelGenerator and RewardGenerator
instead. SimulatorEngine also no longer uses TransitionList and Updater:
these are internal to the ModulesFileModelGenerator which provides
ModelGenerator access to a PRISM model.
Associated simulator classes have been altered too. Path and Sampler
classes now use a ModelInfo and RewardGenerator, rather than a
ModulesFile and TransitionList. Path classes store an action object and
action string, rather than action info specific to a ModulesFile. This
means that the methods getTransitionModuleOrAction and
getTransitionModuleOrActionIndex disappear from SimulatorEngine,replaced
by getTransitionAction and getTransitionActionString.
Usage of SimulatorEngine changes slightly. There is now a loadModel()
method, after which paths are created or statistical model checking
initiated, rather than a ModulesFile being passed to these latter
methods as done previously. The main function of SimulatorEngine is
manual/automatic path creation and statistical model checking. Exploring
states/transitions of a model is now de-emphasised, since this is
already provided directly by the passed in ModelGenerator. But
SimulatorEngine still provide access to information about transitions
etc. in the model because it allows this to be queried for arbitrary
states along created paths. The method checkModelForSimulation() has
been removed - since these checks now occur earlier at the point of
creating a ModelGenerator - and is now in Prism instead.
In Prism, in line with other recent changes, simulation-based methods
now use the currently loaded model, rather than taking a passed in
ModulesFile. For use within these methods, or from other methods that
want to access SimulatorEngine directly, there is a new method
loadModelIntoSimulator().
Various utility methods added to ModelGenerator, all with default (but not
necessarily the most efficient) implementations. These include methods for:
computing indices of choices/transitions (getChoiceIndexOfTransition,
getChoiceOffsetOfTransition, getTotalIndexOfTransition); checking transition
availability (isDeadlock, isDeterministic); computing probability/rate sums
(getChoiceProbabilitySum, getProbabilitySum); action label strings
(getTransitionActionString, getChoiceActionString) and transition strings
(getTransitionUpdateString, getTransitionUpdateStringFull). ModelInfo also
has getActionStringDescription, associated with the last two groups.
Implementations added for most of these methods in ModulesFileModelGenerator
and ModulesFileModelGeneratorSymbolic, mostly just via the existing methods
in the underlying TransitionList. A little bit of additional tidying in these
classes too.
This allows reward info to be specified separately from the model (ModelInfo & ModelGenerator).
Firstly, RewardGenerator includes basic syntactic info: the number of reward structs and their names.
Secondly it provides access to the rewards themselves.
Implementations of RewardGenerator can allow rewards to be queried in one or more ways:
by State object; by (integer) state index; or syntactically by providing a RewardStruct.
Default implementations of all methods are provided which assume that rewards are
looked up by State object and there are no rewards defined (zero reward structs).
A subset of these methods were previously in ModelInfo/ModelGenerator,
so classes that implement those interfaces and implement them should add
“implements RewardGenerator” or remove any @Override annotations.
RewardGenerator is now:
* implemented by ModulesFileModelGenerator and ModulesFileModelGeneratorSymbolic
* created and stored in Prism as needed
* passed to explicit engine model checkers via new method setModelCheckingInfo,
which now replaces setModulesFileAndPropertiesFile
* used in explicit.ConstructRewards to build reward structures
* passed to ModelGenerator2MTBDD for symbolic construction from ModelGenerators
There is also a refactor of the code for looking up index of reward structs:
New methods in ExpressionReward, including switch to RewardGenerator object,
and the methods return the index, not a RewardStruct object.
* Remove some unneeded methods: getExploreState() and getTransitionAction(int i)
* Add a default implementation of getNumVars() based on name list
Existing code which implements the first two methods and annotates them with @Override needs to be changed.
TestModelGenerator, ModulesFileModelGenerator, ModulesFileModelGeneratorSymbolic updated accordingly.
Dave Parker