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

84 Commits (1a4a32a1c534063171cac06e34775ae6528e1081)

Author SHA1 Message Date
gereon 6c19ddb877 Cosmetics: Trailing whitespaces, space indentation, ...
12 years ago
Lanchid 0dcebc8ff0 Start of implementing improved file parser for formulas
12 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.
12 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.
12 years ago
dehnert c784de4d03 Added new model checker that uses topological value iteration. However, does not fully work yet.
12 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.
12 years ago
dehnert fbf28796b8 Fixed bug in gmm++ model checker: missing vector addition.
12 years ago
PBerger d477d752b1 Updated the Jacobi Solver to make use of the new Adapters, refactored the Matrix conversion.
12 years ago
dehnert f1c379bbe3 Moved model checking functionality for MDPs for general superclass such that specialized model checkers only need to implement certain operations. Fixed tests.
12 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.
12 years ago
dehnert 3ab71cc08a Added proper treatment of transition based rewards.
12 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.
12 years ago
dehnert cbf4a2ff3b Small update to model checking reward formulae over MDPs.
12 years ago
dehnert 40f7ccac52 Implemented model checking of instantaneous reward formulae over MDPs in Gmmxx model checker.
12 years ago
PBerger b2c0cfc57c Added a conversion routine GmmXX -> Storm Sparse Matrix
12 years ago
Lanchid 5b57728d7e Merge branch master into PrctlParser
12 years ago
gereon 75d61d3af3 explicit private constructor was not needed after all
12 years ago
gereon b1498ef0bb moved model from specific model checkers to AbstractModelChecker
12 years ago
dehnert 313d48e2da Fixed the method for making rows absorbing for nondeterministic models.
12 years ago
dehnert 73623ff3f6 Added boolean parameter qualitative to all path formulas, i.e. to the checking and the callback methods.
12 years ago
dehnert 5ba7f63bc2 Splitted RewardBoundOperator and ProbabilisticBoundOperator checking methods for model checkers (needed for enabling qualititative model checking for P operator with bounds 0/1). Moved some methods of DtmcModelChecker one level up to AbstractModelChecker. TODO: this should be done for other methods as well, but there are more changes needed for that to work.
12 years ago
dehnert d4cf812c5e Added until-model checking for MDPs. Implemented Prob1A algorithm. Added asynchronous leader example.
12 years ago
dehnert 48dea0199e Started implementing the model checker for MDPs. Added reduce functionality to vector utility. Moved min/max capability to NoBoundOperator.
12 years ago
dehnert 5d849018de Some minor fixes to GraphAnalyzer and model checkers.
12 years ago
dehnert 7d95a45633 Fixed bug in AbstractModelChecker: it does now correctly inherit from a lot more interface classes. NOTE: checking a formula on a model checker that does not support it failed silently. This should NOT be the case. Re-enabled DEBUG option for cmake. NOTE: why was this disabled anyway? Introduced another layer AbstractDeterministicModel and AbstractNonDeterministicModel in model hierarchy to allow for easily distinguishing these classes. Made necessary adaptions in (hopefully) all classes. Move the graph analyzer to utility folder.
12 years ago
dehnert c02271a36a Fixed typo in CTMC class. Moved GraphAnalyzer to utility.
12 years ago
gereon 5bb71a28e9 added more interfaces to AbstractModelChecker.
12 years ago
Lanchid afce8c9d12 Fixed some doxygen warnings
12 years ago
gereon 47cb1aa4d9 renamed BoundOperator to PathBoundOperator (StateBoundOperator is coming soon...)
12 years ago