PBerger
1d3bb3010d
Fixed merge mistake in InternalSylvanDdManager.cpp
Former-commit-id: 5919f2402e
10 years ago
dehnert
7a4d3740de
some more work, not fully working again (yet)
Former-commit-id: 32c8c6eb7e
10 years ago
dehnert
c1953cda46
started refactoring of abstraction
Former-commit-id: 72d9fc9fab
10 years ago
sjunges
23122816ef
parse support for all model types (mostly allows better error messages)
Former-commit-id: cd30340c85 [formerly b824493aca ]
Former-commit-id: 292217d026
10 years ago
sjunges
10419d4bba
improved error message for unsupported operations
Former-commit-id: a5bba8670d [formerly 81693f6d7c ]
Former-commit-id: c4c197d0ee
10 years ago
sjunges
e8d5caa78d
added support for implies
Former-commit-id: 0a4b510b74 [formerly 32a59d85f9 ]
Former-commit-id: 1582f84bf1
10 years ago
sjunges
1dcec6471f
add support for transient var
Former-commit-id: 7898f2b084 [formerly af4af4d291 ]
Former-commit-id: 9ae9361e76
10 years ago
sjunges
ba1f6bf3d5
jani property stub
Former-commit-id: 37f8f63d43 [formerly 54bc32bfd0 ]
Former-commit-id: e934d063fd
10 years ago
ThomasH
4fc8543354
add test routine for checking validity of gspns
Former-commit-id: 165747c9c8
10 years ago
ThomasH
088aabb293
remove debug code
Former-commit-id: c351df36f1
10 years ago
ThomasH
b9297fa513
fix bug
Former-commit-id: 6f2bb74491
10 years ago
ThomasH
35f8d124a1
add more comments
Former-commit-id: 071f85c2ca
10 years ago
ThomasH
3854feae87
add priorities to the parser and an example
Former-commit-id: 1b072a730e
10 years ago
sjunges
b243057884
fix in eliminateAll
Former-commit-id: 93f753d148
10 years ago
sjunges
04cb930bda
removed copied debug output at a silly place
Former-commit-id: 27946240f5
10 years ago
sjunges
4e0f4e8e5a
add region settings
Former-commit-id: 7f2680e126
10 years ago
sjunges
0ef2b55c75
made some region settings attribute to the model checker instead of global
Former-commit-id: e53ca96760
10 years ago
sjunges
548ba8bbeb
somehow managed my way through the policy guessing, several minor extensions to solvers
Former-commit-id: c4bb6453e7
10 years ago
sjunges
051ad702a7
solvers updated, constants updated
Former-commit-id: 011251c695
10 years ago
dehnert
b67e3d6e7b
added 'convergence' (rather success) checks for Eigen solver
Former-commit-id: 25a6fb1d77
10 years ago
sjunges
b826ac92ac
updated setting modules to new interface
Former-commit-id: 2616fa8884
10 years ago
sjunges
a5c09fa801
extended eliminator interface, merged model checking part
Former-commit-id: 5e0028c937
10 years ago
sjunges
ee4cb38d43
lra into multivalueeliminator
Former-commit-id: 981aebe161
10 years ago
sjunges
31228486d3
towards merging, including a extension on the pstateeliminator, come back after generalizing the lra eliminator
Former-commit-id: 8ce98b8287
10 years ago
dehnert
723999f885
intermediate work-place switch commit
Former-commit-id: 818179d286
10 years ago
dehnert
18b0f07581
tweaked Bdd toExpression a bit to be more versatile
Former-commit-id: 858948f1b7
10 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
10 years ago
sjunges
444318e624
refactoring up to tests done
Former-commit-id: 943a396fab
10 years ago
dehnert
20eb0a6e0c
made value type in game abstraction more generic
Former-commit-id: 40286a5a4e
10 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
10 years ago
dehnert
1944b947d3
modified formula parser to parse expressions as operator bounds and then convert them to rationals
Former-commit-id: ebf441c406
10 years ago
sjunges
cf583ec9dd
formulae with rational number bounds
Former-commit-id: 17755ccf84
10 years ago
sjunges
e4b3f4eeb9
intermediate commit, come back after refactoring formulae
Former-commit-id: 147133876f
10 years ago
dehnert
53f83c9214
moved menu-game abstraction to separate folder and made everything compile again
Former-commit-id: a833ca1152
10 years ago
sjunges
8b5a2d4354
intermediate commit, come back after refactoring model checkers
Former-commit-id: 8cfb79b2d5
10 years ago
sjunges
4b20a724dc
weight zero is no weight is now more explicit
Former-commit-id: e7494eb7bd
10 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
10 years ago
sjunges
437e883bcf
first fixes after merge
Former-commit-id: f19347885d
10 years ago
dehnert
4733643bcf
made the games compile again
Former-commit-id: 35f3ab9471
10 years ago
Mavo
5530f908ca
Fixed compile issues under Linux
Former-commit-id: 61a69f9fc7
10 years ago
dehnert
510e525274
removed unnecessary define for boost::variant problem
Former-commit-id: 9c64abbbda
10 years ago
dehnert
cc958bedf0
fixed wrong usage of boost::variant in NextStateGenerator
Former-commit-id: 0ba0e8d565
10 years ago
TimQu
0760e2a7f9
tiny MA example, small fix and test cases for MAs
Former-commit-id: 9fe2b7cc76
10 years ago
PBerger
dbbae87962
Fixed template specialization.
Re-Implemented terminal generation.
Former-commit-id: 253f95b673
10 years ago
PBerger
b01abf831b
Fixing template spec.
Former-commit-id: bc121341e3
10 years ago
PBerger
cdff7d4b0f
Added template specialization for getIdentity.
Former-commit-id: 082b985333
10 years ago
PBerger
1345f018fc
Fixed some issues with pointers.
Former-commit-id: a7fddc12f3
10 years ago
PBerger
9e90f41608
Implemented functions for BDD -> ADD conversion and some helpers.
Former-commit-id: 78c9003366
10 years ago
sjunges
16c1dab062
sylvan dependency duplicate removed
Former-commit-id: 39b9cc5e6e
10 years ago
sjunges
7938ce448e
trying to fix boost variant by adding a define
Former-commit-id: 91c98c91a0
10 years ago