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

Commit Graph

  • e65e5587f0 Support for abort in Gmm++ by throwing exception Matthias Volk 2020-03-06 16:11:56 +0100
  • 823ae23180 Use updateStatus in more cases Matthias Volk 2020-03-06 16:04:04 +0100
  • f50a7a424b General updateStatus function in AbstractEquationSolver Matthias Volk 2020-03-06 15:50:01 +0100
  • c6b984ca51 Do not perform the conversion from a prism program to a jani model twice. Tim Quatmann 2020-03-06 13:39:33 +0100
  • b61775570b minor Sebastian Junges 2020-03-05 10:21:13 -0800
  • b745b10b77 Moved reportStatus() and updateStatusIfNotConverged() to AbstractEquationSolver Matthias Volk 2020-03-05 18:25:00 +0100
  • 9962da7453 Registered missing settings modules in storm-dft and storm-pars Tim Quatmann 2020-03-05 17:32:56 +0100
  • e3663ee740 Portfolio: print true/false instead of 1/0 Tim Quatmann 2020-03-05 17:22:05 +0100
  • 7e9029e5bd Optimization for PRISM model building: Avoid evaluating unnecessarily many guards. Tim Quatmann 2020-03-05 16:57:55 +0100
  • 4012094f9d Use new time bounded environment also in the ctmc solver. Tim Quatmann 2020-03-05 16:57:24 +0100
  • 11ed073632 Making storm-dft compile again... Tim Quatmann 2020-03-05 16:47:15 +0100
  • 3debbbc64d Added more abortion checks Matthias Volk 2020-03-05 15:38:27 +0100
  • d35d31ce94 Added SolverStatus::Abort for abort signal handling Matthias Volk 2020-03-05 15:13:35 +0100
  • acd5a94162 Use general SolverStatus in StandardGameSolver Matthias Volk 2020-03-05 15:06:49 +0100
  • 8168b9d125 Using OVI as default Tim Quatmann 2020-03-05 15:03:10 +0100
  • 7617d4f96f Updated changelog. Tim Quatmann 2020-03-05 14:58:13 +0100
  • 20f5cf158b storm-dft: Using symmetry reduction by default. Tim Quatmann 2020-03-05 14:51:51 +0100
  • 0dd1c70e12 Set waiting time after signal with flag --signal-timeout Matthias Volk 2020-03-05 13:09:31 +0100
  • f6d6d952a6 Fixed warnings Matthias Volk 2020-03-05 11:59:59 +0100
  • 5192bd1623 Merge from qcomp2020 Matthias Volk 2020-03-05 11:53:23 +0100
  • 0f967409e6 post merge compile issues with double vs rationals in storm pomdp Sebastian Junges 2020-03-04 17:34:33 -0800
  • 160043a8b8 Merge branch 'master' into prism-pomdp Sebastian Junges 2020-03-04 16:30:40 -0800
  • d26842d441 Merge branch 'master' into prism-pomdp Sebastian Junges 2020-03-04 15:47:59 -0800
  • d703516d2d make code compile Sebastian Junges 2020-03-04 15:00:58 -0800
  • 7400b0e2e9 Merge branch 'master' into almostsurepomdp Sebastian Junges 2020-03-04 13:23:17 -0800
  • a8c0cfbcdd Enabled OVI for linear equation systems in test cases. Tim Quatmann 2020-03-04 21:00:17 +0100
  • 383e2172d4 Added OVI for linear equation systems (i.e. DTMC/CTMC) Tim Quatmann 2020-03-04 20:59:53 +0100
  • 7c49edb68f Put most of the optimistic value iteration code into a new helper file Tim Quatmann 2020-03-04 20:58:58 +0100
  • 6c095e757a Fixed problem with Windows linebreak \r\n, because this is still a problem in 2020 Matthias Volk 2020-03-04 18:20:33 +0100
  • 502b637df4 Ovi: Use an additional auxiliary row group vector (to allow caching). Tim Quatmann 2020-03-04 16:48:27 +0100
  • ee82f30550 Removed Debug output Tim Quatmann 2020-03-04 16:44:35 +0100
  • 0ba0d94b84 Small update for the default settings. Tim Quatmann 2020-03-04 16:37:23 +0100
  • c33d570610 Merge branch 'qcomp2020' into ovi-implementation Tim Quatmann 2020-03-04 16:33:14 +0100
  • 33975c181e Fixes and improvements in the new unif+ implementation. Tim Quatmann 2020-03-04 16:32:38 +0100
  • 52857d2701 FoxGlyn: Print an error message instead of throwing an exception in cases where an underflow is possible. Tim Quatmann 2020-03-04 16:32:17 +0100
  • 4a34fb1a7c MaTest: Making sure that the 'inner' MinMax solver for unif+ is allowed to switch the solution method. Tim Quatmann 2020-03-04 16:28:28 +0100
  • e54a035ab9 SolverEnvironment: Added the switch `forceExact` to switch to exact solving methods more conveniently. Tim Quatmann 2020-03-04 16:04:43 +0100
  • c3184d3afa Consider relevant states in unif+ TimQu 2020-03-03 23:02:42 +0100
  • ca59635f8a Using new time bounded environment also for IMCA method. TimQu 2020-03-03 22:28:51 +0100
  • 03bf55f4ab Bugfix in new unif+ implementation TimQu 2020-03-03 22:24:23 +0100
  • f8fbf7ace4 Refactored unif+ implementation (introduced relative precision criterion) Tim Quatmann 2020-03-03 17:50:27 +0100
  • bb94110b74 MarkovAutomaton model checkers: Enable consideration of psiStates. Tim Quatmann 2020-03-03 14:44:57 +0100
  • 60670e1fb2 SparseMatrix: fixed getConstraintRowSumVector which did not allocate enough space before filling the resulting vector. Tim Quatmann 2020-03-03 14:38:26 +0100
  • f0d1aff610 Added new settings and environment module for time-bounded settings. Tim Quatmann 2020-03-03 14:35:55 +0100
  • f684e48e9e Support for aborting DFT state space building Matthias Volk 2020-03-02 14:49:01 +0100
  • ce298fa782 Moved signal handling to own file to prevent problems with global static variables being non-unique Matthias Volk 2020-03-02 14:47:54 +0100
  • 05471d94fd Optimizations in JaniNextStateGenerator that avoid unnecessary (re-) allocations of memory. Moreover, before collecting the complete set of enabled edges for each automaton, we first check whether each automaton (that synchronizes with that action) has at least one enabled edge. This avoids checking unnecessarily many edge guards. Tim Quatmann 2020-03-02 14:19:25 +0100
  • e79035c71b Enabled short circuit optimization for & (and) and | (or) in ExprtkExpressionEvaluator Tim Quatmann 2020-03-02 08:54:42 +0100
  • d92e6b97e5 updated exprtk Tim Quatmann 2020-03-02 08:53:58 +0100
  • e945f28a86 Using raw pointers for manager in Variable.h since weak_ptr::lock() often seems to be a bottle neck during, e.g., model building. Tim Quatmann 2020-03-02 08:00:20 +0100
  • b3831d0093 Merge branch 'master' into qcomp2020 TimQu 2020-03-02 07:32:12 +0100
  • 5d8419336f InternalAdds: Added a comment related to GitHub issue #64 TimQu 2020-03-02 06:34:28 +0100
  • 36c410875c Revert "InternalAdds: Making the different splitIntoGroups implementations more consistent to each other (in the sense that the Dd is traversed in the same order)." TimQu 2020-03-02 06:31:39 +0100
  • 1f98f6c557 Reverted 'optimization' for Prob1Max (since that didn't work out). TimQu 2020-03-01 11:39:42 +0100
  • 9d0d8022f9 Revert "Slight optimization in performProb1A" TimQu 2020-02-29 22:49:02 +0100
  • d288701e9d Graph: Changed methods for prob1 methods in performProb1Max / performProb1Min to more efficient variants that can be used as we already know the prob0 states. TimQu 2020-02-29 22:47:54 +0100
  • c74a6ea201 Removal of unused extractActions function Alexander Bork 2020-02-28 13:01:51 +0100
  • e1bd87b91a Added documentation Alexander Bork 2020-02-28 12:45:34 +0100
  • 53d5e9edf5 Code Cleanup Alexander Bork 2020-02-28 12:45:07 +0100
  • 2df4679fbc Slight optimization in performProb1A Tim Quatmann 2020-02-27 22:27:52 +0100
  • fe5cd4db86 Fixed missing ; Tim Quatmann 2020-02-27 22:27:33 +0100
  • 99db5693ca OVI: Implement upper bound only iterations Jan Erik Karuc 2020-02-27 21:33:38 +0100
  • a5d3d0e696 slight optimizations in the JaniNextStateGenerator Tim Quatmann 2020-02-27 20:49:37 +0100
  • f01d8943ad Indicate if result is not fully correct due to abort Matthias Volk 2020-02-27 20:49:18 +0100
  • 3bb3ff9bc7 Support abortion in Unif+ Matthias Volk 2020-02-27 20:48:41 +0100
  • 45aa451be5 Signal handler supporting termination after waiting period Matthias Volk 2020-02-27 20:42:59 +0100
  • 248c0ecd35 Improved performance of SCC Decomposition by avoiding memory (re-)allocations Tim Quatmann 2020-02-27 20:31:23 +0100
  • f56cdb1b93 OVI: Add upper bound only iterations option Jan Erik Karuc 2020-02-27 19:59:40 +0100
  • 1c65a936c3 OVI: Use correct environment variable Jan Erik Karuc 2020-02-27 19:59:10 +0100
  • c016d0716e OVI: Fixed edge case, if x = 0 and ub = 0 Jan Erik Karuc 2020-02-27 19:58:38 +0100
  • 3db9112a27 OVI: Introduced OVI as a minmax solver for topological solving Jan Erik Karuc 2020-02-27 19:56:59 +0100
  • 06787ab9c2 Added calls to setUrgentOptions for binaries Matthias Volk 2020-02-27 19:56:55 +0100
  • 6af34ffbe1 Removed old file Matthias Volk 2020-02-27 18:55:13 +0100
  • 739d6a4420 OVI: Implement the guessing scaler factor option Jan Erik Karuc 2020-02-27 18:19:08 +0100
  • 6ecee7e371 OVI: Add upper bound guessing scaler factor option Jan Erik Karuc 2020-02-27 18:17:07 +0100
  • 8b97895e24 OVI: More debug output & cross case assert Jan Erik Karuc 2020-02-27 17:57:07 +0100
  • 50a51a70c0 OVI: Debug output for inner interval iteration Jan Erik Karuc 2020-02-27 17:28:26 +0100
  • b1dc6fec06 Accelerated zeno check for MAs. Also only apply zeno check if --additional-checks is set. Tim Quatmann 2020-02-27 15:11:38 +0100
  • bf99724f3b Added missing include. Tim Quatmann 2020-02-27 13:36:13 +0100
  • 95b2095151 Implemented simplification of system composition (this enables compatibility for more benchmarks in the dd engine). Tim Quatmann 2020-02-27 13:12:47 +0100
  • 38439fc867 jani/Automaton: Implemented possibility to clone an automaton. TimQu 2020-02-27 10:28:21 +0100
  • 4e7f8af851 Merge branch 'master' into qcomp2020 Tim Quatmann 2020-02-27 09:06:28 +0100
  • 141316943c DdJaniModelBuilder: Also apply max. progress if the system consists of just a single automaton. Tim Quatmann 2020-02-27 09:06:12 +0100
  • 5d530bb532 Improved compatibility of the dd-to-sparse engine (can now handle reward models with state action rewards) Tim Quatmann 2020-02-26 20:52:15 +0100
  • eaacc6c0ac Included the hybrid engine in the MA test. Tim Quatmann 2020-02-26 20:51:10 +0100
  • cefe43f2bf InternalAdds: Making the different splitIntoGroups implementations more consistent to each other (in the sense that the Dd is traversed in the same order). Tim Quatmann 2020-02-26 20:50:42 +0100
  • 7bf1abe136 Implemented LRA properties for the hybrid engine of MAs. Tim Quatmann 2020-02-26 20:46:59 +0100
  • e6597b35a6 OVI: Added a few settings to tweak ovi Tim Quatmann 2020-02-25 17:19:09 +0100
  • 50ff86e709 Polished/ improved ovi. Tim Quatmann 2020-02-25 16:30:42 +0100
  • f73be674a9 Update solver status if iterations exceeded Jan Erik Karuc 2020-02-25 12:51:32 +0100
  • 73b68836c5 Hybrid MA engine: (bounded) reachability probabilities Tim Quatmann 2020-02-25 12:50:04 +0100
  • 72eb58f73d Merge branch 'portfolio' into ma-hybrid Tim Quatmann 2020-02-25 10:25:13 +0100
  • a36e75db67 Fixed error introduced during merge Tim Quatmann 2020-02-25 10:24:48 +0100
  • 04c2938057 Introduced hybrid engine for Markov automata (only reach. rewards for now) Tim Quatmann 2020-02-25 10:24:10 +0100
  • db697e7bfc Split upper bound guessing for relative and absolute Jan Erik Karuc 2020-02-23 17:23:13 +0100
  • 33e21db8ea Provide precision in bound guessing operation Jan Erik Karuc 2020-02-23 16:53:23 +0100
  • cd15c01f2f Relative and absolute error criterion Jan Erik Karuc 2020-02-21 00:56:19 +0100
  • 606087ce85 Absolute ub guessing and in-place center calculation Jan Erik Karuc 2020-02-20 22:29:31 +0100
  • b4e743c4a6 Also update lb in the verification phase Jan Erik Karuc 2020-02-20 21:40:08 +0100
  • 02a346b5b7 Fix: Set lb to ub if difference vector has no positive entry Jan Erik Karuc 2020-02-20 21:24:26 +0100