PR #116 (in particular 5c33a555ac) moved
the post-processing of the BSCC steady state probabilities (weighing
by the exit rates of the CTMC) into computeSteadyStateProbsForBSCC().
This introduced a regression, leading to wrong results, as the
post-processing would be applied on the solution vector that was
returned by the method, but not necessarily on the values passed back
out via the result argument vector.
We fix this by moving the post-processing up, before the copy and
adding a note of caution.
Failure e.g. for
prism prism-tests/papers/Par02/Par02-3.3.3.sm prism-tests/papers/Par02/Par02-3.3.3.sm.props -explicit -testall
The computation reuses the computeSteadyStateBackwardsProbs() method
used for the computation of S=?[ phi ]. We tweak the variable names
and comments in that method to make clear that the solution values of
a BSCC - after multiplication with the mult array - are not
necessarily probabilities anymore.
Provide variants of computeSteadyStateProbs() and computeSteadyStateBackwardsProbs() in DTMCModelChecker
that take a BSCCPostProcessor, which can be used to reweight the steady-state probabilities.
(preparation for steady-state computation for CTMCs)
Previously, during the constructor of GUIMultiModelHandler, a WaitParseThread
was created. If the startup of the other plugins takes longer than the configured delay
(default = 1s, but can be much shorter via settings), the attempted parse can generate
events that reach other plugins/components that are not yet fully initialised, leading
to NullPointerExceptions, etc.
Now, we inhibit the creation of the WaitParseThread until the startup has
completed.
Fixes#111.
The statesOfInterest variables was wrongly not reset to 'reach'.
Not usually caught because the statesOfInterest optimisation is
currently used in very few places. The attached bugfix test shows
an example of where it does go wrong.
This uses a new type of ExpressionFilter with op type "store",
rather than setting a boolean flag on existing filter objects.
Includes two test-cases showing examples where the old code failed.
This cleans up and refactors the iteration over state variable
valuation/value pairs via StateValues. In particular StateValuesMTBDD
learns how to do non-sparse printing.
Furthermore, it
* introduces generic "iterate" and "iterateFiltered"
methods for iterating over the state/values, calling a
StateAndValueConsumer object
* provides a StateAndValueConsumer implementation (StateAndValuePrinter)
that supports printing in the various output styles supported by PRISM
* cleans up the convenience "print" method using default methods in StateValues
* activates the MTBDD engine for one -exportvector based test
Note: Previously, in the StateValuesMTBDD iteration steps, the int[]
array with the current values represented the increments to be added
to the low values of state variables, with the addition
value = low + a[i]
happening on output. Now, we initialise the array with low, i.e.,
the values in the array correspond to the actual variable values.
Avoids DD leak when a previously stored result vector is overwritten (nested filters), e.g. from
prism prism-examples/dice/dice.pm -pf 'filter(sum, P=?[F d=1]) + 0' -mtbdd -exportvector stdout
Exports the value of a model checked property for all states as a vector.
If <file> is "stdout", this is displayed to the log instead of a file.
Currently, only works for a single property: if there is more than one,
then the file gets overwritten each time a property is checked.
Also fixes a bug in the underlying mechanism for storing results vectors
in the explicit engine (within Results objects).
After the previous changes, we are now ready to do MTBDD model checking
even if we can't create the ODD (number of reachable states too large to fit
into an int64_t).
We want to allow MTBDD engine model checking without having an ODD
to encode the BDD state to index information. This allows to deal
with models where the state space is too big for the ODD index type (2^63).
Here, we harden all the places where the ODD information is accessed
to gracefully handle the abscence of the ODD:
* When trying to convert from MTBDD to explicit vector, a
missing ODD is fatal
* When printing state values or a state list, index information is
not available and thus omitted
* For the hybrid and sparse engine, the odd index checks (whether
the number of states fit into an int32_t) are now done using
helper functions that handle both null ODD and out-of-range values.
A : was printed in front of the state variable values, even though
no index was printed, i.e.,
:(3,2,5)=0.5
Only print : after index, as is done for explicit printing. StateValuesMTBDD
currently does not support index-less printing.
Memory allocated with new[] needs to be deallocated with delete[],
not the plain delete operator.
I have not checked whether the code in question is ever called
by PRISM, this is mostly to silence the compiler complaining
(and avoid undefined behaviour).
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.
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 98c019b175,
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)
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.
Joachim Klein