dehnert
b3e77730a9
added uniqueness mechanism in flattenModules to compensate for missing uniqueness in allsat of solvers
Former-commit-id: b4ebd17f68
9 years ago
sjunges
6e64631839
initial value support for booleans, some extra error messages)
Former-commit-id: bb857b0923
[formerly 80b90ed08e
]
Former-commit-id: d529e6b9d2
9 years ago
sjunges
890634ba77
initial value support (bounded integers only)
Former-commit-id: 8930f3233e
[formerly 1a0222dc3c
]
Former-commit-id: 9ccfff2190
9 years ago
PBerger
a1f8382af6
Merge remote-tracking branch 'remotes/origin/menu_games' into sylvanRationalFunctions
# Conflicts:
# test/functional/storage/PrismProgramTest.cpp
Former-commit-id: d7802745d9
9 years ago
dehnert
b14f866e01
added more flatten tests
Former-commit-id: 7e35a90c88
9 years ago
dehnert
3e9f9552b1
fixed tests: using shared_ptr instead of unique_ptr for SMT solver factory in abstraction
Former-commit-id: 6159a20565
9 years ago
PBerger
81311690ab
Fixed errors because of changed API.
Former-commit-id: 7f771dc576
9 years ago
PBerger
2de905fd5f
Merge remote-tracking branch 'remotes/origin/menu_games' into sylvanRationalFunctions
# Conflicts:
# src/abstraction/MenuGameAbstractor.cpp
# src/abstraction/prism/AbstractCommand.cpp
Former-commit-id: 032244f923
9 years ago
PBerger
4fff7b39ef
Added template instanziation for storm::RationalFunction.
Added a test for Prism AbstractPrograms with storm::RationalFunction.
Former-commit-id: 5a696149cb
9 years ago
dehnert
4f7eaa0a43
some more work towards abstraction refinement
Former-commit-id: 360cb016c3
9 years ago
sjunges
cb4e821e7f
give an error message if a distribution occurs in an expression
Former-commit-id: 533bfe34bb
[formerly 09d6896e9c
]
Former-commit-id: a1fa9e7ced
9 years ago
sjunges
d12eccb3f9
Merge branch 'future' into jani_support
Former-commit-id: a62a04e844
[formerly e0b922ea93
]
Former-commit-id: 672c1644fa
9 years ago
sjunges
2a1c317363
removed debug output from cmake
Former-commit-id: f443a42ba9
9 years ago
sjunges
0b160b6650
Merge branch 'future' into jani_support
Former-commit-id: f4b64c62b1
[formerly 894ea5326c
]
Former-commit-id: adae001c60
9 years ago
sjunges
ba81925c1d
renamed smt2smtsolver to smtlibsmtsolver and cleaned make files
Former-commit-id: 78c74dc9a5
9 years ago
sjunges
9d3ffe2792
Merge branch 'future' into merge-pla
Former-commit-id: 5a4019d573
9 years ago
sjunges
19bf801456
Fixed MDP tests
Former-commit-id: 058bcbc4c6
9 years ago
sjunges
46ee949cd4
auto-create source groups
Former-commit-id: 8772c5498f
9 years ago
dehnert
aca21eaf18
commit to switch workplace (no, not now)
Former-commit-id: b725946b28
9 years ago
sjunges
d97b0b2897
cleaned tests
Former-commit-id: 8d376e3c75
9 years ago
sjunges
434f1a4903
obtain scheduler from value iteration
Former-commit-id: ef976fbd6e
9 years ago
sjunges
507952df4e
register smt2lib settings
Former-commit-id: 4da50b02bf
9 years ago
sjunges
b6465020a2
towards working tests in pla
Former-commit-id: 3542f8a1d0
9 years ago
dehnert
2d05555967
added abstraction settings and menu game abstractor
Former-commit-id: 4cac25ac94
9 years ago
dehnert
28d2471d4d
started on menu game abstractor interface
Former-commit-id: 73ca717aec
9 years ago
PBerger
595d9b4293
Merge branch 'menu_games' of https://sselab.de/lab9/private/git/storm into sylvanRationalFunctions
# Conflicts:
# src/abstraction/AbstractionDdInformation.cpp
# src/abstraction/AbstractionDdInformation.h
# src/abstraction/AbstractionExpressionInformation.cpp
# src/abstraction/AbstractionExpressionInformation.h
# src/abstraction/AbstractionInformation.cpp
Former-commit-id: 9def06e790
9 years ago
dehnert
7df822967c
all abstraction tests working again
Former-commit-id: 9de7beb2b6
9 years ago
sjunges
0a1cbb57f0
towards initial value support
Former-commit-id: 32e31b7834
[formerly dced3cef8b
]
Former-commit-id: f7570bff74
9 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
9 years ago
PBerger
1d3bb3010d
Fixed merge mistake in InternalSylvanDdManager.cpp
Former-commit-id: 5919f2402e
9 years ago
dehnert
7a4d3740de
some more work, not fully working again (yet)
Former-commit-id: 32c8c6eb7e
9 years ago
PBerger
6873bd7d17
Merge remote-tracking branch 'remotes/origin/menu_games' into sylvanRationalFunctions
# Conflicts:
# src/storage/dd/sylvan/InternalSylvanDdManager.cpp
# src/storage/dd/sylvan/InternalSylvanDdManager.h
# test/functional/storage/SylvanDdTest.cpp
Former-commit-id: 00e08e2014
9 years ago
dehnert
c1953cda46
started refactoring of abstraction
Former-commit-id: 72d9fc9fab
9 years ago
PBerger
0717ffe053
Added AND_EXISTS to sylvan+RationalFunction
Former-commit-id: 7b462145cf
9 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
9 years ago
sjunges
10419d4bba
improved error message for unsupported operations
Former-commit-id: a5bba8670d
[formerly 81693f6d7c
]
Former-commit-id: c4c197d0ee
9 years ago
sjunges
e8d5caa78d
added support for implies
Former-commit-id: 0a4b510b74
[formerly 32a59d85f9
]
Former-commit-id: 1582f84bf1
9 years ago
sjunges
1dcec6471f
add support for transient var
Former-commit-id: 7898f2b084
[formerly af4af4d291
]
Former-commit-id: 9ae9361e76
9 years ago
sjunges
ba1f6bf3d5
jani property stub
Former-commit-id: 37f8f63d43
[formerly 54bc32bfd0
]
Former-commit-id: e934d063fd
9 years ago
ThomasH
4fc8543354
add test routine for checking validity of gspns
Former-commit-id: 165747c9c8
9 years ago
sjunges
91a3b0c5bc
Merge branch 'future' into jani_support
Former-commit-id: 5e82a2c226
[formerly 6accd0d2c0
]
Former-commit-id: 729d575993
9 years ago
ThomasH
088aabb293
remove debug code
Former-commit-id: c351df36f1
9 years ago
ThomasH
38a7502fe9
Merge branch 'gspn' of https://sselab.de/lab9/private/git/storm into gspn
Former-commit-id: 71d8f4caca
9 years ago
ThomasH
b9297fa513
fix bug
Former-commit-id: 6f2bb74491
9 years ago
ThomasH
35f8d124a1
add more comments
Former-commit-id: 071f85c2ca
9 years ago
ThomasH
3854feae87
add priorities to the parser and an example
Former-commit-id: 1b072a730e
9 years ago
sjunges
2637d51afc
set formula
Former-commit-id: e5d9a4ca30
9 years ago
sjunges
b243057884
fix in eliminateAll
Former-commit-id: 93f753d148
9 years ago
sjunges
04cb930bda
removed copied debug output at a silly place
Former-commit-id: 27946240f5
9 years ago
sjunges
4e0f4e8e5a
add region settings
Former-commit-id: 7f2680e126
9 years ago