When starting the Nailgun server via 'prism -ng', we now allow the main class to be served
to be configured via the NG_MAINCLASS environment variable. If not set, defaults to prism.PrismCL, as before.
This allows to use nailgun also with other test main methods, e.g., those in the LTL-to-automata classes.
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?
(1) In general, for user actions (a_...), ensure that setComputing(false)
is called even if the underlying computing resulted in an exception.
This ensures that the buttons/menu items of the simulator are properly
enabled again and we don't get into a deadlock situation where we
can't even start a new path.
(2) For the automatic step actions, ensure that the path display is
updated even if there is an exception, as there may have been
intermediate steps that had succeeded before the error occurred.
Previously, the resulting distance was considered as a time value,
not a step value. For discrete time models, this coincidently does
the right thing, but for continuous time models this does not work as expected.
Technically, as engine.getPathSize() is a long and the value from the text box
is an int, the result is a long and that leads Java to prefer the a_backTrack(double)
and a_autoStep(double) variants of these methods. We cast to an int to ensure
that the int-parameter variants are taken.
Use enum fields to store the delimiters instead of the map.
Add some more comments to alert the user that proper quoting (for HTML labels) might be necessary.
Graphviz implements a subset of HTML that can be used in node and edge
labels (see https://graphviz.gitlab.io/_pages/doc/info/shapes.html#html
for a description of the subset) as an alternative to the plain-text
default style. The HTML-like style uses different attribute value
delimiters (<>) to the plain text style (""), but the latter is
hardcoded in explicit.graphviz.Decoration. The line delimiters also
differ (<br/> and \n respectively).
Provide support for both plain text and HTML-like labels in Decorator;
the label type can be changed by calling setLabelType() before appending
any label content via labelAddBelow() or labelAddAbove().
Move release building automation from top-level Makefile to main
PRISM Makefile and delete the top-level one: after switching to git,
the required top-level directories (prism-examples, cudd, etc.) are
always present and there is no need for the separation.
Source releases will now be direct copies of the whole git repo. The Makefile
targets for building binary releases have been simplified and updates. They
are now triggered by "make release" or "make release VERSION=4.5".
There is also a new makefile target "doc" that currently pulls down a copy of
the online manual and stores it in the "manual" directory.
Blacklist the following files from version control:
* prism/lib/prism.jar: this is generated by the "binary" target in
prism/Makefile.
* prism/lib/prism-sources.jar: this is generated by the "source-jar"
target in prism/Makefile.
* prism/prism-sources.txt: this is a temporary build file generated by
the "source-jar" target in prism/Makefile and will be deleted if it
succeeds, but will be left behind if jar(1) exits unsuccessfully.
Create a new target "source-jar" that generates a JAR file containing
PRISM's .java, .form and .jj source files. This can be associated with
the regular JAR file in a Java IDE to more easily debug projects that
use PRISM's Java API.
In the "binary" target, parameterise the following directory names to
match the style used in other targets:
classes -> CLASSES_DIR
dtds -> DTDS_DIR (new variable)
images -> IMAGES_DIR (new variable)
lib -> LIB_DIR
src -> SRC_DIR
The generated action vector was stored in the 'actions' member of the
NDSparseMatrix that was the last one that was built (remembered in the
global ndsm pointer variable).
Now, we store it in the 'actions' member of the mdp_ndsm that is
passed in, as intended.
This did not result in problems before because the call to
build_nd_action_vector() was always immediately after the
corresponding NDSparseMatrix was built.
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.
Joachim Klein