This potentially allows checking of "symbolic" expressions for methods/engines
other than the parametric engine. It will also allow simplification of the
mechanisms for storing results from parametric model checking, aligning it
with other parts of the code.
In particular for a whole State, not just a substate.
Also for just some constants, with no variable values.
Can be used to get an expression symbolically in terms of constants.
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.
Export the values of the following standard compiler and compiler flag
variables in the main makefile, avoiding the need to pass through each
one to child make processes manually:
CC
CXX
LD
JAVAC
JAVACC
Since JAVAC is manually exported as "$(JAVAC) $(JFLAGS)" by the main
makefile, additionally separate JAVAC and JFLAGS into separate variables
from the perspective of child make processes.
Rename the following makefile variables for the sake of clarity in child
makefiles:
SRC_DIR -> PRISM_SRC_DIR
CLASSES_DIR -> PRISM_CLASSES_DIR
OBJ_DIR -> PRISM_OBJ_DIR
LIB_DIR -> PRISM_LIB_DIR
INCLUDE_DIR -> PRISM_INCLUDE_DIR
IMAGES_DIR -> PRISM_IMAGES_DIR
DTDS_DIR -> PRISM_DTDS_DIR
The helper script src/scripts/printversion.sh also makes use of the
value of SRC_DIR exported from the main makefile, so use PRISM_SRC_DIR
in that script too.
Previously, when converting from boolean to BigRational, a fresh object was allocated. However,
as BigRationals are immutable, we can just return BigRational.ONE or .ZERO, respectively.
Tag: performance?
Same fix as in the explicit engine (eeb8016184), for issue #29.
This change can currently not be detected by any of the properties supported by the exact/parametric engine.
As noted in #68, the javah tool has been removed in JDK10. Here, we switch to the new way of generating the JNI .h files, using the -h option of the regular javac compiler.
We have to adapt all Makefiles (not only those in directories that contain classes with native methods), as javac compiles all required classes (and generates their JNI headers) beyond the directory with the Makefile.
The .h files generated by javac -h had a different naming scheme, now there is a prefix for the package name. To avoid having to touch all the #includes, we generate the new .h files in prism/include/jni and provide legacy headers in the old location and with the old name, forwarding the the corresponding new header. In the future, at an appropriate moment, those legacy headers can be removed and replace with direct includes.
Currently, there is a post-processing step on Windows: After the .h file is generated, dos2unix is called to replace the Windows CRLF line endings. Otherwise, the generated headers show up as changed files in version control. As now there are no special targets for the generation of the .h files anymore, we move to a global post-processing step and call dos2unix on prism/include/jni/*.h at the end of building.
Expressions are now evaluated exactly in parametric / exact model checking mode for:
- state updates
- command guards
- the if part of if-then-else expressions
- reward guards
- reward values
- Boolean expressions in RESULTS in property files
Add various test cases to check that it is now handled properly.
The parametric engine works under the assumption that models
are well-defined, i.e., that parameter valuations will lead
to graph-preserving probabilities, etc.
If we encounter a point in a region where these assumptions
don't hold, we now treat this by splitting the region. Regions
with such an improper midpoint that are below the precision
threshold are considered to be undefined and further processing
is aborted.
In particular, this treatment ensures that we never perform
policy iteration on a model with parameter instantiation
that is not well defined / supported. E.g., if there
were negative rewards for such a point, policy iteration
would previously not necessarily terminate.
To check that, for all parameter valuations in a region,
(1) some threshold property holds or (2) that a given
scheduler is optimal, a set of constraints is checked.
Currently, only heuristic checking is implemented, i.e., determining
via sampling if the constraints hold. This can produce false positives
in the region computations, i.e., a region is not sufficiently split.
We add a warning if the region computation relied on the heuristic
constraint check and thus can be imprecise.
In particular, align output format with other engines and treat exact mode
specially (print rational numbers instead of functions, approximate values)
For parametric, output results per region.
Print not only the state index, but also the variable valuations for that state
(similar to the other engines).
Example for exact:
prism prism-examples/dice/dice.pm -pf 'filter(print, P=?[ F d=1])' --exact
=== Previously ===
Results (non-zero only) for filter true:
([0.0,1.0])0:={ 1 | 6 }1:={ 1 | 3 }2:={ 0 }3:={ 2 | 3 }4:={ 0 }5:={ 0 }6:={ 0 }7:={ 1 }8:={ 0 }9:={ 0 }10:={ 0 }11:={ 0 }12:={ 0 }
==================
=== Now ==========
Results (non-zero only) for filter true:
0:(0,0)=1/6 (~0.16666666666666666)
1:(1,0)=1/3 (~0.33333333333333337)
3:(3,0)=2/3 (~0.6666666666666666)
7:(7,1)=1 (1.0)
==================
Example for parametric:
=== Previously ===
Results (non-zero only) for filter true:
([0.0,0.5])0:={ ( -1 ) p + 1 }1:={ 1 }2:={ 0 }([0.5,1.0])0:={ p }1:={ 1 }2:={ 0 }
==================
=== Now ==========
Results (non-zero only) for filter true:
([0.0,0.5]):
0:(0)={ ( -1 ) p + 1 }
1:(1)={ 1 }
([0.5,1.0]):
0:(0)={ p }
1:(1)={ 1 }
==================
To ensure that the policy iteration (performed on an MDP where parameters have been replaced
by a parameter valuation) converges and converges on the right result in the presence of
zero-reward end components, we initialise the policy iteration for Rmin[F] with a
proper scheduler, i.e., that reaches the goal with probability one (see [BertsekasTsitsiklis91]).
Together with the previous commit, this fixes#4 and #15.
In the state eliminator, i.e., solving for a DTMC, a state that has probability
zero of reaching the target states (i.e., that can not reach the target state)
should get infinite reward.
Previously, the check for this looked at the returned set of collectStatesBackward(),
which always returns the whole state space (used for backward elimination order).
Now, we use the variant of collectStatesBackward() that only returns the states
that can reach the target set.
Additionally, we now compute the set of infinity states for Rmin/Rmax using
prob0a / prob0e, respectively, and ensure that they get value infinity.
Dave Parker