sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
3196 Commits
2 Branches
0 Tags
187 MiB
Tree: f54e511d74
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from 'f54e511d74'
${ noResults }
Commit Graph

1027 Commits (f54e511d7495d36a45f278a4bc1674991ad927bf)

Author SHA1 Message Date
dehnert 5776b207c3 Changed to new cleaner iterator for matrix.
13 years ago
dehnert 36543de851 Started trying to implement a more clean iterator solution for sparse matrix.
13 years ago
dehnert abf6f85b63 Intermediate commit to switch workplace.
13 years ago
PBerger 42b9072cbf Implemented TBB Parallelization Support into SparseMatrix.h
13 years ago
dehnert 7aa3139b62 Intermediate commit with submatrix computation for scheduler-induced system from MDP.
13 years ago
PBerger cb770020bf Refactored the Jacobi Decomposition
13 years ago
dehnert f040264660 Intermediate commit with submatrix computation for scheduler-induced system from MDP.
13 years ago
PBerger bf5de84ab9 Refactored the parsing and lineFeeding handling.
13 years ago
PBerger 0f7e2835e3 Added an assignment constructor to the SparseMatrix.h
13 years ago
PBerger 0051aec174 Added an assignment constructor to the SparseMatrix.h
13 years ago
PBerger 22f00bc95e Reordered elements of SparseMatrix.h
13 years ago
PBerger 78184f9537 Added a Hash Class in the Utility Namespace.
13 years ago
PBerger d596f126b2 Fixed/added missing Copy Constructors for Models and the SparseMatrix
13 years ago
PBerger b978a4d311 Added more move constructors.
13 years ago
dehnert fabf662edd Added dot output for both deterministic and nondeterministic models. Fixed iterator bug in sparse matrix.
13 years ago
dehnert bba72e452b Fixed off-by-one for our matrix-vector multiplication.
13 years ago
dehnert f44f0ce410 Cleaned interfaces of models from std::shared_ptr. Improved some code in graph utility.
13 years ago
dehnert c8081c4d34 Fixed wrong step-bounded backward search.
13 years ago
dehnert 14fae4883a Added prob 0/1 precomputation for bounded-until model checking for DTMCs. The version for MDPs seems to perform worse: needs to be investigated.
13 years ago
Lanchid ec91dcbe2e Merge branch master into LTLParser
13 years ago
dehnert 64a27bb871 Performance improvement for our matrix multiplication.
13 years ago
dehnert 28facf9034 Fixed bug in iterator.
13 years ago
dehnert fbe1f41213 Removed GraphTransition class, which is now replaced by SparseMatrix in the instances where it was used before. Changed GraphAnalyzer accordingly and adapted tests.
13 years ago
dehnert ed4c6c8429 Fixed SCC decomposition functions. Added performance tests for GraphAnalyzer.
13 years ago
dehnert 69395face2 Moved creation of SCC-dependency graph into abstract model class. Added functionality to sparse matrix class to not give the number of nonzeros upfront, but to to grow on demand.
13 years ago
dehnert fc67cf4e3f Further refactoring of GraphAnalyzer class.
13 years ago
dehnert 94337f5835 Added move-constructor and move-assignment to bit vector class.
13 years ago
dehnert d266d9effe Fixed another bug in sparse matrix. Fixed bug in test.
13 years ago
dehnert 2b4d26023a Fixed one of the remaining bugs introduced by refactoring.
13 years ago
dehnert 00b4797948 Further refactoring. Other classes are now adapted to the changes in the sparse matrix class.
13 years ago
dehnert 9ae177c9b5 Further refactoring. In particular of the matrix class.
13 years ago
dehnert bb441cdeca Refactored some parts of sparse matrix.
13 years ago
gereon 6c19ddb877 Cosmetics: Trailing whitespaces, space indentation, ...
13 years ago
dehnert e524720925 Added prototypical support for in-place matrix-vector multiplication in the style of Gauss-Seidel. This might enhance the speed of convergence for value-iteration model checkers.
13 years ago
dehnert 102f38322d Fixed several bugs in several modules (bit vector, parser, etc.). Topological value iteration now works for the consensus protocol and the two dice example.
13 years ago
gereon 8dce5af515 fixed some warnings (comparison between signed/unsigned)
13 years ago
dehnert af1aa4e1e5 Added native matrix-vector multiplication for our matrix format (as fast as gmm++). Fixed bug in bit vector. Fixed some issues in SCC decomposition. MDP model checkers now have the solving methods by default (native ones) and may override them with their own ones, if desired. Added some aux stuff, like vector helper methods.
13 years ago
dehnert 34b85b956e Moved model checking of DTMCs to superclass. Now, each DTMC model checker only needs to implement matrix-vector multiplication and linear equation solving to be able to fully model check DTMCs. Added subset/disjoint functionality to bit vector. Changed tests for MDP and DTMC model checking a bit.
13 years ago
dehnert 4bcb26ab96 Included subset-test in bitvector.
13 years ago
dehnert 5e3a8a1232 Fixed wrong check for submatrix property of reward matrices.
13 years ago
PBerger 06d78967df Fixed MDP Parser, removed parsing of STATES/TRANSITIONS, see #10
13 years ago
dehnert 7b259120b7 Marked submatrix check in DTMC and sparse matrix as faulty. Needs to be fixed.
13 years ago
dehnert bc4eb661ba Fixed some memory leaks. Fixed bug in vector utility. Fixed bug in sparse matrix printing. Fixed bug in DTMC model checker (computing reachability rewards). Included full reward model checking for MDPs.
13 years ago
PBerger b2c0cfc57c Added a conversion routine GmmXX -> Storm Sparse Matrix
13 years ago
PBerger 4fe071033b Removed std:: from uint type specifier (illegal in VS2012)
13 years ago
Lanchid 5b57728d7e Merge branch master into PrctlParser
13 years ago
dehnert 313d48e2da Fixed the method for making rows absorbing for nondeterministic models.
13 years ago
dehnert d4cf812c5e Added until-model checking for MDPs. Implemented Prob1A algorithm. Added asynchronous leader example.
13 years ago
dehnert 7d7edc5a05 Implemented Prob1E algorithm for nondeterministic models. Added comparison operator to bit vector.
13 years ago
dehnert 73ab4a78a9 Renamed methods get*Pointer in sparse matrix class, because they do not return a pointer. Added initial versions of forward/backward graph transition creation for nondeterministic models.
13 years ago