In addition to declaring some variables to be observable using an
observables ... endobservables block, other observables can be
defined as follows:
observable "top" = y=ymax;
which comprises a name and an expression to define it.
These named observables can appear in properties (e.g., to express
a target for reachability) in the same way as labels.
The ModelGenerator/ModelInfo interfaces are updated accordingly.
The key methods that need to be implemented are getObservableNames()
and getObservableTypes(), in ModelInfo and getObservation(State),
in ModelGenerator. As an optimisation (but essential for efficiency
in practice) isVarObservable() should also be implemented, since this
is needed to construct Belief objects that are as compact as possible.
Implementation/code details:
* New parser AST classes: ObservableVars/Observable (for observable
definitions in ModulesFile) and ExpressionObs (for references to
observables in expressions).
* A few imports are fixed to avoid names clases with Observable
* Observations/unobservations are now just stored as State objects,
so the Observation/Unobservation classes (in parser) are now redundant
and have been removed.
Implementation pushed into a helper class IdentUsage,
used in both ModulesFile and PropertiesFile.
Also, slightly improve error messages for identifier clashes
(say where the original use was, e.g. "constant").
Also, add isIdentUsed and checkIdent to ModelInfo, with default implementations.
This removes another dependency of PropertiesFile on ModulesFile.
Assertions that checked that, e.g., arrays were the same size have been removed.
(These are disabled in the JDK by default anyway)
Some value iteration methods, which take in an "init" array of known values
can violate these assertions, e.g., when it is created to be over size for efficiency
in an abstraction refinement loop.
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.
Dave Parker