sjunges
|
13d45118af
|
initial value support unbounded integers, some extra error messages)
Former-commit-id: 72a35269f3 [formerly 243d50b5af ]
Former-commit-id: 9c7e2bd9eb
|
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 |
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
|
ba81925c1d
|
renamed smt2smtsolver to smtlibsmtsolver and cleaned make files
Former-commit-id: 78c74dc9a5
|
9 years ago |
sjunges
|
46ee949cd4
|
auto-create source groups
Former-commit-id: 8772c5498f
|
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 |
sjunges
|
0a1cbb57f0
|
towards initial value support
Former-commit-id: 32e31b7834 [formerly dced3cef8b ]
Former-commit-id: f7570bff74
|
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 |
ThomasH
|
088aabb293
|
remove debug code
Former-commit-id: c351df36f1
|
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
|
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 |
sjunges
|
0ef2b55c75
|
made some region settings attribute to the model checker instead of global
Former-commit-id: e53ca96760
|
9 years ago |
sjunges
|
548ba8bbeb
|
somehow managed my way through the policy guessing, several minor extensions to solvers
Former-commit-id: c4bb6453e7
|
9 years ago |
sjunges
|
051ad702a7
|
solvers updated, constants updated
Former-commit-id: 011251c695
|
9 years ago |
dehnert
|
b67e3d6e7b
|
added 'convergence' (rather success) checks for Eigen solver
Former-commit-id: 25a6fb1d77
|
9 years ago |
sjunges
|
b826ac92ac
|
updated setting modules to new interface
Former-commit-id: 2616fa8884
|
9 years ago |
sjunges
|
a5c09fa801
|
extended eliminator interface, merged model checking part
Former-commit-id: 5e0028c937
|
9 years ago |
sjunges
|
ee4cb38d43
|
lra into multivalueeliminator
Former-commit-id: 981aebe161
|
9 years ago |
sjunges
|
31228486d3
|
towards merging, including a extension on the pstateeliminator, come back after generalizing the lra eliminator
Former-commit-id: 8ce98b8287
|
9 years ago |
sjunges
|
444318e624
|
refactoring up to tests done
Former-commit-id: 943a396fab
|
9 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
|
9 years ago |
dehnert
|
1944b947d3
|
modified formula parser to parse expressions as operator bounds and then convert them to rationals
Former-commit-id: ebf441c406
|
9 years ago |
sjunges
|
cf583ec9dd
|
formulae with rational number bounds
Former-commit-id: 17755ccf84
|
9 years ago |
sjunges
|
e4b3f4eeb9
|
intermediate commit, come back after refactoring formulae
Former-commit-id: 147133876f
|
9 years ago |
sjunges
|
8b5a2d4354
|
intermediate commit, come back after refactoring model checkers
Former-commit-id: 8cfb79b2d5
|
9 years ago |
sjunges
|
4b20a724dc
|
weight zero is no weight is now more explicit
Former-commit-id: e7494eb7bd
|
9 years ago |
sjunges
|
437e883bcf
|
first fixes after merge
Former-commit-id: f19347885d
|
9 years ago |
Mavo
|
5530f908ca
|
Fixed compile issues under Linux
Former-commit-id: 61a69f9fc7
|
9 years ago |
dehnert
|
510e525274
|
removed unnecessary define for boost::variant problem
Former-commit-id: 9c64abbbda
|
9 years ago |
dehnert
|
cc958bedf0
|
fixed wrong usage of boost::variant in NextStateGenerator
Former-commit-id: 0ba0e8d565
|
9 years ago |
TimQu
|
0760e2a7f9
|
tiny MA example, small fix and test cases for MAs
Former-commit-id: 9fe2b7cc76
|
9 years ago |
sjunges
|
16c1dab062
|
sylvan dependency duplicate removed
Former-commit-id: 39b9cc5e6e
|
9 years ago |
sjunges
|
7938ce448e
|
trying to fix boost variant by adding a define
Former-commit-id: 91c98c91a0
|
9 years ago |
sjunges
|
dc5d9637f5
|
storm-gspn added as target
Former-commit-id: 0ace6ec9a9
|
9 years ago |
Mavo
|
566cef0f91
|
Started on compiling without Carl
Former-commit-id: 5e0895d7c5
|
9 years ago |
sjunges
|
cfd6926add
|
a bit of progress
Former-commit-id: bbbb7ff21b
|
9 years ago |
sjunges
|
85f29ee744
|
Typo in diagnostic ignored fixed
Former-commit-id: 51559c8982
|
9 years ago |
sjunges
|
c9593b9e98
|
trying to fix the boost variant stuff differently
Former-commit-id: a1fb8efece
|
9 years ago |