Various utility methods added to ModelGenerator, all with default (but not
necessarily the most efficient) implementations. These include methods for:
computing indices of choices/transitions (getChoiceIndexOfTransition,
getChoiceOffsetOfTransition, getTotalIndexOfTransition); checking transition
availability (isDeadlock, isDeterministic); computing probability/rate sums
(getChoiceProbabilitySum, getProbabilitySum); action label strings
(getTransitionActionString, getChoiceActionString) and transition strings
(getTransitionUpdateString, getTransitionUpdateStringFull). ModelInfo also
has getActionStringDescription, associated with the last two groups.
Implementations added for most of these methods in ModulesFileModelGenerator
and ModulesFileModelGeneratorSymbolic, mostly just via the existing methods
in the underlying TransitionList. A little bit of additional tidying in these
classes too.
This allows reward info to be specified separately from the model (ModelInfo & ModelGenerator).
Firstly, RewardGenerator includes basic syntactic info: the number of reward structs and their names.
Secondly it provides access to the rewards themselves.
Implementations of RewardGenerator can allow rewards to be queried in one or more ways:
by State object; by (integer) state index; or syntactically by providing a RewardStruct.
Default implementations of all methods are provided which assume that rewards are
looked up by State object and there are no rewards defined (zero reward structs).
A subset of these methods were previously in ModelInfo/ModelGenerator,
so classes that implement those interfaces and implement them should add
“implements RewardGenerator” or remove any @Override annotations.
RewardGenerator is now:
* implemented by ModulesFileModelGenerator and ModulesFileModelGeneratorSymbolic
* created and stored in Prism as needed
* passed to explicit engine model checkers via new method setModelCheckingInfo,
which now replaces setModulesFileAndPropertiesFile
* used in explicit.ConstructRewards to build reward structures
* passed to ModelGenerator2MTBDD for symbolic construction from ModelGenerators
There is also a refactor of the code for looking up index of reward structs:
New methods in ExpressionReward, including switch to RewardGenerator object,
and the methods return the index, not a RewardStruct object.
* Remove some unneeded methods: getExploreState() and getTransitionAction(int i)
* Add a default implementation of getNumVars() based on name list
Existing code which implements the first two methods and annotates them with @Override needs to be changed.
TestModelGenerator, ModulesFileModelGenerator, ModulesFileModelGeneratorSymbolic updated accordingly.
A model is needed for context (i.e., for access to variables, constants, labels, etc.).
Previous methods required the user to pass in a ModelInfo object for this purpose.
These new methods should now be preferred to the old ones.
Calls have been replaced where possible, including a slight reorder of parsing/loading in PrismCL.
In the GUI, the parsed model is cached locally in various places but should always
be the same as the one currently loaded into PRISM.
This is part of an ongoing effort to reduce the extent to which code is
tied to the PRISM language (i.e., ModulesFile) specifically.,
and to push make the Prism object more generally useful as an API.
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)
Dave Parker