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

Commit Graph

  • 152bcd2f20 Porting Program datastructures to use shared_ptr (at least for the moment...) some more cleanups gereon 2013-04-20 16:52:19 +0200
  • b92260fed0 A lot of work on PrismParser: gereon 2013-04-20 01:18:17 +0200
  • 00286b2f01 Added formula classes for CSL Lanchid 2013-04-19 17:46:15 +0200
  • 42489b434d Merge branch 'master' into LtlParser Lanchid 2013-04-19 14:35:13 +0200
  • 45867c33c1 Prctl works now. Lanchid 2013-04-19 14:34:46 +0200
  • 1539062a47 Added build folder of TBB to enable building the repository version from source. dehnert 2013-04-18 22:07:39 +0200
  • e2f95e065f Modified CmakeLists.txt to actually also link the libraries of TBB if requested. Included custom build of TBB for Mac OS using Apple clang 4.2 (based on clang 3.2). dehnert 2013-04-18 22:04:18 +0200
  • fd7971f9aa Added sources to Intel TBB, PATCHED files for MacOSX + CLang > 3.1 PBerger 2013-04-18 19:36:23 +0200
  • 91e3af54c1 Merge branch 'threadplayingblocks-gmm' PBerger 2013-04-18 15:36:47 +0200
  • 2a8920aeef Updated CMakeLists.txt, added an option for Intel TBB Edited gmm_blas.h, reordered includes PBerger 2013-04-18 15:33:56 +0200
  • f5910e8da1 Added Intel TBB 4.1 Update 3 with Binaries for Windows, Linux and Mac OSX. Updated CMakeLists.txt to include default paths. PBerger 2013-04-18 14:58:10 +0200
  • f513e49084 Almost finished restruction of PRCTL formulas; adapted code (including test cases) to work correctly with the new structure Lanchid 2013-04-17 17:31:48 +0200
  • 3e554514cb Correct formulas Lanchid 2013-04-16 15:29:45 +0200
  • ba4a3807dc New header file for all PRCTL formulas Lanchid 2013-04-16 15:00:32 +0200
  • b64fd7c351 Adapted PRCTL formulas to the new structure Lanchid 2013-04-16 14:45:16 +0200
  • 7e4d09cb01 Added abstract reward operators. Lanchid 2013-04-16 14:32:23 +0200
  • 0e0b5ff688 Added methods to check whether child nodes are set (necessary, as sub classes have no direct access to the pointer) Lanchid 2013-04-16 14:16:15 +0200
  • a1ec7a5d54 Derived PRCTL formula classes from abstract ones Lanchid 2013-04-16 11:56:08 +0200
  • adf16e5f9e Added abstract reward formulas Lanchid 2013-04-16 11:41:41 +0200
  • 195c58e60f Small change of plans: Abstract formulas now use a template parameter for subformulas, so it can be determined later which kind formulas they accept as subformulas. Lanchid 2013-04-16 11:03:38 +0200
  • f1383964f0 Adapted abstract formulas to new structure Lanchid 2013-04-15 16:10:51 +0200
  • 38652f44e4 Restructuring formula classes, part I Lanchid 2013-04-15 14:51:43 +0200
  • bb37bc49f2 Compiling version of PrismParser. gereon 2013-04-10 18:58:59 +0200
  • bdd93d8a6a Merge branch 'master' into CslParser1 Lanchid 2013-04-10 15:32:56 +0200
  • f996829836 Some minor changes in output of formulas Lanchid 2013-04-10 15:05:44 +0200
  • 39ff3240d3 More convenient syntax for time bounded formulas, and respective test cases. Lanchid 2013-04-10 14:56:18 +0200
  • 35baa5ff02 Added parsing of time bounded operators Lanchid 2013-04-10 14:08:48 +0200
  • 96fa125fe4 Added time bounded operators for CSL. Lanchid 2013-04-10 14:04:19 +0200
  • bfd2178ca3 Corrected define guards in some header files Lanchid 2013-04-10 11:09:01 +0200
  • 7e91d5b01e Test cases for CSL parser Lanchid 2013-04-09 16:16:05 +0200
  • 509c1a2b47 Added support for SteadyStateNoBoundOperator into the CSL parser. Lanchid 2013-04-09 15:25:16 +0200
  • 2470c31cb0 Added SteadyStateNoBoundOperator Lanchid 2013-04-09 12:15:21 +0200
  • 08815b8c13 Changed "NoBoundOperator" to "PathNoBoundOperator", as I will implement a "StateNoBoundOperator" now... Lanchid 2013-04-09 11:44:57 +0200
  • 6ff25321d4 First version of CSL parser Lanchid 2013-04-09 11:09:14 +0200
  • 9bc8bb2ca8 Some code style and documentation Lanchid 2013-04-08 16:35:16 +0200
  • 5f9876e4c9 WIP on CslParser: c6060eb Minor changes (mainly improving comments) Lanchid 2013-04-08 16:26:16 +0200
  • c3e3ebf1f3 index on CslParser: c6060eb Minor changes (mainly improving comments) Lanchid 2013-04-08 16:26:16 +0200
  • c7afcecf4a Minor changes (mainly improving comments) Lanchid 2013-04-08 13:50:22 +0200
  • da562bcfc9 Merge branch 'master' into PrctlParser Lanchid 2013-04-08 13:38:57 +0200
  • 895c2b6aad Convenient file parser for PRCTL, and correct reward formula parsing (together with some necessary code for that) Lanchid 2013-04-08 12:21:47 +0200
  • 7dc36875ae Added file groups in CMakeLists.txt such that files are now grouped in IDEs, like, e.g., Xcode. dehnert 2013-04-02 21:20:26 +0200
  • d266d9effe Fixed another bug in sparse matrix. Fixed bug in test. dehnert 2013-04-01 15:36:48 +0200
  • 2b4d26023a Fixed one of the remaining bugs introduced by refactoring. dehnert 2013-04-01 12:47:26 +0200
  • 00b4797948 Further refactoring. Other classes are now adapted to the changes in the sparse matrix class. dehnert 2013-04-01 11:42:29 +0200
  • 9ae177c9b5 Further refactoring. In particular of the matrix class. dehnert 2013-03-28 18:03:05 +0100
  • bb441cdeca Refactored some parts of sparse matrix. dehnert 2013-03-27 17:54:06 +0100
  • 840a9b6e07 Somewhat works now. Still has at least one bug and segfaults afterwards :-) gereon 2013-03-26 20:15:12 +0100
  • e55fca3836 Implemented module renaming. gereon 2013-03-26 18:59:05 +0100
  • 43f11ccc5f Refactoring of modelchecker folder. dehnert 2013-03-26 18:18:07 +0100
  • 7ce537adca Adding testbed for prismparser gereon 2013-03-26 10:05:24 +0100
  • c1986bcc0e Refactored two of the model checker classes. dehnert 2013-03-25 23:14:53 +0100
  • 6c19ddb877 Cosmetics: Trailing whitespaces, space indentation, ... gereon 2013-03-22 19:54:28 +0100
  • 16c08f7d24 Merge branch 'master' into PrctlParser Lanchid 2013-03-21 16:33:59 +0100
  • 0dcebc8ff0 Start of implementing improved file parser for formulas Lanchid 2013-03-21 14:41:21 +0100
  • 836bdb3f1c Created new base class OptimizingOperator. gereon 2013-03-21 10:56:40 +0100
  • 78331dfeea Merge branch 'master' of https://sselab.de/lab9/private/git/storm gereon 2013-03-21 10:38:00 +0100
  • a5ad38a46b Added options for optimizing max/min operator to BoundOperators. gereon 2013-03-21 10:35:46 +0100
  • 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. dehnert 2013-03-17 21:14:49 +0100
  • 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. dehnert 2013-03-17 17:42:45 +0100
  • 49ac740459 Changed a bit, how log messages are processed. gereon 2013-03-16 23:07:49 +0100
  • 525fc7c16f Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2013-03-16 16:57:40 +0100
  • c784de4d03 Added new model checker that uses topological value iteration. However, does not fully work yet. dehnert 2013-03-16 16:57:21 +0100
  • bb6afcb1fd Merge branch 'master' of https://sselab.de/lab9/private/git/storm gereon 2013-03-15 16:25:00 +0100
  • 1f3b172c83 Added a simple module that handles segfaults: print a message and provide a backtrace. gereon 2013-03-15 16:21:12 +0100
  • 17e0e8165a Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2013-03-15 15:56:30 +0100
  • bdf173c315 GraphTransition objects can now be build from the SCC decomposition of a system. dehnert 2013-03-15 15:56:12 +0100
  • e4129c37d9 fixed two bugs in ExplicitModelAdapter. gereon 2013-03-15 15:33:31 +0100
  • 5c25116a24 First version of ExplicitModelAdapter that supports transition rewards. gereon 2013-03-15 15:06:38 +0100
  • d9e833680a Added convenience methods RewardModel::hasStateRewards() and RewardModel::hasTransitionRewards() gereon 2013-03-15 15:06:03 +0100
  • 7dc5324a65 Program returns empty RewardModel and emits error, if invalid model is given. gereon 2013-03-15 15:05:14 +0100
  • 928de19fed Reorganized main routine. Catching errors that made it to the top level. gereon 2013-03-15 14:09:09 +0100
  • 341dc50ab7 Added some better error output for basic parsers using errno gereon 2013-03-15 14:08:37 +0100
  • 8dce5af515 fixed some warnings (comparison between signed/unsigned) gereon 2013-03-15 13:42:44 +0100
  • 75ce91082a Forgot to commit actual cpp file... gereon 2013-03-15 13:34:49 +0100
  • a73ae7aed4 Added new option --debug. gereon 2013-03-15 13:02:53 +0100
  • 2bc32fe3de Cleaned up handling of --verbose, proposing correct use of log levels from now on... gereon 2013-03-15 12:52:20 +0100
  • 5f64fd168b Cleaned up structure of ExplicitModelAdapter. gereon 2013-03-15 13:03:59 +0100
  • f52d4eb7a8 Added new option --debug. gereon 2013-03-15 13:02:53 +0100
  • fd30e8ca25 Cleaned up handling of --verbose, proposing correct use of log levels from now on... gereon 2013-03-15 12:52:20 +0100
  • 5976c9e81d More work for ExplicitModelAdapter gereon 2013-03-14 20:21:11 +0100
  • 2005eb7e73 Added getter routines, so we can retrieve the reward models gereon 2013-03-14 20:20:16 +0100
  • 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. dehnert 2013-03-14 17:49:14 +0100
  • fbf28796b8 Fixed bug in gmm++ model checker: missing vector addition. dehnert 2013-03-14 17:45:50 +0100
  • aee63dcf31 Made the SCC generation during decomposition optional. dehnert 2013-03-14 08:52:37 +0100
  • 961909877a Added iterative version of Tarjan's algorithm for performing SCC decomposition of state-based models. dehnert 2013-03-13 17:53:53 +0100
  • df78cccf84 Fixed bug in graph transitions if initialization was done forward. dehnert 2013-03-13 17:53:11 +0100
  • 726324a37a Added missing model files for consensus example. dehnert 2013-03-12 23:07:52 +0100
  • 01779c9e83 Incomplete version of SCC decomposition of nondeterministic models. dehnert 2013-03-12 23:07:14 +0100
  • 84993d24f8 Add documentation for ExplicitModelAdapter. gereon 2013-03-12 15:08:37 +0100
  • dfd601e126 fixed memory leak in addLabeledTransition and removed now obsolete functions. gereon 2013-03-12 14:01:40 +0100
  • e711d16ebf Changed default initial value for BooleanVariable. gereon 2013-03-12 13:48:12 +0100
  • 52225ecf9c Fixes to buildInitialStates. gereon 2013-03-12 13:47:42 +0100
  • 772c03c070 Added routine to create all initial states. gereon 2013-03-12 13:32:05 +0100
  • 98426aa139 Added new MDP example 'consensus'. Added some test checking to storm.cpp. dehnert 2013-03-12 13:19:14 +0100
  • f787044ece Fixed bug in cloning of negated formulas. dehnert 2013-03-12 13:16:37 +0100
  • 8870fa5f94 Changed all existing examples to 0-based indexing. Also, fixed the tests for these examples. dehnert 2013-03-12 13:15:45 +0100
  • 752dda4252 fixing error with difference operator in freeIdentifier gereon 2013-03-12 12:54:51 +0100
  • 018e7ce056 some minor fixes. gereon 2013-03-12 09:43:58 +0100
  • 17d57e742a Added code for labeled transitions. gereon 2013-03-11 20:55:50 +0100
  • 3464ef20c5 next chunk of code for new ExplicitModelAdapter. gereon 2013-03-11 20:11:15 +0100