dehnert
60701cebdb
ADDs and BDDs are no longer mixed in the abstraction layer.
Former-commit-id: 3c31063ea6
10 years ago
dehnert
5bd6ca606f
Started refactoring DD abstraction layer.
Former-commit-id: 60f7713c24
10 years ago
dehnert
eb5d4100a6
Renamed Nondeterminstic equation solver as this name is more than misleading.
Former-commit-id: 7f08ed130c
10 years ago
dehnert
fda3c8a6df
Made CTMC model checker work correctly again.
Former-commit-id: c6e44a16da
10 years ago
dehnert
e8dd83c4da
Further work on performance of CTMC model checker.
Former-commit-id: f62b97c58b
10 years ago
dehnert
1990567b84
Started to improve performance of sparse CTMC model checker.
Former-commit-id: 1d014412ec
10 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
10 years ago
dehnert
f8c867300b
Optimized time-bounded reachability of CTMCs a bit.
Former-commit-id: 6d53a36ae6
10 years ago
dehnert
49bed497b0
Fixed a model building problem. Included checking of reward properties on CTMCs and wrote tests for it.
Former-commit-id: a137bd20ac
10 years ago
David_Korzeniewski
b096180de8
LRA on DTMCs implemented
Former-commit-id: 633d81323d
10 years ago
dehnert
a851fad65d
More work on reward properties for CTMCs.
Former-commit-id: 860fee54c7
10 years ago
dehnert
c84751f632
Started working on reward properties for CTMCs.
Former-commit-id: a4e9b9a663
10 years ago
dehnert
799cbce775
Added function tests for CTMC creation and time-bounded reachability.
Former-commit-id: e56f860a70
10 years ago
dehnert
ccc60ef145
Removed a lot of debug output.
Former-commit-id: cbe28c66ae
10 years ago
dehnert
7fa6b568b4
Currently debugging the computation of transient probabilities in CTMCs.
Former-commit-id: 6671e0205d
10 years ago
David_Korzeniewski
25739720e0
Finished implementation of LRA for MPDs.
No tests yet.
Former-commit-id: 795c0e9842
10 years ago
dehnert
c6521221bd
Added tiny text example for ctmc mc.
Former-commit-id: 498bbec1f2
10 years ago
dehnert
65bf06dd50
Further steps towards CTMC model checking.
Former-commit-id: f057eeb17e
10 years ago
dehnert
6ffd5cea88
Further work on CTMC model checking.
Former-commit-id: 7c02448dfa
10 years ago
dehnert
9d4ded66b2
Started implementing CTMC model checker.
Former-commit-id: 8562e5e54c
10 years ago
dehnert
cde9786dfa
Made Fox-Glynn (hopefully) work.
Former-commit-id: b07c88d122
10 years ago
dehnert
e9d677c792
Further work on MTBDD-based mc.
Former-commit-id: cf2e16850d
10 years ago
dehnert
3434405cf4
Started working on CTMC mc.
Former-commit-id: 7e38c0d7d3
10 years ago
David_Korzeniewski
bc1a97e38a
Merge branch 'master' into LRA_for_dtmc_mdp
Former-commit-id: 2a78b1e8ae
10 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
10 years ago
dehnert
96539f41a5
Fixed simplification of division: division expressions must not be simplified, because it is not (yet) clear whether integer division or floating point division is to be used.
Former-commit-id: 506798c1cd
10 years ago
dehnert
5bbd85c379
Some bugfixes.
Former-commit-id: 70dcc73e91
10 years ago
dehnert
a44a3554c8
Fixed minimal command counterexample generation.
Former-commit-id: 6e7e6208da
10 years ago
dehnert
c7f262bf15
Merge branch 'mtbddIntegration' of https://sselab.de/lab9/private/git/storm into mtbddIntegration
Former-commit-id: 115d7a6c3b
10 years ago
dehnert
00e7121bc4
some work towards BDD-based mc.
Former-commit-id: cae0c4421e
10 years ago
dehnert
546e047b8d
Fixed a bug that prevented correct comparison with bounds in formulas.
Former-commit-id: ae6c28dcbe
10 years ago
dehnert
3fd62bc697
More work on MTBDD-based mc.
Former-commit-id: 52081fc741
10 years ago
dehnert
0c2080f220
Added tests for sparse Prob0/1 to functional tests
Former-commit-id: ef8f9ffb59
10 years ago
dehnert
81100c7afd
debugged and added more tests for prob0/1 for MDPs using BDDs
Former-commit-id: f47fb3631a
10 years ago
dehnert
c70d93f4d3
Qualitative modelchecking algorithms for MDPs using BDDs. Not yet bugfixed.
Former-commit-id: 3215a38c44
10 years ago
dehnert
7e14dc031b
Reverted the last commit. The flag is there for performance reasons and there is no reason why it shouldn't work that way.
Former-commit-id: e551eb461f
10 years ago
masawei
97936cbd8e
Found a fix for a bug causing the functional tests to segfault at DeterministicModelBisimulationDecomposition.Die.
- By setting the blocks to be not sorted and unique a different constructor is used by the boost container. This prevents the segfault.
|- I can't say exactly why this works nor do I know if the blocks are actually sorted and unique in the sense meant by the underlying container implementation.
Former-commit-id: a1bfbab75a
10 years ago
dehnert
923007cdc3
Merge branch 'master' into mtbddIntegration
Former-commit-id: 1fdddfbd8c
10 years ago
dehnert
bda8d63b3b
Merge master into mtbddIntegration.
Former-commit-id: ad1ab84439
10 years ago
David_Korzeniewski
7d2d1cac55
Functional Testing Suite now prints a note if not all optional dependencies were included in the build.
Former-commit-id: 36974ebb66
10 years ago
David_Korzeniewski
95d5ebbb7d
Updated build instructions with list of tested compilers and some new dependencies, but it still looks partially outdated.
Former-commit-id: 1931f71cf9
10 years ago
dehnert
1a1906f811
Added functional tests for DD-based and sparse computation of states with prob 0 and 1.
Former-commit-id: a62c67c657
10 years ago
dehnert
c8007876ae
Symbolic models can now be built from the command line.
Former-commit-id: 2c239df754
10 years ago
dehnert
239caf57eb
Added symbolic models and made DD-based model generator build the correct instances.
Former-commit-id: c054401cfd
10 years ago
dehnert
8a906038f6
Added reward model generation for DD-based model builder.
Former-commit-id: 4837cf9229
10 years ago
dehnert
7c2f60175e
Intermediate commit: fixed parsing bug and started reward generation (DD).
Former-commit-id: a27c815831
10 years ago
dehnert
f0b174b756
Fixed performance tests.
Former-commit-id: f58e2eb923
10 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
10 years ago
David_Korzeniewski
4dc69dd6f5
Fixed performance tests, and again things concerning templates I never heard of before.
Former-commit-id: 1d110c6aad
10 years ago
David_Korzeniewski
7515ca5293
Fixed compile errors caused by parts of the c++ standard I've never heard of before...
Former-commit-id: 8dbd813f42
10 years ago