Matthias Volk
|
325b700c62
|
Explicitly set initialization order for SparseMatrix to avoid nasty segfaults
|
5 years ago |
Tim Quatmann
|
60670e1fb2
|
SparseMatrix: fixed getConstraintRowSumVector which did not allocate enough space before filling the resulting vector.
|
5 years ago |
Sebastian Junges
|
9e13f42a03
|
fix in permute when no rowgroupindices where given
|
5 years ago |
Sebastian Junges
|
8a7e40558d
|
permute for matrices
|
5 years ago |
Tim Quatmann
|
ea04f6dcd2
|
Fixes for LRA computation.
|
5 years ago |
Tim Quatmann
|
bcd193dd57
|
Implemented Value iteration based LRA computation for CTMCs.
|
5 years ago |
Tim Quatmann
|
492348542f
|
SubsystemBuilder: Fix deadlocks with a selfloop (if requested)
|
6 years ago |
Matthias Volk
|
9ebd1af737
|
Removed unused method again
|
6 years ago |
Tim Quatmann
|
3a11a4b3eb
|
Introducing a TBB adapter that #undefs TRUE and FALSE.
|
6 years ago |
Tim Quatmann
|
cf25f2f941
|
SparseMatrix: Create a pretty string of the matrix dimensions.
|
6 years ago |
Tim Quatmann
|
3a21ce8009
|
utility/vector: buildVectorForRange now gets the type of the vector as a template parameter.
|
6 years ago |
TimQu
|
f88ee9d9ae
|
fixed compilation of gmmxx multiplier and sparseMatrix with intel tbb enabled
|
7 years ago |
dehnert
|
48f5608157
|
making policy iteration available for game-based abstraction (prototypical for now)
|
7 years ago |
dehnert
|
9b80c65d72
|
more and more debugging
|
7 years ago |
dehnert
|
14724b529f
|
further debugging
|
7 years ago |
Matthias Volk
|
e513015b49
|
Compute all reachabilities probabilities in a forward manner
|
7 years ago |
dehnert
|
3ad85ba0e6
|
fixes and improvements for game-based abstraction
|
7 years ago |
dehnert
|
0725b5e590
|
changes to tracking values in mult-and-reduce functions of matrix
|
7 years ago |
dehnert
|
9665f4fa30
|
sparse qualitative solving of menu games
|
7 years ago |
TimQu
|
3b394a965e
|
some qvi optimizations
|
7 years ago |
dehnert
|
59666a9fe9
|
slight renaming in matrix builder to better capture semantics
|
7 years ago |
dehnert
|
99647c11fb
|
fixed an issue pointed out by Tim
|
7 years ago |
TimQu
|
8e7d3107ca
|
added function to check whether a matrix is the identity matrix
|
7 years ago |
dehnert
|
0d78367b9a
|
Catching empty selection in getSubmatrix pointed out by Timo Gros
|
7 years ago |
dehnert
|
8e3e99c4ce
|
fixed bug in submatrix computation pointed out by Timo Gros
|
8 years ago |
dehnert
|
1f16008b75
|
added proper exception handling to sylvan-based sharpening
|
8 years ago |
dehnert
|
d612337ebf
|
added bunch of debug output for aliasing problem
|
8 years ago |
dehnert
|
55c787e0d8
|
proper EC elimination in hybrid helper
|
8 years ago |
TimQu
|
6fa4e6b455
|
fixed SOR and gaussseidel linear equation solver methods
|
8 years ago |
dehnert
|
694e6ba240
|
EC elimination for Pmax for hybrid MDP model checker
|
8 years ago |
TimQu
|
142d034765
|
New methods for the SparseMatrix: SetRowGroupIndices and filterEntries
|
8 years ago |
dehnert
|
df0b5fbfa5
|
fixed multiply-reduce operations in the presence of empty row groups
|
8 years ago |
dehnert
|
ec61e110f2
|
introducing solver formats to enable linear equation solvers to take the fixed point rather than the equation system formulation
|
8 years ago |
dehnert
|
c5134c364f
|
Extraction and update of TBB-parallelized stuff
|
8 years ago |
dehnert
|
bba2832e5b
|
finished Walker-Chae method
|
8 years ago |
dehnert
|
5440d164b2
|
started on Walker-Chae algorithm
|
8 years ago |
dehnert
|
c77b9ce404
|
gauss-seidel style multiplication for gmm++
|
8 years ago |
dehnert
|
00f88ed452
|
gauss-seidel-style value iteration
|
8 years ago |
dehnert
|
dd035f7f5e
|
allow for summand in matrix-vector multiplication
|
8 years ago |
dehnert
|
5e2ccaeeb5
|
started moving towards simpler sparse quotient extraction
|
8 years ago |
dehnert
|
115f7734eb
|
more work on dd bisim
|
8 years ago |
Sebastian Junges
|
cd8dafa6ea
|
Check for absence of negative probabilities in matrix
|
8 years ago |
TimQu
|
fb6aa69750
|
started building the model for a given epoch
|
8 years ago |
dehnert
|
3bf40471b4
|
small fixes in matrix builder and removal of debug output
|
8 years ago |
dehnert
|
52b07a0c2f
|
fixed a bug in sparse matrix builder, fixed some tests
|
8 years ago |
dehnert
|
8a01765005
|
enabling symbolic bisimulation from cli
|
8 years ago |
TimQu
|
bff745656c
|
Fixed some matrix builder bugs related to 0x0 matrices
|
8 years ago |
TimQu
|
35c9b58fda
|
added a test case for SparseMatri::restrictRows and fixed it
|
8 years ago |
TimQu
|
3fd72a11d8
|
Improved SparseMatrix::restrictRows so it can handle empty row groups
|
8 years ago |
dehnert
|
ea02ea0838
|
started overhaul of cli/api
|
8 years ago |