If there are exceptions during the iteration, we want to have a working HTML file with the iterations up to that point.
By flushing after each vector, we can ensure that the HTML is in a working state.
Switch from
... took X iterations, Y MV-multiplications and Z seconds.
to
... took X iterations, Y multiplications and Z seconds.
as MV-multiplications does not have a terribly intuitive meaning.
Now aligns with the default implementation in explicit.MDP: If there is a choice consisting of a self-loop,
produces value 0 for zero-reward state/choice and infinite value for positive-reward state/choice
(should be catched before in precomputations).
The previous behaviour (self-loops have infinite value) messes with maximal total reward computations with
Gauss-Seidel, e.g.
prism functionality/verify/mdps/rewards/total-reward-2.nm functionality/verify/mdps/rewards/total-reward-2.nm.props -explicit -gs -test -prop 3
for the PRISM test suite fails.
Also, align comments in MDP.mvMultRewJacMinMaxSingle.
Sometimes, we want to use the prob0/1... methods to generate schedulers instead of doing
the standard precomputations and don't want to have the normal log output.
Not inherited using inheritSettings()
When using an iteration method with two alternating solution vectors (power, jacobi),
we did not copy the result to the second vector when we have detected convergence in
an SCC (for topological interval iteration). Subsequently, as the values for finished
SCCs will never be updated anymore, the values for this states will oscillate between
the final value and the value from the iteration step before, potentially preventing
convergence. This will be mitigated if we enfore convergence from below / above, but
at least from below enforcing convergence should not be necessary.
An example would be
prism prism-examples/dice/two_dice.nm -pf 'Rmin=?[ F s1=7]' -explicit -topological -ii:nomonotonicbelow
where oscillation between 0 and 1 inhibits convergence.
To fix, we tell the iteration method when we are done with an SCC so that we can
copy the results. For singleton SCCs, we already copied the results to both vectors.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12204 bbc10eb1-c90d-0410-af57-cb519fbb1720
Currently, building PRISM with parallel building does not work,
as there are dependencies between targets that are not fully
encoded in the Makefiles. Building with -j n flag would lead to error.
Now, we add the .NOTPARALLEL target to most of the Makefiles,
which tell GNU make to ignore the -j flag. Note that this
only inhibits parallel builds for the current Makefile, we
thus have to specify it for all sub-Makefiles as well
(see https://www.gnu.org/software/make/manual/html_node/Parallel.html)
For the external libraries, CUDD and LPSolve don't seem to mind building
in parallel, so we don't inhibit there and can get some minor compile time
speed-up by using multiple cores if the -j option is specified.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12202 bbc10eb1-c90d-0410-af57-cb519fbb1720
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
Dave Parker