dehnert
241f23f730
fixed bug in abstraction information object
Former-commit-id: 1338ecfa47
8 years ago
PBerger
be7353358f
Added Test for constants in Cudd/Sylvan.
Added functionality for existsAbstractRepresentative in Sylvan. Still very broken!
Former-commit-id: df2b36a8d8
8 years ago
dehnert
f7f14f13fc
minor fix before bedtime
Former-commit-id: c558c23122
8 years ago
dehnert
9e64e998f3
fixed tests wrt. proper bottom state computation
Former-commit-id: 223795c955
8 years ago
dehnert
e2ba3f3725
bottom states appear to be working, tests not yet adapted
Former-commit-id: 801d99c128
8 years ago
dehnert
3bc0b4eacc
more work on proper bottom state computation
Former-commit-id: 38718e1c5c
8 years ago
dehnert
7ab88457a7
corrected reference to wrong settings module
Former-commit-id: 2f35b2dc82
8 years ago
dehnert
e43dfc2784
removed unused setting
Former-commit-id: 18a91c2acb
8 years ago
sjunges
fa9e33da59
option for print timings
Former-commit-id: 845ce83bda
8 years ago
dehnert
4f54759f38
intermediate commit [fixing bottom states/transitions]
Former-commit-id: d457ce2fb4
8 years ago
dehnert
1280c88b4f
renamed prob branching variables to aux variables in preparation for proper bottom state creation in game abstraction
Former-commit-id: e855b14b46
8 years ago
dehnert
b3e77730a9
added uniqueness mechanism in flattenModules to compensate for missing uniqueness in allsat of solvers
Former-commit-id: b4ebd17f68
8 years ago
PBerger
4fff7b39ef
Added template instanziation for storm::RationalFunction.
Added a test for Prism AbstractPrograms with storm::RationalFunction.
Former-commit-id: 5a696149cb
8 years ago
dehnert
4f7eaa0a43
some more work towards abstraction refinement
Former-commit-id: 360cb016c3
8 years ago
sjunges
ba81925c1d
renamed smt2smtsolver to smtlibsmtsolver and cleaned make files
Former-commit-id: 78c74dc9a5
8 years ago
sjunges
46ee949cd4
auto-create source groups
Former-commit-id: 8772c5498f
8 years ago
dehnert
aca21eaf18
commit to switch workplace (no, not now)
Former-commit-id: b725946b28
8 years ago
sjunges
434f1a4903
obtain scheduler from value iteration
Former-commit-id: ef976fbd6e
8 years ago
sjunges
507952df4e
register smt2lib settings
Former-commit-id: 4da50b02bf
8 years ago
sjunges
b6465020a2
towards working tests in pla
Former-commit-id: 3542f8a1d0
8 years ago
dehnert
2d05555967
added abstraction settings and menu game abstractor
Former-commit-id: 4cac25ac94
8 years ago
dehnert
28d2471d4d
started on menu game abstractor interface
Former-commit-id: 73ca717aec
8 years ago
dehnert
7df822967c
all abstraction tests working again
Former-commit-id: 9de7beb2b6
8 years ago
PBerger
428d21cdee
Made code compile with GCC:
- Added cstdint for uint_fast64_t where necessary.
- Moved and/or replaced includes for Expression headers, since std::pair required the concrete implementation and not only the stub.
- Added newlines at the end of .cpp files.
Former-commit-id: 72b57ce513
8 years ago
PBerger
1d3bb3010d
Fixed merge mistake in InternalSylvanDdManager.cpp
Former-commit-id: 5919f2402e
8 years ago
dehnert
7a4d3740de
some more work, not fully working again (yet)
Former-commit-id: 32c8c6eb7e
8 years ago
dehnert
c1953cda46
started refactoring of abstraction
Former-commit-id: 72d9fc9fab
8 years ago
sjunges
b243057884
fix in eliminateAll
Former-commit-id: 93f753d148
8 years ago
sjunges
04cb930bda
removed copied debug output at a silly place
Former-commit-id: 27946240f5
8 years ago
sjunges
4e0f4e8e5a
add region settings
Former-commit-id: 7f2680e126
8 years ago
sjunges
0ef2b55c75
made some region settings attribute to the model checker instead of global
Former-commit-id: e53ca96760
8 years ago
sjunges
548ba8bbeb
somehow managed my way through the policy guessing, several minor extensions to solvers
Former-commit-id: c4bb6453e7
8 years ago
sjunges
051ad702a7
solvers updated, constants updated
Former-commit-id: 011251c695
8 years ago
dehnert
b67e3d6e7b
added 'convergence' (rather success) checks for Eigen solver
Former-commit-id: 25a6fb1d77
8 years ago
sjunges
b826ac92ac
updated setting modules to new interface
Former-commit-id: 2616fa8884
8 years ago
sjunges
a5c09fa801
extended eliminator interface, merged model checking part
Former-commit-id: 5e0028c937
8 years ago
sjunges
ee4cb38d43
lra into multivalueeliminator
Former-commit-id: 981aebe161
8 years ago
sjunges
31228486d3
towards merging, including a extension on the pstateeliminator, come back after generalizing the lra eliminator
Former-commit-id: 8ce98b8287
8 years ago
dehnert
723999f885
intermediate work-place switch commit
Former-commit-id: 818179d286
8 years ago
dehnert
18b0f07581
tweaked Bdd toExpression a bit to be more versatile
Former-commit-id: 858948f1b7
8 years ago
dehnert
52577e2740
added game abstraction tests for sylvan and made them work (in particular implemented toExpression for sylvan BDDs)
Former-commit-id: 8fdc34cb55
8 years ago
sjunges
444318e624
refactoring up to tests done
Former-commit-id: 943a396fab
8 years ago
dehnert
20eb0a6e0c
made value type in game abstraction more generic
Former-commit-id: 40286a5a4e
8 years ago
sjunges
f7a3e02fb6
refactored model checkers st all are templated in the model, have to handle rational function bounds next
Former-commit-id: b665709a52
8 years ago
dehnert
1944b947d3
modified formula parser to parse expressions as operator bounds and then convert them to rationals
Former-commit-id: ebf441c406
8 years ago
sjunges
cf583ec9dd
formulae with rational number bounds
Former-commit-id: 17755ccf84
8 years ago
sjunges
e4b3f4eeb9
intermediate commit, come back after refactoring formulae
Former-commit-id: 147133876f
8 years ago
dehnert
53f83c9214
moved menu-game abstraction to separate folder and made everything compile again
Former-commit-id: a833ca1152
8 years ago
sjunges
8b5a2d4354
intermediate commit, come back after refactoring model checkers
Former-commit-id: 8cfb79b2d5
8 years ago
PBerger
58eb54926c
Fixed Sylvan bugs.
Added a lot of debugging options and output, controlled by #define's.
Added more template specializations for storm::RationalFunction.
Former-commit-id: 416c32d196
8 years ago