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.
In other words, if the result for a state is q, and the bound p falls in the range
[q-e,q+e] where is the error bound from model checking computations, then an
error is generated rather than producing a potentially incorrect true/false result.
Explicit model checking engine only for now.
Test cases are added, and some (unrelated) existing regression tests with dubiously
close bound checks are fixed.
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.
There is no explicit model type keyword added to the parser.
Instead, LTSs are auto-detected by the absence of probabilities.
ConstructModel is extended to build LTSs. Model checking (CTL+LTL)
can be done out of the box using the existing NonProbModelChecker class.
A few MDP regression tests are clarified to make it clear that the
models are MDPs, not LTSs.
Rename the class to match those for other models stored in this way.
And add some missing methods to make it usable as a normal model.
Also tidy up the class a bit.
Make this method, which is used to check that doubles are (approximately) equal,
use relative rather than absolute error, which is more robust in general.
This is now used in places where the same check was done, but with an (identical)
hard-coded epsilon of 1e-12. Property.getExpectedResultString has also been changed,
which previously used 1e-10, but there seems no reason for this not to use 1e-12.
This just sets a null action for all existing transitions. Previously,
this was in DTMCExplicit, but has been removed from there. This means
it can also be removed from DTMCView.
In fact the implementation is taken from DTMCView, which was cleaner.
Furthermore, the same mechanism is now also used for implementing
getTransitionsAndActionsIterator in DTMCFromMDPMemorylessAdversary.
This accesses the MDP storage directly, rather than via getTransitionsIterator.
Not really used at the moment since methods that need to be fast, like matrix-vector
multiplication, are directly implemented already.
Currently these do not actually make much sense anyway since the class is primarily
intended to store distributions over indices into some other list (e.g., states).
This returns a map view of the (optionally stored) label info,
i.e., a map from label name strings to Bitsets of satisfying states.
A default implementation is added using existing methods.
Move getNumTransitions(int) to Model from DTMC.
There is a default implementation using getSuccessorsIterator(int).
This allows us to provide a default implementation of getNumTransitions() too.
Also move getNumTransitions(PrimitiveIterator.OfInt) to Model from DTMC/NondetModel.
A default implementation of createVarList() in ModelInfo now creates
a VarList automatically, so this does not need to be implemented when
creating a ModelGenerator. Instead, just getVarDeclarationType(int i),
which is a newly added method, should be implemented. There is also
a default implementation of this, but it assumes that integer variables
are unbounded, which will not work with the symbolic engine.
In a related change, ModelInfo can now optionally specify which "module"
a variable belongs to (via getVarModuleIndex and getModuleName).
ModulesFile is updated, to fully support the new version of ModelInfo,
and all implementations of ModelGenerator are simplified where possible.
The old VarList constructor which takes a ModulesFile is removed and
replaced with one which takes a ModelInfo object.
Both types of engine now disallow negative/infinite/NaN rewards.
Symbolic engines will mostly still not detect the presence of NaN
due to the way that CUDD deals with this.
Regression tests also added.
Dave Parker