dehnert
|
8ed4a5f849
|
some refactoring in elimination-based model checker
Former-commit-id: 1fb6741479
|
9 years ago |
sjunges
|
1e1400d68d
|
merge
Former-commit-id: eb9efc4bb2
|
9 years ago |
sjunges
|
096778a5d0
|
assorted fixes (builder for no-fix-deadline, semicolon, xercesbuild)
Former-commit-id: 7ae9bcd61e
|
9 years ago |
dehnert
|
dd5af80d5a
|
work towards easier deployment of other ordering heuristics
Former-commit-id: f48dff3630
|
9 years ago |
dehnert
|
d0e15d1a4f
|
more work (and stuff, you know?)
Former-commit-id: ec9f6746b8
|
9 years ago |
dehnert
|
b297cdf38f
|
added some syntatic sugar to PRISM parser in order to enhance performance tests of symbolic model checker
Former-commit-id: d85ce26536
|
9 years ago |
dehnert
|
0d6612352c
|
silenced sylvan and gmm warnings (for clang)
Former-commit-id: 20c561d2e2
|
10 years ago |
dehnert
|
abacfdd28d
|
added sylvan settings. made sylvan available from the cli
Former-commit-id: 3d2403de90
|
10 years ago |
dehnert
|
7376eaf866
|
made symbolic MDP model checker tests work
Former-commit-id: e2e0d07a55
|
10 years ago |
dehnert
|
7f75db2790
|
ADD iterator working for sylvan. enabled more tests for sylvan. symbolic Dtmc model checker now working.
Former-commit-id: b11b2f7476
|
10 years ago |
dehnert
|
8657fb0181
|
introduced relational product operations to prob0/1 algorithms (where possible)
Former-commit-id: 7fcd642030
|
10 years ago |
dehnert
|
19029cd905
|
functional tests compile and run again, yay!
Former-commit-id: 60d3ce16b9
|
10 years ago |
dehnert
|
8bf0f3c87e
|
apparently, changing the DD interface implies some other changes as well...
Former-commit-id: c5cedc720f
|
10 years ago |
dehnert
|
7fa7381047
|
trying to get the new infrastructure of the DD abstraction layer integrated into the other parts of storm
Former-commit-id: 80a6634565
|
10 years ago |
dehnert
|
4e86ef2e47
|
moved CUDD-based DD implementation to own folder
Former-commit-id: a828f92518
|
10 years ago |
dehnert
|
b88165f27c
|
fixed the warnings related to our macros
Former-commit-id: 526b6ea956
|
10 years ago |
dehnert
|
b31d98909b
|
Explicit MDP bisim working but unfortunately slow :(
Former-commit-id: 6714bdbd61
|
10 years ago |
dehnert
|
7156a63b0f
|
tried different approach for bisim for MDPs
Former-commit-id: 92d56a4620
|
10 years ago |
dehnert
|
2484a515a0
|
some more work on bisim
Former-commit-id: aaa8088b00
|
10 years ago |
dehnert
|
40a75baee7
|
using some template magic to make it compile again
Former-commit-id: 69888cac45
|
10 years ago |
dehnert
|
11b04c7940
|
more work towards making the new bisim class available from the cl
Former-commit-id: b177287e00
|
10 years ago |
dehnert
|
1428f1647b
|
commented in some more tests, however the main entry points need to be fixed because of the new templating of the bisimulation class
Former-commit-id: 7133025049
|
10 years ago |
dehnert
|
96954ddd15
|
refactoring of bisimulation class in the prospect of extending it to (CT)MDPs, not yet done
Former-commit-id: 09f47ad977
|
10 years ago |
sjunges
|
86155a5a87
|
extra option for export of a matrix
Former-commit-id: 1ea9046438
|
10 years ago |
sjunges
|
703013b97c
|
program, vector, gurobi
Former-commit-id: 6cfaf78d59
|
10 years ago |
sjunges
|
f914c8a103
|
Filter std::vector by bitvector, could not find such a method before :/
Former-commit-id: b401646d07
|
10 years ago |
dehnert
|
5c838e2006
|
added the feature to build information about the state space that can be retrieved after building the model to the explicit model builder
Former-commit-id: 72b9b18e4e
|
10 years ago |
dehnert
|
4b4c11048f
|
fixed bug in prob1E. added functions to retrieve schedulers for prob0E, probGreater0E and prob1E states of MDPs
Former-commit-id: aea5fe773b
|
10 years ago |
sjunges
|
7884fc37ed
|
explicit model builder supports non-default reward models
Former-commit-id: 97aabc54bb
|
10 years ago |
sjunges
|
ed94184ec8
|
initialize logger with loglevel as an argument
Former-commit-id: 3bac78a39c
|
10 years ago |
sjunges
|
765748c7cf
|
graph stuff for other reward models..
Former-commit-id: e7d4d9b95d
|
10 years ago |
sjunges
|
53dc99deb0
|
prob01A for non.detmodels added (convenience function)
Former-commit-id: 213c8b1b49
|
10 years ago |
dehnert
|
deec423f27
|
fixed infinite recursion in constants comparator
Former-commit-id: b36b352d36
|
10 years ago |
sjunges
|
c3e390c59a
|
extended api with an option to verify model according to given engine
Former-commit-id: b2163590a5
|
10 years ago |
dehnert
|
6a80348150
|
fixed issue related to row groups in sparse matrix and adapted the affected calling sites
Former-commit-id: 96c6fd7e59
|
10 years ago |
sjunges
|
649c928828
|
further refactored api / shifted some highlevel functionality to cli
Former-commit-id: 0fc2dac6a7
|
10 years ago |
sjunges
|
c281efcde3
|
refactored parts of the api
Former-commit-id: 3457c238bb
|
10 years ago |
sjunges
|
01a3748e87
|
Refactored part of the API / more functions
Former-commit-id: eb8deb537c
|
10 years ago |
dehnert
|
bc3f6b8d80
|
fixes for parts that were affected by recent parser templating
Former-commit-id: f71de5cff4
|
10 years ago |
chris
|
a216b5a9d9
|
added support for parsing choice labels for explicit MDPs
Former-commit-id: 89bb1817b4
|
10 years ago |
sjunges
|
b007d45543
|
Extended lp solver factory interface
Former-commit-id: 437e62619d
|
10 years ago |
sjunges
|
f08f66e900
|
added an option for polic extraction to the helper, some includes
Former-commit-id: 44b6a5d03f
|
10 years ago |
sjunges
|
73310b9881
|
fixed tests: glpk had wrong minimize, solver.cpp tested in wrong direction on policy iteration in case we use top. value iteration
Former-commit-id: 71215b8e46
|
10 years ago |
sjunges
|
8568ee3986
|
only one optimization direction enum -- towards integration of termination criterions on the model checker
Former-commit-id: 648855264e
|
10 years ago |
dehnert
|
57338640be
|
added missing include
Former-commit-id: c67bb4a99e
|
10 years ago |
dehnert
|
b418782bcd
|
added missing header
Former-commit-id: b3b4deddb7
|
10 years ago |
dehnert
|
3ea084b777
|
included missing header
Former-commit-id: 7e002652ed
|
10 years ago |
dehnert
|
f409087f47
|
first version of interval reward model support for MDPs. also fixed a missing include that prevented compilation of the main executable
Former-commit-id: 6b7f7a96e7
|
10 years ago |
dehnert
|
21d9e91586
|
work towards interval reward model
Former-commit-id: 24f7e9684f
|
10 years ago |
sjunges
|
35a154f67f
|
Splitted graph in h and cpp`
Former-commit-id: e22ab7f8eb
|
10 years ago |