dehnert
8194454621
more work on making sylvan mtbdds work
Former-commit-id: 98454b0ff4
9 years ago
dehnert
99f096635f
started integrating sylvan
Former-commit-id: 2aec043047
9 years ago
TimQu
f7992f5aa7
Forgot adaptation of test...
Former-commit-id: 263da953bc
9 years ago
TimQu
b4a4a81bb1
Renamed, moved, added some benchmarks
Former-commit-id: 670448c26f
9 years ago
TimQu
f3f3a31e1e
Optimization for policy recycling
Former-commit-id: b66a74b746
9 years ago
dehnert
cb58b79e24
moved cudd's c++ objects to a separate namespace in an attempt to make cudd and sylvan coexist without name clashes
Former-commit-id: 425381c8e8
9 years ago
dehnert
d25bd3a32f
added 'empty' framework for sylvan-based implementation of DD abstraction layer
Former-commit-id: c0f781a515
9 years ago
dehnert
c36d869b3c
done cleaining up
Former-commit-id: 4c732fc188
9 years ago
dehnert
009dabf2f1
started cleanining up
Former-commit-id: 3db6fbc1b2
9 years ago
dehnert
a258d1ab48
restructured ODD to be independent of the DD library being used
Former-commit-id: 83f08ba203
9 years ago
dehnert
19029cd905
functional tests compile and run again, yay!
Former-commit-id: 60d3ce16b9
9 years ago
dehnert
960ef4ff65
same shit, different day
Former-commit-id: 495b9fd952
9 years ago
dehnert
231c3ec060
started lifting toVector, etc. from the internal classes to the general superclasses
Former-commit-id: 0501487b22
9 years ago
TimQu
9c645ba24b
Work on policy recycling
Former-commit-id: b8e94254ce
9 years ago
dehnert
f7c26fd4b1
more modifications needed for refactoring of DD stuff
Former-commit-id: b7b7f52231
9 years ago
TimQu
dae0faa2a0
refactored the quick implementation of the recent bugfix
Former-commit-id: 5c0d1fa3b9
9 years ago
TimQu
4a874a5a29
Added some benchmark models from param website
Fixed two bugs considering nonatomic subformulae and constant results
Qualitative modelchecking needs to be done when applying a policy!
Former-commit-id: bd88228214
9 years ago
dehnert
8bf0f3c87e
apparently, changing the DD interface implies some other changes as well...
Former-commit-id: c5cedc720f
9 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
9 years ago
dehnert
340b39e4a7
more work on refactoring DD abstraction layer
Former-commit-id: 4dc4260798
9 years ago
TimQu
87c8241ec7
policies for games
Former-commit-id: 8bfb325b60
9 years ago
dehnert
eb1619153e
same same
Former-commit-id: 8a5597ca6f
9 years ago
dehnert
52062b523d
more work on refactoring DD abstraction layer
Former-commit-id: 83bf755a91
9 years ago
dehnert
d683e38d4a
started refactoring DD-interface a bit in an attempt to ease the integration of sylvan
Former-commit-id: 3a90e171b8
9 years ago
TimQu
bf450688b4
The variable pool of carl needs to be cleared after executing a test.
Sampling for mdps now uses the policy of the previous iteration as initial guess
Former-commit-id: 3b8b25f30f
9 years ago
dehnert
4e86ef2e47
moved CUDD-based DD implementation to own folder
Former-commit-id: a828f92518
9 years ago
dehnert
7080f954b9
Fixed sylvan cmake file to also work with xcode (stripping the build type from the directory)
Former-commit-id: 5c934c7793
9 years ago
dehnert
226c77db77
added sylvan and started making it compile using cmake
Former-commit-id: b6b6171d0f
9 years ago
dehnert
b88165f27c
fixed the warnings related to our macros
Former-commit-id: 526b6ea956
9 years ago
dehnert
4d36ee3ea1
Merge branch 'master' into future
Former-commit-id: 720869befc
9 years ago
dehnert
8d98403748
small fix for use of carl
Former-commit-id: 63a0e38cf5
9 years ago
TimQu
358bc14ded
Merge branch 'future' into TimParamSysAndSMT
Former-commit-id: f54a7a3c88
9 years ago
TimQu
e8304e7515
Merge branch 'master' into future
Former-commit-id: 1ac7368569
9 years ago
TimQu
b792438d88
Added missing include
Former-commit-id: a073cf157d
9 years ago
TimQu
0089212b7e
adaptation to recent changes in carl
Former-commit-id: 90535a0d66
9 years ago
TimQu
0863d0e51a
don't store ALL the occurring policies...
Former-commit-id: f442b97b8b
9 years ago
dehnert
1d49bc6dd0
extracting the bisimulation quotient for MDPs; tests for MDP bisimulation
Former-commit-id: 5613c653ba
9 years ago
dehnert
b31d98909b
Explicit MDP bisim working but unfortunately slow :(
Former-commit-id: 6714bdbd61
9 years ago
dehnert
7156a63b0f
tried different approach for bisim for MDPs
Former-commit-id: 92d56a4620
9 years ago
dehnert
c2a0bd5ab0
initial outline of strong MDP bisimulation
Former-commit-id: 06452543ea
9 years ago
dehnert
288f0418c2
Merge branch 'future' into mdpbisim
Former-commit-id: 7c75979e67
9 years ago
dehnert
9bac056354
enabled preconditioning for value iteration in gmm++-based MinMax equation solver
Former-commit-id: 39c4efdb52
9 years ago
TimQu
ca917a651c
MinMaxLinearEqSolvers can now use some initial policy as a first guess.
First steps to use this for region approximation
Former-commit-id: 9a8151607f
9 years ago
TimQu
a723cfca14
Made sampling for MDPs correct again
Former-commit-id: 7917200f4e
9 years ago
dehnert
7833025829
reenabled all bisimulation tests
Former-commit-id: 24e8629270
9 years ago
dehnert
3054aa9866
Merge branch 'future' into mdpbisim
Former-commit-id: bfc52e25d9
9 years ago
dehnert
1de6d4ee07
Merge branch 'master' into future
Former-commit-id: ab9d23e0e1
9 years ago
dehnert
9b7d4ec57b
made rational functions use cln again
Former-commit-id: a4b14f9271
9 years ago
dehnert
51bd689c96
fixed a bug in the reward model
Former-commit-id: 5302a85d6f
9 years ago
dehnert
9475d29164
fixed weak bisim for dtmc
Former-commit-id: 05462b99ec
9 years ago