Dave Parker
8962177f20
Set methods for exportAdv stuff in explicit model checkers.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4938 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
ab3d3773a0
Added valiter switch (for use by MDP explicit engine).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4758 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
be4417dbe9
Comment
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4654 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
397fc1b4aa
Tidy of explicit engine settings import, to identify some missing features.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4653 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
750f3fd0ba
Separate setting explicit engine for MDP solution method (stoch games still uses old solnMethod field).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4650 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
1e0dff70d2
Separate setting explicit engine for linear equation system solution method.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4649 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
4a1163a86d
Added ability to disable precomputation algs independently (switches -noprob0 and -noprob1).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4103 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
6a046b4431
Tidy/improve passing of settings to explicit model checkers.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3708 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
3351288f3a
StateValues has an associated model in explicit engine; improved printing.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3592 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
14025e109d
Improvements to StateValues class + it's use in explicit model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3581 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
58c6955d29
Handle bounded P/R operators in explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3572 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
c79d0ccafb
Small fixes in explicit rewards.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3375 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
075822347e
Reward constrcution for explicit engine pushed into separate class, and added state rewards for MDPs.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3370 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
0728db06cf
Explicit engine reward construction handles model constants properly.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3255 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
8bbda8f530
Added new expression evaluation methods (needed for explicit model checker). Unfortunately breaks some existing calls to evaluate(constVals, null) due to ambiguities. Need to replace them with evaluate(constVals).
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3254 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
85147f1a71
Explicit engine improvements, mainly MDP rewards:
* Explicit engine gets MDP rewards (transition rewards only) from the model
* Rewards detached from MDPs (but attached ones still available, e.g. for A-R)
* Various bug fixes in MDPSparse, especially wrt rewards
* Few code tidies
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3215 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
d061af7deb
More rewards handled in explicit engine: state rewards for Markov chains.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3208 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
ea14a0a7b6
Explicit engine: better error reporting of some unsupported properties.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3207 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
1c33e4b551
Explicit engine: better error reporting of some unsupported properties + support for property references.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3205 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
52d2d21447
Update to newest version of explicit code (from prism-qar) plus -explicit switch for command-line and MDP solution settings.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3047 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago