9ae9116ff4
(interval iteration) currently, multi objective model checker should not use interval iteration
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12138 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c8335ca642
(interval iteration) prepare settings for interval iteration
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12137 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
9735731c59
PrismSettings: refactor option splitting (for -switch:options), provide access to raw option string
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12136 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
430713ca65
(interval iteration) PrismUtils: add helper methods for interval iteration
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12135 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
9d98dab1c3
(interval iteration) include/Measures.h: provide helper functions for interval iteration
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12134 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c4b7b0db3e
explicit.IncomingChoiceRelation
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12133 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
e97b72f6e6
explicit.MDPModelChecker: check for zero-reward ECs for Rmin=?[ F ] computations, use quotient model if necessary
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12132 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
1ce1446eb5
explicit.MDPModelChecker: support backward Gauss-Seidel during policy iteration
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12131 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
452d89e411
(explicit iteration refactoring) Expose topological value iterations via the -topological switch
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12130 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
12e377de4a
(explicit iteration refactoring) DTMCModelChecker: use the new infrastructure for doing the numerical iteration computations.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12129 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
fae160729c
(explicit iteration refactoring) DTMCModelChecker: use the new infrastructure for doing the numerical iteration computations.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12128 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
9b94039049
(explicit iteration refactoring) new infrastructure to provide consolidated methods for doing the numerical iteration computations.
Support for topological iteration, periodic updates, backwards Gauss-Seidel.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12127 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
7486c6d7ed
For MDP model checking (explicit, symbolic), support -pmaxquotient option (computation in MEC quotient)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12126 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
87675e828a
explicit.MDPModelChecker: split numeric computation part of computeReachProbs into separate method
Preparation for upcoming interval iteration commits, etc.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12125 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
2fe2f918b3
explicit.MDPSparse: add constructor from arbitrary MDP [with Steffen Maercker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12124 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
265e827391
explicit.ZeroRewardECQuotient
Quotient of an MDP where the zero-reward maximal end components
are collapsed to single states.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12123 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
03dafaa170
explicit.modelviews: Various helpers for providing modified views of a given DTMC / MDP [with Steffen Maercker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12122 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
ec4e55d708
IteratorTools [with Steffen Maercker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12121 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
61701b9f1b
some more helpers for iterators / predicates [with Steffen Maercker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12120 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
86f75d975a
explicit.BasicModelTransformation [with Steffen Maercker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12119 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
7073b3bc4e
explicit.StateValues: getType()
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12118 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
798dd1e859
Distribution: provide constructor from Iterator over the transitions (Entry<Integer, Double>)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12117 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
20ae1aa61d
(for trunk) PeriodicTimer
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12116 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
881a571870
explicit DOT export: support decorators
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
9 years ago
59745d025c
explicit.graphviz: infrastructure for more flexible DOT exports
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12114 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
0cc16c1f9f
explicit.SCCComputer: convenience method forSCCs for functional-style iteration over the SCCs of a model
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12113 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
7d5105c8c1
explicit.SCCInfo, SCCComputer: method for obtaining topological ordering (SCCInfo)
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
9 years ago
3d8c4e1ff8
explicit.SCCComputer: provide variant of computeSCCs where the state space is restricted with an IntPredicate
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12111 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
97074f5d58
Refactor explicit SCC computation, splitting SCCConsumer from SCCComputer.
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
9 years ago
fe5d031751
SCCTarjan: use SuccessorsIterator
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12109 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
810f149e88
PrismUtils: findMaxFinite
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12108 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
a11d7c9797
JDD, prism.StateValues: find max finite value
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12107 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
95283773a9
explicit: StateValues, implement maxFiniteOverBitSet
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12106 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
f4fdac9baa
add common.IntSet: interface for an ordered set of integers, providing fast membership test
Wrappers for BitSet and singleton values are provided.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12105 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
9b5245f04f
explicit DTMCSimple, MDPSimple refactor: remove mv... specialisations so the default methods from DTMC/MDP are used
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12104 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
dc8e331a36
explicit.MDP: provide OfInt-based variants for mvMultMinMax, mvMultGSMinMax, mvMultRewMinMax, mvMultRewGSMinMax
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12103 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
803f856ca9
explicit.MDP: default implementations for several mvMult methods
mvMultMinMaxSingle
mvMultMinMaxSingleChoices
mvMultSingle
mvMultJacMinMaxSingle
mvMultJacSingle
mvMultRewMinMaxSingle
mvMultRewSingle
mvMultRewJacMinMaxSingle
mvMultRewJacSingle
mvMultRewMinMaxSingleChoices
mvMultRight
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12102 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
a216904acb
explicit.MDP: use OfInt based iterator in default implementations of mv... methods
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12101 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
3c691c980a
explicit.DTMC/NondetModel: add default method getNumTransitions(OfInt states)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12100 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
aec833edfd
explicit.MDP: move mvMultMinMax, mvMultGSMinMax, mvMultRewMinMax, mvMultRewGSMinMax from MDPExplicit to default methods in MDP
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12099 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
1dd339ede5
explicit.DTMC: mvMultRewGS for Gauss-Seidel style reward computations
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12098 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
a89228dff1
explicit.DTMC: provide mv... methods for Jacobi-style iteration
mvMultJac, mvMultRewJac, mvMultRewJacSingle
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12097 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
a29887d36d
explicit.DTMC: provide variants for mvMult, mvMultGS, mvMultRew, taking OfInt iterators
This allows finer grained control over the iteration order.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12096 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
11fde2c393
explicit.DTMC: provide default implementations for mvMultSingle, mvMultJacSingle, mvMultRewSingle, vmMult (based on forEachTransition / sumOverTransition)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12095 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
3fbc7903dc
explicit.DTMCFromMDPAndMDStrategy: simplify getTransitionsIterator, provide forEachTransition specialization
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12094 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
0c08af644d
explicit.DTMCEmbeddedSimple: simplify getTransitionsIterator, provide forEachTransition specialization
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12093 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
f669ac11d9
explicit.DTMC/MDP: provide forEachTransition and sumOverTransitions methods
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12092 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
2bd70172ce
explicit.DTMC, refactor: move mvMult, mvMultGS, mvMultRew from DTMCExplicit to default methods in DTMC
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12091 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
ae1bbd379e
explicit.MDPSimple: remove specializations for prob0/prob1, use default methods from explicit.MDP
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12090 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
cd9b1f4285
explicit.MDP, refactor: provide default prob0 / prob1 related methods
prob0step, prob1Astep, prob1Estep, prob1step, prob1stepSingle
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12089 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
Joachim Klein