Currently, the hybrid engine internally uses int (signed 32bit) index variables
So, if the number of states is larger than Integer.MAX_VALUE, there is a problem
and the code will most probably crash or do nonsensical things.
We check this before calling into the native hybrid engine code and
throw a PrismNotSupportedException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12021 bbc10eb1-c90d-0410-af57-cb519fbb1720
Currently, the sparse engine internally uses int (signed 32bit) index variables
So, if the number of states is larger than Integer.MAX_VALUE, there is a problem
and the code will most probably crash or do nonsensical things.
We check this before calling into the native sparse engine code and
throw a PrismNotSupportedException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12020 bbc10eb1-c90d-0410-af57-cb519fbb1720
Before, the ODD offsets (for indexing into the reachable states) were
stored as longs, resulting in inconsistent numbers of (symbolic)
states that can be treated. In particular, on Win64, long is 32bit.
We switch to int64_t for the ODD offsets everywhere, allowing
MTBDD computations for models with >2^31 states.
Additionally, we check for arithmetic overflow in the offset
computations. Due to the symbolic storage for the models and the
state space explosion, it's possible to construct simple model files
that reach the 2^63 states limit.
If this limit is reached, we now throw an error message. In the future
it might be worthwile to ensure that PRISM can deal with the absence
of an ODD for all the computations that don't absolutely require it
and carry on (most MTBDD engine algorithms should be fine).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12019 bbc10eb1-c90d-0410-af57-cb519fbb1720
As Windows 64bit uses IL32P64 data model (long is 32bit, pointers are
64bit), the various casts from pointer to long used in our version of CUDD
mangle the top-level half of pointers. On Java 8, the memory allocations
seem to generate benign pointers at first, but for larger symbolic models
this can lead to strange behaviour or crashes. For Java 9, crashes are more
immediate (https://github.com/prismmodelchecker/prism/issues/13).
The CUDD 3.0.0 release fixes those issues by using intptr_t and uintptr_t
for the pointer-to-integer casts. As we don't want to fully switch to 3.0.0
at the moment, this commit backports these fixes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12016 bbc10eb1-c90d-0410-af57-cb519fbb1720
We check after each DD operation whether the returned DdNode* is NULL
and abort the computation. The NULL return value is then caught in the
JDD.ptrToNode() method, which raises a CuddOutOfMemoryException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12008 bbc10eb1-c90d-0410-af57-cb519fbb1720
We check after each DD operation whether the returned DdNode* is NULL
and abort the computation. The NULL return value is then caught in the
JDD.ptrToNode() method, which raises a CuddOutOfMemoryException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12007 bbc10eb1-c90d-0410-af57-cb519fbb1720
(1) use dedicated printColoured method, which suppresses
colouring if isColourEnabled() is false (e.g., when piping to a file)
(2) use dedicated colour (light red) for warnings, as before
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12003 bbc10eb1-c90d-0410-af57-cb519fbb1720
Missing case for NE operator in BoxRegion.cmpOp. This affects the check routines
for the != operator in the parametric/exact engines, e.g., for state formulas
such as s!=t
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11976 bbc10eb1-c90d-0410-af57-cb519fbb1720
If the ProbModelTransformationOperator does not modify the non-row / non-column
variables in the transformation of the transition function, it can also be used
for MDPs (modifying the successor state only depending on the originating state).
This can be useful in standard product transformations that are agnostic of
the non-deterministic choice.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11947 bbc10eb1-c90d-0410-af57-cb519fbb1720
By specifying a NondetModelTransformationOperator, we can easily transform
a given symbolic NondetModel (MDP) to a transformed model. The necessary
handling of the meta-information is done in NondetModelModel.getTransformed.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11946 bbc10eb1-c90d-0410-af57-cb519fbb1720
By specifying a ProbModelTransformationOperator, we can easily transform
a given symbolic ProbModel (DTMC/CTMC) to a transformed model. The necessary
handling of the meta-information is done in ProbModel.getTransformed.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11945 bbc10eb1-c90d-0410-af57-cb519fbb1720
Joachim Klein