sjunges
|
896d2bcaef
|
propositional model checking for further interval reward model types
Former-commit-id: b8d2c89335
|
9 years ago |
|
sjunges
|
e4aab761d2
|
updates to perm schedulers
Former-commit-id: b3404cac21
|
9 years ago |
|
sjunges
|
98162d1d7e
|
interface for rew. model extended for reinforcement learning
Former-commit-id: b69474fc4f
|
9 years ago |
|
sjunges
|
765748c7cf
|
graph stuff for other reward models..
Former-commit-id: e7d4d9b95d
|
9 years ago |
|
sjunges
|
e8799963fe
|
compiles again
Former-commit-id: fb79c334d8
|
9 years ago |
|
sjunges
|
b8343255be
|
fixed headers, allow changes in rew. model again
Former-commit-id: 4617000d30
|
9 years ago |
|
sjunges
|
53dc99deb0
|
prob01A for non.detmodels added (convenience function)
Former-commit-id: 213c8b1b49
|
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 |
|
dehnert
|
7ecd9958e8
|
more work on game-stuff
Former-commit-id: 62a56c9ba7
|
9 years ago |
|
sjunges
|
131ab5b674
|
Updates on perm. schedulers
Former-commit-id: 16b65774a1
|
9 years ago |
|
sjunges
|
edbd7e827b
|
MDPs, restrict choices, get choiceindex
Former-commit-id: 6d1f2ff37d
|
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
|
4b24be7204
|
commit to switch workplace
Former-commit-id: c50e423557
|
9 years ago |
|
sjunges
|
2f49418e63
|
Add dependency on xercesc
Former-commit-id: 595b4d294d
|
9 years ago |
|
sjunges
|
21b0829b69
|
...
Former-commit-id: 55a29b1517
|
9 years ago |
|
sjunges
|
e9b4aa5de4
|
xerces 2nd part
Former-commit-id: bcd783c277
|
9 years ago |
|
sjunges
|
73073d2fff
|
Added Xerces
Former-commit-id: 9e5eeb3b86
|
9 years ago |
|
sjunges
|
288f34b083
|
Added Xerces
Former-commit-id: 42a3347ab6
|
9 years ago |
|
dehnert
|
8574d474a4
|
added support for computation of bottom states. not yet done
Former-commit-id: 49c2a28b28
|
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
|
6c804732e1
|
introduced (probably buggy) versions of existsAbstractRepresentative on BDDs and prob0 for games
Former-commit-id: 5e7225fe29
|
9 years ago |
|
dehnert
|
0cfc4dfd4d
|
(re)introduced min/maxAbstractRepresentative for ADDs
Former-commit-id: 5a5d269339
|
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
|
88bcd7d74c
|
deadlock states now get fixed in abstract game
Former-commit-id: efaa5d007e
|
9 years ago |
|
dehnert
|
7f767993c6
|
Merge branch 'future' into menu_games
Former-commit-id: 5757903efe
|
9 years ago |
|
dehnert
|
a8f89c3875
|
fixed cmake file
Former-commit-id: a62e21ef52
|
9 years ago |
|
dehnert
|
f1d9e65db7
|
Merge branch 'future' into menu_games
Former-commit-id: deff6eb8d0
|
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
|
75632f932d
|
added state-set abstractor as a means to, e.g., derive the initial states BDD
Former-commit-id: 34257c7196
|
9 years ago |
|
dehnert
|
97c90d5437
|
added correct insertion of probabilities into BDD and reachability analysis
Former-commit-id: 51e91d4d64
|
9 years ago |
|
dehnert
|
c6f1cb40d3
|
more work on games
Former-commit-id: d89f025da4
|
9 years ago |
|
dehnert
|
3bc629561e
|
Merge branch 'future' into menu_games
Former-commit-id: 4c9ddacf52
|
9 years ago |
|
dehnert
|
50296571f5
|
Merge branch 'master' into future
Former-commit-id: 1a3d651953
|
9 years ago |
|
dehnert
|
deec423f27
|
fixed infinite recursion in constants comparator
Former-commit-id: b36b352d36
|
9 years ago |
|
dehnert
|
1198951c3e
|
more work on game abstraction of PRISM programs
Former-commit-id: b5bec829e2
|
9 years ago |
TimQu
|
adc5c8d1c1
|
Fixed another memory leak: CheckResults have not been destructed properly.
Former-commit-id: 5631c101bb
|
9 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
|
9 years ago |
|
dehnert
|
b28f36bb34
|
work on game-based abstraction
Former-commit-id: 4635199f84
|
9 years ago |
