dehnert
|
81c627b9b7
|
First version of fully symbolic game solver.
Former-commit-id: 34406f25b9
|
10 years ago |
David_Korzeniewski
|
5623e66566
|
Ignore empty lines in property file and only warn if a line could not be parsed
Former-commit-id: 1d2767e90d
|
10 years ago |
David_Korzeniewski
|
c3d0112975
|
Actually try to read all lines from property file
Former-commit-id: 588d80c8c1
|
10 years ago |
David_Korzeniewski
|
7d84b0a4c5
|
Added ability to check properties from property file to cli utility.
Added minimal example for lra on dtmc
Former-commit-id: eec774f05a
|
10 years ago |
dehnert
|
e4968b1dde
|
Fixed minor issue in cli
Former-commit-id: ed63925765
|
10 years ago |
dehnert
|
e3320ee086
|
Started working on hybrid MDP model checker.
Former-commit-id: 63a8efb93c
|
10 years ago |
dehnert
|
be66ef2751
|
Finalized hybrid CTMC model checker.
Former-commit-id: c217e11b06
|
10 years ago |
dehnert
|
e1761fa774
|
Enabled hybrid CTMC model checker in cli. Further work on hybrid CTMC model checker (not yet working). Fixed some minor issues in sparse CTMC model checker.
Former-commit-id: f9c0f976e1
|
10 years ago |
dehnert
|
c1917ce6d9
|
Finalized hybrid DTMC model checker. It now passes its tests.
Former-commit-id: 99d79e1bc6
|
10 years ago |
dehnert
|
3b4dca1a03
|
Improved Jacobi method a bit.
Former-commit-id: f4affeebf6
|
10 years ago |
dehnert
|
06bfc17ec6
|
Started making hybrid (dd/sparse) model checking work.
Former-commit-id: 23fac3a672
|
10 years ago |
dehnert
|
60701cebdb
|
ADDs and BDDs are no longer mixed in the abstraction layer.
Former-commit-id: 3c31063ea6
|
11 years ago |
dehnert
|
eb5d4100a6
|
Renamed Nondeterminstic equation solver as this name is more than misleading.
Former-commit-id: 7f08ed130c
|
11 years ago |
dehnert
|
1990567b84
|
Started to improve performance of sparse CTMC model checker.
Former-commit-id: 1d014412ec
|
11 years ago |
dehnert
|
d545fac471
|
Restructured solvers a bit: they now get the matrix upon construction and the model checkers use factories to retrieve solvers.
Former-commit-id: 9c727f41f9
|
11 years ago |
dehnert
|
f8c867300b
|
Optimized time-bounded reachability of CTMCs a bit.
Former-commit-id: 6d53a36ae6
|
11 years ago |
dehnert
|
a851fad65d
|
More work on reward properties for CTMCs.
Former-commit-id: 860fee54c7
|
11 years ago |
dehnert
|
ccc60ef145
|
Removed a lot of debug output.
Former-commit-id: cbe28c66ae
|
11 years ago |
dehnert
|
7fa6b568b4
|
Currently debugging the computation of transient probabilities in CTMCs.
Former-commit-id: 6671e0205d
|
11 years ago |
dehnert
|
65bf06dd50
|
Further steps towards CTMC model checking.
Former-commit-id: f057eeb17e
|
11 years ago |
dehnert
|
9d4ded66b2
|
Started implementing CTMC model checker.
Former-commit-id: 8562e5e54c
|
11 years ago |
dehnert
|
cde9786dfa
|
Made Fox-Glynn (hopefully) work.
Former-commit-id: b07c88d122
|
11 years ago |
dehnert
|
e9d677c792
|
Further work on MTBDD-based mc.
Former-commit-id: cf2e16850d
|
11 years ago |
dehnert
|
3434405cf4
|
Started working on CTMC mc.
Former-commit-id: 7e38c0d7d3
|
11 years ago |
David_Korzeniewski
|
7e672cddd9
|
Started implementation of LRA for MDPs
- adapted storm::utility::graph::getReachableStates to work for non-deterministic matrices
Former-commit-id: cd7e469757
|
11 years ago |
dehnert
|
a44a3554c8
|
Fixed minimal command counterexample generation.
Former-commit-id: 6e7e6208da
|
11 years ago |
dehnert
|
00e7121bc4
|
some work towards BDD-based mc.
Former-commit-id: cae0c4421e
|
11 years ago |
dehnert
|
81100c7afd
|
debugged and added more tests for prob0/1 for MDPs using BDDs
Former-commit-id: f47fb3631a
|
11 years ago |
dehnert
|
c70d93f4d3
|
Qualitative modelchecking algorithms for MDPs using BDDs. Not yet bugfixed.
Former-commit-id: 3215a38c44
|
11 years ago |
dehnert
|
1a1906f811
|
Added functional tests for DD-based and sparse computation of states with prob 0 and 1.
Former-commit-id: a62c67c657
|
11 years ago |
dehnert
|
c8007876ae
|
Symbolic models can now be built from the command line.
Former-commit-id: 2c239df754
|
11 years ago |
dehnert
|
a1dae8849e
|
Reworked (sparse) model files: moved them into their own namespace and deleted some functionality that is never used and not that nicely implemented.
Former-commit-id: d4e6df30b5
|
11 years ago |
David_Korzeniewski
|
8ebc0e4640
|
Final touches on cuda nondeterministic linear equation solver & modelchecker
Former-commit-id: c549ae0401
|
11 years ago |
David_Korzeniewski
|
b623384dda
|
Fixed merge errors and adapted to changes in master
Former-commit-id: 08054e7bec
|
11 years ago |
dehnert
|
706ea56963
|
Now DDs are either MTBDDs or BDDs. This makes it possible to use BDDs where possible, which is faster.
Former-commit-id: 07ffb5882d
|
11 years ago |
dehnert
|
8c1870eb54
|
Intermediate commit.
Former-commit-id: e5f251718f
|
11 years ago |
dehnert
|
e58d38fadf
|
More work on integrating DD-based model building.
Former-commit-id: 84f5a5c603
|
11 years ago |
dehnert
|
6347e19da8
|
Intermediate commit: integrating MTBDD model generation/model checking to main tool.
Former-commit-id: a312d3a425
|
11 years ago |
dehnert
|
c3c83fbe4f
|
Fixed some compilation errors.
Former-commit-id: dc626450b8
|
11 years ago |
dehnert
|
f0b591be77
|
Further work on reintegrating parametric model checking into main executable.
Former-commit-id: be95ce2722
|
11 years ago |
dehnert
|
53b77e673b
|
Fixed a minor issue.
Former-commit-id: 7df7a0b38f
|
11 years ago |
dehnert
|
5794bbea56
|
Made some adaptions to make parametric model checking work in the main executable.
Former-commit-id: 0f56bec3e2
|
11 years ago |
dehnert
|
f5e383722f
|
Fixed use of uninitialized value. Deleted assignment operators for classes derived from BaseExpression.
Former-commit-id: 3d6250b393
|
11 years ago |
dehnert
|
3f44b1295f
|
started polishing pstorm a bit
Former-commit-id: bd9c2a42a7
|
11 years ago |
dehnert
|
8fa67a6158
|
Enabled output file generation.
Former-commit-id: 0e4c0598c0
|
11 years ago |
dehnert
|
40e148d9a4
|
Added overall performance measurements.
Former-commit-id: bbe4461167
|
11 years ago |
dehnert
|
6585e56768
|
Changed program header.
Former-commit-id: 37bbb6b2ff
|
11 years ago |
dehnert
|
072b7d0e1a
|
Added performance statistics for model building.
Former-commit-id: d7de4f93e3
|
11 years ago |
dehnert
|
5343ea622a
|
Fixed bug concerning conditional probabilities.
Former-commit-id: be8442deb6
|
11 years ago |
dehnert
|
f49d89144e
|
Fixed issue that could cause wrong models to be generated.
Former-commit-id: 8f1f9b4612
|
11 years ago |