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
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
dehnert
1d49bc6dd0
extracting the bisimulation quotient for MDPs; tests for MDP bisimulation
Former-commit-id: 5613c653ba
9 years ago
dehnert
7833025829
reenabled all bisimulation tests
Former-commit-id: 24e8629270
9 years ago
dehnert
46fee522ff
made strong bisim for DTMCs work again
Former-commit-id: e42bafef4d
9 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
9 years ago
dehnert
11c21eb338
on my way of making (the refactored version) bisimulation work again for deterministic models
Former-commit-id: 79c089a693
9 years ago
dehnert
96954ddd15
refactoring of bisimulation class in the prospect of extending it to (CT)MDPs, not yet done
Former-commit-id: 09f47ad977
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
9 years ago
dehnert
b3ce727f6c
fixed minor bug, tests for smt-based permissive schedulers (for upper-bounded properties) now passing
Former-commit-id: bf0261e981
9 years ago
dehnert
59501dd347
removed some object files of xerces. started working on smt-based permissive schedulers
Former-commit-id: de95333225
9 years ago
sjunges
160f9e476f
test descr for milp perm sched
Former-commit-id: 54dfa2587e
9 years ago
TimQu
046afd3804
Refactored SamplingModel
Former-commit-id: b51ed752b4
9 years ago
dehnert
de58c73c5a
forgot to commit some files
Former-commit-id: 74aaea662a
9 years ago
sjunges
e4aab761d2
updates to perm schedulers
Former-commit-id: b3404cac21
9 years ago
sjunges
131ab5b674
Updates on perm. schedulers
Former-commit-id: 16b65774a1
9 years ago
dehnert
15b97057dd
silenced some warnings within boost (new clang version) and fixed an unused variable issue
Former-commit-id: d19970b278
9 years ago
TimQu
d26f38b9a2
minor stuff, some more pmdp examples and an mdp test case
Former-commit-id: f48e308e5f
9 years ago
TimQu
78bd4a041a
Added Mdp class, sampling might work already (untested)
Former-commit-id: f0d5c77645
9 years ago
TimQu
70dd76c08b
Splitted region modelchecker in abstract class and dtmc class (to easily add an mdp class soon)
Former-commit-id: e722c8f2bd
9 years ago
TimQu
0043d3ebf5
changed template argument, used unordered_map
Former-commit-id: a563503d4a
9 years ago
dehnert
ccad5741a7
added test case for game solver
Former-commit-id: 9bf486aa00
9 years ago
TimQu
5b1494b9a9
Made use of this new cool rewardModel thing
Former-commit-id: d670d09278
9 years ago
dehnert
e659dd8c4a
some work on sparse game solver
Former-commit-id: 74450365b3
9 years ago
TimQu
d377e6b289
Minor improvements everywhere. Also implemented some tests
Former-commit-id: be74e5f459
9 years ago
dehnert
bc3f6b8d80
fixes for parts that were affected by recent parser templating
Former-commit-id: f71de5cff4
9 years ago
dehnert
27e06940a9
templated all explicit parsers so that they may now be modified to produce non-double models
Former-commit-id: dd7f8767f8
9 years ago
sjunges
7fd28d4564
refactored cmakelists
Former-commit-id: 34e4e217a6
9 years ago
sjunges
2213b01ece
changes in milp permissive scheduler
Former-commit-id: 6b11d01b88
9 years ago
sjunges
6d10ba0ad0
compiles again
Former-commit-id: 1c09323cd1
9 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
9 years ago
sjunges
8568ee3986
only one optimization direction enum -- towards integration of termination criterions on the model checker
Former-commit-id: 648855264e
9 years ago
dehnert
08bc810b2c
added missing include
Former-commit-id: 7eed5aaba7
9 years ago
dehnert
57338640be
added missing include
Former-commit-id: c67bb4a99e
9 years ago
sjunges
e3122e5ede
Faster compilation and topological failing test failed
Former-commit-id: 55c816594f
9 years ago
sjunges
f219437acf
Faster compilation times!
Former-commit-id: a8dc8fa612
9 years ago
sjunges
1086ffc1cc
Added allow early termination for min/max solvers
Former-commit-id: eaad511158
9 years ago
sjunges
f006d54995
vector min_if, max_if
Former-commit-id: afff48d2e5
9 years ago
dehnert
7f5e775395
adapted counterexample generation to refactoring
Former-commit-id: e73d2885cd
9 years ago
dehnert
f9f5a4e206
reincluded tbb in gmm. fixed missing header. extended formula parser to return multiple formulas
Former-commit-id: a2849d6534
9 years ago
dehnert
29716ea5f8
performance tests now compile again. also fixed some warnings
Former-commit-id: 2fa8c2abd9
9 years ago
dehnert
b94e978843
another round of fixes
Former-commit-id: 67f4e4be47
9 years ago
sjunges
707a4f500b
vector sum_if
Former-commit-id: 67b2ef9ff6
9 years ago
sjunges
d4ba7905fa
Extra constructor for simple testing.
Former-commit-id: 0fcef3d5e7
9 years ago
sjunges
faf31156e0
fix for last changes + is probabilistic
Former-commit-id: 38df3f515f
9 years ago
dehnert
972c391eb1
fixed some more bugs/warnings
Former-commit-id: 2748793daf
9 years ago