If the underlying file handle corresponds to stdout, we ignore the
close() call. Correspondingly, we should not mark the log as closed,
as some of the functionality in PrismCL (e.g., for export to 'stdout'
in the explicit engine) relies on the possibility of closing the
corresponding log, leading to an exception. Bug was introduced during
recent efforts to make log closing more robust and catch
write-after-close use of logs.
Test case:
prism prism-examples/dice/dice.pm --exportmodel stdout.all -ex
Previously, if DebugJDD found a fatal problem (deref of a node with 0
refs, ...), it would throw an exception, which would then usually lead
to a huge number of leaked nodes on PRISM termination, cluttering the
log.
Now, we don't bother with leak checkes until all the fatal problems
are dealt with.
'testsfull' runs the test cases from prism-tests against all the
different engines (explicit, hybrid, sparse, mtbdd, exact), with and
without interval iteration and topological ordering, where appropriate.
Tweak the result strings for the CTL with step bounds cases (currently
computation is not supported with any engine). Previously, an error was
expected, but the properties are not actually erroneous. Additonally, the
error message was not uniform between the different engines, leading to
spurious failures against the exact engine.
Some of the result values for the test cases were floating-point approximations,
which results in 'close but inaccurate' errors when running the test cases against
the exact engine.
We replace those results either with the exact values or mark the approximated
results with ~... (mostly for a few CTMC properties, where the exact results
are a bit unwieldly).
We now count non-convergence (i.e., error message contains 'did not converge') as a sub-type of failures.
Additionally, count skipped export-runs and skipped duplicate runs as sub-types of skipped tests.
In case that no export_name is passed to one of the PM_Export..., PS_Export.... functions,
ReleaseStringUTFChars() would be called even though there was no previous call to
GetStringUTFChars(), leading to a SEGFAULT.
This is for robustness, PRISM always passes an export_name string.
Previously, the flags for interval/topological iteration and
for Pmax-quotienting would not be initialised if the ModelChecker
was constructed directly.
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.
During model exploration of a CTMC, when using fast adaptive uniformisation,
only the last part of an update (rate & successor state) is used, as the
indexing of the outgoing transitions is buggy.
We now store all outgoing transitions and handle the case of multiple
choices/enabled commands in the CTMC.
+ two test cases
As the nondeterminism is resolved to generate the paths, e.g., for an MDP
the model checking happens in the resulting DTMC, allow the use of the
DTMC-style operators.
If we remove the nondeterminism in a model (e.g., using uniform choice
of actions in the simulator/statisticial model checking), we'd like to
know the resulting model type.
Similar to the behaviour in the properties list, if we double-click
inside the constant or label table but not on an existing entry, we
add a new contant/label line in the table.
On first close, we set the file pointer to 0 to indicate that it
is not valid anymore. As PrismLog implements Close/AutoCloseable, multiple
close calls have to be supported.
Before, calling close multiple times could result in double free
crashes on Linux (seen in development branches, not master).
We also check that we don't write on a closed FILE pointer, but raise
an exception instead. Here, we use a RuntimeException
(IllegalStateException) instead of a PrismException as changing the
PrismLog interface would be quite disruptive to the rest of the code.
(addresses #72)
If the desired accuracy is to small, the naive weight computation can run
into an infinite loop, as floating point precision / rounding leads to
non-termination of the loop.
To partially address this, we move the accuracy check up, so that it
is also applied in the case of the 'naive' computation. This should make
it much less likely to run into this in practice.
For a full fix, we'd either need to check for non-progress in the loop
or do an analysis that the floating-point precision of double always
suffices for the remaining allowed input values.
Previously, despite the error message being printed, the Fox-Glynn computation
was nevertheless performed and the weights returned to the caller.
Now, we return and let the caller deal with the error condition.
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.
Joachim Klein