This commit refactors the exportToDotFile infrastructure of
the explicit engine to allow the flexible decoration of the
nodes and edges in the DOT file, e.g., for annotating rewards,
marking certain states, etc.
We provide default implementations in explicit.Model for most methods,
only exportTransitionsToDotFile needs to be provided in derived classes
to allow DOT export.
Note that the abstract method in ModelExplicit
abstract void exportTransitionsToDotFile(int i, PrismLog out);
has been removed, which will lead to errors in derived classes
where implementations of this method have been marked with the
@Override annotation.
To fix this, simply replace the signature of your implementation of
void exportTransitionsToDotFile(int i, PrismLog out);
by
void exportTransitionsToDotFile(int i, PrismLog out, Iterable<explicit.graphviz.Decorator> decorators)
(as defined in explicit.Model). You can simply ignore the decorators
parameter at first. Later on, if you want to support decoration,
have a look at the implementations of this method in DTMCExplicit
and MDPExplicit for the proper handling.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12115 bbc10eb1-c90d-0410-af57-cb519fbb1720
An SCCInfo provides IntSet-based access to the various SCCs. This storage option
can be more efficient than to store BitSets for each individual SCC, in particular
if trivial SCCs are not filtered and there are lots of states.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12112 bbc10eb1-c90d-0410-af57-cb519fbb1720
To obtain the previous behaviour, change
SCCComputer sccs = SCCComputer.createSCCComputer(parent, model);
sccs.computeSCCs();
... = sccs.getSCCs();
to
SCCConsumerStore sccs = new SCCConsumerStore();
SCCComputer sccComp = SCCComputer.createSCCComputer(parent, model, sccs);
sccComp.computeSCCs();
... = sccs.getSCCs();
This additional flexibility in how SCCs can be consumed can be used
in the future for example to handle SCCs on-the-fly, without
having to store all of them at the same time.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12110 bbc10eb1-c90d-0410-af57-cb519fbb1720
The getSuccessorsIterator provides an iterator over the set of successors,
i.e., deduplication is sometimes required (e.g. for MDPs).
We introduce here a SuccessorsIterator class that allows to make deduplication
optional, which may have benefits in performance. Additionally, SuccessorsIterator
implements a primitive OfInt iterator, which can avoid auto-boxing.
Subclasses of explicit.Model now have to provide an implementation for getSuccessors(int s),
getSuccessorsIterator(int s) is provided via a default method that automatically
requests deduplication.
Subclasses of explicit.NondetModel now have to provide an implementation for getSuccessors(int s, int).,
getSuccessorsIterator(int s, int i) is provided via a default method that automatically
requests deduplication.
Adapt the existing subclasses of explicit.Model.
Provides additional default methods and removes unneeded specializations in sub-classes:
boolean isSuccessor(int s1, int s2)
boolean allSuccessorsInSet(int s, BitSet set)
boolean someSuccessorsInSet(int s, BitSet set)
boolean allSuccessorsMatch(int s, IntPredicate p)
boolean someSuccessorsMatch(int s, IntPredicate p)
and for NondetModel:
boolean allSuccessorsInSet(int s, int i, BitSet set)
boolean someSuccessorsInSet(int s, int i, BitSet set)
boolean allSuccessorsMatch(int s, int i, IntPredicate p)
boolean someSuccessorsMatch(int s, int i, IntPredicate p)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12085 bbc10eb1-c90d-0410-af57-cb519fbb1720
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
Joachim Klein