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: d0913f7912faa14240175d10bd9711e4dba74bb1
|
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 |
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
|
00e7121bc4
|
some work towards BDD-based mc.
Former-commit-id: cae0c4421e
|
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 |
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 |
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
|
239caf57eb
|
Added symbolic models and made DD-based model generator build the correct instances.
Former-commit-id: c054401cfd
|
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
|
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 |
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
|
10 years ago |
dehnert
|
e79233bd7b
|
Added check in PRISM program that prevents global varibles from written in possibly synchronizing commands.
Former-commit-id: 34e34cacbe
|
10 years ago |
dehnert
|
3977cafe73
|
Extended DD-based model building to also build the MDP models of our benchmark suite. Added (MDP) tests for DD-based model building and explicit model building.
Former-commit-id: 4e18f98ee6
|
10 years ago |
dehnert
|
8c1870eb54
|
Intermediate commit.
Former-commit-id: e5f251718f
|
10 years ago |
dehnert
|
0f0baf61a4
|
Made DD-based model construction work for all DTMC benchmarks we have. Included tests for both DD-based and excplicit model generation from PRISM models.
Former-commit-id: e4af6d9f8a
|
10 years ago |