For determining syntactic co-safety, we are not interested in
the complex state formulas (e.g., with P, R, E, A, ... operators),
so we iterate without recursing into nested operators.
Furthermore, we currently don't support temporal operator bounds
for co-safety LTL formulas; check for those as well.
* Separate data structures for BeliefMDPState and POMDPStrategyModel
* Push reward construction/storage into the code for the belief MDP
* Factor out prob/reward backup operations into methods for re-use
* Store value function + backup using functional interfaces
* Collapse (now simpler) buildStrategyModel into one method
It requires that the available actions are the same and appear in
the same order (in terms of choice indexing) in each equivalent state.
This always happens for PRISM models built via ConstructModel since
the model construction considers actions one by one in the same
order in each state (and actions must be unique for POMDPs).
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.
Joachim Klein