TimQu
3ce8643d96
Added benchmarks
Former-commit-id: 6979a9aece
9 years ago
dehnert
0f6e6e4da1
added feature to compute step-bounded until probabilities in parametric models
Former-commit-id: 172e87cb55
9 years ago
TimQu
1225b056f2
a little refactoring
Former-commit-id: 9af14c006c
9 years ago
sjunges
1e1400d68d
merge
Former-commit-id: eb9efc4bb2
9 years ago
dehnert
d0e15d1a4f
more work (and stuff, you know?)
Former-commit-id: ec9f6746b8
9 years ago
dehnert
f8fc39870a
hybrid and symbolic model checkers working with sylvan
Former-commit-id: d01b92e328
9 years ago
dehnert
7376eaf866
made symbolic MDP model checker tests work
Former-commit-id: e2e0d07a55
9 years ago
dehnert
7f75db2790
ADD iterator working for sylvan. enabled more tests for sylvan. symbolic Dtmc model checker now working.
Former-commit-id: b11b2f7476
9 years ago
TimQu
91fb664910
Refactored a little and implemented functions for prophesy
Former-commit-id: a61f1eaff2
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
dehnert
19029cd905
functional tests compile and run again, yay!
Former-commit-id: 60d3ce16b9
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
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
TimQu
1860502a3a
Deterministic states with only constant outgoing transitions are now eliminated
Former-commit-id: be5bf4f7cc
9 years ago
TimQu
77c2f397a9
fix for approximation model, additional test for mdps, minor changes
Former-commit-id: cc837ddf3e
10 years ago
TimQu
046afd3804
Refactored SamplingModel
Former-commit-id: b51ed752b4
10 years ago
dehnert
de58c73c5a
forgot to commit some files
Former-commit-id: 74aaea662a
10 years ago
TimQu
d26f38b9a2
minor stuff, some more pmdp examples and an mdp test case
Former-commit-id: f48e308e5f
10 years ago
TimQu
78bd4a041a
Added Mdp class, sampling might work already (untested)
Former-commit-id: f0d5c77645
10 years ago
TimQu
70dd76c08b
Splitted region modelchecker in abstract class and dtmc class (to easily add an mdp class soon)
Former-commit-id: e722c8f2bd
10 years ago
TimQu
0043d3ebf5
changed template argument, used unordered_map
Former-commit-id: a563503d4a
10 years ago
TimQu
5b1494b9a9
Made use of this new cool rewardModel thing
Former-commit-id: d670d09278
10 years ago
TimQu
d377e6b289
Minor improvements everywhere. Also implemented some tests
Former-commit-id: be74e5f459
10 years ago
dehnert
27e06940a9
templated all explicit parsers so that they may now be modified to produce non-double models
Former-commit-id: dd7f8767f8
10 years ago
sjunges
e3122e5ede
Faster compilation and topological failing test failed
Former-commit-id: 55c816594f
10 years ago
sjunges
f219437acf
Faster compilation times!
Former-commit-id: a8dc8fa612
10 years ago
sjunges
1086ffc1cc
Added allow early termination for min/max solvers
Former-commit-id: eaad511158
10 years ago
dehnert
f9f5a4e206
reincluded tbb in gmm. fixed missing header. extended formula parser to return multiple formulas
Former-commit-id: a2849d6534
10 years ago
dehnert
b94e978843
another round of fixes
Former-commit-id: 67f4e4be47
10 years ago
dehnert
fbd05cd780
more and more bugfixes
Former-commit-id: 7f1ba98797
10 years ago
dehnert
b3178e17f6
more bug fixes
Former-commit-id: 0b33b30efa
10 years ago
dehnert
73a2491dfb
more bugfixes
Former-commit-id: 5afecd5a21
10 years ago
dehnert
dbc7d860a4
functional tests compile again, started to debug changes
Former-commit-id: efef0e6487
10 years ago
sjunges
5e428a795a
And more includes on the right spot.
Former-commit-id: 72bb348687
10 years ago
dehnert
72cb30d6b0
started replacing ValueType template argument by model class in all instantiations
Former-commit-id: 197e3876a4
10 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
10 years ago
sjunges
3c2040f4b7
Removed many superfluous includes, added some source files -- towards faster compilation
Former-commit-id: a575a97d40
10 years ago
dehnert
e338cbe069
fixed a lot of warnings in the tests
Former-commit-id: b6752202ac
10 years ago
dehnert
04f789619c
some work towards eliminating compiler warnings
Former-commit-id: d1eca470a4
10 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
4c35bc0f66
symbolic DTMC model checker working
Former-commit-id: d0913f7912
10 years ago
PBerger
0c3c057f83
Fixed the usual "typename" errors in Clang-code.
Former-commit-id: 20606ed360
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