Export the values of the following variables in the main makefile,
avoiding the need to pass through each one to child make processes
manually:
CFLAGS
CXXFLAGS
LDFLAGS
JFLAGS
LIBPREFIX
LIBSUFFIX
In cudd/Makefile, don't declare the following variables, as this
prevents them from being inherited from the environment created by the
top-level make process:
CC
CXX
CXXFLAGS
LDFLAGS
EXE
In the top-level makefile, CFLAGS is defined in terms of CUDD_XCFLAGS on
every OS and architecture; the only difference between them is that
CFLAGS incorporates the value of OPTIMISE, whereas CUDD_XCFLAGS doesn't.
This is because the CUDD makefile draws a distinction between
"machine-independent flags" (ICFLAGS) and "machine-dependent flags"
(XCFLAGS), and the optimisation level is a machine-independent flag. The
same is true of DEBUG (-g) and WARNINGS (-Ox), but for some reason they
aren't treated the same way as OPTIMISE.
Rather than defining CFLAGS in terms of CUDD_XCFLAGS, do the following:
* define CFLAGS directly;
* remove CUDD_XCFLAGS;
* define ICFLAGS and XCFLAGS in the CUDD-related targets in terms of the
relevant flags in CFLAGS - i.e., extract the values (if any) of DEBUG,
OPTIMISE and WARNINGS from CFLAGS and pass them to the CUDD makefile
as ICFLAGS, and whatever's left as XCFLAGS.
This will also help to standardise the compiler flags used across all
the libraries (e.g., currently CUDD is compiled with -g but nothing else
is).
The use of $(filter-out) means that weird things might happen if DEBUG,
OPTIMISE or WARNINGS ever contain % symbols, but this (hopefully) isn't
likely...
The CC, CXX and JAVACC makefile variables are all redefined in the
"compiler flags" section of the makefile, which makes them easy to miss.
Define them in the "compilers" section instead.
Export the values of the following standard compiler and compiler flag
variables in the main makefile, avoiding the need to pass through each
one to child make processes manually:
CC
CXX
LD
JAVAC
JAVACC
Since JAVAC is manually exported as "$(JAVAC) $(JFLAGS)" by the main
makefile, additionally separate JAVAC and JFLAGS into separate variables
from the perspective of child make processes.
Rename the following makefile variables to their standard implicit
equivalents in GNU Make for the sake of clarity:
C -> CC
CPP -> CXX
CPPFLAGS -> CXXFLAGS
Rather than overriding the default path to the PRISM source directory by
setting the PRISM_SRC_DIR environment variable, do so by supplying an
argument to the script.
Rename the following makefile variables for the sake of clarity in child
makefiles:
SRC_DIR -> PRISM_SRC_DIR
CLASSES_DIR -> PRISM_CLASSES_DIR
OBJ_DIR -> PRISM_OBJ_DIR
LIB_DIR -> PRISM_LIB_DIR
INCLUDE_DIR -> PRISM_INCLUDE_DIR
IMAGES_DIR -> PRISM_IMAGES_DIR
DTDS_DIR -> PRISM_DTDS_DIR
The helper script src/scripts/printversion.sh also makes use of the
value of SRC_DIR exported from the main makefile, so use PRISM_SRC_DIR
in that script too.
Not usually triggered (I think) because the classes are actually compiled
indirectly before this Makefile is even called.
Could be fixed more systematically in all Makefiles by cd-ing into the SRC_DIR directory,
rather than .. or ../..
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).
Dave Parker