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

Commit Graph

  • 8b87d79c3e Removed copy-pasted references to DFTs Matthias Volk 2019-02-14 17:14:34 +0100
  • 87cd72f237 Output exception type in exception message Matthias Volk 2019-02-14 16:48:24 +0100
  • 87d078f897 Output error by STORM_LOG_ERROR Matthias Volk 2019-02-13 12:53:18 +0100
  • 47b2cb737d Merge branch 'master' into dft Matthias Volk 2019-02-11 10:10:58 +0100
  • 04164d8b02 Fixed crucial typo in symmetry ordering Matthias Volk 2019-02-10 20:04:00 +0100
  • 5ad100e652 quantiles: Added some statistics. TimQu 2019-02-08 17:00:39 +0100
  • fb7078770d rewardbounded: Various fixes. TimQu 2019-02-08 15:32:22 +0100
  • ed4f61d3ee BIsmulation simplification bisimulation + fix lattice Jip Spel 2019-02-07 16:44:00 +0100
  • dd93b1dae9 rewardbounded: Improved code structure. TimQu 2019-02-07 16:30:43 +0100
  • 8fbc8d56c0 graph preservation properties correctly computed for CTMCs Sebastian Junges 2019-02-06 23:01:22 +0100
  • b13dbd11f3 Fix for monotonicitychecker Jip Spel 2019-02-06 20:25:42 +0100
  • 1c336be51e Merge branch 'master' into storm-pars-analysis-monotonicity Jip Spel 2019-02-06 18:55:59 +0100
  • ed0768cf60 Update implementation Jip Spel 2019-02-06 18:39:41 +0100
  • 6aeb75e3bd quantiles: Supporting two-dimensional quantiles with the same optimization direction of quantile bounds (max,max or min,min). TimQu 2019-02-05 19:14:15 +0100
  • 46aa007f33 Use flat_set Jip Spel 2019-02-05 11:57:43 +0100
  • f6da9644b0 Improve efficiency Jip Spel 2019-02-05 11:29:12 +0100
  • 26429925d6 Speedup Jip Spel 2019-02-04 20:03:32 +0100
  • f41b61fb7b Make cyclic part faster Jip Spel 2019-02-02 14:31:18 +0100
  • a99dd5e4d1 quantiles: Better code re-usage, better structure, support for 'open' and 'non-open' dimensions, single dimensional quantiles should work now. TimQu 2019-02-01 19:05:57 +0100
  • 1d5f2410b5 rewardBounded/RewardUnfolding: Allowed the case that not all dimensions have a bound a priori. TimQu 2019-02-01 19:04:32 +0100
  • 9e690c95c6 Fix cyclic monotonicity check Jip Spel 2019-01-31 19:55:04 +0100
  • ab14245350 Remove bool for stateElimination Jip Spel 2019-01-31 18:55:21 +0100
  • c33a8df85f Eliminate selfloop introduced by SCC elimination Jip Spel 2019-01-31 18:34:26 +0100
  • 44cde3314c Fix checking derivative Jip Spel 2019-01-31 18:34:02 +0100
  • 48cba66d96 Add scc elimination Jip Spel 2019-01-31 13:10:51 +0100
  • 4ac23d630f quantiles: Added support for formulas with trivial bounds (i.e., >=0). TimQu 2019-01-31 11:53:05 +0100
  • bcde728c3c Transform formulas to deterministic-time as well Matthias Volk 2019-01-30 22:14:42 +0100
  • 374071670a Activated symbolic bisimulation for parametric models Matthias Volk 2019-01-30 22:05:20 +0100
  • b2ea3993ef Fixed assertion in symbolic bisimulation Matthias Volk 2019-01-30 22:04:58 +0100
  • 3397d6aec0 Add state to reachability order, if there are not yet added states and nothing changed during loopiteration Jip Spel 2019-01-30 17:01:09 +0100
  • a72c7a244a Fix bug with acyclic pmcs and more than one assumption Jip Spel 2019-01-30 14:45:06 +0100
  • 6e8aef2acc Checking formulas with >=0 bound. Tim Quatmann 2019-01-30 12:54:12 +0100
  • a1c5aa946c Integrated symbolic verification of parametric systems into storm-pars Matthias Volk 2019-01-30 12:49:39 +0100
  • 399c061086 Typos Matthias Volk 2019-01-29 21:12:34 +0100
  • 267efd692a Construct time reward model Matthias Volk 2019-01-29 21:12:24 +0100
  • dfd1fec8c5 Fixed compile issues Matthias Volk 2019-01-29 20:46:27 +0100
  • 66ab97ba4f transformer: Added functionality to also translate expected time formulas to expected rewards. TimQu 2019-01-29 18:09:42 +0100
  • f99a24acd2 more work on quantiles. Tim Quatmann 2019-01-29 13:09:32 +0100
  • 82402ba3ae rewardbounded: Moved epoch model analysis to a separate file. Tim Quatmann 2019-01-29 13:08:20 +0100
  • 661d922d2e logic/bound: Added method to compare a bound with a value. Tim Quatmann 2019-01-29 12:56:29 +0100
  • 8d95e71c3e Change output, Fix some small bugs Jip Spel 2019-01-29 10:33:50 +0100
  • d796ee74de (workplace switch) TimQu 2019-01-29 10:28:59 +0100
  • d3abeb5f45 Started implementation on quantiles. Tim Quatmann 2019-01-28 12:58:18 +0100
  • dc2654ce60 Quantiles: made the SparseMdpPrctlModelChecker call the QuantileHelper for quantile formulas TimQu 2019-01-25 21:08:24 +0100
  • a631a9d210 Merge branch 'master' into dft Matthias Volk 2019-01-25 14:44:33 +0100
  • fe535b9ba6 Fixed QuantileFormula's writeToStream. TimQu 2019-01-25 10:54:56 +0100
  • 9e282c8bb2 QuantileFormulas: A boost::spiritual abyss. TimQu 2019-01-25 10:53:28 +0100
  • 09a5c44c6e Fixed usage of denominatorAsNumber Matthias Volk 2019-01-24 13:58:47 +0100
  • 7e66787c9c logic: Added QuantileFormulas. TimQu 2019-01-24 12:42:57 +0100
  • 6384a1927f Merge branch 'master' into storm-pars-analysis-monotonicity Jip Spel 2019-01-11 15:07:40 +0100
  • 32f757e4b4 Fixed json export for FDEPs Matthias Volk 2019-01-08 17:13:09 +0100
  • ef09fab716 Better check if element name is already used Matthias Volk 2019-01-08 17:12:45 +0100
  • babf951bce Merge branch 'master' into dft Matthias Volk 2019-01-04 19:03:16 +0100
  • 7abf0c2a8f Update failable dependencies if trigger was set to dont care Matthias Volk 2019-01-04 18:48:54 +0100
  • 2768d15f4f fixing minor issue in symboiic bisimulation relation pointed out by Tim dehnert 2018-12-29 19:33:49 +0100
  • 98b628b269 Moved failableBE/Dependencies to own struct Matthias Volk 2018-12-16 22:48:37 +0100
  • 53fa42f279 Ensure failable dependencies are only added once Matthias Volk 2018-12-14 14:12:46 +0100
  • 1fcc375608 BE can no longer fail after triggered failure Matthias Volk 2018-12-14 14:12:27 +0100
  • fb1ea21f9c Added assertions to exclude self-loops in DFT state generation Matthias Volk 2018-12-14 14:12:08 +0100
  • 9b11fed0c8 Fixed warning Matthias Volk 2018-12-11 17:51:51 +0100
  • e5049c67da Storm version 1.3.0 Matthias Volk 2018-12-08 11:59:58 +0100
  • d3356cd3e4 Use master14 branch for Carl Matthias Volk 2018-12-08 00:38:21 +0100
  • 3e2da7eba1 Merge branch 'unifplus_refactor' Matthias Volk 2018-12-08 00:25:46 +0100
  • 99808240bf Updated changelog Matthias Volk 2018-12-08 00:25:10 +0100
  • fceaeed557 Fixed a recently introduced issue with interval bounded ctmcs. TimQu 2018-12-07 17:44:29 +0100
  • 8c572ba550 Merge branch 'master' into unifplus_refactor Matthias Volk 2018-12-07 17:03:20 +0100
  • 230ac20480 Added progress measurements for Unif+ iterations and steps Matthias Volk 2018-12-07 17:02:40 +0100
  • 2197f3c34a Updated changelog Matthias Volk 2018-12-07 16:47:35 +0100
  • aacdf5c0b5 Updated changelog. TimQu 2018-12-07 16:16:47 +0100
  • 629de20da0 Fixed running in an infinite loop when computing LRA on markov automata with relative precision. TimQu 2018-12-07 16:06:45 +0100
  • 0c905e2323 Fixed an issue where time-bounded properties were wrongly computed on a ctmc that only consists of goal-states. TimQu 2018-12-07 16:06:04 +0100
  • 384e7ace06 TopologicalMinMaxLinearEquationSolver: Reduced clutter in the --verbose output. TimQu 2018-12-07 16:05:08 +0100
  • 03b5c70c79 support for POMDPs in symoblic description Sebastian Junges 2018-12-07 13:12:46 +0100
  • 36ed6f0a91 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Sebastian Junges 2018-12-07 11:41:23 +0100
  • cab2b3d8f1 changelog preparation for version 1.3.0 Sebastian Junges 2018-12-07 11:41:04 +0100
  • 94a1d47103 Use IMCA method for bounded until with lower bound > 0 Matthias Volk 2018-12-07 11:32:36 +0100
  • c1119fcd8d Triggered conversion from PRISM to JANI when building an MA with the dd engine since MAs are unsupported in the DdPrismModelBuilder. TimQu 2018-12-07 11:26:53 +0100
  • 01a23856a8 Drastically decreased memory consumption of Unif+ Matthias Volk 2018-12-07 00:26:33 +0100
  • d054f3c64a Result for upper bounds needs only be calculated for k=0 Matthias Volk 2018-12-07 00:06:58 +0100
  • 4c5b041340 Debug output Matthias Volk 2018-12-06 20:12:19 +0100
  • 6220b114b5 Small simplifications Matthias Volk 2018-12-06 20:11:57 +0100
  • f9fb90499d Only keep track of results from the last iteration (instead of all iterations) for 2 of the 3 vectors Matthias Volk 2018-12-06 16:13:24 +0100
  • 8ae800b130 Changed iteration order to iterate over stepsize in outer loop Matthias Volk 2018-12-06 11:42:53 +0100
  • cbd6139613 Small changes Matthias Volk 2018-12-06 11:28:00 +0100
  • b8b2c58dab Started on some refactoring in Unif+ Matthias Volk 2018-12-05 18:36:45 +0100
  • 6066ecd590 Added struct for Unif+ vectors Matthias Volk 2018-12-05 18:35:54 +0100
  • 70d3f8d811 Unified order of function arguments for Unif+ Matthias Volk 2018-12-05 12:11:43 +0100
  • 97b14e35d5 Small renaming Matthias Volk 2018-11-23 18:22:44 +0100
  • 19f353591f Added an option to transform CTMCs to MAs and DTMCs to MDPs. TimQu 2018-12-03 12:08:45 +0100
  • 27d87da93d Fixed value iteration based LRA method for Markov Automata, where end components do not contain probabilistic states. TimQu 2018-12-03 12:07:22 +0100
  • 6e3639c8f1 Added new minmax method: Vi-to-Pi, which first performs value iteration with doubles, to find a good initial policy for (potentially exact) policy iteration. TimQu 2018-12-02 17:48:56 +0100
  • 240faff125 BuilderOptions: Added terminal states for bounded until and reachability reward formulas. TimQu 2018-12-02 17:46:08 +0100
  • fa2bcbd71b storm-conv: Fixed wrong jani export of step-bounded until properties in discrete time models. TimQu 2018-12-02 13:40:28 +0100
  • 605c13238e Correctly handle the case where no model description is provided to the builder options. TimQu 2018-12-02 11:58:51 +0100
  • 02977da3d7 Apply maximum progress assumption while building a Markov Automaton explicitly. TimQu 2018-12-01 23:03:30 +0100
  • b84ce33956 TopologicalMinMaxLinearEquationSolver: Handled prob 1 selfloops more correctly. TimQu 2018-11-29 18:58:56 +0100
  • c614e9d747 Fixed Value Iteration based LRA computation TimQu 2018-11-29 18:57:45 +0100
  • 26ee89a856 Check assumptions on a region Jip Spel 2018-11-29 12:48:50 +0100
  • 2aeab4b2e7 Let the topological equation solvers handle singleton SCCs with self-loops directly. TimQu 2018-11-27 22:12:17 +0100
  • 4924a0e557 Fixed 'isZero' function in ConstantsComparator. TimQu 2018-11-27 20:37:19 +0100