Commit Graph

  • adfe82d0d6 Fixed typo to void Matthias Volk 2019-07-04 10:18:12 +0200
  • 944c4a5fc3 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-07-08 09:24:13 +0200
  • 230a2c86d3 Mentioning QVBS as Benchmark source in README Tim Quatmann 2019-07-08 09:23:02 +0200
  • 74f7810233 implemented relative precision Tim Quatmann 2019-07-05 16:57:57 +0200
  • f1536369be DeterministicSchedsLpChecker: Bug fixes, further experiments with upper reward bounds Tim Quatmann 2019-07-05 15:44:48 +0200
  • 549774abc9 Added state remapping in state elimination Alexander Bork 2019-07-05 15:18:15 +0200
  • d0596ecf0c Changed cmake policy for finding packages: Now path specified via -D<Packagename>_ROOT=/path/to/package/ are automatically considered when searching for packages. Tim Quatmann 2019-07-04 11:57:20 +0200
  • 27e65d5669 Added construction of the state remapping for elimination of non-Markovian states in MAs Alexander Bork 2019-07-03 15:44:52 +0200
  • add2a40a62 Integrated results of FDEP conflict search in DFT state space generation Alexander Bork 2019-06-28 15:26:55 +0200
  • fedac853df Fixed gitignore to only exclude build dirs in the root folder. Matthias Volk 2019-06-27 12:18:03 +0200
  • 06c0aff14c Merge branch 'master' into deterministicScheds Tim Quatmann 2019-06-27 11:15:40 +0200
  • b357868a32 GurobiLpSolver: Fixed rounding of integral results. Tim Quatmann 2019-06-06 21:16:08 +0200
  • 5e0aba7509 Testing a few MAX-FLow approximation ideas. Tim Quatmann 2019-06-27 11:15:10 +0200
  • 9780ffeb1e Git ignore for any dir with infix 'build' Matthias Volk 2019-06-27 10:31:45 +0200
  • 47344f9080 Removed unused flat_set includes Matthias Volk 2019-06-25 18:47:17 +0200
  • 6a4c18e4a2 Use custom FlatSet to account for allocator changes in flat_set in Boost 1.70. Boost 1.70 changed the default allocator parameter from new_allocator<T> to void to reduce symbol lenghts. This reverts the default to the old allocator. Matthias Volk 2019-06-25 18:31:02 +0200
  • 1e3686480a is_equal_to_one() is not used in Boost 1.70 Matthias Volk 2019-06-25 17:10:34 +0200
  • 9e6e78c69e Merge branch 'deterministicScheds' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm into deterministicScheds radioGiorgio 2019-06-21 11:34:35 -0700
  • b2d7b1e096 choice labeling radioGiorgio 2019-06-21 11:21:06 -0700
  • 0e9880c9f8 non deterministic transitions based memory structure radioGiorgio 2019-06-21 07:01:23 -0700
  • 3616bdbf13 Added two test cases for the FDEP conflict search Alexander Bork 2019-06-19 11:19:14 +0200
  • e2ef6bc52a Added missing initialization of result vector Alexander Bork 2019-06-19 11:18:31 +0200
  • 589555c75f Moved dynamic behavior computation from builder to DFT and added SEQ and SPARE cases Alexander Bork 2019-06-18 16:07:15 +0200
  • 6db964363e Update for artifact evaluation ATVA Jip Spel 2019-06-18 11:18:58 +0200
  • 4a1f98a0ba Fix segfaults Jip Spel 2019-06-13 12:11:02 +0200
  • 84467267e0 Second try to improve performance for relevant events Matthias Volk 2019-06-07 15:56:08 +0200
  • aa150fc2e3 Extended FDEP conflict search by not considering pairs of FDEPs with static behavior Alexander Bork 2019-06-07 15:36:33 +0200
  • bec75813b1 Added computation of dynamic behavior vector for DFTs Alexander Bork 2019-06-07 15:34:44 +0200
  • 39ec751f8d Removed debugging output Alexander Bork 2019-06-07 15:28:59 +0200
  • 6d6dc7c6a7 EndComponentEliminatorTest: Fixed expected results since the order of end components changed. TimQu 2019-05-24 10:19:53 +0200
  • 187d47d8ac Try to improve performance for relevant events Matthias Volk 2019-06-07 00:11:20 +0200
  • 3a8f352329 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-06-06 21:16:19 +0200
  • e06852689c GurobiLpSolver: Fixed rounding of integral results. Tim Quatmann 2019-06-06 21:16:08 +0200
  • 681665c881 DetSchedsParetoExplorer: Fixed an assertion. Tim Quatmann 2019-06-06 21:15:29 +0200
  • 834bcebd9c LpChecker: Changed end component formulation. Added validity check. Tim Quatmann 2019-06-06 21:14:39 +0200
  • e92966c3e4 ParetoCourveCheckResult: Print approx. value in case of exact checking. Tim Quatmann 2019-06-06 21:13:57 +0200
  • 9bfc7858d0 Added improved upper bound correction Alexander Bork 2019-06-05 16:30:34 +0200
  • 583a880620 Adjusted DFT to SMT conversion to deal with constant failures Alexander Bork 2019-06-05 16:29:27 +0200
  • a0c42fa630 Added debugging messages for transformations Alexander Bork 2019-06-05 16:24:35 +0200
  • d0494d07e6 Get settings only once for takeFirstDependency Matthias Volk 2019-06-03 20:10:22 +0200
  • 09ddd4aef9 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-05-31 19:08:25 +0200
  • bc623d1203 MinMaxLinearEquationSolver: Added a flag 'hasNoEndComponent' that is true if the system is known to have no end components. This decides if policy iteration does require a valid initial scheduler. Renamed the 'hasNoEndComponents' solver requirement to 'hasUniqueSolution' as this is the actual thing we require for, e.g. sound value iteration. Tim Quatmann 2019-05-31 18:58:39 +0200
  • 5467043807 DeterministicSchedsLpChecker: Only consider end components with value zero for all objectives. Tim Quatmann 2019-05-31 11:49:27 +0200
  • 820b48354d Silenced warning Matthias Volk 2019-05-30 17:28:20 +0200
  • 24d0576009 Merge from master Matthias Volk 2019-05-29 18:50:15 +0200
  • 9c28ed990e Use isBasicElement() instead of type Matthias Volk 2019-05-29 18:48:21 +0200
  • 51b210a1d6 Test case for symmetry reduction Matthias Volk 2019-05-29 18:47:37 +0200
  • 08859bd3e6 Fixed bug in computation of symmetry groups. Thanks to Enno Ruijters for pointing out this issue. Matthias Volk 2019-05-29 18:34:05 +0200
  • 0dcb271866 Added assertions for better debugging Matthias Volk 2019-05-29 18:25:04 +0200
  • 3033d5444c Refactoring Matthias Volk 2019-05-29 18:22:24 +0200
  • 1d505d2ee0 Added check if DFT transformation is needed Alexander Bork 2019-05-29 12:32:02 +0200
  • dde18d45eb Added tests for DFT transformator Alexander Bork 2019-05-29 12:14:34 +0200
  • c8ea0f60da JaniBuilder: Fixed several issues that occurred with branch reward expressions over non-transient variables, including GitHub issue #47 Tim Quatmann 2019-05-28 13:22:32 +0200
  • ce9d784c35 QCVBS: Fixed models with empty 'open-paremeter-values' entry. Tim Quatmann 2019-05-28 13:20:21 +0200
  • 8865857f21 Fixed awkward printing of eventually formulas with reward accumulations. TimQu 2019-05-28 13:16:24 +0200
  • 74aa93d23d Moved elimination of non-binary dependencies from builder to the DFT transformator Alexander Bork 2019-05-24 18:30:44 +0200
  • 2779d13d2c Fix for FindDoxygen with CMake 3.12 Matthias Volk 2019-05-24 15:22:40 +0200
  • 12c0a6d72c Added unique constant failure in transformation Alexander Bork 2019-05-24 14:44:42 +0200
  • 69987cc76c Copying of original DFT and changing all constant BEs to be failsafe Alexander Bork 2019-05-24 13:37:46 +0200
  • 8df0a05ab8 Fix assertion Jip Spel 2019-05-24 13:32:55 +0200
  • 2883f81be1 Move settings to separate file Jip Spel 2019-05-24 13:32:36 +0200
  • 49570eb92d Travis: install correct package for dot Matthias Volk 2019-05-24 10:36:53 +0200
  • 6b8997c6ba Merge branch 'master' into storm-pars-analysis-monotonicity Jip Spel 2019-05-24 09:26:03 +0200
  • 719baa58f5 Set some more options for Doxygen Matthias Volk 2019-05-23 20:59:50 +0200
  • b27e7774af Travis: install dot for doxygen generation Matthias Volk 2019-05-23 20:42:49 +0200
  • c8dd748943 DeterministicScheds: Various bug fixes. TimQu 2019-05-23 19:01:24 +0200
  • 19cca3585f PcaaWeightVectorChecker: Initializing weightedPrecision. TimQu 2019-05-23 18:56:35 +0200
  • 4f6822ec1d EndComponentEliminator now provides an entry point where an end component decomposition can be given from outside. TimQu 2019-05-23 18:56:08 +0200
  • 71731e8003 Z3LpSolver: Fixed incremental support. TimQu 2019-05-23 18:55:29 +0200
  • 9b74bc393f Travis: updated scripts and incorporated doxygen deployment Matthias Volk 2019-05-23 14:42:59 +0200
  • f258afa8a2 Added basis for DFT transformator Alexander Bork 2019-05-22 18:29:41 +0200
  • b3cf06d6dd Check in SMT checker that only one BE is constantly failed Alexander Bork 2019-05-22 17:09:18 +0200
  • ca4dceaae1 Added experimental support for constant BEs Alexander Bork 2019-05-22 14:26:51 +0200
  • 31f4683094 Added activation for experimental DFT SMT analysis Alexander Bork 2019-05-22 11:10:38 +0200
  • e06bb99cc4 Changed DEP conflict constraint to avoid double check Alexander Bork 2019-05-22 11:02:47 +0200
  • 51d4652a25 Updated generation of Doxygen documentation Matthias Volk 2019-05-21 14:26:39 +0200
  • da31ca2952 Main page info of Storm for Doxygen Matthias Volk 2019-05-21 14:12:24 +0200
  • 531aa82705 Merge branch 'master' into deterministicScheds TimQu 2019-05-21 10:56:42 +0200
  • 511c2d7987 Changelog: Update. TimQu 2019-05-21 10:56:28 +0200
  • 5e3506a0e1 GeneralSettings: Issue a warning when precision is set via --general:precision and not --precision. TimQu 2019-05-21 10:50:19 +0200
  • 208854bf02 settings: Detect whether an option was set with or without the module prefix. TimQu 2019-05-21 10:48:43 +0200
  • 5d40880883 Flagging a few more options as advanced. TimQu 2019-05-21 10:47:52 +0200
  • b6a5fcfd84 Settings: Do not hard-code executable name in help message. TimQu 2019-05-21 10:12:01 +0200
  • f788a398b5 Merge branch 'master' into deterministicScheds TimQu 2019-05-20 18:59:22 +0200
  • bb0c2282b3 Fixed levenshtein distance TimQu 2019-05-20 18:52:37 +0200
  • f453b2bddd storm-conv: also don't print the help message in case of errors in storm-conv. TimQu 2019-05-20 18:51:57 +0200
  • d6e91183d7 cli: don't print the whole help message when an error occurred during option parsing. TimQu 2019-05-20 18:50:56 +0200
  • 0a02fecd6b settings/modules: Flagged several options as advanced. TimQu 2019-05-20 18:50:16 +0200
  • 8807bb5a0b Settings: Added facilities to flag options as advanced and only display them with '--help all'. TimQu 2019-05-20 17:02:33 +0200
  • e8cd922552 utility/string.h: Added method to check whether a string is considered similar. TimQu 2019-05-20 14:57:57 +0200
  • c5a583a0d1 Merge branch 'master' into deterministicScheds TimQu 2019-05-20 11:44:48 +0200
  • 777d6001a1 SettingsManager: Better error message when an option argument can not be parsed. TimQu 2019-05-20 11:44:06 +0200
  • 1e81d0487d LpChecker: implemented computation of upper reward bounds with end components. TimQu 2019-05-20 11:41:38 +0200
  • baa8a6dbcb Improved conflict search by directly capturing DEPs with same trigger Alexander Bork 2019-05-17 16:56:12 +0200
  • 965c54b76d Fixed error that only one FDEP was required to be active for a possible conflict to be detected Alexander Bork 2019-05-17 15:21:15 +0200
  • 5765824782 Reworked SMT result interface Alexander Bork 2019-05-17 13:33:30 +0200
  • 38ccd51ae1 Added check for conflicts between dependencies in the DFT Alexander Bork 2019-05-17 13:31:46 +0200
  • 80fc8fb56b Fix for error that checkbound may be large than number of Markovian states Alexander Bork 2019-05-17 13:30:34 +0200
  • 0070b7762a Merge branch 'master' into dft_iso Matthias Volk 2019-05-17 11:14:54 +0200
  • 9ebd1af737 Removed unused method again Matthias Volk 2019-05-17 10:35:06 +0200