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

Commit Graph

  • a427eae699 fixed severe bug in symbolic bisimulation minimization dehnert 2017-10-12 14:27:36 +0200
  • 529e31a1ba fixed multiple initial states in pomdp unfolder TimQu 2017-10-12 11:03:01 +0200
  • 91bd638c18 Fixed segfault Matthias Volk 2017-10-12 10:46:53 +0200
  • 45a4b63a2e fixed some issue in sylvan sharpen and forward minmax bounds to linear equation solver dehnert 2017-10-11 21:38:14 +0200
  • a9a1c4feed Region model checker can now also return a (quantitative) upper/lower bound for a given region TimQu 2017-10-11 18:50:53 +0200
  • 5ad60051c3 Region model checker can now also return a (quantitative) upper/lower bound for a given region TimQu 2017-10-11 18:50:53 +0200
  • 8a74be1b72 Refactored DFT settings Matthias Volk 2017-10-11 17:57:15 +0200
  • f2e581b3df rational search for symbolic linear equation solvers dehnert 2017-10-11 15:59:36 +0200
  • 9350e281c7 Renamed storm-dyftee to storm-dft Matthias Volk 2017-10-10 11:38:44 +0200
  • 349e276c9b Removed include of cpp file in storm-pars-cli and storm-dft-cli Matthias Volk 2017-10-10 11:30:25 +0200
  • 1a4bc33e5b Fixed setting of debug settings in storm-dft-cli Matthias Volk 2017-10-10 11:14:04 +0200
  • 7ec9f3415e Merge branch 'master' into pomdp_datastructures TimQu 2017-10-11 10:23:28 +0200
  • 73b23e133e DRN parser now supports state rewards TimQu 2017-10-11 10:22:13 +0200
  • 086201ac43 corrected some output and adapted requirements of symbolic minmax solver dehnert 2017-10-10 22:54:47 +0200
  • a8c6c62275 rational search working for symbolic MDPs dehnert 2017-10-10 20:22:00 +0200
  • 2be3f553e0 fixes TimQu 2017-10-10 18:53:40 +0200
  • 7fe24e912e more output TimQu 2017-10-10 18:53:33 +0200
  • 31f8ec98e4 implemented the pomdp unfolding to convert k-memory-bounded pomdps to memoryless pomdps TimQu 2017-10-10 17:32:37 +0200
  • 5d80aa60d7 extended pomdp settings TimQu 2017-10-10 17:31:32 +0200
  • b09cb95254 fixed wrong call in sylvan double to rational number conversion dehnert 2017-10-10 18:44:29 +0200
  • da02237769 work towards symbolic rational search dehnert 2017-10-10 18:21:24 +0200
  • de86713226 Merge branch 'master' into pomdp_datastructures Sebastian Junges 2017-10-10 18:13:14 +0200
  • af60db2c38 work towards symbolic rational search dehnert 2017-10-10 15:53:56 +0200
  • a42e8e965a more robust drn parser Sebastian Junges 2017-10-10 11:54:01 +0200
  • 9901995280 Export of weight vector in the cdf TimQu 2017-10-10 09:56:19 +0200
  • 6e8465e9f1 started on symbolic rational search dehnert 2017-10-09 16:31:52 +0200
  • 55c787e0d8 proper EC elimination in hybrid helper dehnert 2017-10-08 21:46:53 +0200
  • 94788dbd74 Removed old files Matthias Volk 2017-10-06 16:37:35 +0200
  • 026cb3dfdf Small change in travis generation Matthias Volk 2017-10-06 16:32:00 +0200
  • e5387ecc85 Deactivated conversion to CTMC for trivial non-determinism in MA as it is not correct at the moment Matthias Volk 2017-10-06 16:31:26 +0200
  • b97f75698b Merge branch 'master' into reward-bounded-multi-objective TimQu 2017-10-06 15:15:33 +0200
  • 6fa4e6b455 fixed SOR and gaussseidel linear equation solver methods TimQu 2017-10-06 15:15:08 +0200
  • fb21ffca63 Respected whether the linear equation solver wants the fix point or eq sys formulation TimQu 2017-10-06 15:08:50 +0200
  • 694e6ba240 EC elimination for Pmax for hybrid MDP model checker dehnert 2017-10-06 13:27:42 +0200
  • 384f17e32e Workaround for jit and sylvan tests on travis Matthias Volk 2017-10-05 17:09:18 +0200
  • e557a8e069 started on EC elimination for hybrid engine dehnert 2017-10-05 15:52:48 +0200
  • 64a804137e export of cdf's TimQu 2017-10-05 14:50:06 +0200
  • a4a8bc2e69 accessing the epoch manager and the dimensions from the outside TimQu 2017-10-05 14:49:42 +0200
  • 20a76f01e2 Better error output for jit Matthias Volk 2017-10-05 11:19:25 +0200
  • 682a0483d2 helped gmm to converge... TimQu 2017-10-05 09:32:22 +0200
  • 4da61d972c fixed correctly setting the result bounds for weight vector checker TimQu 2017-10-05 09:27:44 +0200
  • 58ca07584d rational search for native linear equation solver and several involved fixes dehnert 2017-10-04 20:25:13 +0200
  • b788c1b403 reuse scheduler from previous epoch as initial hint TimQu 2017-10-04 16:34:44 +0200
  • 952f49fb10 fix for interval iteration in weight vector checkers TimQu 2017-10-04 11:03:07 +0200
  • fcf3d984fb 5th build stage in travis seems not to be needed anymore Matthias Volk 2017-10-03 13:09:05 +0200
  • 4626aa0e69 Updated search for mathsat in cmake and fixed linker problem Matthias Volk 2017-10-02 17:44:01 +0200
  • 57065bdabd glpk and hwloc now in homebrew/core Matthias Volk 2017-10-02 15:27:59 +0200
  • ba9534da0a apple-clang was not recognized in travis Matthias Volk 2017-10-02 14:36:34 +0200
  • bc0e432e11 Changed compilers in travis Matthias Volk 2017-10-02 14:17:24 +0200
  • 1ec19a1e6c Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Matthias Volk 2017-10-02 13:44:02 +0200
  • 36ffd2682d Merge branch 'master' into reward-bounded-multi-objective TimQu 2017-10-02 12:25:22 +0200
  • 11da1ddc14 upper bounds for expected reward objectives TimQu 2017-10-02 12:22:34 +0200
  • 765890f3f2 Moved dockerfiles to own repository Matthias Volk 2017-10-02 12:11:05 +0200
  • 20960d56e7 added missing 'this->'. Also avoid in-place matrix vector multiplication when extracting a scheduler TimQu 2017-10-02 12:05:39 +0200
  • f83dbf741b fixed wrong template argument TimQu 2017-10-02 12:02:45 +0200
  • 96f45fe77a fixed missing return statements TimQu 2017-09-28 12:15:54 +0200
  • 1396de3c5f Enforce no end components when we want to compute a scheduler from a minmax equation system TimQu 2017-09-28 12:15:37 +0200
  • 50ba6866eb checking solver requirements for PLA TimQu 2017-09-28 12:14:27 +0200
  • a8d32eb0be Merge pull request #8 from kleinj/cmake-old-carl-fix cdehnert 2017-10-01 20:22:15 +0200
  • 93a3bff8e0 Merge branch 'master' into cmake-old-carl-fix cdehnert 2017-10-01 20:21:22 +0200
  • df05711f3e finished rational search for MinMax solver, preparing rational search for NativeLinearEquationSolver dehnert 2017-09-29 15:53:10 +0200
  • 0c8866203c tracking bugs, lots of debug output dehnert 2017-09-28 23:04:06 +0200
  • c396ab0ca5 more solver requirements for multi-objective model checking TimQu 2017-09-28 18:59:26 +0200
  • d58f751491 Merge branch 'master' into reward-bounded-multi-objective TimQu 2017-09-28 16:31:36 +0200
  • 64ca58494d considered solver requirements for multiobjective model checking TimQu 2017-09-28 16:31:25 +0200
  • afd2acd06b more work on Kwek-Mehlhorn approach dehnert 2017-09-28 15:52:13 +0200
  • 4afaca7f84 fixed missing return statements TimQu 2017-09-28 12:15:54 +0200
  • 3f6464c59d Enforce no end components when we want to compute a scheduler from a minmax equation system TimQu 2017-09-28 12:15:37 +0200
  • 4991a3ec5e checking solver requirements for PLA TimQu 2017-09-28 12:14:27 +0200
  • b3349dc344 fixed fill() method of bit vectors TimQu 2017-09-28 09:38:31 +0200
  • 4a66ab2e57 Merge branch 'master' into reward-bounded-multi-objective TimQu 2017-09-28 09:01:46 +0200
  • 254bc05e94 more work on RationalSearch dehnert 2017-09-27 21:45:40 +0200
  • 088c2d8b15 fixed missing suffix dehnert 2017-09-27 15:26:00 +0200
  • b3f0aa511e started on Kwek-Mehlhorn-based exact value computation dehnert 2017-09-27 15:23:12 +0200
  • cb15db041c add missing include dehnert 2017-09-25 18:12:04 +0200
  • 76fa67fd35 added missing include dehnert 2017-09-25 16:26:41 +0200
  • c84a84cba4 corrected ms to s dehnert 2017-09-24 13:47:21 +0200
  • 20afe3d48b Merge branch 'master' into conditional_optimizations dehnert 2017-09-24 09:33:00 +0200
  • 2d41de479e added progress outputs to iterative solvers dehnert 2017-09-23 21:04:37 +0200
  • 4e79e8715b Merge branch 'master' into pomdp_datastructures TimQu 2017-09-22 16:55:01 +0200
  • 142d034765 New methods for the SparseMatrix: SetRowGroupIndices and filterEntries TimQu 2017-09-22 16:47:26 +0200
  • 88339f4cff invoking new functionalities in the cli. Also silenced some debug output TimQu 2017-09-22 16:45:47 +0200
  • 1d1a198f5e generalizing the Selfloop elimination ideo to MECs TimQu 2017-09-22 16:45:02 +0200
  • 412ecbcd36 Qualitative analysis of pomdps TimQu 2017-09-22 16:44:33 +0200
  • d8d3404b87 fixed termination criteria and equipped interval value iteration methods with check whether the method converged for the relevant states dehnert 2017-09-22 16:07:05 +0200
  • 7f56c82523 moved to providing solve goals in sparse model checkers and helpers dehnert 2017-09-22 14:44:48 +0200
  • 904e49dab3 Fix wrong type hbruintjes 2017-09-22 11:48:37 +0200
  • e7b6587170 minor fixes for new relative convergence test dehnert 2017-09-21 19:01:02 +0200
  • e719a37c6c fixes related to relative termination criterion dehnert 2017-09-21 14:35:40 +0200
  • 99832d2694 only expanding epsilon in sound power methods when the absolute convergence criterion is used dehnert 2017-09-21 11:41:53 +0200
  • c5884a27b4 fixed termination condition applications in a number of spots, fixed uint64 vs uint64_t issue dehnert 2017-09-21 10:59:43 +0200
  • 4fd472fdd6 added difference heuristic to sound VI in MinMax solver dehnert 2017-09-20 22:25:57 +0200
  • c8e19d2e44 fixed priority queue implementation and upper reward bound computation dehnert 2017-09-20 21:22:20 +0200
  • 51e64b8ebd started on Baier-style upper reward bound computation dehnert 2017-09-20 14:39:45 +0200
  • 52d729b1c7 upper bounds computation for reachability rewards in sparse MDPs dehnert 2017-09-20 14:09:21 +0200
  • fcd277c42a added an option that enables building of state valuations. Also include the state valuations when the model is exported to .dot format TimQu 2017-09-20 10:12:31 +0200
  • 9039323fa9 optimized setting the epoch class TimQu 2017-09-20 09:06:20 +0200
  • 68f14c728a added missing check for existence of model dehnert 2017-09-19 23:03:38 +0200
  • b4a0016362 zero-reward MEC elimination for reachability rewards dehnert 2017-09-19 22:40:09 +0200
  • fe8c3820fd started cleanup of reachability rewards in sparse MDP helper dehnert 2017-09-19 14:47:30 +0200