dehnert
c5985be437
Minor fixes for GlpkLpSolver.
Former-commit-id: 07595da7f3
11 years ago
dehnert
8ebd924ca6
Further work on refactoring solvers: cleaned LP solver interface a bit and adapted glpk- and Gurobi-based implementations of the interface.
Former-commit-id: 25b7a22bcc
11 years ago
dehnert
588a4b60b6
Refactored linear equation solvers and nondeterministic linear equation solvers. Added functional tests for both.
Former-commit-id: 0abb11828a
11 years ago
masawei
3598b7195e
Refactored the DeterministicSparseTransitionParser.
Former-commit-id: 9012aadd9d
11 years ago
dehnert
ae270cc917
Added two more example files that form a Markov automaton.
Former-commit-id: fa605690cf
11 years ago
dehnert
79730379e4
Started refactoring the linear equation system solvers.
Former-commit-id: 72d647fd42
11 years ago
dehnert
ee0026e0e6
Fixed minor bug in Markov automata time-bounded reachability.
Former-commit-id: 6454223cd3
11 years ago
dehnert
efb244a447
Added functional tests for scheduler classes.
Former-commit-id: d7f7da5ab0
11 years ago
dehnert
f79329bd9d
Fixed SCC decomposition. Added functional tests for SCC decomposition.
Former-commit-id: 25a7805fcb
11 years ago
dehnert
e80bb0caa5
Added functional tests for MEC decomposition.
Former-commit-id: 66b1265ebb
11 years ago
dehnert
f32853b6aa
Beautified remaining storage classes a bit.
Former-commit-id: 93f272727f
11 years ago
dehnert
35d16a1191
Replaced VectorSet bei boost::container::flat_set, which does essentially the same. Fixed a bug in sparse matrix creation.
Former-commit-id: cb632bcfd4
11 years ago
dehnert
f684ce7799
Removed obsolete constructors of sparse matrix class as the new matrix builder is supposed to be used anyway. Fixed some minor issues.
Former-commit-id: ee8a7cc440
11 years ago
dehnert
5e12a65d67
Adapted performance-critical iterations in graph utility to the iterator formulation with less overhead.
Former-commit-id: 44bf732bb4
11 years ago
dehnert
41cb1a8227
Merge branch 'master' into storageRefactoring
Former-commit-id: 7ae25e7ab2
11 years ago
dehnert
f2670883a8
Merge branch 'master' of https://sselab.de/lab9/private/git/storm
Former-commit-id: 6637a6fac4
11 years ago
dehnert
72531bcebb
Added proper TBB multi-threading to all operation relevant to model checking MDPs.
Former-commit-id: dcb4bde1d3
11 years ago
dehnert
d723272cc1
Added some performance tests for matrix-vector multiplication.
Former-commit-id: 521dbf788d
11 years ago
dehnert
cdc369b96a
Temporarily removed the detection of the repository version of TBB from CMakeLists.txt. Corrected TBB sparse matrix-vector multiplication. Added TBB parallel vector addition.
Former-commit-id: f90ae764c8
11 years ago
dehnert
81cf0e2b22
Added SparseMatrixBuilder class that actually builds the matrices. A call to build() will then generate the matrix. This eliminates superfluous checks in the matrix that slowed down performance.
Former-commit-id: af5d946fb8
11 years ago
dehnert
cf2b84b281
Further work on iterators for sparse matrix.
Former-commit-id: 8e78262161
11 years ago
dehnert
ab5b5be1ac
First step towards pair-based column and value storage in sparse matrix.
Former-commit-id: c0ad97be8f
11 years ago
David_Korzeniewski
91125c3c6d
Fixed build errors on Windows
Former-commit-id: 6ddc16cd5a
11 years ago
dehnert
e08b61b9f7
Added functional and performance tests for sparse matrix.
Former-commit-id: dd9abe1826
11 years ago
dehnert
97fb2f9750
All tests working with (partially) new sparse matrix implementation/interface.
Former-commit-id: 0272dd3524
11 years ago
masawei
f8566e9dc2
A thousand things.
- More tests.
- Changed SparseStateRewardParser to a static class
- Added comments here and there
- Some reformatting.
- Fixed some warnings.
- Eliminated some unnecessary includes.
- ...
Former-commit-id: efe1c96fee
11 years ago
masawei
9ce47989ed
The MA transition parser is now able to handle arbitrary labels.
Former-commit-id: 9643f41141
11 years ago
dehnert
a271e5ce63
Working towards making every (remaining) test work
Former-commit-id: e4560e07f2
11 years ago
dehnert
a26f63be30
Finished reworking the sparse matrix implementation. Adapted all other classes to the (partially) new API of the matrix.
Former-commit-id: 2c3b5a5bc3
11 years ago
dehnert
ef041982b5
Further work on sparse matrix implementation.
Former-commit-id: df4eb9c476
11 years ago
dehnert
4376708a46
Further maintenance work on sparse matrix implementation.
Former-commit-id: 56885d90bf
11 years ago
dehnert
8a47d03cf7
Started to rework the interface of the sparse matrix class.
Former-commit-id: 6ae2699da6
11 years ago
dehnert
84bd5f3b40
Renamed ConstTemplates to constants. Removed all calls to constGetZero, constGetOne and constGetInfinity by the new names. Created performance test for bit vector iteration.
Former-commit-id: 6d90ec961e
11 years ago
dehnert
d5cadc0f4b
Finalized interface of bit vector. Added unit tests for all methods of the bit vector.
Former-commit-id: 6c7834ed20
11 years ago
dehnert
30322ec57d
Now officially made the iterator over bit vectors an input iterator so that it can be used for constructing STL containers and other containers.
Former-commit-id: 1bcd8c43b3
11 years ago
dehnert
a7c8c3a1a3
Added checklist file for refactoring classes.
Former-commit-id: 97a3d875d6
11 years ago
dehnert
07fbff7a07
Started refactoring bit vector class.
Former-commit-id: a2fecfce2b
11 years ago
dehnert
716f3366fc
Added configuration file for astyle (a code-formatting tool) that is tailored to our formatting style.
Former-commit-id: ba2f428b6f
11 years ago
masawei
cb870c28c7
Began testing of the MarkovAutomatonSparseTransitionParser to identify inflexibilities or bugs.
- Noticed to my astonishment that seemingly arbitrary use of whitespaces (as long as each transition is in its own line) is no problem for the parser.
- As predicted, handling of action labels of arbitrary length especially such starting with an '!' is not supported.
Next up: Handle arbitrary labels.
Former-commit-id: 339578e72a
11 years ago
dehnert
e2cec086a3
Merge branch 'imca'
Former-commit-id: 680ee6406d
11 years ago
dehnert
c336fd7ff8
Minor fixes for implementation of GlpkLpSolver if glpk is unavailable.
Former-commit-id: 778f93a33c
11 years ago
dehnert
344e1b6dd3
Enabled checking of some untimed properties on Markov automata.
Former-commit-id: e71aa66c62
11 years ago
dehnert
3dab26463d
Introduced precision for digitization-based techniques as a new parameter.
Former-commit-id: e9c57f821b
11 years ago
dehnert
ece4085a61
Another bugfix for matrix creation during LRA computation.
Former-commit-id: c3325b8913
11 years ago
dehnert
fde78ad759
Bugfix for matrix creation in LRA computation.
Former-commit-id: cb4c9cb728
11 years ago
dehnert
b3601782a9
Added Lp Solver class for glpk and added it as an option in CMakeLists.txt.
Former-commit-id: e5c5215a29
11 years ago
dehnert
0a89d65f93
Started refactoring Markov automaton model checker.
Former-commit-id: c4278de4f0
11 years ago
dehnert
18711c01a3
First working version of time-bounded reachability for Markov automata.
Former-commit-id: 6501cbfca4
11 years ago
dehnert
2ef0405104
Merge branch 'master' into imca
Conflicts:
src/storage/SparseMatrix.h
Former-commit-id: 7e28105e8b
11 years ago
dehnert
dce43d78e7
Started implementation of time-bounded reachability of Markov automata.
Former-commit-id: 512bb117a6
11 years ago