Commit Graph

  • f6d62d8cf5 Completed integration of master. dehnert 2014-11-27 18:40:26 +0100
  • 08959a6a32 Intermediate commit. dehnert 2014-11-27 18:36:08 +0100
  • fd617efc91 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2014-11-27 18:35:30 +0100
  • 79798e2cb1 Fixed the reward-issue even harder. dehnert 2014-11-27 18:35:09 +0100
  • c4c7794069 Intermediate commit. dehnert 2014-11-27 18:23:17 +0100
  • b07963bd46 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2014-11-27 18:22:24 +0100
  • a7bce9e520 Removed debug output and fixed the reward issue a bit more. dehnert 2014-11-27 18:21:51 +0100
  • 0d2440d4a9 Merge branch 'master' of https://sselab.de/lab9/private/git/storm dehnert 2014-11-27 18:12:49 +0100
  • 7cd0dfe8b0 Fixed an issue regarding the reward model generation. dehnert 2014-11-27 18:12:32 +0100
  • 33994e8285 Merge branch 'master' into parametricSystems dehnert 2014-11-27 17:42:53 +0100
  • 7644a74fcd Removed some superfluous lines in test. dehnert 2014-11-27 17:38:22 +0100
  • 1b4d2a92db Started working on making bisimulation work for models with (state-based) rewards. dehnert 2014-11-27 15:48:36 +0100
  • 370a0ae476 Fixed some issues in bisimulation and added some tests. dehnert 2014-11-27 15:22:47 +0100
  • f8a06b69f5 Fixed a clang-warning related to a throws declaration. dehnert 2014-11-27 11:40:34 +0100
  • 2f20abf47f The user can now select on the command line which reward model of a symbolic model is to be used (as a second [optional] argument to --symbolic). dehnert 2014-11-27 11:33:32 +0100
  • a4a15dd774 Add general setting to enable CUDA on runtime svkurowski 2014-11-27 10:15:30 +0100
  • 00ec9a7db6 Integrate CUDA into buildsystem and add example function svkurowski 2014-11-27 10:15:20 +0100
  • a0b54fbca4 Add src/utility/storm-version.cpp to ignored files svkurowski 2014-11-24 23:04:53 +0100
  • 9fc68a554c Cherry-picked a fix for GCC from branch. PBerger 2014-10-29 22:50:22 +0100
  • 71ceb3f34b Removed some time measurements and fixed simplify functionality. dehnert 2014-10-29 20:57:25 +0100
  • 23c6d14426 Replaced inline conversions to explicit conversions in an attempt to prevent gcc from using uninitialized values when using chrono. dehnert 2014-10-29 20:13:28 +0100
  • 25d87bae06 Builds fine, still no tests yet David_Korzeniewski 2014-10-29 18:34:52 +0100
  • 2e92d66bf3 Cmake scripts for linking mathsat and gmp or mpir which is required by mathsat David_Korzeniewski 2014-10-29 17:00:58 +0100
  • d3721196c4 Typed return value of lambda instead of using 'auto'. dehnert 2014-10-29 16:30:42 +0100
  • 064da9f0aa Added crowds20-5 as parametric model. dehnert 2014-10-29 14:06:31 +0100
  • 1cf8674fa5 Added noexcept Destructors to the exceptions to fix the picky Clang3.5 compiler errors. PBerger 2014-10-27 02:05:41 +0100
  • 77d7555268 Added random order for state elimination. dehnert 2014-10-26 16:58:49 +0100
  • 63daaafc15 Altered some output. dehnert 2014-10-26 16:55:46 +0100
  • f5e6cdb207 Merge branch 'master' into parametricSystems dehnert 2014-10-26 16:48:16 +0100
  • 23c7c9b7d4 Further work on ordering options. dehnert 2014-10-26 16:48:13 +0100
  • aa4836e085 Minor bugfix in bisimulation options. dehnert 2014-10-26 16:47:36 +0100
  • 646f894e92 Merge branch 'master' into parametricSystems dehnert 2014-10-26 16:23:43 +0100
  • ed6f3dae9f Renamed the newly added method. dehnert 2014-10-26 16:23:26 +0100
  • 01adbe0129 Merge branch 'master' into parametricSystems dehnert 2014-10-26 16:22:39 +0100
  • a987233507 Started working on more options for sorting and integrating pure state elimination dehnert 2014-10-26 16:22:36 +0100
  • 2437601a85 Added function to compute distances of states to some other set of states. dehnert 2014-10-26 16:19:53 +0100
  • df7c0f4a95 Weak bisimulation now works for parametric systems. dehnert 2014-10-25 18:53:47 +0200
  • 6185ddc153 Merge master in parametricSystems. dehnert 2014-10-25 18:40:48 +0200
  • f3048d31c2 Small bugfix for bisimulation decomposition. dehnert 2014-10-25 18:40:26 +0200
  • 72c178dd08 Merge branch 'weakBisimulation' dehnert 2014-10-25 18:10:48 +0200
  • e6904dcb21 Renamed bisimulation decomposition class to reflect that now also weak bisimulations can be computed. dehnert 2014-10-25 18:09:50 +0200
  • f90ac5c8c3 First working version of weak bisimulation for DTMCs. dehnert 2014-10-25 17:03:37 +0200
  • 7257bb23c3 Further work on weak bisimulation. Model checking can now be done from tne command line again. dehnert 2014-10-24 18:50:44 +0200
  • 391f3225e4 Added unparameterized NAND example. Further work on weak bisimulation. dehnert 2014-10-24 16:21:39 +0200
  • 5bc593174e Further work on weak bisimulation. dehnert 2014-10-23 20:05:44 +0200
  • eeb859272f Added (non-parametric) brp case study. dehnert 2014-10-23 18:58:51 +0200
  • 56aec18a48 Added bisimulation settings. Further work on weak bisimulation. dehnert 2014-10-23 18:05:51 +0200
  • 97158ee72e Started on weak bisimulation. dehnert 2014-10-22 20:24:50 +0200
  • 1a4d4fd5a7 Added a test I used for finding the SCC Bug. PBerger 2014-10-22 18:56:12 +0200
  • cc9ad6beab Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2014-10-22 17:17:04 +0200
  • eb9c1de59b Added Boost DECLTYPE for MSVC. PBerger 2014-10-22 17:15:09 +0200
  • 3e9c2fc296 Merge master into parametricSystems. dehnert 2014-10-22 12:52:48 +0200
  • 79c9f2c662 Merge master into parametricSystems. dehnert 2014-10-22 12:51:56 +0200
  • 754e168ace Bugfix for bisimulation. dehnert 2014-10-22 12:51:27 +0200
  • d3fc2d8fbf Fixed small but important bug in SCC decomposition that led to wrong results when using MSVC. dehnert 2014-10-22 09:50:48 +0200
  • 94a83e423e Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2014-10-21 22:53:45 +0200
  • ba4b71a353 Added boost define BOOST_RESULT_OF_USE_DECLTYPE for gcc. dehnert 2014-10-21 22:33:18 +0200
  • ec95f8f16d Merge branch 'master' of https://sselab.de/lab9/private/git/storm PBerger 2014-10-21 22:26:56 +0200
  • e54a774e80 Minor spellcheck. PBerger 2014-10-21 22:26:34 +0200
  • 08ac566db2 Corrected typedef. Clang and gcc should now also be fine under Linux. dehnert 2014-10-21 22:11:41 +0200
  • 74351f9884 Switched from const_iterator to iterator in bisimulation to make stdlibc++ happy (libc++ is already happy, though). dehnert 2014-10-21 18:41:25 +0200
  • 3dfc6a7b74 Pimped bisimulation a bit. dehnert 2014-10-21 17:54:18 +0200
  • 0fdda922cd Added more detailed statistics for bisim. dehnert 2014-10-21 14:21:05 +0200
  • 40e07b2ea5 Interpolation and AllSat implemented. David_Korzeniewski 2014-10-20 19:38:54 +0200
  • 582b4a5862 Enabled formula-dependent lumping to speed-up bisimulation. dehnert 2014-10-18 21:46:29 +0200
  • d64279bb77 Stored iterators in bisimulation rather than const_iterators because of gcc. -.- dehnert 2014-10-18 21:03:46 +0200
  • 3d99e35c0d Removed duplicate output of resulting function. dehnert 2014-10-18 19:33:49 +0200
  • 13555cca4d Some 'fixes' here and there. dehnert 2014-10-18 19:20:12 +0200
  • d092d0ca50 a little assertion added sjunges 2014-10-18 03:10:00 +0200
  • 92d27134d8 Merge branch 'parametricSystems' of https://sselab.de/lab9/private/git/storm into parametricSystems sjunges 2014-10-18 02:24:23 +0200
  • 70464128aa Too tired for a message. dehnert 2014-10-18 00:54:23 +0200
  • da8ca2bda9 Merge branch 'master' into parametricSystems dehnert 2014-10-17 11:27:40 +0200
  • 484bbf3e83 Atomic propositions in formulas can now also be surrounded by quotation marks (to be compatible with the PRISM syntax). dehnert 2014-10-17 11:26:14 +0200
  • 6eb846da97 Fixed minor issue in constants comparator. dehnert 2014-10-17 09:28:59 +0200
  • c38ce8cf68 Small fix for autoParser TimQu 2014-10-17 00:21:03 +0200
  • d06c5b4a0c Fixed simplify. dehnert 2014-10-16 15:06:40 +0200
  • cb3c8abe34 Introduced parameter (for coin flip probability) in die example and added it to the list of parametric examples. dehnert 2014-10-16 11:51:27 +0200
  • 02b1564e8c Added some debug output in bisimulation code. dehnert 2014-10-16 11:13:49 +0200
  • 4d20e099bf Added stuff, you know? dehnert 2014-10-16 04:41:08 +0200
  • 7ce1ee2c75 Screw this. dehnert 2014-10-15 22:46:54 +0200
  • 5be3402fe6 Temporary workaround to make it compile with gcc. dehnert 2014-10-15 22:44:37 +0200
  • 60510d07f7 Fixed one parametric model. Added debug output. dehnert 2014-10-15 22:32:30 +0200
  • 9756de998a Bunch of fixes. dehnert 2014-10-15 21:09:06 +0200
  • c2abd9968f Introduced constants comparator in explicit model adapter. dehnert 2014-10-15 13:39:46 +0200
  • 7464f95864 Reenabled bisimulation, because carl now supports operator< for rational functions. dehnert 2014-10-15 10:22:49 +0200
  • 946311469b Merged master and started to fix DirectEncoding.h. Removed some debug output. dehnert 2014-10-14 23:10:06 +0200
  • 843a1d1fdf Added comparator use for checking validity of probability matrices such that only if the value is actually constant it is required to be one. dehnert 2014-10-14 19:03:46 +0200
  • aa6e44a1e2 Some fixes after merge. dehnert 2014-10-14 18:07:52 +0200
  • 113722d55f Merge master into parametricSystems. dehnert 2014-10-14 17:50:45 +0200
  • 1c091d7640 Renamed some classes to indicate that only strong bisimulation can be computed. Added option to start with an initial partition that preserves only certain formulas. Added ConstantsComparator concept that is to be used when constants have to be compared with other constants. dehnert 2014-10-14 17:46:40 +0200
  • ff5902a17c Some fixes. dehnert 2014-10-14 17:03:02 +0200
  • 56edf1e126 Initial MathSat integration. David_Korzeniewski 2014-10-13 19:47:07 +0200
  • 6fa974dcb9 Merge branch 'master' into sparseBisimulation dehnert 2014-10-13 18:50:49 +0200
  • af270dee8a Enabled bisimulation quotienting. dehnert 2014-10-13 17:24:52 +0200
  • 4804ed636d Adapted some code to work with carl. dehnert 2014-10-13 17:24:09 +0200
  • 01e4dd3367 Commit to switch workplace. dehnert 2014-10-13 13:29:46 +0200
  • 0e0027aa8e Further work on sparse bisimulation. dehnert 2014-10-13 11:59:57 +0200
  • bc43ce52ab Eliminated two bugs, more to come. dehnert 2014-10-12 22:51:33 +0200
  • 404b12848e More (and more) work on bisimulation minimization. dehnert 2014-10-12 21:03:36 +0200
  • 8c64a1911c Still bugs in bisimulation minimization. dehnert 2014-10-10 14:24:46 +0200