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
dehnert
15a4d4757f
added feature to linear equation solver factories to take posession of the matrix to forward it to the solvers
Former-commit-id: ed183f1820
9 years ago
PBerger
b99a063cce
Replaced calls to std::abs with calls to std::fabs and included cmath.
Former-commit-id: 40fb587e2f
9 years ago
dehnert
40a7948540
started generalizing elimination to equation system solving
Former-commit-id: aabe89b65f
9 years ago
dehnert
3ba5902821
removed debug output and fixed small bug in adaptation of Eigen
Former-commit-id: 5e1a70d933
9 years ago
dehnert
13f8f21a70
upgrade to eigen 3.3 and made modifications for different value types via template specializations
Former-commit-id: 8ea9d1e0c4
9 years ago
TimQu
ad31b2d769
Extended test a little
Former-commit-id: 5e983ae6fb
9 years ago
dehnert
99b9f11d49
removed eigen-3.2.6
Former-commit-id: 74fc9f0dbe
9 years ago
dehnert
852afd1718
fixed crowds models to work with exact arithmetic. fixed dynamic state priority queue implementation. added setting to use dedicated elimination-based model checker instead of regular model checker (+ elimination solver)
Former-commit-id: 1b0802ff05
9 years ago
dehnert
82d4164c39
added obeying a state ordering to elimination linear equation solver
Former-commit-id: 5a62842963
9 years ago
dehnert
a699272dc6
renamed storm::Variable to storm::RationalFunctionVariable to avoid confusion with storm::expressions::Variable. fixed some Eigen tests
Former-commit-id: 62c70330c2
9 years ago
TimQu
9939341c9d
Another test
Former-commit-id: 76b9c0ebbb
9 years ago
TimQu
3cd198c5e3
Some tests, correct handling of results obtained in preprocessing, fixes
Former-commit-id: e7eb1f67cb
9 years ago
dehnert
f3fa90cc37
more work towards exact solving
Former-commit-id: 38edbcf2ca
9 years ago
PBerger
be9648fc18
Added -fPIC to Sylvan. Since it is linked into Storm it is necessary for relocation to be possible, hence PIC.
Added includes for cmath at various points. This is a default include on Mac OS but not on any sane systems.
Changed calls to std::abs to std::fabs to resolve ambigious call errors.
Former-commit-id: 4d3da21bce
9 years ago
dehnert
d3de111b3b
more work to enable storm to use rational arithmetic
Former-commit-id: 72933b5184
9 years ago
dehnert
af35a4c3ed
Merge branch 'jani_support' into exact_solver
Former-commit-id: 63cf5c5117
9 years ago
dehnert
3bb36997a1
minor bugfix
Former-commit-id: 409e84e8f5
9 years ago
dehnert
8f12b3b8c4
added option 'exact' (in addition to parametric)
Former-commit-id: ccc026a44d
9 years ago
TimQu
ce9a6b415c
Added tests for some of the benchmarks
Former-commit-id: 816f33faf8
9 years ago
TimQu
a02e0eedf7
moved files around
Former-commit-id: 77b89a7e3e
9 years ago
TimQu
cb9cf68632
output of runtime of mec decomposition
Former-commit-id: 5238f9a7ad
9 years ago
TimQu
8bb25234a3
fixed prism model code (formula used before definition)
Former-commit-id: d610960b0e
9 years ago
TimQu
4a4a9ad954
fixed/improved the qualitative checks
Former-commit-id: 5e889a0d95
9 years ago
Mavo
dcf5468b29
Fixed linker error with static function
Former-commit-id: 95e220763d
9 years ago
Mavo
17ba53dafa
Division by Interval not supported
Former-commit-id: 86b2f555c9
9 years ago
TimQu
18623f304b
some benchmarks
Former-commit-id: 3f3e9306fe
9 years ago
dehnert
2096c54b84
more explicit instantiations for rational function and some more tests for eigen solver
Former-commit-id: b97e838b22
9 years ago
dehnert
4e14ecb869
made elimination-based linear solver work in an alpha version. changed minor things in Eigen's SparseLU implementation to make it work with rational numbers and rational functions
Former-commit-id: e5622bd981
9 years ago
TimQu
cf648b5bf1
output of runtimes and other statistics
Former-commit-id: 3eaf89f5d5
9 years ago
TimQu
19fa7767a0
scheduler retrival for value iteration of native minMaxLinEqSolver
Former-commit-id: 641991da86
9 years ago
TimQu
b58c9d67b9
step bounded objectives
Former-commit-id: 067f4b8dae
9 years ago
TimQu
18c1fc3b3f
removed debug output
Former-commit-id: 575700421c
9 years ago
TimQu
2fed3b647c
scheduler benchmark now considers expected reachability reward (total reward was infinite).
Bugfix.
Former-commit-id: f53d19194c
9 years ago
TimQu
5604733854
improvements for preprocessing regarding finite/infinite rewards
Former-commit-id: a57e979bdd
9 years ago
dehnert
35bb3a3c26
renamed elimination settings
Former-commit-id: 5155d0a465
9 years ago
dehnert
8ce9e56af8
some refactoring of state-elimination-related things
Former-commit-id: c51fd9c47c
9 years ago
dehnert
ec640c12b7
minor fixes to Eigen adapter
Former-commit-id: 9095bbc9d4
9 years ago
dehnert
a17cffbbe3
added missing switch case for new eigen solver
Former-commit-id: fbbb6e5828
9 years ago
dehnert
023325b53d
added tests for Eigen solver
Former-commit-id: ede9efcee2
9 years ago
dehnert
002bd58b2d
added shipped version of Eigen to CMakeList
Former-commit-id: b262c2023e
9 years ago
dehnert
48e1d20c92
added eigen to resources
Former-commit-id: a07c2d6368
9 years ago
dehnert
bb700457de
some minor fixes
Former-commit-id: f114c397f6
9 years ago
dehnert
512a1ec558
added special label 'deadlock' to models and builders
Former-commit-id: 4edc57216e
9 years ago
dehnert
74ee726e35
fixed some typos
Former-commit-id: de3cd92c62
9 years ago
dehnert
94fd4cd9a8
fixed bug related to instantaneous reward properties in formula parser
Former-commit-id: 8d799f8678
9 years ago
dehnert
2accd81aaa
fixed bug in reward generation for PRISM models
Former-commit-id: 72399da7ed
9 years ago
dehnert
f3701f66fb
bugfix for symbolic reachability reward computation
Former-commit-id: c197203539
9 years ago
ThomasH
7fef54ab10
modify the ma builder such that it resprects priorities
Former-commit-id: 2aa01e8e5d
9 years ago