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.
E.g., -const x=0:1/3:1 now works in non-exact/non-parametric mode as well.
Additionally, catch the case where the constants are not finite numbers (infinities, NaN).
Using the infrastructure from the previous commit, we request exact evaluation
of constants in exact and parametric model checking mode.
Additionally, note where we deliberately choose non-exact evaluation mode.
Add corresponding test cases.
Previously, constants that are defined via an expression
were evaluated using standard (integer or floating point) arithmetic,
even in parametric or exact model checking mode.
This commit provides the infrastructure for requesting that constant
expressions are evaluated using exact arithmetic.
To keep the API backward compatible, we introduce additional methods that
offer an 'exact' flag, but keep the old methods as well. Those default to
normal arithmetic.
TypeDouble constants are kept as rational numbers, while int and boolean
constants are converted to Java data types. For int, an exception is raised
if the value can't be exactly represented by Java int.
Support matching of constants in RESULT strings for the case
that constants in the model are exact rational
numbers (implemented in subsequent commits).
This allows storage of BigRational values in StateValues / Values vectors, e.g.,
to store constants that have been evaluated exactly.
TypeDouble.castValueTo now returns a Number instead of a Double, requiring the use
of the doubleValue() method in several places where the value is evaluated using
double arithmetic.
To guarantee convergence, the power method requires the precomputation
P = (Q * deltaT + I)
from: William J. Stewart: Introduction to the Numerical Solution of Markov Chains p. 124.
For JDK10, the test suite did not run as the JDK8 binary installed in /usr/bin/ was used for the PRISM runs instead of the JDK10 binaries, even though the JDK10 bin directory comes first on the PATH. This is due to the python startup helpers (when running prism-auto for the tests) fiddling with the PATH variable, prepending /usr/bin/...
So, we now just set the PRISM_JAVA environment variable to the java binary on the PATH from the travis build script, which is then picked up correctly in the prism startup script.
Print test statistics also in the (not particularly useful) case that the timeout is set to 0 by testing against None instead to see if a timeout was set.
The occurence of a line with 'Error:' does not necessarily imply a
failed test result, e.g., for test cases that test against the error
messages.
So we revert the previous change related to the printing of 'Error' lines
and tweak the handling in verbose-test mode some more.
Only F/U operators with upper bound have a bounded path length and can
thus skip the maximal path length checks.
Test cases (will continue sampling beyond the default max path length,
appearing to hang):
prism prism-examples/dice/dice.pm -pf 'P=?[ F>2 s=0 ]' -sim
prism prism-examples/dice/dice.pm -pf 'P=?[ F>2 s=0 ]' -sim -ctmc
After this fix, the usual error message for unbounded operators is
generated.
We now explicitly remember if there was an upper bound instead of
relying on an upper bound of Integer.MAX_VALUE in the case of an
absent bound.
Statistical MC, P[F]/P[U] in discrete time setting with time bounds.
The action object attached to a transition can be null (internal action), leading to a null pointer
exception when trying to call the toString method.
+ test case
These were previously deprecated and now removed in Java 10.
The 32/64-bit scripts are now identical, but kept separate
for now in case of later changes.
If there is a problem in ASTElement.toString for the AST element
that is optionally attached to the exception, we catch the exception
and return the error message without it.
The state information of the model-automaton product are stored as an int array, with one
entry for every combination of model state index and automaton state index. Thus, |S|*|A| has to be
less than INT_MAX, even if the reachable state space could be index with an int.
Thus, we use Math.multiplyExact to catch the case that the product of the two numbers of states overflows
the int range and throw an Exception.
In non-test mode, PRISM and prism-auto both write to stdout, without
prism-auto seeing/processing the output of PRISM. If the output of
prism-auto is piped to another program or to a file, the prism-auto
output is buffered. Then, the output by prism-auto (e.g., printing the
command lines) is not properly synchronized with the output of the
PRISM instances.
So, we flush stdout at appropriate locations.
Additionally, on timeout we prepend a '\n' to ensure that the timeout
message starts at a new line (in particular for the common case of a
timeout during explicit model building, where there is no newline from
PRISM until the model is fully built).
Joachim Klein