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.
In Java 9, there is a new system class java.lang.Module that is implicitly imported
everywhere and which clashes with the parser.ast.Module class, resulting in
compilation errors, as javac is not able to disambiguate between the two
automatically.
We are therefore more specific when referencing the PRISM parser's 'Module' class,
by using the full 'parser.ast.Module' name.
Joachim Klein