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

Commit Graph

  • 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
  • 6d0d7e21c5 First chunk of code for new ExplicitModelAdapter. gereon 2013-03-11 19:20:05 +0100
  • d477d752b1 Updated the Jacobi Solver to make use of the new Adapters, refactored the Matrix conversion. Residuum Calculcation still requires decision by CDehnert PBerger 2013-03-11 02:51:48 +0100
  • 22ce042472 Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2013-03-11 01:32:42 +0100
  • 5cdfba685e Added resources for Usage of Intels Thread Building Blocks PBerger 2013-03-11 01:31:42 +0100
  • 2365b7e6ea Updated gitignore file with a few more useful extensions PBerger 2013-03-11 01:25:11 +0100
  • f1c379bbe3 Moved model checking functionality for MDPs for general superclass such that specialized model checkers only need to implement certain operations. Fixed tests. dehnert 2013-03-09 21:18:36 +0100
  • 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. dehnert 2013-03-09 00:36:39 +0100
  • 4bcb26ab96 Included subset-test in bitvector. dehnert 2013-03-08 16:33:52 +0100
  • 5e3a8a1232 Fixed wrong check for submatrix property of reward matrices. dehnert 2013-03-08 16:21:15 +0100
  • a6ae3d713a Fixed test for nondeterministic model parser. dehnert 2013-03-08 16:06:53 +0100
  • c7f58ed5f5 Modified parsers such that the reward matrices are of the same size as the transition matrices. dehnert 2013-03-08 15:33:32 +0100
  • abae304719 Included tests for model checkers in test suite. dehnert 2013-03-08 15:32:47 +0100
  • 74ad17bc90 Merge branch 'master' of https://sselab.de/lab9/private/git/storm gereon 2013-03-08 12:06:14 +0100
  • cf772688f0 added setter for options in Settings class. gereon 2013-03-08 12:04:42 +0100
  • b7d4d974ec Added a lot of test checking routines to main file. dehnert 2013-03-07 15:29:44 +0100
  • 5b49307eaf Added PRISM files for all of our examples. Added missing reward models. Added result files that indicate the results of PRISM on our examples. dehnert 2013-03-07 15:28:38 +0100
  • aacd8b1fa2 Merge branch 'prismparser' of https://sselab.de/lab9/private/git/storm into prismparser + tiny fixes gereon 2013-03-07 14:00:26 +0100
  • ba49792d29 Perform two runs in PrismParser. gereon 2013-03-07 13:54:13 +0100
  • 38cec01978 Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2013-03-07 04:28:22 +0100
  • 06d78967df Fixed MDP Parser, removed parsing of STATES/TRANSITIONS, see #10 Refactored the Sparse Adapters, see #17 PBerger 2013-03-07 04:20:20 +0100
  • fb7b910f51 Reverted PRISM example to original reward formulation, because we can now deal with transition rewards on MDPs. dehnert 2013-03-06 17:21:18 +0100
  • 3ab71cc08a Added proper treatment of transition based rewards. dehnert 2013-03-06 17:20:26 +0100
  • 7b259120b7 Marked submatrix check in DTMC and sparse matrix as faulty. Needs to be fixed. dehnert 2013-03-06 17:20:01 +0100
  • d38e7eeeb8 Implemented new utility functions and improved existing ones. dehnert 2013-03-06 17:19:31 +0100
  • 69acbdef63 Fixed a few things in the parsers and implemented proper treatment of reward files by these parsers. dehnert 2013-03-06 17:18:54 +0100
  • 2a044d9a7c Changed example files to comply with our current format, i.e., removed header. dehnert 2013-03-06 17:17:29 +0100