This method transforms X phi operators to X ("label" & phi).
This will be used to ensure "strong" semantics for the next-step
operator for co-safe LTL reward computations.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12060 bbc10eb1-c90d-0410-af57-cb519fbb1720
This method provides a variant of the recursive computation
of maximal state subformulas during LTL model checking.
Here, the satisfaction sets of maximal state subformulas
are directly attached using fresh labels to the model,
and the formula is transformed appropriately.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12054 bbc10eb1-c90d-0410-af57-cb519fbb1720
In general, this should provide a significant performance benefit, as
the reachable state space of the product model becomes smaller in the
usual cases (i.e., where we are only interested in the results from
the initial states or for some filter).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12050 bbc10eb1-c90d-0410-af57-cb519fbb1720
This starts the reachability in the product from the set of states of interest
(with the corresponding initial state in the deterministic automaton).
Additionally, these statesOfInterest in the product become the
initial states of the product model.
Deprecated legacy methods for obtaining product models as before (with
the initial states in the product model being those that were initial states
in the original model) are provided.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12049 bbc10eb1-c90d-0410-af57-cb519fbb1720
Previously, this method used the implicit knowledge that only
the stored JDDNode is cleared when clear() is called on a StateValuesMTBDD.
Now, it performs a copy() on the JDDNode and calls clear() on the StateValues object.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12043 bbc10eb1-c90d-0410-af57-cb519fbb1720
Only filter(state, ...) has special handling for TypeVoid results (special
results such as e.g. pareto results from multi-objective model checking).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12034 bbc10eb1-c90d-0410-af57-cb519fbb1720
Multi-objective model checking only supports checking for a single state.
Previously, this check required a state-filter with a single matching state (e.g.,
the default filter(state, ..., "init") placed around a top-level expression).
Now, we check that statesOfInterest is a singleton set.
Thus, now expressions such as
filter(max, multi(P=?[...]. P>0.5[...], "label")
filter(print, multi(P=?[...]. P>0.5[...], "label")
with single-state labels will work.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12033 bbc10eb1-c90d-0410-af57-cb519fbb1720
Additionally, provide more consistent JavaDoc/@Override annotations for these methods.
Often, we are only interested in a subset of the states. E.g., for the top-level
expression, PRISM by default only reports on the initial states; for filters, only
the filtered states are of interest, etc.
By providing a statesOfInterest set to the check methods, they can in principle
exploit this knowledge. One prominent candidate is the automata-based LTL model
checking, which can start the product construction only from the states of interest
instead of from all states. The statesOfInterest information is merely a hint, i.e.,
a checkXYZ method can return values for more states than those specified as the states
of interest. However, the caller should not rely on any results beyond those for
the statesOfInterest.
This commit only provides the basic infrastructure, i.e., adding the stateOfInterest
argument to the method signatures, passing this set to recursive method calls where
appropriate, etc, but does not yet exploit this information. Subsequent commits will
then begin to exploit this information.
The called checkXYZ method is responsible for dereferencing the JDDNode for the
statesOfInterest set. Generally, care should be taken that statesOfInterest is indeed
an MTBDD over the row-variables of the model and that it is a subset of the reachable
states of the model. If one is interested in results for all states, use
model.getReach().copy() as the statesOfInterest.
An analoguous mechanism already exists for the explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12032 bbc10eb1-c90d-0410-af57-cb519fbb1720
findMaximalStableSetOld has not been in use since 2013 (replaced by findMaximalStableset),
maxStableSetTrans is replaced by getStableTransReln.
Methods were private, so we just remove instead of marking as deprecated.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12029 bbc10eb1-c90d-0410-af57-cb519fbb1720
Numeric computations (relying on sum of outgoing transitions > 1 - epsilon to detect choices that
remain in the EC) are not precise, better to just do a graph-based computation.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12028 bbc10eb1-c90d-0410-af57-cb519fbb1720
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
Joachim Klein