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 |
dehnert
|
72cb30d6b0
|
started replacing ValueType template argument by model class in all instantiations
Former-commit-id: 197e3876a4
|
9 years ago |
sjunges
|
84ecabd2c8
|
further fixes, for performance tests and windows
Former-commit-id: 47a4502fd0
|
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
|
f85d28325e
|
Further work towards faster and more modular compilation
Former-commit-id: 9de50910b8
|
9 years ago |
sjunges
|
3c2040f4b7
|
Removed many superfluous includes, added some source files -- towards faster compilation
Former-commit-id: a575a97d40
|
9 years ago |
sjunges
|
a129983ae9
|
cleaning includes for better compilation times
Former-commit-id: e2878ae043
|
9 years ago |
dehnert
|
d7f1012509
|
got rid of more warnings
Former-commit-id: 514624a4b1
|
9 years ago |
dehnert
|
56b4f53ce7
|
got rid of more warnings
Former-commit-id: 5c39f63c69
|
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
|
c683934ea0
|
removed debug output and fixed bug
Former-commit-id: 0c33f61bbe
|
9 years ago |
dehnert
|
8985ad77cf
|
added first debug output to track down bug
Former-commit-id: ad333216c1
|
9 years ago |
dehnert
|
d62539165e
|
'Identity updates' can now be described as applying 'true' in PRISM programs.
Former-commit-id: b2f70eb465
|
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
|
6c4162fae4
|
more work towards steady state for CTMCs
Former-commit-id: c3e17d1fc0
|
10 years ago |
dehnert
|
4c35bc0f66
|
symbolic DTMC model checker working
Former-commit-id: d0913f7912
|
10 years ago |
dehnert
|
81c627b9b7
|
First version of fully symbolic game solver.
Former-commit-id: 34406f25b9
|
10 years ago |
PBerger
|
0c3c057f83
|
Fixed the usual "typename" errors in Clang-code.
Former-commit-id: 20606ed360
|
10 years ago |
dehnert
|
a4663ccfd3
|
added missing input file for tests
Former-commit-id: 7d1c7f8570
|
10 years ago |
PBerger
|
287393abc4
|
Added Policy Iteration to the NativeMinMaxLinearEquationSolver.
Added a test.
Former-commit-id: 087934eb47
|
10 years ago |
PBerger
|
f63e5fc873
|
Implemented Policy Iteration inside the GmmxxMinMaxLinearEquationSolver.
Added an option for selecting Value- or Policy Iteration in the GeneralSettings.
Former-commit-id: 6d12f10f60
|
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
|
3b4dca1a03
|
Improved Jacobi method a bit.
Former-commit-id: f4affeebf6
|
10 years ago |
dehnert
|
e83d191be3
|
ODDs can now also be constructed from BDDs directly (without a transformation step to ADDs).
Former-commit-id: d19bbc3ff5
|
10 years ago |
dehnert
|
c8d8f75a10
|
Working on ODD generation for BDDs (not yet working).
Former-commit-id: 5665dd1f24
|
10 years ago |
dehnert
|
d787b80fec
|
CTMC examples now build properly using the DD-based model generator.
Former-commit-id: ac97b005e3
|
10 years ago |
dehnert
|
8f4a4397e0
|
Started working on Markovian commands in PRISM programs.
Former-commit-id: 94ed3c747c
|
10 years ago |
dehnert
|
60701cebdb
|
ADDs and BDDs are no longer mixed in the abstraction layer.
Former-commit-id: 3c31063ea6
|
10 years ago |
dehnert
|
eb5d4100a6
|
Renamed Nondeterminstic equation solver as this name is more than misleading.
Former-commit-id: 7f08ed130c
|
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 |