sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity

Commit Graph

  • cfef571365 Merge branch 'master' into PrctlParser Lanchid 2013-02-06 17:37:02 +0100
  • ab4174183b Changed PrctlParser to directly parse the input string as formula, and added PrctlFileParser to parse formulae from a file Lanchid 2013-02-06 17:19:40 +0100
  • f35fff7061 Replaced log4cplus with its state in the master branch Lanchid 2013-02-06 16:47:08 +0100
  • e829e613c0 Changed grammar such that brackets are not necessary around each binary operator, and changed some test cases to check that it works Lanchid 2013-02-06 16:38:42 +0100
  • 34aff4cbd9 Added constructor for ExplicitModelAdapter class. dehnert 2013-02-06 16:04:27 +0100
  • e2f6b4b265 Extended parseComplexFormulaTest to use nested path formulas Lanchid 2013-02-06 14:53:33 +0100
  • 93af6147c4 Minor change to .gitignore. dehnert 2013-02-06 14:29:13 +0100
  • 10e25fbd61 fixed warnings in ParseMdpTest gereon 2013-02-06 12:59:01 +0100
  • 51a5012dba fixed warnings in SparseMatrix gereon 2013-02-06 12:56:07 +0100
  • 03bee97786 Merge branch 'master' into PrctlParser Lanchid 2013-02-06 12:28:17 +0100
  • 3833c8af41 Some more test cases for PRCTL formula parsing Lanchid 2013-02-06 12:08:22 +0100
  • e52379bb54 Added XCode stuff to .gitignore. Fixed a few tests to compile with clang under -Werror. dehnert 2013-02-06 11:52:53 +0100
  • b66e1a34db Some fixes in formulas Additional test case for reward formulas Lanchid 2013-02-06 11:35:14 +0100
  • 02528f2bd9 Test cases for Prctl parser Lanchid 2013-02-06 11:04:43 +0100
  • 777aa3a914 Intermediate commit to switch workplace. dehnert 2013-02-06 09:53:05 +0100
  • 86965ff12a removed obsolete typedef gereon 2013-02-04 16:31:10 +0100
  • bd39a9b44c Merge branch 'interfacelogic' gereon 2013-02-04 16:30:03 +0100
  • d7a288d05a fixed "copy" constructor gereon 2013-02-04 09:50:09 +0100
  • 55c2d5c03f implemented clone for BoundedNaryUntil gereon 2013-02-04 09:46:44 +0100
  • 54565ddd55 changed rowMapping to vector<int> gereon 2013-02-04 09:41:09 +0100
  • 583ebf62bd made rowMapping from NDSTParser available in MDP model class gereon 2013-02-03 20:42:07 +0100
  • 1d1f9da315 made rowMapping from NDSTParser available in MDP model class gereon 2013-02-03 20:42:07 +0100
  • be182293ee Small fix on Eigen-based model checker to make it compile with clang. dehnert 2013-02-02 20:26:11 +0100
  • 21e0ecd9f0 Change in CmakeLists.txt: When building debug, add -g as CXX flag (For clang) Lanchid 2013-02-01 16:19:04 +0100
  • 7e87f35e95 First test case for prctl parser, and some necessary modifications for the code Lanchid 2013-02-01 16:15:46 +0100
  • a598d3751c The DeterministicSparseTransitionParser.cpp was still broken, rewrote it in a simpler and more convenient way. All Deterministic Tests complete now. PBerger 2013-02-01 15:55:13 +0100
  • 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