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

Commit Graph

  • 663e1b0a8f Fixed wrong model name in dot output. dehnert 2013-06-21 11:37:51 +0200
  • 36f1306b4a Now schedulers get computed correctly. dehnert 2013-06-19 20:31:45 +0200
  • 7e74bfbff2 Fixed bug in creation of scheduler, but there is still one really obvious one. Added small MDP example. dehnert 2013-06-19 18:01:41 +0200
  • 89ba67ed47 Using the boost map as actionsToCommandIndexMap on Linux, as emplace() is not implemented for the gcc standard library yet... Lanchid 2013-06-19 15:30:32 +0200
  • c3cc58d43b Revert to old starting point of value iteration. Tests run fine now. dehnert 2013-06-19 10:46:43 +0200
  • 3eb489a2bc Merge branch 'master' into SchedulerGuessingMdp dehnert 2013-06-18 23:27:05 +0200
  • 7095f8e67f Fixed a lot of issues introduced by refactoring. dehnert 2013-06-18 23:13:42 +0200
  • da6de536d4 Merge. dehnert 2013-06-18 17:34:06 +0200
  • abf6f85b63 Intermediate commit to switch workplace. dehnert 2013-06-18 17:30:49 +0200
  • d31db0c637 Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2013-06-18 17:28:22 +0200
  • 42b9072cbf Implemented TBB Parallelization Support into SparseMatrix.h Re-factored Includes in CMake for TBB PBerger 2013-06-18 17:27:09 +0200
  • 69b0c4e236 On my way of implementing scheduler-guessing. dehnert 2013-06-17 21:16:31 +0200
  • 7aa3139b62 Intermediate commit with submatrix computation for scheduler-induced system from MDP. dehnert 2013-06-17 17:56:29 +0200
  • 41db9a8092 Small changes to MDP model checker. dehnert 2013-06-17 19:24:34 +0200
  • 04c7d5ba12 On my way of implementing scheduler-guessing. dehnert 2013-06-17 21:16:31 +0200
  • 4c780a945c Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2013-06-17 20:12:59 +0200
  • cb770020bf Refactored the Jacobi Decomposition PBerger 2013-06-17 20:12:42 +0200
  • eae169727a Fixed a critical bug in the GmmxxAdapter.h PBerger 2013-06-17 20:11:17 +0200
  • c5050313c5 Added model information output for explicit input. dehnert 2013-06-17 17:47:30 +0200
  • f040264660 Intermediate commit with submatrix computation for scheduler-induced system from MDP. dehnert 2013-06-17 17:56:29 +0200
  • 736a9864ac Added model information output for explicit input. dehnert 2013-06-17 17:47:30 +0200
  • 35c23525a1 Removed debug output from AbstractModel.h PBerger 2013-06-17 16:10:47 +0200
  • f05e04495e Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2013-06-17 00:14:11 +0200
  • 0113f5e6dc Added a OS Branch to C-style functions in Parser.cpp PBerger 2013-06-16 23:28:24 +0200
  • 01fd3c18e3 Added move constructors, added move-calls where fitting. PBerger 2013-06-16 20:34:28 +0200
  • 48571cd12c Fixed a regression in the LtlParserTest.cpp PBerger 2013-06-13 22:46:40 +0200
  • 88fbf032e6 Added BASE_PATH to ParsePrismTest.cpp PBerger 2013-06-13 22:43:25 +0200
  • f73342c56a Corrected color output in dot export of models. Fixed minimumOperator stack in SparseMdpPrctlModelChecker a bit, but this needs some further work. dehnert 2013-06-13 22:09:07 +0200
  • c0b454d8b0 Removed debugging output from GmmxxMdpPrctlModelCheckerTest.cpp PBerger 2013-06-13 21:34:13 +0200
  • 4212858013 Fixed a few Rebasing Issues. PBerger 2013-06-13 20:42:23 +0200
  • bf5de84ab9 Refactored the parsing and lineFeeding handling. PBerger 2013-06-13 19:59:13 +0200
  • 2a6ca6b92f Fixed a dimension bug in the labeling Parser PBerger 2013-06-13 19:57:31 +0200
  • 484c4e8151 Added more debugging output into the MDP Model PBerger 2013-06-13 17:32:32 +0200
  • c1afe65d5c Fixed an initializer-list ordering PBerger 2013-06-13 16:05:54 +0200
  • 0f7e2835e3 Added an assignment constructor to the SparseMatrix.h Now fixed this "constructor" to be a real operator and compile. PBerger 2013-06-13 15:43:40 +0200
  • 0051aec174 Added an assignment constructor to the SparseMatrix.h PBerger 2013-06-13 15:35:26 +0200
  • 767680537e Added missing namespaces to Parser functions PBerger 2013-06-13 15:35:07 +0200
  • fb3209dfc3 Added missing template parameters in the abstract models PBerger 2013-06-13 15:08:07 +0200
  • 22f00bc95e Reordered elements of SparseMatrix.h PBerger 2013-06-13 14:59:59 +0200
  • 83d0e7d6af Refactored LineEndings Handling. Added missing default cases. PBerger 2013-06-13 14:55:34 +0200
  • 1d2717c69a Added Debugging output to GmmxxMdpPrctlModelCheckerTest.cpp PBerger 2013-06-12 23:50:29 +0200
  • 78184f9537 Added a Hash Class in the Utility Namespace. Added a function getHash() which returns a size_t to most of the used Models and Containers. PBerger 2013-06-12 23:50:09 +0200
  • 5be52118ba Fixed issues with the refactored parser interface and move semantics PBerger 2013-06-12 21:05:32 +0200
  • 8a8a0c1ce8 Fixed a bug in the DeterministicModelParser.cpp, the wrong file was passed into the Parser PBerger 2013-06-12 21:05:03 +0200
  • 2fc666892d Added multi plattform new-line handling for parsers PBerger 2013-06-12 21:04:32 +0200
  • d596f126b2 Fixed/added missing Copy Constructors for Models and the SparseMatrix PBerger 2013-06-12 21:03:53 +0200
  • 531293955a Added std::move() calls in SparseMdpPrctlModelChecker.h PBerger 2013-06-12 21:02:30 +0200
  • 6ef6b139c9 Fixed a missing control path in the ExplicitModelAdapter.cpp PBerger 2013-06-12 21:02:15 +0200
  • b978a4d311 Added more move constructors. PBerger 2013-06-09 23:48:03 +0200
  • 89909fe8dc Edited all Parsers to lose its class. Modified many classes to provide a reference-constructor. Fixed a few bugs in Tests. PBerger 2013-06-07 17:30:11 +0200
  • e79a4abc3e Added Windows MSVC2012 x64 Binaries for GTest (cherry picked from commit 39cd7d56cd) PBerger 2013-06-06 22:50:12 +0200
  • 750c829f7a Fixed CUDD Project Setup. Added Windows MSVC2012 x64 binaries for CUDD PBerger 2013-06-06 22:04:57 +0200
  • 7d82a44d53 Added Windows Binaries from VC2012 x64 to Repo. Will be cherry-picked back to master. (cherry picked from commit 696cbb2d9e) PBerger 2013-06-06 21:37:42 +0200
  • 02d0f9e1ea Added a Win64 Project for LTL2DStar Edited same sources to compile in windows PBerger 2013-06-06 21:09:23 +0200
  • 7a758abd3b Corrected syntax on Pointer-Sign position. PBerger 2013-06-05 17:49:40 +0200
  • 50f81e10db Added override Keyword to visit() functions. PBerger 2013-06-05 17:47:14 +0200
  • f4050e5b18 Edited Parsers, re factored interface into a single function without an encapsulating class. Warning, this is work in Progress and not yet compiling. PBerger 2013-06-05 17:11:58 +0200
  • 68c27f99ef Mass-added Keyword "override" PBerger 2013-06-05 17:10:46 +0200
  • 405094f768 Refactoring on Parser, introduced new keyword "override" PBerger 2013-05-29 20:46:47 +0200
  • e7601eb7b7 Included scheduler generation in model checking procedure for MDPs. dehnert 2013-06-13 19:11:10 +0200
  • 913bd173c3 Fix: local indices of variables are now treated correctly. dehnert 2013-06-13 11:29:09 +0200
  • fabf662edd Added dot output for both deterministic and nondeterministic models. Fixed iterator bug in sparse matrix. dehnert 2013-06-12 17:15:37 +0200
  • 4dadedf39d Added methods to retrieve module index by variable name from IR. This fixes an issue in the symbolic adapter. dehnert 2013-06-12 11:11:24 +0200
  • ac8e01a5fa Merge branch 'master' into prismparser_refactorings dehnert 2013-06-11 13:49:16 +0200
  • dd317bf6a4 Fixed issues with PRISM parser. dehnert 2013-06-11 13:43:50 +0200
  • 9505f553dd Added copy-constructors for all IR classes. TODO: make tests run again... dehnert 2013-06-10 23:28:49 +0200
  • 23f25beb27 More fixes. Still TODO: copy constructors for IR classes. dehnert 2013-06-10 22:14:51 +0200
  • a0ee0b46c7 Fixed minor bug. dehnert 2013-06-10 21:36:39 +0200
  • 7b8b1ebd4f Further refactoring of IR classes. dehnert 2013-06-10 21:25:10 +0200
  • e30c386f23 On my way of splitting header/source files in IR to make forward-declaration easy. dehnert 2013-06-10 16:21:32 +0200
  • 8abc703f6a Further refactoring of IR and PRISM parser. dehnert 2013-06-10 12:06:01 +0200
  • 82430ca12d Fixed dummy returns in VariableState.cpp. dehnert 2013-06-09 22:53:10 +0200
  • 22ddf9c5be On my way of cleaning up Gereon's mess. :P dehnert 2013-06-09 22:37:11 +0200
  • ab8585656c Started to refactor PRISM parser. dehnert 2013-06-07 18:18:06 +0200
  • bba72e452b Fixed off-by-one for our matrix-vector multiplication. dehnert 2013-06-07 18:15:22 +0200
  • 16e1e2cedf Fixed wrong dimension bug in MDP model checkers. dehnert 2013-06-06 18:48:32 +0200
  • 81025757f8 Minor fix (Changed function name) Lanchid 2013-06-06 14:50:40 +0200
  • 65ebe3dcc3 Enabled check whether initial states are contained in the set of states for which the probability/reward values could be determined via graph algorithms to shorten computation times if possible. dehnert 2013-06-05 20:52:44 +0200
  • f44f0ce410 Cleaned interfaces of models from std::shared_ptr. Improved some code in graph utility. dehnert 2013-06-05 13:13:45 +0200
  • 4b68cb7bbf Removed all references to LTL2DStar in Master branch Lanchid 2013-06-05 14:04:09 +0200
  • 669feb03bc Merge branch 'master' into LtlParser Lanchid 2013-06-05 11:41:23 +0200
  • 30e69ee4d4 Corrected CMakeLists.txt (from merge) Lanchid 2013-06-05 11:10:47 +0200
  • c8081c4d34 Fixed wrong step-bounded backward search. dehnert 2013-06-04 19:34:32 +0200
  • 0ee248e88c Merge branch 'master' into LtlParser Lanchid 2013-06-04 18:42:23 +0200
  • 97a3fc7fa0 Provided test class for ltl2dstar, to avoid copypasting the code to construct the labeling in each test. Lanchid 2013-06-04 18:13:37 +0200
  • 1e5de29eec Conversion adapter to create LTL2DStar formulas out of "ours" Lanchid 2013-06-04 17:46:38 +0200
  • 14fae4883a Added prob 0/1 precomputation for bounded-until model checking for DTMCs. The version for MDPs seems to perform worse: needs to be investigated. dehnert 2013-05-30 23:54:43 +0200
  • a619303a1a Removed unnecessary command line utilities. dehnert 2013-05-30 15:23:43 +0200
  • 64b883f695 Some cleanup in storm.cpp. Refactored and commented the utility module for vector operations. dehnert 2013-05-30 11:28:26 +0200
  • 94a717941c Removed const declarations for the vistor callbacks, as the visitor should be able to store information on the formulas during the process. Lanchid 2013-05-29 16:19:34 +0200
  • 1301025bea Added visitor pattern for LTL formulas (which hopefully will make the implementation of an adapter to ltl2dstar easier) Lanchid 2013-05-29 15:22:19 +0200
  • a96380259a Added ltl2ba and ltl2dstar to ressources Lanchid 2013-05-28 15:29:17 +0200
  • ec91dcbe2e Merge branch master into LTLParser Lanchid 2013-05-28 14:14:42 +0200
  • 21e6ee70b9 Added static asserts to ensure that sub formulas are formulas ;) Lanchid 2013-05-28 12:03:16 +0200
  • cd9e2ba549 Some minor cleanups, added lot of documentation in prismparser gereon 2013-05-27 13:22:44 +0200
  • cb14f2e771 Made choiceIndices work in ExplicitModelAdapter, added code to somehow use --symbolic (parse model, show model information) gereon 2013-05-23 17:52:13 +0200
  • 6d144f3d99 Merge branch 'master' of https://sselab.de/lab9/private/git/storm gereon 2013-05-23 13:23:27 +0200
  • ad86c22249 Replaced positional arguments by --explicit and --symbolic. gereon 2013-05-23 13:22:44 +0200
  • cae3d6cc6a Renamed PrismParser directory to prismparser. dehnert 2013-05-22 15:18:59 +0200
  • cd3706707d Corrected test names and corresponding file names. dehnert 2013-05-22 15:01:38 +0200