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

Commit Graph

  • ca591dff9f better error message Sebastian Junges 2020-08-20 10:49:15 -0700
  • 6eeecaf7f8 Fixed compatibility with older boost versions. TimQu 2020-08-20 10:23:27 +0200
  • 3d9b53723b OVI: added case where the guessed upper bound corresponds to the fixpoint. Tim Quatmann 2020-08-19 17:17:14 +0200
  • 2273fda7c9 ovi helper: Take the relative/absolute precision and the maximal iteration count as a parameter because otherwise it is not clear whether we should take this information from the NativeEnvironment or the MinMaxEnvironment. Tim Quatmann 2020-08-19 16:53:21 +0200
  • 5a76128e3f Removed DdType::None because there is no use for this anymore. Tim Quatmann 2020-08-19 16:07:30 +0200
  • f94d45483e Use the new model representation enum in the model checking helpers. Tim Quatmann 2020-08-19 16:06:09 +0200
  • cf20e340de Added a new enum that describes the model representation (sparse, dd with sylvan, dd with cudd). Tim Quatmann 2020-08-19 16:05:39 +0200
  • d0cc24ae51 Updated Changelog. Tim Quatmann 2020-08-19 15:26:37 +0200
  • a6c5225f31 Added test case for scheduler generation for LRA Property Tim Quatmann 2020-08-19 15:26:23 +0200
  • 3e79e6e5ea LraMdp Test: Added an additional test case. Tim Quatmann 2020-08-19 15:26:04 +0200
  • b6fc409dd8 Merge branch 'modelchecker-helper-refactor' Tim Quatmann 2020-08-19 14:06:22 +0200
  • fd77b71084 OVI helper: fixed spacing in source code, changed two while loops to for loops Tim Quatmann 2020-08-19 14:04:53 +0200
  • 585dd675d1 OviSettings: Made help message a bit shorter Tim Quatmann 2020-08-19 14:02:02 +0200
  • 84a5faef62 Merge branch 'ovi-implementation' Tim Quatmann 2020-08-19 12:10:58 +0200
  • 6f6773f8ca PgclParser: Do not reject variable names with a keyword as proper prefix. (fixes GitHub issue #84) Tim Quatmann 2020-08-19 12:05:21 +0200
  • 87ef49a2d0 Do not show a conversion warning if no conversion happens. Tim Quatmann 2020-08-19 12:02:43 +0200
  • eb02d56b69 LraViHelper: Changed type of toSubModelStateMapping to std::map, which is faster in this scenario. Also fixed some awkward const&'s Tim Quatmann 2020-08-19 12:01:03 +0200
  • 5f119ed149 Fixed weird error when invoking Storm with portfolio engine and no input model. Tim Quatmann 2020-08-12 17:10:14 +0200
  • 923f779a09 explicit-state-lookup, for finding states in a model based on the variable assignment Sebastian Junges 2020-08-17 21:09:38 -0700
  • 584fbf23c1 add assertion for module indices in second Stefan Pranger 2020-08-13 18:49:53 +0200
  • e0a71f331c do not clear moduleToIndexMap for second run Stefan Pranger 2020-08-13 11:42:46 +0200
  • 321bb9121f Merge branch 'master' into modelchecker-helper-refactor Tim Quatmann 2020-08-12 17:12:36 +0200
  • 7e18fbf3c2 Fixed weird error when invoking Storm with portfolio engine and no input model. Tim Quatmann 2020-08-12 17:10:14 +0200
  • 7e6b0c27c3 Merge remote-tracking branch 'refs/remotes/origin/master' into modelchecker-helper-refactor Tim Quatmann 2020-08-12 16:00:45 +0200
  • b7883a8ef1 Used the new SparseMatrixBuilder::addDiagonalEntry to simplify some of the LRA code. Tim Quatmann 2020-08-12 15:59:50 +0200
  • 6f59c4f3eb SparseMatrixBuilder: Added a function to easily add diagonal entries. Tim Quatmann 2020-08-12 15:58:41 +0200
  • 8627cde4dc Removing old LRA code in old helpers. Tim Quatmann 2020-08-12 10:50:31 +0200
  • 38af6357d7 Using the new hybrid infinite horizon helper in the model checkers Tim Quatmann 2020-08-12 10:43:49 +0200
  • f8d4fd8862 New utility function for exchanging informations between deterministic helpers. Tim Quatmann 2020-08-12 10:42:26 +0200
  • 5eb2bcc71f Fixing bad cast exception Tim Quatmann 2020-08-12 10:41:15 +0200
  • 64b9c176e7 symbolic Ctmc: Added method to compute the probability matrix. Tim Quatmann 2020-08-12 10:31:31 +0200
  • 9c82fe7b0d Making hybrid infinite horizon helper ready for deterministic models. Tim Quatmann 2020-08-12 10:30:45 +0200
  • 19f6552b05 Fixed insufficient precision in CTMC LRA test Tim Quatmann 2020-08-11 16:56:48 +0200
  • 959e035153 Use the new infinite horizon helper for sparse ctmc and dtmc. Tim Quatmann 2020-08-11 16:56:01 +0200
  • 462ce5dce3 Ctmc: added a method that returns the probabilistic transition matrix. Tim Quatmann 2020-08-11 16:54:43 +0200
  • d92905a7c3 LraVi: Fixed uninitialized bool member. Tim Quatmann 2020-08-11 16:54:04 +0200
  • ef2448410b Fixed selecting wrong reward kind Tim Quatmann 2020-08-11 16:53:41 +0200
  • c674de5893 Deterministic infinite horizon: Added gain-bias and lra-distribution based solution methods Tim Quatmann 2020-08-11 16:53:05 +0200
  • 1187981b5d fixes in creation of dice expressions Sebastian Junges 2020-08-10 20:33:59 -0700
  • 72813a9774
         Revelant DFT events are not part of symmetries Matthias Volk 2020-08-10 18:54:00 +0200
  • 693237a304
         Improved hashing for BEColourClass Matthias Volk 2020-08-10 18:44:29 +0200
  • f7930d22b0
         Fixed typo which lead to wrong symmetries for voting gates Matthias Volk 2020-08-10 18:43:07 +0200
  • e933df1fc1
         Fixed parsing of ' in GalileoParser Matthias Volk 2020-08-10 18:41:14 +0200
  • 0cc2b1c749 First version of sparse infinite horizon helpers for deterministic and nondeterministic models. Tim Quatmann 2020-08-10 18:38:45 +0200
  • 6ecbf113b3 Adding template instantiation for deterministic LRA VI Tim Quatmann 2020-08-10 18:38:14 +0200
  • f145aa2c94 Adding includes for component utility. Making functions inline. Tim Quatmann 2020-08-10 18:37:45 +0200
  • 572e7ace9d Moving some includes to the header file Tim Quatmann 2020-08-10 18:35:58 +0200
  • f316bb9d38 Added missing include. Tim Quatmann 2020-08-10 18:35:12 +0200
  • 05d2af2bfd Fixing destructors of model checker helpers. Tim Quatmann 2020-08-10 18:34:00 +0200
  • cec37005ae
         Set relevant DFT elements earlier in code Matthias Volk 2020-08-10 17:37:14 +0200
  • 485d75f466 Towards using the infinite horizon helpers also for deterministic models. TimQu 2020-08-07 11:53:41 +0200
  • 35c57fe980 LraViHelper: Put component utility functions to separate file. TimQu 2020-08-07 11:52:59 +0200
  • fa6c47db64 Removed old LRA code for Markov automata. Tim Quatmann 2020-08-06 14:53:18 +0200
  • aabe3ce776 Added simple infinite horizon helper for the hybrid engine. Tim Quatmann 2020-08-06 14:52:19 +0200
  • 7795ce5f35 ModelCheckerHelper: Added utility function that copies model checking information from one helper to another. Tim Quatmann 2020-08-06 14:51:29 +0200
  • 626b7a819a InfiniteHorizon: Fixed storing backwardstransition properly. Allowed to specify a mec decomposition. Pushed _produceScheduler flag to the SingleValueModelCheckerHelper. Tim Quatmann 2020-08-06 14:50:16 +0200
  • 68b4d8dbd2 Nondet Lra: Fixed LP implementation for Markov automata. Tim Quatmann 2020-08-06 10:13:59 +0200
  • 9fbb587884 LraViHelper: Fix for NondetTsNoIs Tim Quatmann 2020-08-05 11:46:19 +0200
  • f113ac7187 NondeterministicLraHelper: Removed old ViHelper code. Tim Quatmann 2020-08-05 11:41:23 +0200
  • 7e65e797fa SingleValueModelCheckerHelper: Fixed signature of getOptimizationDirection so that a const& is returned. Tim Quatmann 2020-08-05 11:40:43 +0200
  • 6e55dba8d4 Moved LraViHelper to a separate file. Merged MDP and MA implementation. Tim Quatmann 2020-08-05 11:39:03 +0200
  • 15ccd6e653 Merge branch 'master' into rubicon Sebastian Junges 2020-08-04 18:29:51 -0700
  • a618147192 gmm Multiplier: Added support for computing y += A*x in Parallel. Tim Quatmann 2020-08-03 16:45:03 +0200
  • 51c8779e73 Added missing template instantiations. Tim Quatmann 2020-08-03 16:44:18 +0200
  • 5917b020fc GMM Multiplier: Support for y += A*x Tim Quatmann 2020-08-03 15:09:48 +0200
  • 9d2e5c2193 Relaxed precision requirements on an MA LRA test-case to correctly represent a relative precision criterion. Tim Quatmann 2020-08-03 14:58:35 +0200
  • 32503594d5 Use new LRA helper for Markov automata. Tim Quatmann 2020-08-03 14:57:38 +0200
  • b5bd7aa0c2 Introduced a utility function that sets information from a CheckTask to a helper. Tim Quatmann 2020-08-03 14:57:12 +0200
  • 092873e99a LRA VI: Added helper for Markov Automata. Tim Quatmann 2020-08-03 14:53:25 +0200
  • ab045f2865
         Ignore zoom attribute in pnpro files Matthias Volk 2020-08-01 15:57:17 +0200
  • fc66e01ed5 Nondeterministic Infinite horizon: Split value getters into StateValueGetter and ActionValueGetters. Made VI code more general, so that they may also be used for Markov Automata. Tim Quatmann 2020-07-31 16:53:50 +0200
  • 31dd1d8f49 sparse/StandardRewardModel: Added a method that only yields the action-based rewards (excl. state rewards) Tim Quatmann 2020-07-31 16:25:01 +0200
  • 9d3de84122 MaximalEndComponent: Added size() method. Tim Quatmann 2020-07-31 16:24:15 +0200
  • 395081cdf9
         Moved DFT preprocessing in api functions Matthias Volk 2020-07-30 11:38:25 +0200
  • d06a39eb79 Dropping old MDP LRA code. Tim Quatmann 2020-07-29 16:55:54 +0200
  • 3c84e68216 Using the new helper for MDP LRA properties. Tim Quatmann 2020-07-29 16:55:13 +0200
  • 486d62ff2c First version of newly structured ModelCheckerHelpers (only MDP LRA properties, for now) Tim Quatmann 2020-07-29 16:54:45 +0200
  • d49210ac2e Added DdType::None to encode that an explicit representation should be used. Tim Quatmann 2020-07-29 16:51:35 +0200
  • 1929cfaf77 utility/vector: Added a few asserts in utility functions. Tim Quatmann 2020-07-29 16:35:12 +0200
  • 6c70b42549 OVI: Defaulting to M1/M2, changed CLI option for termination guarantee Jan Erik Karuc 2020-07-26 13:14:18 +0200
  • fe5e4c4e1d
         Updated DFT test which is not throwing an exception anymore Matthias Volk 2020-07-22 15:17:05 +0200
  • 190e36605a
         Refactored computation of relevant events Matthias Volk 2020-07-22 15:11:57 +0200
  • a1c6b998ec
         Ignore SEQ and FDEP children Matthias Volk 2020-07-21 17:58:53 +0200
  • a7096f748b
         Fix segfault for empty spare modules Matthias Volk 2020-05-17 16:51:39 +0200
  • ed8a48a24c
         Correct check if claiming labels are supported Matthias Volk 2020-05-17 15:37:41 +0200
  • 936985f536
         Add labels for claiming in Markov chain with flag --labels-claiming Matthias Volk 2020-05-12 17:37:17 +0200
  • 2d543d1314
         Added BE class for distribution defined by samples Matthias Volk 2020-05-12 15:15:50 +0200
  • e9dfcb8e45
         Fixed type comparision for BEs Matthias Volk 2020-05-12 14:30:37 +0200
  • df28d8ef84
         Added getUnreliability() for BEs Matthias Volk 2020-05-11 14:27:19 +0200
  • 641c9992a1
         Distinguish between different BEType and use single BE type in DFTElementTypes Matthias Volk 2020-05-10 20:49:52 +0200
  • 41acd92e71 dice, first version of support for modulo Sebastian Junges 2020-07-21 20:45:01 -0700
  • d6bfcb4818 refactoring: moving some code out of the util folder Sebastian Junges 2020-07-21 20:41:40 -0700
  • b4b8d12415 Merge branch 'master' into rubicon Sebastian Junges 2020-07-20 19:01:07 -0700
  • 5722c1258c pipe all rf-variable creations through a single object file Sebastian Junges 2020-07-20 17:14:24 -0700
  • 8d75b84ba6
         Throw error when using ThinLTO and GCC Matthias Volk 2020-07-20 11:30:08 +0200
  • 17a1d02757 Cmake: Detection for the old in-source "storm-version.cpp" file. The file will now be deleted (if found) to prevent build issues for people that upgraded from older storm versions. TimQu 2020-07-20 10:47:35 +0200
  • c6fd7423f2 Disabling stack checks once again for all clang versions >= 11.0.0 because they somehow interfere with exception handling in the PrismParser. (most likely a clang bug). TimQu 2020-07-20 10:13:18 +0200
  • b3e37c1eb8 partial (parametric) model instantiators Sebastian Junges 2020-07-16 23:41:39 -0700
  • 03e0b01ae2 Making POMDPs simple now does not introduce further initial states Sebastian Junges 2020-07-16 20:52:54 -0700
  • 1343ae5c19 Fixed 'boost/optional.hpp file not found' error in storm-version library (simply by not using boost). TimQu 2020-07-15 09:53:54 +0200