This is a rebased version of the code previously published in the prism-ext repo,
with various bits of code refactored, tidied and improved.
Model construction and model checking support is added to the explicit engine.
The PRISM modelling language is extended with the 'pomdp' model keyword
and observables...endobservables blocks to indicate observable variables.
Accuracy info for numerical results is computed and stored during model checking. For now,
it is always the worst-case accuracy over all states for which results are computed. The
information is stored in a class prism.Accuracy, instances of which are created in a
consistent fashion using prism.AccuracyFactory. Accuracy info is stored in the
prism.Result class.
Accuracy information is generated for all 4 main engines (sparse/hybrid/MTBDD/explicit),
and attached to the Result object when model checking the filter that is wrapped around a
property (currently, just for the default "state" filter). The accuracy is printed with
the main result at the end of model checking. e.g.:
Result: 0.1666666865348816 (+/- 1.1920928955078125E-7; rel err 7.152556520395694E-7)
For now, accuracy info is generated for the majority of properties for DTMCs and MDPs
(no support yet for multi-objective model checking). For methods like value iteration,
where a guaranteed error bound is not generated, convergence information is used, but
reported as being only an estimate.
Test mode has been updated (code in prism.ResultTesting) to use the reported accuracy of
a result to check correctness against a reference result. If it is missing, or only
estimated, the old approach of using default check of 1e-5 with relative error is used.
For the explicit engine, accuracy info is stored in explicit.ModelCheckerResult, returned
by most numerical computation methods i.e. those in the explicit.ModelChecker and
explicit.IterationMethod (sub)classes. At a higher level, the accuracy info is then stored
in explicit.StateValues, when this created from ModelCheckerResult in
explicit.ProbModelChecker.
For symbolic (sparse/hybrid/MTBDD) engines, the error bound info from C++ code is stored
in a variable last_error_bound that be accessed (or reset) from prism.PrismNative, using
the methods getLastErrorBound() and resetModelCheckingInfo(). At a higher level, this is
then stored in subclasses of prism.StateValues, which are created in the
prism.*ModelChecker classes from the results of computations.
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.
The computation reuses the computeSteadyStateBackwardsProbs() method
used for the computation of S=?[ phi ]. We tweak the variable names
and comments in that method to make clear that the solution values of
a BSCC - after multiplication with the mult array - are not
necessarily probabilities anymore.
Sometimes, we want to use the prob0/1... methods to generate schedulers instead of doing
the standard precomputations and don't want to have the normal log output.
Not inherited using inheritSettings()
- Extended functionality available through the prism.Prism API when using ModelGenerators
- Improvements to ModelGenerator interface wrt handling of rewards (and also labels)
- Explicit engine model checkers now build rewards from a ModelGenerator, not a RewardStruct.
This is now (optionally) attached with the setModulesFileAndPropertiesFile method.
- New code to generate symbolic models from ModelGenerators (useful, if not super efficient)
- Move createVarList() method from ModelGenerator up to ModelInfo
- Some code tidying in LabelList
Code was previously at https://github.com/prismmodelchecker/prism-svn/tree/model-generator
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11772 bbc10eb1-c90d-0410-af57-cb519fbb1720
Joachim Klein