dehnert
de58c73c5a
forgot to commit some files
Former-commit-id: 74aaea662a
9 years ago
dehnert
27e06940a9
templated all explicit parsers so that they may now be modified to produce non-double models
Former-commit-id: dd7f8767f8
9 years ago
sjunges
e3122e5ede
Faster compilation and topological failing test failed
Former-commit-id: 55c816594f
9 years ago
sjunges
f219437acf
Faster compilation times!
Former-commit-id: a8dc8fa612
9 years ago
sjunges
1086ffc1cc
Added allow early termination for min/max solvers
Former-commit-id: eaad511158
9 years ago
dehnert
f9f5a4e206
reincluded tbb in gmm. fixed missing header. extended formula parser to return multiple formulas
Former-commit-id: a2849d6534
9 years ago
dehnert
b94e978843
another round of fixes
Former-commit-id: 67f4e4be47
9 years ago
dehnert
fbd05cd780
more and more bugfixes
Former-commit-id: 7f1ba98797
9 years ago
dehnert
b3178e17f6
more bug fixes
Former-commit-id: 0b33b30efa
9 years ago
dehnert
73a2491dfb
more bugfixes
Former-commit-id: 5afecd5a21
9 years ago
dehnert
dbc7d860a4
functional tests compile again, started to debug changes
Former-commit-id: efef0e6487
9 years ago
sjunges
5e428a795a
And more includes on the right spot.
Former-commit-id: 72bb348687
9 years ago
dehnert
72cb30d6b0
started replacing ValueType template argument by model class in all instantiations
Former-commit-id: 197e3876a4
9 years ago
sjunges
92082dc970
gurobi lp solver refactored in case gurobi is not found, and fixes for linux - sorry about earlier lack of checks on linux
Former-commit-id: badef77583
9 years ago
sjunges
3c2040f4b7
Removed many superfluous includes, added some source files -- towards faster compilation
Former-commit-id: a575a97d40
9 years ago
dehnert
e338cbe069
fixed a lot of warnings in the tests
Former-commit-id: b6752202ac
9 years ago
dehnert
04f789619c
some work towards eliminating compiler warnings
Former-commit-id: d1eca470a4
9 years ago
dehnert
c99a61307f
hybrid dtmc model checker can now also treat lra
Former-commit-id: 2db1d9a600
10 years ago
dehnert
39abecbad3
added some tests for LRA in CTMCs
Former-commit-id: 3b847d542e
10 years ago
dehnert
1e5398c8b7
LRA finally working for ctmcs
Former-commit-id: 699e4714a4
10 years ago
dehnert
331ea9fc19
further work on steady state probabilities
Former-commit-id: d2497ac7eb
10 years ago
dehnert
4c35bc0f66
symbolic DTMC model checker working
Former-commit-id: d0913f7912
10 years ago
PBerger
0c3c057f83
Fixed the usual "typename" errors in Clang-code.
Former-commit-id: 20606ed360
10 years ago
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
dd399c5f85
Finalized hybrid MDP model checker. It passes its tests now.
Former-commit-id: 47de0b9433
10 years ago
dehnert
2bf7eafb4b
Further work on hybrid MDP model checker.
Former-commit-id: 3192a13f55
10 years ago
dehnert
869f8c50c9
Fixed some minor CTMC-related bugs.
Former-commit-id: 3abb948542
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
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