Dave Parker
95c3f7db43
Add a missing method in DTMCFromMDPAndMDStrategy.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@11411 bbc10eb1-c90d-0410-af57-cb519fbb1720
10 years ago
Dave Parker
b12953b937
Make use of the new PrismNotSupportedException.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9999 bbc10eb1-c90d-0410-af57-cb519fbb1720
11 years ago
Dave Parker
b970c2740b
Fix oddity in return type of DTMC.getNumTransitions(s) - double not int.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@8254 bbc10eb1-c90d-0410-af57-cb519fbb1720
12 years ago
Dave Parker
dada1bc4b1
Add "type" option to -exportstrat (explicit engine only) + a few changes in Strategy classes.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@7602 bbc10eb1-c90d-0410-af57-cb519fbb1720
12 years ago
Dave Parker
d30e52c2a4
DTMCFromMDPMemorylessAdversary class treats a choice of -1 as "do nothing".
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6906 bbc10eb1-c90d-0410-af57-cb519fbb1720
13 years ago
Dave Parker
70b1ac94f9
Bug fix and implemente dmissing methods in DTMCFromMDPMemorylessAdversary.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6905 bbc10eb1-c90d-0410-af57-cb519fbb1720
13 years ago
Ernst Moritz Hahn
55025ee63b
too slow
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6622 bbc10eb1-c90d-0410-af57-cb519fbb1720
13 years ago
Ernst Moritz Hahn
4ae35b1beb
began modifying for storing actions
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@6621 bbc10eb1-c90d-0410-af57-cb519fbb1720
13 years ago
Dave Parker
99d2139f55
Add getSuccessorsIterator to explicit Model interface.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5331 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
a218d09b2b
* Continued major changes to PRISM API
- keeps track of model, builds when needed
- takes care of explicit engine stuff too
* Changes to deadlock handling:
- new option for "fix deadlocks" (defaults to *true*) (and new switch -fixdl)
- consistent deadlock handling everywhere, incl. GUI and experiments
- changes to model-level deadlock storage (symbolic and explicit)
* Explicit engine added as true engine, also available from GUI
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@4562 bbc10eb1-c90d-0410-af57-cb519fbb1720
14 years ago
Dave Parker
bedfccb2ec
Re-arrangement of explicit model classes:
* merge ModelSimple and ModelSparse as ModelExplicit
* add ModelSimple as separate interface
* created DTMCExplicit to capture some common methods for DTMC classes
* (still need to do same for other models)
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3514 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
e5b7ad597e
Expansion of transition-matrix-export functionality for explicit engine.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3357 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
edab23b581
More updates to explicit library:
* removed some old rewards code from explicit models
* (and temporarily disabled a few things in PrismSTPGAbstractRefine accordingly)
* added method addActionLabelledChoice to MDPSimple
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3325 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
1a21d7f342
Explicit engine handles "deadlock" and "init" labels, if not embedded in a (logical) expression.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3124 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
4ec5f0f9ae
Transient probability computation in explicit engine + some connection to CL.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3110 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
Dave Parker
5c0e7cd4f8
Broken copyright header.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2492 bbc10eb1-c90d-0410-af57-cb519fbb1720
15 years ago
Dave Parker
6b992f1df6
Deadlocks and permutations for explicit.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1852 bbc10eb1-c90d-0410-af57-cb519fbb1720
16 years ago
Dave Parker
3321e1df7d
Explicit model export has option to just do tra file.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1850 bbc10eb1-c90d-0410-af57-cb519fbb1720
16 years ago
Dave Parker
d40ffd38e9
Preliminary code to attach explicit stuff to PRISM + some more Model class re-arrangements.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1836 bbc10eb1-c90d-0410-af57-cb519fbb1720
16 years ago
Dave Parker
57a404cc05
Fixes in explicit CTMC solving + some CTMDP stuff.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1824 bbc10eb1-c90d-0410-af57-cb519fbb1720
16 years ago
Dave Parker
8f2748a711
Redesign/tidy of model interfaces + more CTMC model checking.
git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1794 bbc10eb1-c90d-0410-af57-cb519fbb1720
16 years ago