This potentially allows checking of "symbolic" expressions for methods/engines
other than the parametric engine. It will also allow simplification of the
mechanisms for storing results from parametric model checking, aligning it
with other parts of the code.
In particular for a whole State, not just a substate.
Also for just some constants, with no variable values.
Can be used to get an expression symbolically in terms of constants.
For now, this provides a cleaner implementation of the default (unspecified)
model type being set to an MDP. Later, this will allow the actual model type
to be omitted or partially specified and derived from langage features.
Code is split into different methods for each type of test.
It is also mostly relocated to a new class prism.ResultTesting,
since it should not really be tied to the Property object.
The result for testing can now be passed as a Result object,
as well as Double, Integer, etc., with the former being preferred.
This will allow info attached to the Result object to be used
for the correctness, notably accuracy/error info.
Also add a new testing regression test - just some constants,
including border cases - infinity, NaN, etc.
Was previously being parsed as a PRISM expression as a fallback,
but the parser currently does not handle big integers.
Test case added. And these tests moved to a new "testing" directory.
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.
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 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.
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.
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.
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
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
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.
Using the infrastructure from the previous commit, we request exact evaluation
of constants in exact and parametric model checking mode.
Additionally, note where we deliberately choose non-exact evaluation mode.
Add corresponding test cases.
Previously, constants that are defined via an expression
were evaluated using standard (integer or floating point) arithmetic,
even in parametric or exact model checking mode.
This commit provides the infrastructure for requesting that constant
expressions are evaluated using exact arithmetic.
To keep the API backward compatible, we introduce additional methods that
offer an 'exact' flag, but keep the old methods as well. Those default to
normal arithmetic.
TypeDouble constants are kept as rational numbers, while int and boolean
constants are converted to Java data types. For int, an exception is raised
if the value can't be exactly represented by Java int.
Support matching of constants in RESULT strings for the case
that constants in the model are exact rational
numbers (implemented in subsequent commits).
This allows storage of BigRational values in StateValues / Values vectors, e.g.,
to store constants that have been evaluated exactly.
TypeDouble.castValueTo now returns a Number instead of a Double, requiring the use
of the doubleValue() method in several places where the value is evaluated using
double arithmetic.
Dave Parker