We did not perform a required deepCopy of the path expression before checking/replacing maximal state formulas, thus modifying the original expression, which breaks later model checking when doing experiments.

Found by Steffen Märcker.

For 'Export path' from the simulator in the GUI:

If there are reward structures in the model, ask the user whether the
exported path should include the reward information as well.

Provides a switch that allows to specify that reward information
should be included in path export functions, as well as API compatible
forwarding functions.

Indicate in the "Method" part of the result in the GUI that
nondeterminism in the model was resolved uniformly by the
statistical model checking engine.

Print explanation after result to indicate uniform resolution
of nondeterminism in the model by statistical model checking engine.

Installation script failures on Travis...

Previously, we have called java as a child process of the startup
script. This is a bit problematic, as killing the startup script (in a
non-interactive setting, e.g., by running via a script that enforces a
time limit or killing it via a process manager) does not necessarily kill the
Java child process. This can leave potentially long-running Java processes
consuming resources floating around.

We avoid this by using 'exec java ...' to invoke Java, which replaces
the shell process with the Java process for PRISM, keeping the process
ID.

As a fallback, if it turns out there a unforseen problems with the new
exec-based approach, one can set the environment variable
PRISM_NO_EXEC to 'yes' to obtain the old behaviour, i.e.,

export PRISM_NO_EXEC=yes
bin/prism ...

Previously, the PRISM startup scripts on MacOS and Linux would call a
GUI notification tool when the PRISM execution has finished and the
environment variable NOTIFY was set to 'yes'.

This feature was not advertised and probably not used much in
practice.  We remove it because it interferes with an exec-based
mechanism of starting the Java VM for PRISM (see next commit).

It is simple to get similar functionality by using a small wrapper
script or other shell functionality.

We should propagate the EvaluateContext into the inner expression.

The missing 'ec' led to exceptions in model construction for exact/parametric mode, as variable valuations are then not available, e.g., when used in guards ('-s' where 's' is a state variable).

Checked the other evaluateExact calls, those are fine.

We have observed crashes during GUI startup, during the splash screen phase, with the following exception stack trace:

Exception in thread "main" java.util.ConcurrentModificationException
	at java.util.Vector$Itr.checkForComodification(Vector.java:1184)
	at java.util.Vector$Itr.next(Vector.java:1137)
	at javax.swing.plaf.basic.BasicDirectoryModel$LoadFilesThread.cancelRunnables(BasicDirectoryModel.java:340)
	at javax.swing.plaf.basic.BasicDirectoryModel$LoadFilesThread.cancelRunnables(BasicDirectoryModel.java:346)
	at javax.swing.plaf.basic.BasicDirectoryModel.validateFileCache(BasicDirectoryModel.java:135)
	at javax.swing.plaf.basic.BasicDirectoryModel.propertyChange(BasicDirectoryModel.java:69)
	at java.beans.PropertyChangeSupport.fire(PropertyChangeSupport.java:335)
	at java.beans.PropertyChangeSupport.firePropertyChange(PropertyChangeSupport.java:327)
	at java.beans.PropertyChangeSupport.firePropertyChange(PropertyChangeSupport.java:263)
	at java.awt.Component.firePropertyChange(Component.java:8422)
	at javax.swing.JFileChooser.setCurrentDirectory(JFileChooser.java:598)
	at userinterface.GUIPrism.setupResources(GUIPrism.java:262)
	at userinterface.GUIPrism.<init>(GUIPrism.java:228)
	at userinterface.GUIPrism.main(GUIPrism.java:127)

The problem seems to be that creating a JFileChooser and then using setCurrentDirectory a short time later might result in some race condition in the Java platform code (the JFileChooser asynchronously pre-caches the directory contents and has to cancel these threads when the directory is changed). We have also not been able to reliably trigger it.

While this doesn't look to be our fault, we avoid this by doing the currentDir logic before creating the JFileChooser and then passing this directly during the construction of the JFileChooser.

(with Philipp Chrszon)

The HTML file generated by the iteration export loads Javascript and
CSS resources from www.prismmodelchecker.org. Previously, those URLs
used http as the protocol. If such a generated HTML file was loaded
via an https-connections, current browsers would reasonably block
access to the Javascript, as it's not be loaded over a secure
connection.

As the prismmodelchecker.org site now supports https, we switch to
https for loading those resources.

Due to the change in 98c019b1,
the C-level 'Gauss-Seidel not supported' checks of the MTBDD engine
get triggered now more often. Before, they would just return, now we
actually do the usual DD cleanup there to avoid DD reference leaks.

(plus: put breaks in switch statements on separate lines to better see code-flow)

Automatically switch to MTBDD engine before model checking if hybrid/sparse engine can not handle state space

If, after model building with hybrid or sparse engine, we detect that the
configured engine can definitely not handle the model (i.e., if number of states
is larger than Integer.MAX_VALUE), we auto-switch to the MTBDD engine.

As currently there is no support for Rmin/max[C] computations using hybrid engine, and hybrid is the default engine, automatically switch to the sparse engine, similar to what is done for other computations.

When constructing a model using the explicit engine, the set of
reachable states is always sorted. This is done purely for aesthetic
reasons and is potentially time-consuming for large models, so make it
optional (although enable it by default for backwards-compatibility, and
explicitly enable state sorting in the test cases that use
ConstructModel in case this default changes at a later time).

The corresponding `checkNumStates(odd)` were missing.

The corresponding `checkNumStates(odd)` were missing.

Fix typo in the variable definition. Changed files under src/param/ were not be recompiled if only files in param/ were changed.

When the model has to be transformed (Pmax-quotienting) to apply interval iteration, we currently don't support strategy generation and thus have to properly deallocate the strategy array that has been prepared.

When converting an MTBDD to an integer vector (as is done to prepare the storage for the computed strategy for Pmax-Until using the sparse engine), the MTBDD has to be zero for non-reachable states, as that could lead to out-of-bounds writes to the array during conversion.

This commit adds the required restriction to reach in prism.NondetModelChecker.

+ test case
+ fixes deref of 'yes' during initialization

Successful instanceof implies non-null.

Unused, unfinished old code.

Silences compile warnings (JDKs >=9).

(adapted by Joachim Klein from https://github.com/prismmodelchecker/prism/pull/91)

Tag: performance

For the evaluation of integer math operations, use the ...Exact methods from
java.lang.Math to catch integer under-/overflows and throw PrismLangExceptions.

(adapted by Joachim Klein from https://github.com/prismmodelchecker/prism/pull/91)

Tag: performance

(split from https://github.com/prismmodelchecker/prism/pull/91)

The oraclejdk10 target offered by travis is sometimes unstable due to
JDK download brittleness. We thus switch to the openjdk10
target. Additionally, add openjdk11 as a target.

Expressions.evaluate (binary,unary,function): Avoid explicit boxing of Booleans, Integers and Doubles

During the evaluate calls, the code previously used 'new Boolean' and 'new
Integer' constructors for the result values. By removing these allocations
and simply letting Java take care of boxing the resulting primitive
values, the integrated caching of Java can avoid creating objects in a
lot of cases (always for Boolean, and often for Integers in a certain
range).

(adapted by Joachim Klein from https://github.com/prismmodelchecker/prism/pull/91)

Tag: performance

When DOT graphs of a model are exported, their maximum permitted size is
hardcoded to 8 inches wide by 5 inches high, which is too small for the
rendered drawing to be useful (e.g. during debugging) for all but the
simplest of models. Remove the maximum size restriction, allowing tools
to render the drawing with its natural dimensions.