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

Commit Graph

  • 2cc5b6e080 Added Z3ExpressionAdapter to translate IR expressions to the Z3 format. Improvements to label-/command set generators. Disabled MILP-call from main(). dehnert 2013-10-04 19:48:43 +0200
  • bd3edb5f8b Naive enumeration of command set works. dehnert 2013-10-04 15:10:24 +0200
  • a7dda9131b Intermediate commit to switch workplace. dehnert 2013-10-04 11:28:52 +0200
  • e3234b54f3 Step towards minimal command generator using MaxSAT and model checking. dehnert 2013-10-03 23:04:10 +0200
  • f33bf69daa Another merge. dehnert 2013-10-02 13:39:56 +0200
  • 2e570f6311 Merge. dehnert 2013-10-02 13:38:49 +0200
  • 623d9ee7c4 Added capability to restrict model to certain action choices. dehnert 2013-10-02 11:00:14 +0200
  • 121cbb7610 ExplicitModelAdapter now labels updates for synchronizing commands correctly. dehnert 2013-10-01 19:52:36 +0200
  • a45e9423b8 Sparse matrix can now also be used without knowing the number of rows/columns/nonzeros upfront. Adapted ExplicitModelAdapter to use that capability to not explore the state space twice. Added support for Z3 to CMakeLists.txt. Added correct submatrix checks for transition rewards in MDPs. Extended a test for the ExplicitModelAdapter a bit. dehnert 2013-10-01 17:31:08 +0200
  • c82efc1f41 Minor fix. dehnert 2013-10-01 10:51:43 +0200
  • f7293ee4a9 Merge branch 'master' into MinimalCommandCounterexample dehnert 2013-10-01 10:32:22 +0200
  • 129fd296d6 Several fixes. MinimalLabelSetGenerator can now treat labeled values. dehnert 2013-09-30 19:09:35 +0200
  • a99bdf1b17 Switched to more elegant solution to query initial states of a model. dehnert 2013-09-30 18:24:27 +0200
  • 84f1b192b4 Added globally unique indexes to updates in IR. Finalized support for labeled values in ExplicitModelAdapter. Modified tests to comply with the new usage of ExplicitModelAdapter. dehnert 2013-09-30 16:39:11 +0200
  • 61e12601ed Further step towards refactored ExplicitModelAdapter. dehnert 2013-09-29 20:37:20 +0200
  • a08a403eec Ongoing refactoring work on ExplicitModelAdapter. dehnert 2013-09-27 14:39:36 +0200
  • e2b0c4f1aa Started refactoring ExplicitModelAdapter to finally make it nice. dehnert 2013-09-26 17:22:58 +0200
  • fdfb8ecc97 Minor fixes. dehnert 2013-09-26 14:46:15 +0200
  • f39fb24f65 Removed pointers from Model Checker Interface (and callback methods in formulas). From now on, the results are returned in form of an object. Because of the existing move semantics for the types in question, this does not come at a performance penalty. dehnert 2013-09-26 13:16:07 +0200
  • 2aa8d11101 Removed unnecessary option. Fixed performance tests. dehnert 2013-09-25 12:20:27 +0200
  • d8e85ec071 Removed guessing of initial scheduler as this was just an idea and not meant to be in master at this point. dehnert 2013-09-24 18:49:49 +0200
  • 11cc7fc6bc Introduced a new Object called InternalOptionMemento to handle required settings for tests which auto-reset after the test is done Refactored many constants to be of type ull where required Edited all tests that used the set() function of the Settings to make use of the new InternalOptionMemento PBerger 2013-09-24 17:30:18 +0200
  • 0f4e51e646 Changed notation to query option slightly. dehnert 2013-09-24 10:26:45 +0200
  • 79c40126f3 Fixed a bug in the SparseMatrix.h where the multi threaded implementation would crash sometimes Added a new definition to CMakeLists.txt for MSVC as to undefine the MIN/MAX macros PBerger 2013-09-24 01:48:27 +0200
  • c242dcbd97 Refactored CMakeLists.txt for better editing and overview Refactored all Defines for Gurobi, TBB, etc into the storm-config file Fixed a missing cast int SymbolicModelAdapter.h Fixed changed iterator structures in SparseMatrix.h Fixed bugs in CuddUtility.cpp where a 64bit shift was executed on a 32bit literal (1 should be 1ull) Fixed a Type Error in graph.h PBerger 2013-09-24 00:22:34 +0200
  • b546118c98 Gurobi output now only gets printed to standard out and logfile if --debug has been set. dehnert 2013-09-23 18:15:00 +0200
  • 5d76fd5ba0 Disabled model output to file. dehnert 2013-09-23 17:56:45 +0200
  • 014be3cb39 MinimalLabelSetGenerator can now handle multiple initial states properly. dehnert 2013-09-23 17:54:46 +0200
  • 6fca000233 Removed defines.hxx from source tree Added a new include path for storm as to include the generated out-of-source defines.hxx PBerger 2013-09-23 16:48:42 +0200
  • 6e41ee360d Fixes to several problems with gcc. dehnert 2013-09-23 15:32:54 +0200
  • e4e4c783da Readded defines.hxx. dehnert 2013-09-23 15:24:38 +0200
  • 1934bdd801 Disabled MinimalLabelSetGenerator test code in storm.cpp and fixed minor issue in ExplicitModelAdapter that treated constant strings incorrectly. dehnert 2013-09-22 22:03:50 +0200
  • 6125898e69 Merge branch 'MinimalCommandCounterexample' of https://sselab.de/lab9/private/git/storm into MinimalCommandCounterexample dehnert 2013-09-22 21:49:37 +0200
  • cb1c3965ba Removed a wrong and unnecessary validation function from ExplicitModelAdapter.cpp PBerger 2013-09-22 21:48:09 +0200
  • 8d59e1c91e Removed an config input file from the repo PBerger 2013-09-22 21:47:37 +0200
  • b782288833 Merge branch 'MinimalCommandCounterexample' of https://sselab.de/lab9/private/git/storm into MinimalCommandCounterexample dehnert 2013-09-22 21:45:33 +0200
  • 0ac3efb082 Finished merge of CMakeLists.txt dehnert 2013-09-22 21:45:05 +0200
  • 4b3d4a7c11 Removed buggy logging in setup-routines PBerger 2013-09-22 21:42:17 +0200
  • fe3012f69d Merge branch 'master' into MinimalCommandCounterexample dehnert 2013-09-22 21:17:05 +0200
  • f1c800f382 Minor fixes to MinimalLabelSetGenerator and AbstractModel. dehnert 2013-09-22 21:04:07 +0200
  • ef850b213b Added the option -ftemplate-depth=1024 for Clang PBerger 2013-09-21 22:12:03 +0200
  • 3a38abec6f Removed unnecessary names for unused variables in the ExplicitModelAdapter.cpp PBerger 2013-09-21 22:10:37 +0200
  • f7a7ea8383 Fixed the StringValidator for the constants option Fixed a bug in the MinimalLabelSetGenerator.h where a non static variable was initialized Added the new constants option in storm.cpp PBerger 2013-09-21 22:08:52 +0200
  • ef8008d6e3 Merge branch 'MinimalCommandCounterexample' of https://sselab.de/lab9/private/git/storm into MinimalCommandCounterexample PBerger 2013-09-21 21:12:33 +0200
  • b79fde1a42 Added a definition for GTest to build with MSVC on Windows PBerger 2013-09-21 02:27:30 +0200
  • 59ca0373a5 Removed a template specialization for std::less with the SafraTree. PBerger 2013-09-21 02:06:35 +0200
  • 8e93238e18 Fixed a stray void* to char* conversion (still trying to please Clang) PBerger 2013-09-21 01:58:36 +0200
  • 08a30c6aad Patched types for the strange version of qsort included in CUDD PBerger 2013-09-21 01:51:25 +0200
  • 1a4a32a1c5 Next take at static modifiers for Clang. PBerger 2013-09-21 01:41:17 +0200
  • 1d6b6c83e0 Fixed header/implementation mismatches which Clang detects and can not ignore. This might introduce bugs, but it was my best guess as to what atrocity the author was trying to to there. PBerger 2013-09-21 01:38:42 +0200
  • c4c690908a Removed "static" modifier from functions which are defined as EXTERN in a header file PBerger 2013-09-21 01:24:34 +0200
  • 11198c648c Fixed include pathes for CUDD in CMakeLists.txt Added a variadic macro for MSVC since the PrismGrammar makes use of emplace magic Patched log4cplus to disable unicode from a parent project "Patched" various serious issues in CUDD, where size_t <-> int problems and forced int to bool conversions piss of the compiler. And me. PBerger 2013-09-21 00:48:49 +0200
  • 659df778dd Refactored all in-repository includes to make use of CMakes great features PBerger 2013-09-20 19:14:14 +0200
  • c9d3012adb Removed the superfluous main file from ltl2dstar, so that CMake will not compile it and include its main() in Storm PBerger 2013-09-20 19:13:04 +0200
  • d0498254f0 Updated gtest from version 1.6.0 to 1.7.0 PBerger 2013-09-20 19:08:29 +0200
  • 7812c6639e Added missing obj/cuddObj files PBerger 2013-09-20 19:03:21 +0200
  • d42a2151c5 Added a CMakeLists.txt for CUDD Moved CUDD sources to src/ directory Fixed a lot of signed/unsigned mismatches in CUDD Removed the extra version for Win32, is now merged with the other source PBerger 2013-09-20 18:17:14 +0200
  • 8f3182b520 Working (and most importantly refactored) version of MinimalLabelSetGenerator. dehnert 2013-09-20 16:33:01 +0200
  • d743e222f7 Refactored ltl2ba to compile under windows Added a CMakeLists.txt for ltl2ba PBerger 2013-09-20 15:55:31 +0200
  • 1b60b08ca6 Deleted the obsolete boost sources from ltl2dstar Removed an unneeded SamplePlugin.cpp from ltl2dstars source tree Added a CMakeLists.txt build file for ltl2dstar Updated fdstream.hpp and TempFile.hpp to use non-outdated POSIX functions on windows PBerger 2013-09-20 15:29:36 +0200
  • e0ee4ea2fd Implemented a method for generating a choiceLabeling based on the stateIds PBerger 2013-09-20 14:31:29 +0200
  • fad8371d7a Added an Option for the Constants of the ExplicitModelAdapter Implemented very basic validation of the input PBerger 2013-09-20 14:27:16 +0200
  • 3c22a669af On my way of refactoring the minimal label set generator. Intermediate commit: does not compile, so be careful when pulling. dehnert 2013-09-19 22:45:37 +0200
  • 5ff550194c Minimal label set generator now works for coin example, yay dehnert 2013-09-19 17:32:20 +0200
  • 735cd2013f Further work on minimal label set generator. Intermediate commit. dehnert 2013-09-19 14:20:21 +0200
  • 1a20ce7f33 A few additions to the minimal label set generator. dehnert 2013-09-17 18:37:12 +0200
  • 84e7061a6d Undefined constants are now undefined again after the explicit adapter has created the model (using specific constant values). dehnert 2013-09-16 21:39:11 +0200
  • 816f12f2f6 Added global variables to string output of probabilistic program. Added number of choices to model information output of nondeterministic models. dehnert 2013-09-16 20:31:48 +0200
  • 3aeb755e61 Bugfix: undefined constant expressions for the same constant now share a common structure internally that defines their value and definedness. dehnert 2013-09-16 20:21:24 +0200
  • 12a92fc6ee Several fixes and additions to IR. Modifications to CMakeLists.txt of log4cplus to enable proper compilation under Mac OS. Fixes to coin2.nm. Added global variables to grammar and IR. Established basis for defining undefined constants of the model. Started to write MinimalLabelSetGenerator. dehnert 2013-09-16 18:57:11 +0200
  • 47f7bf875d Fixed static conversion bugs in the IR section PBerger 2013-09-16 02:04:08 +0200
  • 85e674266d Added support for linking against Gurobi to CMakeLists.txt. Prepared work on the generator of minimal label sets. dehnert 2013-09-15 19:46:34 +0200
  • eeb700167b Fixed failing tests. dehnert 2013-09-15 11:03:18 +0200
  • 1978b39d49 Removed static libs for gtest from repository. dehnert 2013-09-15 10:45:37 +0200
  • 947581dd25 Refactored and fixed bugs in explicit model adapter. Added support for labeling of choices of a model. The explicit model adapter uses that functionality to label each choice with the involved PRISM commands. dehnert 2013-09-15 10:39:48 +0200
  • bf732ad4c4 Removed static libraries from repository. dehnert 2013-09-15 09:16:04 +0200
  • 3697f5819d Merge branch 'settings' of https://sselab.de/lab9/private/git/storm into settings PBerger 2013-09-15 01:47:33 +0200
  • 64c4a0c7c3 Fixed log4cplus CMakeLists.txt to default to C++11 on GCC and Clang Added libgtest to repository Added libltl2dstar.a to repository PBerger 2013-09-15 01:45:19 +0200
  • d7f9d1d3c6 Added log4cplus libraries for linux, x86_64 build with clang and its defines.hxx PBerger 2013-09-14 17:29:42 +0200
  • 8bd449b83e Merge branch 'settings' of https://sselab.de/lab9/private/git/storm into settings PBerger 2013-09-14 16:20:08 +0200
  • f4c9fc0825 Fixed a dereferencing typo in GmmxxAdapter.h PBerger 2013-09-14 16:19:47 +0200
  • edeedd2bed Added ConversionHelper.h to single out the needed no-strict-aliasing target Replaced a few "auto" variables as GCC4.7 fails to infer the correct type PBerger 2013-09-14 15:56:49 +0200
  • 82053c4822 Fixed missing suffix for static library of log4cplus. dehnert 2013-09-12 22:23:16 +0200
  • 158430418e Replaced boost integer mask includes with cstdint Reimplemented Gmm conversion with in place constructors PBerger 2013-09-12 20:36:47 +0200
  • df21fbbbde Added new version of Log4CPlus, updated from v1.1.0 to v.1.1.2-rc2 Updated CMakeLists.txt, included new Log4Cplus PBerger 2013-09-09 05:03:51 +0200
  • a30f570c2a Added logging to all Settings classes Removed unnecessary instance variables in the Settings.h PBerger 2013-09-08 02:45:35 +0200
  • 58ff007654 Fixed the Settings structure Fixed the standard settings to comply with the infrastructure PBerger 2013-09-07 16:03:04 +0200
  • 938959de56 Added a set() Method to the Settings.h for the Tests Moved all standard options into a helper class/compilation unit as to reuse it in the Tests Moved the MaxIteration set call in the tests PBerger 2013-09-07 03:30:21 +0200
  • e69c9f1962 Added all options from StoRM Rewrote all calls to the Settings instance with the new Syntax Implemented new ArgumentValidators.h PBerger 2013-09-07 02:16:08 +0200
  • d5a9656cac Removed OptionsAccumulator.h and merged it into Settings.h Implemented some helper functions and convenience accessors PBerger 2013-09-06 18:13:04 +0200
  • bde10b750e Added my initial implementation of Settings PBerger 2013-09-05 23:32:25 +0200
  • dc5ddca9d7 Fixed another bug in explicit model adapter. dehnert 2013-08-19 14:56:33 +0200
  • 0473d1a757 Fixed a lot of issues with the IR and the explicit state space generator. dehnert 2013-08-19 14:17:50 +0200
  • 6af5ce4860 Another container for which gcc does not support emplace yet... Lanchid 2013-06-30 09:52:37 +0200
  • 973e51bacb Beautified the code a bit. dehnert 2013-06-28 11:15:16 +0200
  • b36b460a4e Added some comments to scheduler guessing. dehnert 2013-06-28 10:28:59 +0200
  • d168b1848e Made GMRES and LSCG solution methods work for linear equation solving. Some further work on scheduler guessing. dehnert 2013-06-26 16:25:20 +0200
  • 15542d46da Changes: * included small consensus example * made backward-transition generation more beautiful and versatile * included Dijkstra search for most probable paths * included first rough scheduler-guessing (there's room for improvement though) dehnert 2013-06-25 22:38:43 +0200
  • 5776b207c3 Changed to new cleaner iterator for matrix. dehnert 2013-06-23 16:42:27 +0200
  • 36543de851 Started trying to implement a more clean iterator solution for sparse matrix. dehnert 2013-06-21 23:16:26 +0200