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).
When using -x to add additional options, i.e., to force a specific engine,
often runs of PRISM are effectively duplicated, e.g., if there are .args files
that select multiple engines.
Using the --skip-duplicate-runs, prism-auto tries to clean up the argument list,
remove switches that don't have an effect and to detect duplicate runs, only actually
executing the first one.
Option to allow skipping PRISM runs that do exports.
This is useful when overriding the engine, as the exports differ slightly
between engines and some export options are not supported.
In nailgun mode, if --ngprism is not specified, we derive the location of the ngprism
binary from the --prog setting: We simply replace the file part with ngprism, as usually
the ngprism binary is located in the same directory as the prism startup script.
When saving the settings file, we now create non-existent directories on the path to the file
(mkdir -p style).
Additionally, use try (...) {} construction so that the FileWriter is closed on any exception.
When PrismSettings loads a settings file from a previous version,
in loadSettingsFile(File) it resaves the file to add the settings
of the current version.
Previously, for resave it would write to the default location, no
matter if the settings file location passed to loadSettingsFile
pointed to another file (e.g., due to loading the settings on the
command-line PRISM with -settings ...).
Now, we resave to the same file as that used for loading.
Now, all the top-level packages have Makefiles and search for Java files
in subpackages.
If a .java file does not get picked up by the Makefiles, it will
nonetheless be compiled if referenced from somewhere else in the
project, but dependency tracking at the level of 'make' is broken.
The FileSetting object stores a FileSelector, which is allocated
using defaultSelector() during construction. It can also be set via setFileSelector().
To avoid constructing a FileSelector (and thus call into the Swing/AWT Java package) in
headless / command-line mode, we allocate the default selector on first use, i.e.,
whenever the selector is null in a call to getFileSelector().
Currently, most of the Setting classes construct a SettingRenderer and SettingEditor statically, for use in the GUI.
When running PRISM from the command-line (PrismCL), we make sure to run Java in headless mode and generally those calls then don't matter.
If there are problems with the AWT configuration, there can be exceptions even for PrismCL. So, here, we
switch from static allocation on class loading to static allocation on first use of getSettingsEditor() and getSettingsRenderer().
The formula may have bounds attached to the temporal operators, so we
strive to preserve them.
Dualizing the operators does not change the bounds, so we can just
attach them (see ExpressionTemporal.convertToUntilForm()) to the new
temporal operator.
It looks like the value of col_offset is never actually used
during the recursion steps. For the moment, we just initialise with 0
(can not be worse than starting with uninitialised value) and mark
as candidate for refactoring after thorough inspections of
the various code paths.
(via linting)
In test mode, we'd like to have proper 'not supported' handling during the tests,
so we don't exit immediately when encountering an engine / iteration method that
is incompatible, as that would count as a failure.
Due to a typo, the upper iteration uses `updateValueFromBelow` instead of `updateValueFromAbove`
to update the value vector. When the flag for monotonicity enforcement from above is active (default),
all values are thus forced to be above the upper bound, preventing convergence.
Example:
prism functionality/verify/mdps/reach/mdp_simple.nm functionality/verify/mdps/reach/mdp_simple.nm.props -sparse -intervaliter
+ test case
Steffen Märcker