sjunges
cf583ec9dd
formulae with rational number bounds
Former-commit-id: 17755ccf84
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
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
4f1b8f12f0
Extra method
Former-commit-id: 44b165558d
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
TimQu
f2035523af
Fixed a bug in rewardModel's reduceToStateBasedRewards. Also added a function to check whether all rewards are zero.
Former-commit-id: 4dabd07c66
9 years ago
hbruintjes
8546786e17
Fix missing template argument in builder utility
Former-commit-id: 23d683f29c
9 years ago
TimQu
12287e5090
small fix for building MAs
Also fixed a test for explicit MA parsing, where the transitions of a probabilistic choice did not sum up to one
Former-commit-id: c2f920a4d6
9 years ago
hbruintjes
ffe325b196
Fix unitialized data in coresettings
Former-commit-id: 7c0dac26ba
9 years ago
hbruintjes
a2140141a3
Fix virtual destructor
Former-commit-id: ff3ee6cafa
9 years ago
hbruintjes
556b8e8726
Return reference to settings module, not a copy
Former-commit-id: 0a5befee57
9 years ago
TimQu
f681206393
building markov automata from prism code
Former-commit-id: 791c49c7cf
9 years ago
dehnert
83c4b1647c
solvers now can allocated auxiliary memory
Former-commit-id: 76dc1a1679
9 years ago
dehnert
be5fdeb636
started working on internal auxiliary storage of solvers
Former-commit-id: d895041c50
9 years ago
TimQu
cf299a6344
fixed the case where an expression occurred twice in the formulas
Former-commit-id: 5054ebcae4
9 years ago
dehnert
95b95d9c64
fixed some minor issues and renamed equation solver methods slightly to make the names a bit more compact
Former-commit-id: de103e19ad
9 years ago
dehnert
b1f2c26df0
made all instantiations to call MDP model checking with rational numbers
Former-commit-id: d3f8df7804
9 years ago
dehnert
d27c75c3d8
fixed missing virtual keyword
Former-commit-id: 1aa26ab679
9 years ago
dehnert
61a8b9bb29
more work on solvers
Former-commit-id: 14fad8ac36
9 years ago
dehnert
9ab33528b4
started to fill value iteration implementation in new general min-max solver
Former-commit-id: e54cb8a0f9
9 years ago
dehnert
b4e0cabef6
started working on general min-max solver that uses an underlying linear equation solver. provided necessary factories. adapted code and removed old min-max solvers
Former-commit-id: c1895472c7
9 years ago
dehnert
248b257f20
enabled rationals/rational functions in CTMC model checker
Former-commit-id: dc15cd6020
9 years ago
dehnert
d661454179
started working on instantiating CTMC model checker to rational numbers
Former-commit-id: 3923c9a7e4
9 years ago
dehnert
8153306ced
fixed wrong call to Eigen's iterative solvers
Former-commit-id: 0e2e836729
9 years ago
dehnert
46ce68743c
enabled precision/max iterations for eigen solver
Former-commit-id: 370a78a02f
9 years ago
dehnert
2a7dc0fad0
renamed MarkovChainSettings
Former-commit-id: 39024731f8
9 years ago
dehnert
5616004e6e
remove debug output
Former-commit-id: 0ae7597785
9 years ago
dehnert
07c787b49d
added unsupported solvers of eigen
Former-commit-id: e11b335c2d
9 years ago
dehnert
d24fb0cf9a
avoid temporary in Eigen solver by providing .noalias(). slightly rewrote matrix-vector expression to benefit more from Eigen's optimization capabilities
Former-commit-id: 838eac1449
9 years ago
dehnert
69da4ff147
fixed some more problems with Eigen solver
Former-commit-id: c6ed18c4ab
9 years ago
dehnert
f46bcd31c5
fixed typo
Former-commit-id: 0e6ab55389
9 years ago
dehnert
ba43e23984
using maps for Eigen solver instead of copies of the vectors
Former-commit-id: d53075ab36
9 years ago
dehnert
711d5cfa12
fixed bug in sparse dtmc elimination model checker. commented out weird eliminaton functions in CTMC model checker and storm.h
Former-commit-id: 3000123a3d
9 years ago
dehnert
49f59052f8
made model checkers give up possession of matrix to solver when possible
Former-commit-id: 8d689470bd
9 years ago
dehnert
00d331ebb4
moved linear equation solver factories to the respective solver files (and away from utility). restructured settings in factories and the way they are forwarded to the linear equation solvers. fixed all resulting errors
Former-commit-id: 27e1ae2466
9 years ago
Mavo
e443384b91
Added assertion
Former-commit-id: beeff9bff9
9 years ago
dehnert
b30db17f8c
added rvalue reference overload to all linear equation solver factories
Former-commit-id: 2d09211d19
9 years ago