Generates HTML file with the individual steps of the iterative procedures.
Relies on external JavaScript and CSS.
Is already prepared for exporting interval iteration steps (possibility
to export multiple vectors with type flag per iteration step)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12073 bbc10eb1-c90d-0410-af57-cb519fbb1720
Currently, the LTL2WDBA construction is not yet optimized for performance and
does not perform the minimization step that ensures that the WDBA are indeed minimal.
So, we don't activate it.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12070 bbc10eb1-c90d-0410-af57-cb519fbb1720
The DFA needed for co-safe LTL reward computation need to have a
specific structure, i.e., all states that satisfy Sigma^omega have
to be already goal states.
The previous approach did not necessarily ensure this.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12067 bbc10eb1-c90d-0410-af57-cb519fbb1720
The DFA needed for co-safe LTL reward computation need to have a
specific structure, i.e., all states that satisfy Sigma^omega have
to be already goal states.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12066 bbc10eb1-c90d-0410-af57-cb519fbb1720
The DFA needed for co-safe LTL reward computation need to have a
specific structure, i.e., all states that satisfy Sigma^omega have
to be already goal states.
The previous approach did not necessarily ensure this.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12065 bbc10eb1-c90d-0410-af57-cb519fbb1720
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
Joachim Klein