David_Korzeniewski
cf5442fe45
Bugfix and test-fix: Only the "never leave MEC"-states have cost > 0 and transition costs are all 0 in the ssp.
Former-commit-id: f6688a8956
10 years ago
David_Korzeniewski
8e688f71ff
Tests for DTMC LRA and some bugfixes. All tests pass.
Former-commit-id: 589db6c2b3
10 years ago
David_Korzeniewski
0ba629ad3f
More tests, bugfixes: All tests pass.
Former-commit-id: f37c02a9d7
10 years ago
David_Korzeniewski
716cf3abdd
Adapted to new solver interface some tests and bugfixes. Tests still failing.
Former-commit-id: da3b75aefd
10 years ago
David_Korzeniewski
d4f051c4f0
Fixed Windows build
Former-commit-id: 53c99736de
10 years ago
David_Korzeniewski
1f87e7c8b2
First test for LRA on MDPs
Former-commit-id: c022ceaf01
10 years ago
dehnert
c1917ce6d9
Finalized hybrid DTMC model checker. It now passes its tests.
Former-commit-id: 99d79e1bc6
10 years ago
dehnert
d787b80fec
CTMC examples now build properly using the DD-based model generator.
Former-commit-id: ac97b005e3
10 years ago
dehnert
eb5d4100a6
Renamed Nondeterminstic equation solver as this name is more than misleading.
Former-commit-id: 7f08ed130c
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
dehnert
799cbce775
Added function tests for CTMC creation and time-bounded reachability.
Former-commit-id: e56f860a70
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
8ebc0e4640
Final touches on cuda nondeterministic linear equation solver & modelchecker
Former-commit-id: c549ae0401
10 years ago
David_Korzeniewski
b623384dda
Fixed merge errors and adapted to changes in master
Former-commit-id: 08054e7bec
10 years ago
David_Korzeniewski
ea2e616196
All tests for CUDA based TopologicalValueIterationMdpPrctlModelChecker passing on Windows.
Former-commit-id: 68cafa6f84
10 years ago
David_Korzeniewski
84f8a41302
More tests adapted, decreased verbosity of TopologicalValueIterationNondeterministicLinearEquationSolver
Former-commit-id: 6e0b492533
10 years ago
David_Korzeniewski
8b4309e53c
Adapted first test to new interface. Test passes.
Former-commit-id: 49dc8228f3
10 years ago
David_Korzeniewski
8066bb6637
Small fix for test.
CPU implementation of TopologicalValueIterationMdpPrctlModelChecker seems to be working, adapted parts of tests passing!
Former-commit-id: 7ed1e11f91
10 years ago
David_Korzeniewski
3748905bcf
Fixes and test refactoring for TopologicalValueIterationMdpPrctlModelChecker
- Explicit instantiation of matrix and scc decomposition for float
- Started to adapt TopologicalValueIterationMdpPrctlModelCheckerTest.cpp to new formulas
Former-commit-id: 4685ae4939
10 years ago
dehnert
b5f907d99d
Added propositional model checker. Put some of the new classes in new folders. Fixed an issue that prevented compilation.
Former-commit-id: 517a870d2f
10 years ago
dehnert
c85df2cd74
Conditional Probabilities working. Included two tests.
Former-commit-id: a89255c4ef
10 years ago
dehnert
9e8d8a2c27
Fixed wrong calculation of reachability rewards in state-elimination-based model checker.
Former-commit-id: bee99d61b0
10 years ago
dehnert
89fc5be1ab
Fixed some things and wrote tests for elimination-based DTMC modelchecker. They fail: apparently rewards are not correctly computed in some cases.
Former-commit-id: 000ad6b049
10 years ago
dehnert
89df9621a9
MDP model checker works again.
Former-commit-id: 2c24da6192
10 years ago
dehnert
9026aa9ac9
Adapted first model checker to the new properties.
Former-commit-id: 206d6c9858
10 years ago
dehnert
1699732dce
More work on logic classes.
Former-commit-id: 9d94e02b74
10 years ago
dehnert
433bae1156
Switched from an option to fix deadlocks to an option to not fix the deadlocks. Hence, deadlocks are now fixed by default unless otherwise requested.
Former-commit-id: 9434215807
11 years ago
dehnert
266d660d89
Added functions responsible for printing the help. Started adapting the tests to the new option system.
Former-commit-id: 0407d8223e
11 years ago
dehnert
9ad12616e2
Renamed files in settings module a bit. Started on the pseudo-modular module-settings.
Former-commit-id: b3162aa86b
11 years ago
dehnert
96e1f8faf9
Renamed Settings class to SettingsManager.
Former-commit-id: 2b33f4c8d0
11 years ago
masawei
7f7ddc06e1
Removed two erronous keywords.
Former-commit-id: ecc36e0b07
11 years ago
masawei
d75e32b83e
Renames the folder formula to properties and the namespace property to properties.
Former-commit-id: 236ed22c7d
11 years ago
masawei
27df78c2b0
Finished testing Ltl.
- Regrettably, the LtlFilterTest could not be done, since an Ltl modechecker would be needed for that. Which, we don't have.
|- So that is a TODO until such a modelchecker is implemented.
- This concludes the testing for the refactured formulas.
Next up: Documentation.
Former-commit-id: 2d731edcd9
11 years ago
masawei
2687809591
Finished testing of Csl.
Former-commit-id: 91172a1b89
11 years ago
masawei
b7357c2cf9
Testing, noticed that vectors of pointers are not good. Changing that.
Former-commit-id: 460854c49c
11 years ago
masawei
1c4d7b9ef9
Some more testing.
Former-commit-id: 3105a0bf3b
11 years ago
masawei
ee1ebdf91d
Removed the visitor from LTL and refactured the formulas to use shared pointer in stead of standart pointer.
Next up: Continue testing.
Former-commit-id: 0103895e13
11 years ago
PBerger
d2f4c85711
Made changes to comply with new SparseMatrix Interface (YUCK).
Fixed tests, all that stuff.
Former-commit-id: c78de5f8ce
11 years ago
masawei
3271e73f01
Fixed the last test. All tests green now (well, except the ones that need gurobi, which I don't have).
Former-commit-id: 7636a2a6ab
11 years ago
masawei
9a28e5b580
Added proper formula string method to filters.
- Lots of debugging
- Changed the way the filter keeps information about the scheduler to use for probability/reward queries.
| This was done by keeping a special action at the first position of the action list.
| Which was not exactly consistent with the idea behind the filter actions.
| Now the filter keeps this information as an enum value in a member variable.
- All but one tests are green. So we almost reestablished full functionality.
|- The last test that still fails is SparseMdpPrctlModelCheckerTest.Dice where the second to last model check returns the wrong result.
Next up: Debug. Then introduce the full range of filter actions.
Former-commit-id: fd311966cc
11 years ago
masawei
4bf0299279
Changed the Prctl/Csl formula parsers to be static classes.
- Also fixed up control flow and some tests for new interfaces.
|-> It now compiles again.
Next up: More functionallity in the filter.
Former-commit-id: 21d43e75c4
11 years ago
dehnert
92ee6187fa
Added more query methods to expressions. SparseMatrix now keeps track of non zero entries and models show correct number of transitions by referring to nonzero entries rather than all entries in the matrix.
Former-commit-id: 48180be2fe
11 years ago
PBerger
0922921b24
Updated cudaForStorm/CMakeLists.txt to make use of the new GIT based version schema.
Added version functions to the Cuda Plugin.
Edited storm.cpp to show version infos for the CUDA Plugin.
Fixed a critical error in basicValueIteration.cu which causes random SEGFAULTs... :P
Streamlined the TopologicalValueIterationNondeterministicLinearEquationSolver.cpp. The SCC group optimizer now returns flat_sets instead of a vector as the sets are ordered, which is required for the Solver to work.
This is now a stable version of StoRM containing a fully wor
Former-commit-id: 47d5c2825c
11 years ago
PBerger
af650b6666
Removed debug outputs from the TopologicalValueIterationNondeterministicLinearEquationSolver
Fixed the topo tests, since the comparison values are a bit off for this solver
Former-commit-id: 56c763b37a
11 years ago
dehnert
f049a9f0af
Bugfix for topological equation solver.
Former-commit-id: b8563f8b3e
11 years ago
PBerger
98b0bcf187
Reimplemented the TopologicalValueIterationNondeterministicLinearEquationSolver with splitting into submatrices.
Added a dtmc example for tests with the StronglyConnectedComponentDecomposition.
Former-commit-id: 0c33793fe6
11 years ago
PBerger
3052b19c58
Created a "real" scc example.
Modified the TopologicalValueIterationMdpPrctlModelCheckerTest.cpp to show the crash when not using TBB.
Former-commit-id: 98b47e9573
11 years ago
PBerger
4eef3b0d57
Added an example for SCC related testing which will change soon
Removed unnecessary code from the TopologicalValueIterationMdpPrctlModelChecker.h
Fixed Bugs in graph.h (changes from Sparse Matrix Iterator, it didnt even compile anymore! Unused Code HAUNTS us)
Former-commit-id: 96669adec9
11 years ago