dehnert
|
96464fdcbc
|
added model classes for two-player stochastic games
Former-commit-id: 8dccae2ea9
|
10 years ago |
dehnert
|
37cd2ad682
|
started working on game solver
Former-commit-id: 59c3528d23
|
10 years ago |
PBerger
|
3bb0346407
|
Fixed missing typenames and member initialization reordering.
Former-commit-id: bdf24399d6
|
10 years ago |
PBerger
|
0c3c057f83
|
Fixed the usual "typename" errors in Clang-code.
Former-commit-id: 20606ed360
|
10 years ago |
PBerger
|
dce1d728e5
|
I added a few small documentation fixes.
Former-commit-id: d5d8f7fbb0
|
10 years ago |
PBerger
|
b9eaddfcb3
|
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 82835c1f72
|
10 years ago |
David_Korzeniewski
|
772ab33ad1
|
Merge remote-tracking branch 'remotes/origin/master'
Former-commit-id: d2d3f54d07
|
10 years ago |
David_Korzeniewski
|
5623e66566
|
Ignore empty lines in property file and only warn if a line could not be parsed
Former-commit-id: 1d2767e90d
|
10 years ago |
dehnert
|
a4663ccfd3
|
added missing input file for tests
Former-commit-id: 7d1c7f8570
|
10 years ago |
dehnert
|
68b786d47b
|
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: c8944f81e5
|
10 years ago |
dehnert
|
f672f8d8d8
|
Merge branch 'mtbddIntegration'
Former-commit-id: 5a388df365
|
10 years ago |
PBerger
|
21d1039152
|
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 00ddae78e2
|
10 years ago |
David_Korzeniewski
|
c3d0112975
|
Actually try to read all lines from property file
Former-commit-id: 588d80c8c1
|
10 years ago |
PBerger
|
287393abc4
|
Added Policy Iteration to the NativeMinMaxLinearEquationSolver.
Added a test.
Former-commit-id: 087934eb47
|
10 years ago |
PBerger
|
56e1b79085
|
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 3a9965dcfd
|
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
|
7d84b0a4c5
|
Added ability to check properties from property file to cli utility.
Added minimal example for lra on dtmc
Former-commit-id: eec774f05a
|
10 years ago |
David_Korzeniewski
|
1cf0a73c4e
|
Added methods to update nonzero entry count and update it when necessary
And a fix for a compile error on gcc&clang.
Former-commit-id: 2a095ca864
|
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
|
5acaed6048
|
Added flag to keep zeros when transposing.
Former-commit-id: 811f6824cf
|
10 years ago |
David_Korzeniewski
|
0ba629ad3f
|
More tests, bugfixes: All tests pass.
Former-commit-id: f37c02a9d7
|
10 years ago |
David_Korzeniewski
|
dfab1c291c
|
Error fixed.
Former-commit-id: b2514633a7
|
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
|
3872e17a4e
|
Merge branch 'master' into LRA_for_dtmc_mdp
Former-commit-id: 0f7464cdc0
|
10 years ago |
David_Korzeniewski
|
d4f051c4f0
|
Fixed Windows build
Former-commit-id: 53c99736de
|
10 years ago |
David_Korzeniewski
|
073ce2ee2c
|
Merge branch 'master' into LRA_for_dtmc_mdp
Conflicts:
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
test/functional/modelchecker/SparseMdpPrctlModelCheckerTest.cpp
Former-commit-id: bbd68de871
|
10 years ago |
David_Korzeniewski
|
1f87e7c8b2
|
First test for LRA on MDPs
Former-commit-id: c022ceaf01
|
10 years ago |
David_Korzeniewski
|
8fc58439bc
|
Computing LRA as expected reward in MDPs.
- Everything compiles without error. No tests yet.
Former-commit-id: d8cceb02fc
|
10 years ago |
dehnert
|
e4968b1dde
|
Fixed minor issue in cli
Former-commit-id: ed63925765
|
10 years ago |
David_Korzeniewski
|
0fdb3685d1
|
Computing LRA for states not in bsccs as expected reward
Former-commit-id: 4bcb5f0a6e
|
10 years ago |
David_Korzeniewski
|
916c821b3e
|
Compute steady state for all BSCCs together by solving just one equation system instead of solving an equation system for each BSCC.
Former-commit-id: 74f715c3a8
|
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 |
David_Korzeniewski
|
9a83dfac10
|
Typo in DTMC, tried to use same approach for MDPs, which won't work.
Former-commit-id: 5c1e835d09
|
10 years ago |
dehnert
|
e3320ee086
|
Started working on hybrid MDP model checker.
Former-commit-id: 63a8efb93c
|
10 years ago |
David_Korzeniewski
|
53f2fdf51e
|
Changed implementation of LRA to be weighted with the probability to reach BSCCs instead of choosing min/max
Former-commit-id: 347fda8e22
|
10 years ago |
dehnert
|
869f8c50c9
|
Fixed some minor CTMC-related bugs.
Former-commit-id: 3abb948542
|
10 years ago |
David_Korzeniewski
|
a448cd8973
|
Calculating steady state using standard equation system for eigenvectors, removed all-in-one matrix transformation (nicer looking code)
Former-commit-id: 2502615686
|
10 years ago |
dehnert
|
be66ef2751
|
Finalized hybrid CTMC model checker.
Former-commit-id: c217e11b06
|
10 years ago |
dehnert
|
8868a50864
|
Removed superfluous code.
Former-commit-id: 06c2309d3c
|
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
|
76b99a5515
|
Commit to switch workplace.
Former-commit-id: e80da5e90b
|
10 years ago |
dehnert
|
c1917ce6d9
|
Finalized hybrid DTMC model checker. It now passes its tests.
Former-commit-id: 99d79e1bc6
|
10 years ago |
David_Korzeniewski
|
04c1d51313
|
intermediate commit, copied transpose and get submatrix code over and started adapting it.
(changing workplace)
Former-commit-id: af4a34dd3b
|
10 years ago |
dehnert
|
72166bed37
|
Created new class for storing hybrid check results (symbolic as well as explicit parts) and the surrounding functionality.
Former-commit-id: d4ad6da5a1
|
10 years ago |
dehnert
|
3b4dca1a03
|
Improved Jacobi method a bit.
Former-commit-id: f4affeebf6
|
10 years ago |
dehnert
|
06bfc17ec6
|
Started making hybrid (dd/sparse) model checking work.
Former-commit-id: 23fac3a672
|
10 years ago |
dehnert
|
907e3512c0
|
Fixed a potential bug in the ODD generation and it now uses hash maps instead of regular maps.
Former-commit-id: f8e5fb3018
|
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 |