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

Commit Graph

  • 0e34bdbfc4 split weight vector checker into one for MDPs and one for MAs TimQu 2016-06-30 19:36:14 +0200
  • c43a315b08 Merge branch 'future' of https://sselab.de/lab9/private/git/storm into future PBerger 2016-06-30 17:13:41 +0200
  • 8546786e17 Fix missing template argument in builder utility hbruintjes 2016-06-30 17:11:54 +0200
  • 9134b44f7f Merge future and future hbruintjes 2016-06-30 15:26:27 +0200
  • 49a812d996 Merge branch 'future' into multi-objective TimQu 2016-06-30 12:44:56 +0200
  • 12287e5090 small fix for building MAs Also fixed a test for explicit MA parsing, where the transitions of a probabilistic choice did not sum up to one TimQu 2016-06-30 12:43:02 +0200
  • d2c1c2d6f7 updated fragment checking for multi objective formulas TimQu 2016-06-30 12:07:59 +0200
  • ffe325b196 Fix unitialized data in coresettings hbruintjes 2016-06-30 11:29:00 +0200
  • a2140141a3 Fix virtual destructor hbruintjes 2016-06-29 18:05:56 +0200
  • 556b8e8726 Return reference to settings module, not a copy hbruintjes 2016-06-29 17:15:20 +0200
  • aae8fc8e87 regarding preprocessing for MAs TimQu 2016-06-29 21:33:32 +0200
  • 6010266e5b merge fix and fix in model file TimQu 2016-06-29 17:31:17 +0200
  • 98898dde84 Merge branch 'future' into multi-objective TimQu 2016-06-29 17:30:09 +0200
  • f681206393 building markov automata from prism code TimQu 2016-06-29 16:49:56 +0200
  • 0f84cdcadb Fixed performance tests. WARNING: I had to remove the SolverSelection in the call due to the new API - the performance tests might now all use the same Solver. PBerger 2016-06-29 15:05:12 +0200
  • 2c2049dc0b Merge branch 'exact_solver' into future dehnert 2016-06-28 18:48:26 +0200
  • 83c4b1647c solvers now can allocated auxiliary memory dehnert 2016-06-28 18:48:14 +0200
  • be5fdeb636 started working on internal auxiliary storage of solvers dehnert 2016-06-28 15:54:45 +0200
  • 8d3ac50909 Merge branch 'future' into multi-objective TimQu 2016-06-28 15:45:04 +0200
  • cf299a6344 fixed the case where an expression occurred twice in the formulas TimQu 2016-06-28 15:44:42 +0200
  • 4496b53002 merge fixes TimQu 2016-06-28 15:29:59 +0200
  • 625e98a01a Merge remote-tracking branch 'origin/future' into multi-objective TimQu 2016-06-28 15:29:18 +0200
  • 4e1019e682 Removed all mentions of EIGEN_DEPRECATED from Eigen Sources. Each instance triggers an error about an unexpected attribute "deprecated". It seems to be a combination of Eigen + Storm or other 3rd party libraries since this error does not apprear in stand-alone compilations with Eigen3. PBerger 2016-06-28 02:25:30 +0200
  • d80423b760 Fixed the stupid array with size zero warning in Sylvan/Lace. PBerger 2016-06-28 01:26:05 +0200
  • 95b95d9c64 fixed some minor issues and renamed equation solver methods slightly to make the names a bit more compact dehnert 2016-06-27 23:23:45 +0200
  • b1f2c26df0 made all instantiations to call MDP model checking with rational numbers dehnert 2016-06-27 20:58:26 +0200
  • d27c75c3d8 fixed missing virtual keyword dehnert 2016-06-27 19:15:21 +0200
  • 512da83a42 added proper mult_add to gmm++ dehnert 2016-06-27 19:10:42 +0200
  • 61a8b9bb29 more work on solvers dehnert 2016-06-27 16:59:37 +0200
  • fbb7e12ff5 first steps towards MAs TimQu 2016-06-27 16:57:44 +0200
  • 6bd95789bd pareto curve output improvements TimQu 2016-06-27 11:29:33 +0200
  • 9ab33528b4 started to fill value iteration implementation in new general min-max solver dehnert 2016-06-26 23:10:35 +0200
  • b4e0cabef6 started working on general min-max solver that uses an underlying linear equation solver. provided necessary factories. adapted code and removed old min-max solvers dehnert 2016-06-26 16:28:07 +0200
  • 248b257f20 enabled rationals/rational functions in CTMC model checker dehnert 2016-06-25 19:43:43 +0200
  • d661454179 started working on instantiating CTMC model checker to rational numbers dehnert 2016-06-25 18:06:11 +0200
  • 80a7126313 postprocessing for pareto curve queries TimQu 2016-06-25 17:59:56 +0200
  • 8153306ced fixed wrong call to Eigen's iterative solvers dehnert 2016-06-25 15:33:41 +0200
  • 46ce68743c enabled precision/max iterations for eigen solver dehnert 2016-06-24 23:07:43 +0200
  • 2a7dc0fad0 renamed MarkovChainSettings dehnert 2016-06-24 21:14:40 +0200
  • 5616004e6e remove debug output dehnert 2016-06-24 20:41:29 +0200
  • 07c787b49d added unsupported solvers of eigen dehnert 2016-06-24 20:34:35 +0200
  • d24fb0cf9a avoid temporary in Eigen solver by providing .noalias(). slightly rewrote matrix-vector expression to benefit more from Eigen's optimization capabilities dehnert 2016-06-24 19:53:32 +0200
  • 69da4ff147 fixed some more problems with Eigen solver dehnert 2016-06-24 19:44:04 +0200
  • f46bcd31c5 fixed typo dehnert 2016-06-24 16:55:26 +0200
  • ba43e23984 using maps for Eigen solver instead of copies of the vectors dehnert 2016-06-24 16:52:40 +0200
  • 7944778b54 Merge branch 'future' into exact_solver dehnert 2016-06-23 19:17:36 +0200
  • 711d5cfa12 fixed bug in sparse dtmc elimination model checker. commented out weird eliminaton functions in CTMC model checker and storm.h dehnert 2016-06-23 18:59:23 +0200
  • 49f59052f8 made model checkers give up possession of matrix to solver when possible dehnert 2016-06-23 18:27:20 +0200
  • 00d331ebb4 moved linear equation solver factories to the respective solver files (and away from utility). restructured settings in factories and the way they are forwarded to the linear equation solvers. fixed all resulting errors dehnert 2016-06-23 18:13:06 +0200
  • e443384b91 Added assertion Mavo 2016-06-23 17:39:03 +0200
  • b30db17f8c added rvalue reference overload to all linear equation solver factories dehnert 2016-06-23 13:24:44 +0200
  • 15a4d4757f added feature to linear equation solver factories to take posession of the matrix to forward it to the solvers dehnert 2016-06-23 13:11:13 +0200
  • b99a063cce Replaced calls to std::abs with calls to std::fabs and included cmath. PBerger 2016-06-23 00:23:55 +0200
  • 40a7948540 started generalizing elimination to equation system solving dehnert 2016-06-22 23:12:13 +0200
  • 3ba5902821 removed debug output and fixed small bug in adaptation of Eigen dehnert 2016-06-22 17:46:02 +0200
  • 13f8f21a70 upgrade to eigen 3.3 and made modifications for different value types via template specializations dehnert 2016-06-22 16:57:36 +0200
  • ad31b2d769 Extended test a little TimQu 2016-06-22 16:33:48 +0200
  • 99b9f11d49 removed eigen-3.2.6 dehnert 2016-06-22 13:59:07 +0200
  • 852afd1718 fixed crowds models to work with exact arithmetic. fixed dynamic state priority queue implementation. added setting to use dedicated elimination-based model checker instead of regular model checker (+ elimination solver) dehnert 2016-06-22 13:11:54 +0200
  • 82d4164c39 added obeying a state ordering to elimination linear equation solver dehnert 2016-06-21 22:40:51 +0200
  • a699272dc6 renamed storm::Variable to storm::RationalFunctionVariable to avoid confusion with storm::expressions::Variable. fixed some Eigen tests dehnert 2016-06-21 21:44:20 +0200
  • 9939341c9d Another test TimQu 2016-06-21 20:48:28 +0200
  • 3cd198c5e3 Some tests, correct handling of results obtained in preprocessing, fixes TimQu 2016-06-21 19:57:22 +0200
  • f3fa90cc37 more work towards exact solving dehnert 2016-06-21 17:02:15 +0200
  • be9648fc18 Added -fPIC to Sylvan. Since it is linked into Storm it is necessary for relocation to be possible, hence PIC. Added includes for cmath at various points. This is a default include on Mac OS but not on any sane systems. Changed calls to std::abs to std::fabs to resolve ambigious call errors. PBerger 2016-06-21 03:03:52 +0200
  • d3de111b3b more work to enable storm to use rational arithmetic dehnert 2016-06-20 23:51:33 +0200
  • af35a4c3ed Merge branch 'jani_support' into exact_solver dehnert 2016-06-20 23:33:48 +0200
  • 3bb36997a1 minor bugfix dehnert 2016-06-20 23:31:33 +0200
  • 8f12b3b8c4 added option 'exact' (in addition to parametric) dehnert 2016-06-20 20:07:39 +0200
  • ce9a6b415c Added tests for some of the benchmarks TimQu 2016-06-20 15:46:37 +0200
  • a02e0eedf7 moved files around TimQu 2016-06-20 14:22:19 +0200
  • cb9cf68632 output of runtime of mec decomposition TimQu 2016-06-20 14:13:36 +0200
  • 8bb25234a3 fixed prism model code (formula used before definition) TimQu 2016-06-20 13:43:14 +0200
  • 4a4a9ad954 fixed/improved the qualitative checks TimQu 2016-06-20 13:42:00 +0200
  • dcf5468b29 Fixed linker error with static function Mavo 2016-06-20 11:40:07 +0200
  • 17ba53dafa Division by Interval not supported Mavo 2016-06-20 11:39:14 +0200
  • 18623f304b some benchmarks TimQu 2016-06-20 10:17:12 +0200
  • 2096c54b84 more explicit instantiations for rational function and some more tests for eigen solver dehnert 2016-06-19 23:20:05 +0200
  • 4e14ecb869 made elimination-based linear solver work in an alpha version. changed minor things in Eigen's SparseLU implementation to make it work with rational numbers and rational functions dehnert 2016-06-19 18:58:31 +0200
  • cf648b5bf1 output of runtimes and other statistics TimQu 2016-06-19 18:30:05 +0200
  • 19fa7767a0 scheduler retrival for value iteration of native minMaxLinEqSolver TimQu 2016-06-19 15:56:21 +0200
  • b58c9d67b9 step bounded objectives TimQu 2016-06-19 15:43:34 +0200
  • 18c1fc3b3f removed debug output TimQu 2016-06-19 15:41:50 +0200
  • 2fed3b647c scheduler benchmark now considers expected reachability reward (total reward was infinite). Bugfix. TimQu 2016-06-19 12:35:50 +0200
  • 5604733854 improvements for preprocessing regarding finite/infinite rewards TimQu 2016-06-18 20:47:37 +0200
  • 35bb3a3c26 renamed elimination settings dehnert 2016-06-18 15:12:24 +0200
  • 8ce9e56af8 some refactoring of state-elimination-related things dehnert 2016-06-18 14:53:58 +0200
  • ec640c12b7 minor fixes to Eigen adapter dehnert 2016-06-18 10:32:04 +0200
  • a17cffbbe3 added missing switch case for new eigen solver dehnert 2016-06-17 17:58:05 +0200
  • 023325b53d added tests for Eigen solver dehnert 2016-06-17 16:50:59 +0200
  • 002bd58b2d added shipped version of Eigen to CMakeList dehnert 2016-06-17 13:39:12 +0200
  • 48e1d20c92 added eigen to resources dehnert 2016-06-17 13:37:37 +0200
  • bb700457de some minor fixes dehnert 2016-06-17 13:22:49 +0200
  • 512a1ec558 added special label 'deadlock' to models and builders dehnert 2016-06-17 11:09:20 +0200
  • 74ee726e35 fixed some typos dehnert 2016-06-17 09:28:17 +0200
  • 94fd4cd9a8 fixed bug related to instantaneous reward properties in formula parser dehnert 2016-06-16 23:56:09 +0200
  • 2accd81aaa fixed bug in reward generation for PRISM models dehnert 2016-06-16 23:48:43 +0200
  • f3701f66fb bugfix for symbolic reachability reward computation dehnert 2016-06-16 18:39:54 +0200
  • 7fef54ab10 modify the ma builder such that it resprects priorities ThomasH 2016-06-16 18:07:41 +0200
  • 3f4b82cf39 add priorities to the transition model ThomasH 2016-06-16 18:00:18 +0200