Commit Graph

  • 02cb1a2418 Replaced all calls to Matrix->toEigenSparseMatrix with calls to the adapter. PBerger 2013-02-01 15:53:40 +0100
  • ff0f2197b2 Merge with master. dehnert 2013-01-31 15:17:24 +0100
  • 6fb56748a6 Bugfix for correctly counting the number of values the parser inserts. dehnert 2013-01-31 15:10:36 +0100
  • 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. dehnert 2013-01-31 10:40:28 +0100
  • 9a9cd968d9 Added a test to verify the RowSum Function in the Sparse Matrix. Added an option to the settings for auto-fixing missing no-selfloop states. Kind of a super-option above fix-nodeadlocks, perhaps some Cleanup later on. Modified tra Files to comply with formats... PBerger 2013-01-31 00:00:47 +0100
  • 43b56fce62 first version of BoundedNaryUntil. clone() does not work yet... gereon 2013-01-29 21:22:56 +0100
  • 1edd306032 Silenced warning of clang: Changed NULL to nullptr as this should be used in C++11. dehnert 2013-01-29 21:16:16 +0100
  • 0a6a0b9fd3 Eliminated warning of clang by introducing proper getter. dehnert 2013-01-29 21:11:23 +0100
  • 9a73a2740a second hald of documentation. I guess that's it :-) gereon 2013-01-29 20:54:50 +0100
  • 3716dedc78 first half of documentation. gereon 2013-01-29 20:40:52 +0100
  • 8077952331 adding needed methods for more formula classes gereon 2013-01-29 20:14:38 +0100
  • 8449c5ee11 implemented formula checker gereon 2013-01-29 18:44:59 +0100
  • c47b559986 Fixed minor bugs for Jacobi decomposition. dehnert 2013-01-29 09:13:06 +0100
  • 5f57cbb12a Now able to build the BDD for the die example, including the reachability analysis! Booyah dehnert 2013-01-28 19:58:41 +0100
  • 4d813999e3 Backup commit. On my way of buidling appropriate BDDs. dehnert 2013-01-27 21:48:11 +0100
  • 9d65bdeef3 next iteration on formulas... gereon 2013-01-27 20:58:22 +0100
  • 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. dehnert 2013-01-26 22:49:17 +0100
  • 5b0af74fa6 Integrated a few more functions to CUDD which are necessary (PRISM adds them as well). dehnert 2013-01-26 22:47:19 +0100
  • 278b425a35 Switched to die example. dehnert 2013-01-26 14:05:54 +0100
  • 7e121b030e Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2013-01-26 12:58:26 +0100
  • 7331544377 Added output functionality to bit vector and moved test-checking lines in storm.cpp to the right place. dehnert 2013-01-26 11:23:20 +0100
  • 8a719bed22 some more form on formulas. seems to work for formula objects changed yet... gereon 2013-01-26 00:54:31 +0100
  • edd3a9a20e Added possibility to evaluate expressions without concrete variables. Fixed some minor things in CUDD Makefiles. Renamed IR adapter. dehnert 2013-01-25 19:43:32 +0100
  • 70181387a3 Add forward declarations Lanchid 2013-01-25 17:37:56 +0100
  • 94efb3bcf4 Merge branch 'master' into PrctlParser Lanchid 2013-01-25 17:31:13 +0100
  • d23b3dbee5 First compiling version of PRCTL parser Lanchid 2013-01-25 17:27:33 +0100
  • 1485eae477 Added cudd to gitignore so the changes to cudd (e.g. compiling) will not be committed to repo. dehnert 2013-01-25 16:47:59 +0100
  • 9fbebb9349 Added CUDD to the repository. dehnert 2013-01-25 16:47:03 +0100
  • df91728da0 first "kind of working" version. gereon 2013-01-24 23:28:45 +0100
  • a17c99902b The PRISM parser can now parse DTMC models that do not use synchronization. dehnert 2013-01-24 20:11:41 +0100
  • aec55c8ef5 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2013-01-24 10:32:18 +0100
  • 756cbd4ed1 Fixed some bugs in GmmxxAdapter and added row-vector product to sparse matrix. dehnert 2013-01-24 10:32:15 +0100
  • 4bb76d0268 Added EigenAdapter and a Test for the Adapter. Fixed a type in EigenDtmcPrctlModelChecker.h Added missing transitions in one example input file PBerger 2013-01-24 01:18:22 +0100
  • ad3922ec18 Fixed a bug in the GmmAdapter with non-square matrices being truncated. PBerger 2013-01-23 22:49:32 +0100
  • 9e416b69e5 The GmmxxAdapter converts to a Row-Major Matrix, not column-major. PBerger 2013-01-23 22:44:34 +0100
  • d4b5a24757 Fixed the Jacobi Decomposition in the Matrix, Diagonal Matrix was not inverted. Implemented solveLinearEquationSystemWithJacobi for GMM based Solver. PBerger 2013-01-23 20:08:09 +0100
  • 3a73e0838c make memcheck targets call the binaries with -v and --fix-deadlocks gereon 2013-01-22 21:36:25 +0100
  • f9923bac95 Fixed memory leaks involving Settings class gereon 2013-01-22 20:12:30 +0100
  • 4fd1d672ef fixed valgrind errors gereon 2013-01-22 19:11:51 +0100
  • 5ac5acf6c4 Added hint to existing DTMC examples. dehnert 2013-01-22 13:52:18 +0100
  • e8fd897852 Fixed bug in copy constructor of matrix. dehnert 2013-01-22 13:51:49 +0100
  • a2c5ee805b Refactored calls to SetBitCount PBerger 2013-01-21 14:40:27 +0100
  • aea711b9f7 JacobiDecomposition Copy Constructor should throw exception: Now it throws an InvalidAccessException. This closes #40 PBerger 2013-01-21 14:34:01 +0100
  • c2669ccec4 "Creating" DeterministicModelParser gereon 2013-01-20 20:54:14 +0100
  • facec2b040 experimented with custom style checker, fixed a few minor issues gereon 2013-01-20 20:19:38 +0100
  • 062960b94c Some cleanups, removing memleaks gereon 2013-01-18 19:52:49 +0100
  • b13f1ff37f Adding check "transitionRewards submatrix of transitions" gereon 2013-01-18 19:51:48 +0100
  • f5f04a1c05 Added dummy test to check for valid push to new repo. dehnert 2013-01-16 22:28:14 +0100
  • 0f450f9cab Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2013-01-16 22:25:25 +0100
  • e2f894fe5d Deleted unnecessary files. dehnert 2013-01-16 14:59:46 +0100
  • 152923e14b Reverted the PrismParser in the sense that it now again builds a full string of the input first and then parses it, because apparently the adapter iterators of Boost give an awful output under valgrind. dehnert 2013-01-15 11:18:56 +0100
  • 0992df5c66 fixing test for deadlock nodes in parsers gereon 2013-01-15 00:35:40 +0100
  • 3dc82759af some error output, if Dtmc matrix is invalid gereon 2013-01-15 00:34:39 +0100
  • 7092544e9f Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC gereon 2013-01-14 23:35:40 +0100
  • 3a1b0f0433 adding sloppy mode for Settings, load settings in tests gereon 2013-01-14 23:33:47 +0100
  • 54499c35ee adding missing include gereon 2013-01-14 23:31:48 +0100
  • aba470960f Intermediate commit to test code under linux. dehnert 2013-01-14 20:55:01 +0100
  • 7873dbca74 Merge with master. dehnert 2013-01-14 20:28:25 +0100
  • ed43401c37 Reenable logging to prevent exception. dehnert 2013-01-14 20:26:09 +0100
  • 7800132684 Added Mdp Class, Parser and support in the AutoParser. Added Test for MdpParser PBerger 2013-01-14 18:24:37 +0100
  • 1b0449addb Prctl parser... not yet working Lanchid 2013-01-14 17:38:14 +0100
  • c19418b871 Intermediate commit to switch workplace. dehnert 2013-01-14 16:59:15 +0100
  • a69faa9f6a Added typecast when dealing with some Eigen functions to avoid comparing signed and unsigned values Lanchid 2013-01-14 15:17:23 +0100
  • d414b93bad Added some functionality to IR. Introduced case distinction for boolean/integer assignments in updates. Started writing an IR adapter. dehnert 2013-01-13 22:47:29 +0100
  • 9ca0acd0d6 removed obsolete cmake files, renamed license file gereon 2013-01-12 22:30:07 +0100
  • d5eb8ccfab renamed mrmc-tests to storm-tests gereon 2013-01-12 22:26:41 +0100
  • 989c0a51ea a few more style issues gereon 2013-01-12 22:03:15 +0100
  • 7a1bf4d834 fixed some style issues reported by cpplint gereon 2013-01-12 21:58:29 +0100
  • 57274b3f09 Fixed missing newline and warning about nested comments. dehnert 2013-01-12 21:42:32 +0100
  • 78c0245d16 Added rowMapping to MDP transition parser. gereon 2013-01-12 20:30:36 +0100
  • 4d709ed9c2 Implemented second pass in NonDeterministicTransitionParser gereon 2013-01-12 20:15:48 +0100
  • 37ed70836a adding format hints gereon 2013-01-12 20:15:30 +0100
  • 50f891b9f2 Removed some unnecessary boost stuff from IR expressions. Separated header and source file for all non-expression IR entities (expressions are still to come). Added comments for these classes. dehnert 2013-01-12 19:35:00 +0100
  • b8f1ddd5da Implemented first run for NonDeterministicTransitionParser gereon 2013-01-12 19:30:13 +0100
  • 82ff9f3891 adding initializer for variable gereon 2013-01-12 19:29:53 +0100
  • 867d477afc removing pointless comment gereon 2013-01-12 19:29:02 +0100
  • ea84f91cf3 made a run of cpplint and fixed some of the warnings... gereon 2013-01-12 18:33:13 +0100
  • 5668b95d9b added missing include. gereon 2013-01-12 18:12:55 +0100
  • a8517c7246 fixed some documentation and changed position of const in Settings class. gereon 2013-01-12 18:10:41 +0100
  • 650a0f0a27 added documentation for AbstractModel and operator<< for ModelType gereon 2013-01-12 17:58:37 +0100
  • a695208d0e implemented check for deadlocks in parser gereon 2013-01-12 16:50:27 +0100
  • 4e71cab4a7 using AutoParser in storm.cpp gereon 2013-01-12 16:15:12 +0100
  • cdec5d44c9 adding format hint to tiny examples gereon 2013-01-12 16:13:05 +0100
  • 4dbbb1486b first working version of AutoParser gereon 2013-01-12 16:12:15 +0100
  • b4ea27d7c4 Added checks to parser: Now only local variables may be written in updates and each variable at most once. dehnert 2013-01-12 15:37:19 +0100
  • a82c8b3153 Moved implementation of PrismParser completely to source file. Fixed some minor things in IR classes. dehnert 2013-01-12 13:54:27 +0100
  • 4dc780ef77 modified AutoParser to reflect changes in the model type system. gereon 2013-01-12 13:39:06 +0100
  • b4862360ba made Ctmc and Dtmc subclasses of AbstractModel implement getType() fixed typo gereon 2013-01-12 13:38:15 +0100
  • 004633b79a fixed brackets in BaseException gereon 2013-01-12 13:37:25 +0100
  • 006c9e6b88 changed model base class gereon 2013-01-12 13:35:11 +0100
  • 4b7c6a8941 Splitted PrismParser class into header and implementation file. Commented both files properly. Cleaned interface of PrismParser. dehnert 2013-01-11 19:53:35 +0100
  • f52201466c Parsing labels works now. dehnert 2013-01-11 16:56:00 +0100
  • 6a33f84512 Another step towards PRISM model parsing: small models get recognized correctly. dehnert 2013-01-11 00:12:28 +0100
  • a44da7d50a Commit to switch workplace. dehnert 2013-01-10 18:24:52 +0100
  • 261750df9b removing two warnings from cpplint gereon 2013-01-10 13:23:26 +0100
  • 3deca3f2d3 Intermediate Commit to switch workplace. dehnert 2013-01-10 09:59:42 +0100
  • bad870f085 integrated cpplint gereon 2013-01-09 19:14:45 +0100
  • f7194a416d Cleaned IR classes a bit and made attributes private. Changed grammar rules accordingly. dehnert 2013-01-09 17:19:48 +0100
  • 1776f8ce12 first steps towards an AutoParser gereon 2013-01-09 11:13:28 +0100
  • 946128cae1 Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC gereon 2013-01-09 11:12:18 +0100