168 Commits (4b3d4a7c114a20c38c44c4c9cbd56eaf3e569664)

Author SHA1 Message Date
dehnert aee63dcf31 Made the SCC generation during decomposition optional. 12 years ago
dehnert 961909877a Added iterative version of Tarjan's algorithm for performing SCC decomposition of state-based models. 12 years ago
dehnert 01779c9e83 Incomplete version of SCC decomposition of nondeterministic models. 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
gereon cf772688f0 added setter for options in Settings class. 12 years ago
dehnert d38e7eeeb8 Implemented new utility functions and improved existing ones. 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
Lanchid 5b57728d7e Merge branch master into PrctlParser 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 7d7edc5a05 Implemented Prob1E algorithm for nondeterministic models. Added comparison operator to bit vector. 12 years ago
dehnert 7ceb1ed9b2 Added logging for errors in labeling class. Corrected wrong labeling of MDP in examples. Extended test checking for first MDP example in main. 12 years ago
dehnert 8a9d766c73 Changed input format for non-deterministic models to PRISMs output format. Added min/max capability to probabilistic operator without bounds. Implemented Prob0E. Added a simple MDP model to example suite. 12 years ago
dehnert 8c248c05c5 Renamed NonDeterministic to Nondeterministic in all places. Fixed (hopefully) all occurrences of these names. Implemented Prob0A algorithm. 12 years ago
dehnert 19cbe13691 Prepared methods for performing reachability searches for non-deterministic models. Removed storage of backward transition relation: it is now (re-)created on demand in the model checkers. 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
PBerger 7f956b0d35 Added Cotire to Storm to build PCH on all plattforms. 12 years ago
Lanchid 7e87f35e95 First test case for prctl parser, and some necessary modifications for 12 years ago
dehnert 726569d5f1 Fixed bug in parser that inserted 0-entries on the diagonal at the wrong places. Enabled link-time-optimizations for Release-Build when using clang. Fixed bug in base exception: what() returned a pointer to a char array belonging to a local variable, which got deallocated and thus invalidates the char array content. 12 years ago
PBerger 9a9cd968d9 Added a test to verify the RowSum Function in the Sparse Matrix. 12 years ago
dehnert 5f57cbb12a Now able to build the BDD for the die example, including the reachability analysis! Booyah 12 years ago
dehnert 4d813999e3 Backup commit. On my way of buidling appropriate BDDs. 12 years ago
dehnert c4af78b859 Added singleton utility class for CUDD-based things. Added some first methods to expression classes to generate ADDs, but this should be moved to a separate class implementing the expression visitor pattern. 12 years ago
gereon f9923bac95 Fixed memory leaks involving Settings class 12 years ago
gereon facec2b040 experimented with custom style checker, fixed a few minor issues 12 years ago
gereon 062960b94c Some cleanups, removing memleaks 12 years ago
gereon 3a1b0f0433 adding sloppy mode for Settings, load settings in tests 12 years ago
Lanchid 1b0449addb Prctl parser... not yet working 12 years ago
gereon 989c0a51ea a few more style issues 12 years ago
gereon ea84f91cf3 made a run of cpplint and fixed some of the warnings... 12 years ago
gereon a8517c7246 fixed some documentation and changed position of const in Settings class. 12 years ago
gereon a695208d0e implemented check for deadlocks in parser 12 years ago
PBerger 557461a77d Renamed SquareSparseMatrix to SparseMatrix 12 years ago
PBerger b89db58fbb Made changes to all files that use the Sparse Matrix, as the diagonal entries are now included in the main storage. This refs #34 12 years ago
dehnert 58cf8118fe Initial version of reward model checking for DTMCs. Added two convenience operators to PCTL (Eventually and Globally) and added missing reward formulas. 12 years ago
PBerger f983317b54 Renaming MRMC to STORM, see #42 12 years ago
dehnert b26a731383 Added reward parsing: 12 years ago
Lanchid 48098b596d Removed the parameter from const templates, as types can be stated 12 years ago
Lanchid afb0373358 Added DtmcParser class that parses a whole DTMC, making use of the 12 years ago
Lanchid daa5cf297a Changed type of parameter filename to std::string const & (was const 12 years ago
Lanchid 64784d4e92 Renamed LabParser to AtomicPropositionLabelingParser 12 years ago
Lanchid 3c741fae4a Changed filename parameter for DeterministicSparseTransitionParser to a 12 years ago
Lanchid b0b8c98f6b Renamed TraParser to DeterministicSparseTransitionParser 12 years ago
dehnert 89e38fed8f Added temporary check() method to ProbabilisticNoBoundsOperator. 12 years ago
gereon 470fa4c4b7 added sys/mman.h for linux target 12 years ago
PBerger 01ea2c8427 Moved os specific includes into OsDetection.h 12 years ago
PBerger 96c7dd9a79 Added the (default) external build path /build to git ignore. 12 years ago
PBerger 08f87d545c Some more refactoring, renaming, adding #ifndef guards... 12 years ago