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
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
437e883bcf
first fixes after merge
Former-commit-id: f19347885d
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
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
Mavo
566cef0f91
Started on compiling without Carl
Former-commit-id: 5e0895d7c5
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
sjunges
9398cfa54a
gcc pendantic warning switched off
Former-commit-id: c5b389f737
9 years ago
TimQu
c672f7aea2
fix in bounded reachability computation with Markov automata
Former-commit-id: fe2b399778
9 years ago
sjunges
380bed563c
updated the jani parser to actually buidl models
Former-commit-id: d0189e33e5
[formerly 4910b31ca3
]
Former-commit-id: cd7f6ca5cb
9 years ago
hbruintjes
8ef899ef1c
Fix log file name argument
Former-commit-id: c13b4ca3ad
9 years ago
hbruintjes
efae19b092
Use toString() for exit rates, ADL not working for some reason
Former-commit-id: cbc9eaf722
9 years ago
hbruintjes
4e4bc255b5
Fix some typos in l3pp usage
Former-commit-id: c9da06a596
9 years ago
hbruintjes
d9cb1a79f8
Replace cout macros with l3pp
Former-commit-id: 0cde42558d
9 years ago
sjunges
88af02e723
towards new jani version
Former-commit-id: 0c5e6825ca
[formerly b98985e8eb
]
Former-commit-id: 9f5ef53aec
9 years ago
sjunges
4f1b8f12f0
Extra method
Former-commit-id: 44b165558d
9 years ago
sjunges
eff2acdbc6
parser update
Former-commit-id: 9a21a09597
9 years ago
TimQu
d02c918f6a
forgot a little something...
Former-commit-id: dc5b68bdb6
9 years ago
hbruintjes
ebe6775b27
Fix missing ValueType template arguments (which defaulted to double)
Former-commit-id: a97910eaf9
9 years ago
PBerger
67244869db
src/storage/BitVector: Replaced constant 1 unsigned long long with cast to decltype. This fixes a template resolvation error in std::max.
src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp: Replaced "auto state = 0" with decltype declaration. This solves an issue where state is always signed, but should be unsigned.
src/storage/dft/DFTBuilder.cpp: Added a static_cast to enforce proper conversion to size_t and silence the signed/unsigned comparison warning.
Former-commit-id: 7a1a4c1f45
9 years ago