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 |
sjunges
|
cb913658cc
|
removed perm schedulers from gspn to circumvent error msg for now
Former-commit-id: 7d10ec8367
|
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 |
dehnert
|
31be908c5a
|
mathsat does not like boolean arguments to ite-expressions, so we encode it ourselves now
Former-commit-id: e30e7fcd55
|
9 years ago |
sjunges
|
131ab5b674
|
Updates on perm. schedulers
Former-commit-id: 16b65774a1
|
9 years ago |
dehnert
|
beee4a9e82
|
fixed a bug in the tests that caused a segfault
Former-commit-id: b0c4b1c764
|
9 years ago |
dehnert
|
2376905810
|
more work
Former-commit-id: 7182125a9e
|
9 years ago |
dehnert
|
381fe6d9a8
|
more work on translating BDDs to expressions
Former-commit-id: 0f361f76f5
|
9 years ago |
dehnert
|
781610b05d
|
extended tests for validity of returned strategies
Former-commit-id: fb6a1c23f0
|
9 years ago |
dehnert
|
c624b19427
|
added no-cuts option. prob1 tests for game now passing.
Former-commit-id: 3806747948
|
9 years ago |
dehnert
|
e8b7928831
|
fixed minor bug
Former-commit-id: 6d208b877a
|
9 years ago |
dehnert
|
1c42ed792b
|
fixed some bugs, added some test, added some prob1 algorithm, and did some stuff, you know?
Former-commit-id: 00fa21d1fe
|
9 years ago |
dehnert
|
972795912a
|
added some convenience accessor methods in symbolic model/games. added return type for prob01 for games that can also store strategies. added tests for prob0 for games
Former-commit-id: f0a8b156ca
|
9 years ago |
dehnert
|
0bd0b963d7
|
introduced new menu game class
Former-commit-id: f27691f9d6
|
9 years ago |
dehnert
|
7cd1e6324f
|
the abstraction now properly builds an instance of the game class
Former-commit-id: 26d4effa00
|
9 years ago |
dehnert
|
1199ab95e3
|
fixed bug in expressions. all tests now passing
Former-commit-id: 86b4b2a04a
|
9 years ago |
dehnert
|
0cd148c600
|
fixed more bugs. however, a test still fails, because the abstraction is wrong
Former-commit-id: 6e326acaf3
|
9 years ago |
dehnert
|
e8794dee22
|
added more tests, not working yet, however
Former-commit-id: 2badd7ce35
|
9 years ago |
dehnert
|
5934d67514
|
DD meta variables can now be inserted at particular locations. added some tests for game abstraction
Former-commit-id: 1c870dc0de
|
9 years ago |
dehnert
|
8911d2ba63
|
added debug output and fixed some bugs
Former-commit-id: 8d2b7a4dd5
|
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 |
dehnert
|
c6f1cb40d3
|
more work on games
Former-commit-id: d89f025da4
|
10 years ago |
TimQu
|
d26f38b9a2
|
minor stuff, some more pmdp examples and an mdp test case
Former-commit-id: f48e308e5f
|
10 years ago |
dehnert
|
f013ddfb4c
|
The determined relevant predicates are now added to the SMT solver of an abstract command. Also, variable bounds are enforced.
Former-commit-id: 703b49e732
|
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 |
dehnert
|
ccad5741a7
|
added test case for game solver
Former-commit-id: 9bf486aa00
|
10 years ago |
TimQu
|
5b1494b9a9
|
Made use of this new cool rewardModel thing
Former-commit-id: d670d09278
|
10 years ago |
dehnert
|
e659dd8c4a
|
some work on sparse game solver
Former-commit-id: 74450365b3
|
10 years ago |
TimQu
|
d377e6b289
|
Minor improvements everywhere. Also implemented some tests
Former-commit-id: be74e5f459
|
10 years ago |
dehnert
|
bc3f6b8d80
|
fixes for parts that were affected by recent parser templating
Former-commit-id: f71de5cff4
|
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
|
7fd28d4564
|
refactored cmakelists
Former-commit-id: 34e4e217a6
|
10 years ago |
sjunges
|
2213b01ece
|
changes in milp permissive scheduler
Former-commit-id: 6b11d01b88
|
10 years ago |
sjunges
|
6d10ba0ad0
|
compiles again
Former-commit-id: 1c09323cd1
|
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 |