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

Commit Graph

  • e5572db54e eliminating ECs for sound value iteration for until probabilities dehnert 2017-09-19 14:27:30 +0200
  • b4bfd0c39f performance improvement in DS-MPI; some cleanups dehnert 2017-09-18 20:46:57 +0200
  • 630acb7459 parsing of until formulas with multiple bounds TimQu 2017-09-18 18:43:04 +0200
  • 36c3a4d9ef Avoided conversion of memory states. They are now directly represented as 64 bit integers TimQu 2017-09-18 17:54:38 +0200
  • 19ac4a360f intermediate commit dehnert 2017-09-18 14:58:25 +0200
  • 37d5dceaab added small check TimQu 2017-09-18 11:35:34 +0200
  • 7fc65707a9 set the maximal value for each dimension. Also support for dependent dimensions TimQu 2017-09-18 11:35:16 +0200
  • 8f8f0bf804 corrected the search for the set of reachble epoch classes TimQu 2017-09-18 11:34:20 +0200
  • d0209a804b Setting reachable product states now also uses the transformMemoryState method TimQu 2017-09-18 09:49:56 +0200
  • cb849a9ab8 started on computing upper bounds for rewards for interval value iteration dehnert 2017-09-17 22:49:21 +0200
  • 9d98bf5fa8 automatically switching solvers if soundness is enforced dehnert 2017-09-16 12:46:22 +0200
  • df0b5fbfa5 fixed multiply-reduce operations in the presence of empty row groups dehnert 2017-09-16 11:52:23 +0200
  • 17a45a43eb better transformation of memory states TimQu 2017-09-15 23:19:30 +0200
  • d25cc4b05f first version of sound value iteration dehnert 2017-09-15 14:48:07 +0200
  • 7d4a438e82 Fixes for lower bounds TimQu 2017-09-15 13:20:59 +0200
  • ade8078759 added test for lower bounded properties TimQu 2017-09-15 12:59:18 +0200
  • ec61e110f2 introducing solver formats to enable linear equation solvers to take the fixed point rather than the equation system formulation dehnert 2017-09-14 22:45:07 +0200
  • b054b67312 first version for lower bounded properties TimQu 2017-09-14 17:43:21 +0200
  • 4ba20d11d4 more functionality for epoch manager TimQu 2017-09-14 17:42:45 +0200
  • 8e8fc34c30 fixed some TBB-related issues and added power method for linear equation systems dehnert 2017-09-14 15:54:06 +0200
  • bac50a32ab warkaround for gcc 7.2.0: make modernjson compile again dehnert 2017-09-14 13:35:46 +0200
  • 2d99ff3126 preserving action knowledge from first to second PRISM parser pass dehnert 2017-09-14 10:47:14 +0200
  • c5134c364f Extraction and update of TBB-parallelized stuff dehnert 2017-09-13 18:46:55 +0200
  • d129683c61 gathered dimension related data into a struct. Also started with lower reward bounds TimQu 2017-09-13 17:22:25 +0200
  • 41cf4e76db The solutions are now stored epoch-wise and will be erased as soon as all predecessor epochs are computed TimQu 2017-09-13 13:34:21 +0200
  • 3044aaa3f5 The product model is now handled in a separate class TimQu 2017-09-13 12:17:16 +0200
  • 1ccc241462 computations on epochs are now handled in a separate class TimQu 2017-09-13 10:30:16 +0200
  • d3e50b8769 optimized productInState Computation TimQu 2017-09-13 09:22:02 +0200
  • bba2832e5b finished Walker-Chae method dehnert 2017-09-11 22:17:42 +0200
  • 47ab74a16b implemented single objective queries TimQu 2017-09-11 15:32:46 +0200
  • 8b466f1fa7 extended multidimensional bounded until formulas to have different subformulas in each dimension TimQu 2017-09-11 15:28:36 +0200
  • 5440d164b2 started on Walker-Chae algorithm dehnert 2017-09-11 13:27:48 +0200
  • c77b9ce404 gauss-seidel style multiplication for gmm++ dehnert 2017-09-10 22:23:09 +0200
  • 43643b9699 bump gmm++ version to 5.2 (from 5.0) dehnert 2017-09-10 10:30:46 +0200
  • d27954622a slightly changed handling of gauss-seidel invocations in linear equation solver dehnert 2017-09-10 09:30:23 +0200
  • 6e548627ee adding storm-pgcl as a dependency to target binaries dehnert 2017-09-10 09:11:26 +0200
  • 00f88ed452 gauss-seidel-style value iteration dehnert 2017-09-09 20:56:16 +0200
  • cbe73081f8 zig zag epoch computation order TimQu 2017-09-08 17:17:02 +0200
  • 6ae05560fc setting solutions in place TimQu 2017-09-08 16:07:59 +0200
  • 9d95d2adcf first version of multiply-and-reduce (only for native) dehnert 2017-09-08 16:10:20 +0200
  • e37d5869ef extracted static version to separate cmake file dehnert 2017-09-08 13:58:13 +0200
  • dd035f7f5e allow for summand in matrix-vector multiplication dehnert 2017-09-08 13:57:57 +0200
  • 488479b5a7 better objectiveRewardFilter TimQu 2017-09-08 12:11:53 +0200
  • cd6a79de23 used cache memory when checking each epoch TimQu 2017-09-08 11:40:55 +0200
  • 13ade58fa0 using pair<uint, uint> in the map instead of vectors of size 2 TimQu 2017-09-08 09:29:59 +0200
  • 3c844a487f some more optimizations dehnert 2017-09-07 22:15:10 +0200
  • 3a309caafc epochs are now uints instead of vector<int>s TimQu 2017-09-07 18:53:32 +0200
  • 5fafe835cb started on some optimizations for conditionals in MDPs dehnert 2017-09-07 14:56:32 +0200
  • 27ee299f63 more efficient comparison of epoch classes TimQu 2017-09-07 14:49:33 +0200
  • cf91a34970 use cached memory for the epoch results TimQu 2017-09-07 14:35:05 +0200
  • 9735ff98d0 SolutionType is now a single vector instead of a struct TimQu 2017-09-07 11:38:09 +0200
  • d6099a91a7 Further optimizations for setEpoch + started to work on single objective mode TimQu 2017-09-07 10:39:18 +0200
  • 57e604a815 optimized setCurrentEpoch a little TimQu 2017-09-07 09:45:59 +0200
  • e4ac32a6fc fixed selection of considered state in reduced model and optimized setting the stepsolutions TimQu 2017-09-06 17:54:53 +0200
  • 45e0796228 updated changelog dehnert 2017-09-06 14:52:08 +0200
  • 11fc1d29eb more output for statistics TimQu 2017-09-06 14:40:30 +0200
  • cffc3e606e Merge branch 'master' into solver_requirements dehnert 2017-09-06 12:38:51 +0200
  • 1985a29c5d Merge branch 'master' into reward-bounded-multi-objective TimQu 2017-09-06 11:44:18 +0200
  • b7e2aec82c Fixed issue where variable names were reserved symbols of Exprtk TimQu 2017-09-06 11:43:33 +0200
  • ff8c7813bb commented out failing tests in the fragmentchecker TimQu 2017-09-06 11:33:19 +0200
  • 83fdffadc6 adapted tests; in particular enabled previously disabled rewards test dehnert 2017-09-06 11:27:25 +0200
  • 9bda631795 symbolic MDP helper respecting solver requirements dehnert 2017-09-06 10:53:31 +0200
  • 7c24607427 started on symbolic solver requirements dehnert 2017-09-05 22:16:54 +0200
  • e81d979d56 hybrid MDP helper respecting solver requirements dehnert 2017-09-05 18:18:05 +0200
  • 1bb8b3b497 only store the results that will be needed eventually TimQu 2017-09-05 17:04:21 +0200
  • 62e4558af1 reduced number of states considered in the epoch model TimQu 2017-09-05 16:46:08 +0200
  • 8e56efed3a reduced the number of states in the product model TimQu 2017-09-05 16:09:37 +0200
  • 999fd0752c The model memory product can now retrieve the reachable states without actually building the product TimQu 2017-09-05 13:49:12 +0200
  • 11a4f8d016 restructured initialization of modelmemory product TimQu 2017-09-05 11:30:46 +0200
  • a3cbaedcc1 intermediate commit to switch workplace dehnert 2017-09-05 11:20:54 +0200
  • 90a7ea4907 printing timing information TimQu 2017-09-05 10:36:54 +0200
  • 12b10af672 started on hybrid MDP helper respecting solver requirements dehnert 2017-09-04 21:32:06 +0200
  • 61a6b178b7 restricted the number of reachable product states TimQu 2017-09-04 17:30:59 +0200
  • 3c4de8ace3 moved requirements to new file dehnert 2017-09-04 16:16:32 +0200
  • 4c5cdfeafc Sparse MDP helper now also respects solver requirements for reachability rewards dehnert 2017-09-04 15:51:34 +0200
  • f327ff75e9 showing progress for bisimulation dehnert 2017-09-04 09:28:15 +0200
  • 74eeaa7f81 computing unbounded until on MDPs with the sparse helper now respects solver requirements dehnert 2017-09-03 21:29:47 +0200
  • 40edc0ca4d assert that there are no endcomponents with positive rewards TimQu 2017-09-01 18:13:17 +0200
  • e48c822941 fixed csma test TimQu 2017-09-01 17:59:41 +0200
  • 529526593b improved structure in rewardunfolding TimQu 2017-09-01 17:36:38 +0200
  • 2bccb7af78 modelMemoryProduct can now return the considered model and memory structure TimQu 2017-09-01 16:28:02 +0200
  • de1e9967a3 added some necessary conditions for the rewardbounded weight vector checker TimQu 2017-09-01 16:26:32 +0200
  • 0cca4a51d0 added weight vector checker for reward bounded objectives TimQu 2017-09-01 14:30:17 +0200
  • 721dd37a62 Moved reduction of the preprocessed model into the weightvectorchecker TimQu 2017-09-01 14:12:33 +0200
  • 76c01de25c use utility::vector::max_if to compute the maximum exit rate in an MA TimQu 2017-09-01 14:11:05 +0200
  • 4d248eb0a1 fixed assertion TimQu 2017-09-01 14:08:43 +0200
  • 8efccd76d2 started to make multi-objective preprocessing more flexible w.r.t. different checkers TimQu 2017-08-31 12:05:39 +0200
  • dae09653e5 Merge remote-tracking branch 'origin/master' into reward-bounded-multi-objective TimQu 2017-08-31 08:27:16 +0200
  • 569b0122b8 introduced different minmax equation system types for requirement retrieval dehnert 2017-08-30 21:30:02 +0200
  • f7c803827b remove debug output dehnert 2017-08-30 21:00:15 +0200
  • 4adee85fa5 added checking requirements of MinMax solvers to model checker helpers dehnert 2017-08-30 20:59:20 +0200
  • 3829b58e0d introduced top-level solve equations function to centrally check for requirements dehnert 2017-08-30 19:26:54 +0200
  • 72234e96b2 started on requirements for MinMax solvers dehnert 2017-08-30 18:13:47 +0200
  • 31af523ea1 implemented caching of the EC elimination result in the standard weight vector checker TimQu 2017-08-30 16:02:31 +0200
  • 9716289f6a Added abstract superclass for WeightVectorCheckers TimQu 2017-08-30 15:17:39 +0200
  • 3c8f9a2ecf Added 5th build stage Matthias Volk 2017-08-30 14:46:02 +0200
  • e278c3ef69 moving from internal reference to pointer in StandardMinMax solver equipped MinMax solvers with default constructors dehnert 2017-08-30 12:39:27 +0200
  • 591a53582a fixed test TimQu 2017-08-30 09:39:05 +0200
  • e0253ecba2 fixed new test TimQu 2017-08-29 17:15:49 +0200
  • acd6c5e9be fix for toIntegralVector TimQu 2017-08-29 17:13:37 +0200