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
2bcdab29a5
explicit.NondetModel: provide default successorsSafeAndCanReach methods
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12088 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
1a12114f30
explicit.DTMC, refactor: remove specialized prob0step, prob1step in sub-classes in favor of default methods in DTMC
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12087 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
ed6c0a1cfb
explicit.DTMC, refactor: provide default implementation for prob0step and prob1step, as well as new single state prob0step, prob1step methods
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12086 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
985a939102
refactor explicit.Model/NondetModel, getSuccessorsIterator: new abstract method getSuccessors, getSuccessorsIterator becomes default method
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
9 years ago
7a106e9f0d
IterableStatSet: slight refactoring, support reverse iteration [with Steffen Maercker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12084 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
285ccd52e2
common.IterableBitSet: return a primitive OfInt iterator, allow reverse iteration [with Steffen Maercker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12083 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
85281b2f2a
common.iterable: add several helper classes [with Steffen Maercker]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12082 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
0f94f49a11
PrismUtils: doublesAreClose with OfInt, measureSupNorm helpers
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12081 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
522adb9b57
PH iteration methods: use MeasureSupNorm.
Uses common code that was refactored to Measures.h
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12080 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
7c612640da
PS iteration methods: use MeasureSupNorm. MultiObjective remains todo.
Uses common code that was refactored to Measures.h
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12079 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
b96f9ca13b
add prism/include/Measures.h (refactor common code in PS and PH engines)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12078 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
1fc8dfa9c4
(export-iterations) Explicit engine (DTMC/MDP): If enabled, export iterations to HTML file
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12077 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
00a5721cbe
(export iterations) MTBDD engine: If enabled, export iterations to HTML file
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12076 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
06e23c9b4f
(export iterations) Hybrid engine: If enabled, export iterations to HTML file
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12075 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
3c2a2232e1
(export-iterations) Sparse engine: If enabled, export iterations to HTML file
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12074 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
30f7def86c
(export-iterations) introduce --exportiterations option, ExportIterations helper classes for C and Java
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
9 years ago
3a36527b5b
Demote -exportmodeldotview to a hidden option for now (not ready yet).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12071 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
17977dfbb7
LTL2DA: prepare for optionally using LTL2WDBA construction for the obligation fragment of LTL
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
9 years ago
3527a6763e
ParamModelChecker: more helpful error messages for unsupported reward computations (co-safe LTL, ...)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12069 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c5deedebbb
prism.StochModelChecker: handle co-safe LTL reward computation for CTMCs
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12068 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
f24e1bc41d
symbolic MDP model checker: Use LTL2WDBA construction to obtain DFA for co-safe LTL reward computations
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
9 years ago
d96873b876
symbolic DTMC checker: Use LTL2WDBA construction to obtain DFA for co-safe LTL reward computations
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
9 years ago
37dff4f997
explicit: Use LTL2WDBA construction to obtain DFA for co-safe LTL reward computations
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
9 years ago
9ef03e0c11
LTLModelCheckers: constructDFAForCosafetyRewardLTL
This method constructs a DFA for a co-safe LTL formula
with appropriate semantics for co-safe LTL reward computations.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12064 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
9fc0899fb5
ConvertForJltl2ba: catch translation of temporal operators with bounds
Normally, that should be caught before, defense in depth.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12063 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
71b4862567
LTL2WDBA: Compute DFA for the co-safety LTL fragment, weak deterministic Büchi automata for the obligation fragment [with David Mueller]
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12062 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
39c2dadc38
jltl2ba.LTLFragments: Determine syntactic LTL fragment (safety, guarantee, persistence, obligation) for a given SimpleLTL formula
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12061 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
b0f5ffeeee
SimpleLTL: extendNextStepWithAP
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
9 years ago
13fe2c54c8
prism.StochModel: provide getEmbeddedDTMC()
Allows the direct construction of a ProbModel (DTMC) for
the embedded Markov chain.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12059 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
39c9f43549
prism.StateModelChecker: add createModelChecker() helper method
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12058 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
f5b8aa9fd7
prism.NondetModelChecker: add createNewModelChecker
Analogous to ProbModelChecker.createNewModelChecker
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12057 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
42949bee96
prism.StateValues: add switchModel() method
Will be used to efficiently switch the result vectors from embedded DTMC to the original CTMC.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12056 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
c930c151c5
refactor prism.StateValues: split constructor to provide seperate (private) method for setting the model
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@12055 bbc10eb1-c90d-0410-af57-cb519fbb1720
9 years ago
67f34d1de2
prism.StateModelChecker: add handleMaximalStateFormulas
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
9 years ago
Joachim Klein