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

Commit Graph

  • 5f831d156f forceBounds option for native solver TimQu 2018-01-18 18:01:41 +0100
  • 7bdecad4ad fixed compiling TimQu 2018-01-18 18:00:55 +0100
  • 25260c7602 added settings for the new topological min max solver TimQu 2018-01-18 17:53:06 +0100
  • b69543802d completed the renaming from topologicalValueIterationMinMaxSolver to TopologicalCudaMinMax... TimQu 2018-01-18 17:51:31 +0100
  • 29b40899bf Removed settings of old topologicalvalueiteration solver TimQu 2018-01-18 17:50:44 +0100
  • a2bd1e0026 renamed argument from getRequirements so that it is easier to understand TimQu 2018-01-18 17:32:03 +0100
  • 6b3a02d732 Fixing topological cuda TimQu 2018-01-18 16:58:15 +0100
  • 7eab8589bd Fixed issue in qpower TimQu 2018-01-18 16:34:21 +0100
  • 2d910b79ed Introduced new topological min max solver TimQu 2018-01-18 16:33:47 +0100
  • 4ab47671f5 Renamed TopologicalMinMaxLinearEquationSolver -> TopologicalCudaMinMaxLinearEquationSolver TimQu 2018-01-18 11:57:13 +0100
  • 3b394a965e some qvi optimizations TimQu 2018-01-18 11:43:16 +0100
  • 8c3991fb2f respecting lower/upper bounds from preprocessing in quick sound power method TimQu 2018-01-18 10:38:59 +0100
  • 96845e2669 restructured quick power iterations a little TimQu 2018-01-18 09:52:47 +0100
  • 68c91e4fa2 Merge branch 'pomdp_datastructures' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm into pomdp_datastructures Sebastian Junges 2018-01-17 11:52:16 +0100
  • 78cfb10c7e fixed qvi with negative rewards TimQu 2018-01-16 15:20:43 +0100
  • 31821bc1d0 Display DFT stats Matthias Volk 2018-01-15 18:24:51 +0100
  • 24d9b8dfc6 minor reformulation dehnert 2018-01-15 16:33:52 +0100
  • 096d532aa0 Small changes Matthias Volk 2018-01-15 14:04:57 +0100
  • e4e467622f Minor fixes Matthias Volk 2018-01-15 13:28:30 +0100
  • ca0d76e502 Finished JSON export for GSPNs Matthias Volk 2018-01-15 11:34:59 +0100
  • ea2a56ece7 Json translation for places and transitions Matthias Volk 2018-01-15 00:19:43 +0100
  • b901b2ce7d Started on GSPN to Json export Matthias Volk 2018-01-14 23:50:03 +0100
  • e9a57aa3e5 Cleanup after processing options Matthias Volk 2018-01-14 23:18:03 +0100
  • 770fc83e7f Generalization loadDFT Matthias Volk 2018-01-14 23:13:59 +0100
  • 0289f12d45 Merge branch 'master' into pomdp_datastructures sjunges 2018-01-14 16:17:39 +0100
  • 09d31a3b66 Merge branch 'pomdp_datastructures' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm into pomdp_datastructures sjunges 2018-01-14 16:16:52 +0100
  • d34a2dd9fd fix for mec choice elimination TimQu 2018-01-14 15:53:16 +0100
  • 355510c808 Fixed call of wrong 'specify' method TimQu 2018-01-14 15:11:33 +0100
  • e2f8fe2b30 Merge branch 'pla_without_simplification' TimQu 2018-01-14 14:41:22 +0100
  • eab7e409e9 Fixed Running PLA without simplification TimQu 2018-01-14 14:40:39 +0100
  • e023f27714 test case for disabled simplification Sebastian Junges 2018-01-13 15:12:03 +0100
  • 8cd3f1bc1a added a switch to disable simplifications within PLA Sebastian Junges 2018-01-13 14:19:39 +0100
  • 820f2ddf4c extended mec eliminator to minimal rewards TimQu 2018-01-12 19:25:28 +0100
  • 90087ff526 added transformation to binary pomdp TimQu 2018-01-12 19:25:07 +0100
  • 895fda241c Merge branch 'master' into sound-vi TimQu 2018-01-12 18:45:20 +0100
  • 61a44121b3 improved computation of lower/upper bounds for multi-objective model checking TimQu 2018-01-12 13:49:56 +0100
  • fd7f8c7bac Fixed an issue related to multi-objective model checking of models with potentially infinite expected reward TimQu 2018-01-11 21:51:58 +0100
  • 93eb0b19d4 Merge remote-tracking branch 'origin/master' into highlevelcex dehnert 2018-01-12 15:56:39 +0100
  • 59666a9fe9 slight renaming in matrix builder to better capture semantics dehnert 2018-01-12 10:05:13 +0100
  • fc422af557 making things compile again in debug mode TimQu 2018-01-11 21:48:47 +0100
  • 99647c11fb fixed an issue pointed out by Tim dehnert 2018-01-11 19:18:36 +0100
  • 9dea83055b added cache to Z3 expression translator to speed up the translation of large constraints dehnert 2018-01-11 14:42:59 +0100
  • 459763c019 investigating a cut-related issue in high-level cex dehnert 2018-01-10 16:42:06 +0100
  • 4a321aab28 delete comment Timo Philipp Gros 2018-01-06 18:55:00 +0100
  • 6a52a953c2 clean up code Timo Philipp Gros 2018-01-06 17:56:47 +0100
  • 2ea911f865 finished version of implementation Timo Philipp Gros 2018-01-06 17:09:02 +0100
  • 0d1de8aba9 restructured code, SCC missing Timo Philipp Gros 2018-01-06 13:23:20 +0100
  • fa7f74f0f1 quicker iterations when the decision value blocks the bound TimQu 2018-01-05 14:53:24 +0100
  • 0215258709 made qvi implementation a little bit more readable TimQu 2018-01-05 14:18:22 +0100
  • 01dc240eea fixed checking carl version dehnert 2018-01-04 16:32:02 +0100
  • ebeb34b791 implemented heuristic for pla that helps to decide with respect to which parameters a region should be splitted TimQu 2018-01-04 13:48:27 +0100
  • c81c7b0be5 Fixed issue with restarting TimQu 2018-01-04 09:28:55 +0100
  • 00e0997850 Merge branch 'straight' Timo Philipp Gros 2018-01-03 18:41:16 +0100
  • 58a4a7cd68 Merge remote-tracking branch 'upstream/master' Timo Philipp Gros 2018-01-03 18:40:58 +0100
  • 80219e4a2d quick value iteration restart TimQu 2018-01-03 13:38:31 +0100
  • 7cd7cd60a7 Added new minmax settings: force computation of a priori bouds and tweak the qvi restart heuristic TimQu 2018-01-03 13:29:12 +0100
  • 7aac41d8f2 optimized qvi implementation TimQu 2018-01-03 09:00:37 +0100
  • 116bd58b22 log improvements + minor bugfixes for qvi TimQu 2018-01-02 17:22:30 +0100
  • f65bb48195 fixed missing initialized value in progressMeasurement TimQu 2018-01-02 17:21:56 +0100
  • 9c96bd0a1c First implementation of quick value iteration for MinMax Equation systems TimQu 2018-01-02 13:54:57 +0100
  • 8260455a55 Added multiplication of a single matrix row with a vector to the linear equation solver interface TimQu 2018-01-02 11:55:43 +0100
  • b9007aa2e9 removed logprints Timo Philipp Gros 2018-01-02 10:34:44 +0100
  • feabd1186d Merge remote-tracking branch 'origin/master' into sound-vi TimQu 2017-12-23 21:34:29 +0100
  • 66cb8c60d0 fixed applying a custom row-grouping if there is none in high-level cex dehnert 2017-12-22 07:53:07 +0100
  • cdb35c8bac fixed issue related to high-level counterexamples for liveness properties dehnert 2017-12-21 22:01:39 +0100
  • cfd1986c52 Merge branch 'highlevelcex' dehnert 2017-12-21 18:46:45 +0100
  • 4591dba631 made maxsat-based counterexample generation be applicable to DTMCs and MDPs dehnert 2017-12-21 18:46:34 +0100
  • 3a94b8ad69 ignoring kappa, taking in account epsilon Timo Philipp Gros 2017-12-21 17:50:54 +0100
  • 676120229b intermediate stage dehnert 2017-12-21 15:59:39 +0100
  • d2785bb1d7 Merge remote-tracking branch 'origin/master' into sound-vi TimQu 2017-12-21 13:13:01 +0100
  • f90eb4708d fix for boost 1.66 TimQu 2017-12-21 13:08:18 +0100
  • 0004c9b2bb adding version with value iteration Timo Philipp Gros 2017-12-21 01:08:57 +0100
  • 284a792c1a highlevel counterexamples for smt: get conflict set directly sjunges 2017-12-21 00:37:51 +0100
  • 8ce3eaddc3 PrismProgram -- Used Constants sjunges 2017-12-21 00:37:31 +0100
  • 91d0cdf41d fix non-terminating while loop in high level counterexamples sjunges 2017-12-21 00:36:57 +0100
  • 5ecb84b209 Merge remote-tracking branch 'upstream/master' Timo Philipp Gros 2017-12-21 00:18:20 +0100
  • d366126a63 solved merge conflict Timo Philipp Gros 2017-12-21 00:17:33 +0100
  • 8646d614d4 reduced the number of initial buckets for the hash map used in explicit model building dehnert 2017-12-20 20:45:47 +0100
  • d1641f09eb added a script to check multiple cmake configurations and updated the release checklist TimQu 2017-12-20 11:24:38 +0100
  • 0ce91b7eb4 updated changelog TimQu 2017-12-20 11:23:45 +0100
  • ea6c957030 tests for multi-dimensional cost bounded DTMCs TimQu 2017-12-20 10:46:56 +0100
  • c59d2160ee Implemented (multi-dimensional) cost bounded properties for DTMCs (sparse engine only) TimQu 2017-12-20 10:46:38 +0100
  • 8e7d3107ca added function to check whether a matrix is the identity matrix TimQu 2017-12-20 10:45:39 +0100
  • 95c23b50d1 removing log prints again Timo Philipp Gros 2017-12-19 18:26:56 +0100
  • 7577ca48ec changed loop of diff checking; ; Timo Philipp Gros 2017-12-19 17:17:51 +0100
  • 8aa9df8db9 solved Timo Philipp Gros 2017-12-19 10:35:13 +0100
  • e5f71aa851 prints for foxGlynn Timo Philipp Gros 2017-12-19 10:30:09 +0100
  • e4800543df update settings objects Sebastian Junges 2017-12-19 09:43:17 +0100
  • 88851f0105 install headers to include/storm sjunges 2017-12-18 23:34:58 +0100
  • 37e0385e69 Remove hack in travis tests Matthias Volk 2017-12-15 11:05:14 +0100
  • 109b738258 adding some more output to Fox-Glynn dehnert 2017-12-14 17:31:52 +0100
  • dd864c05e0 properly resizing weights vector in Fox-Glynn if the right bound is moved further due to the desired accuracy dehnert 2017-12-14 11:43:04 +0100
  • cc8b6f6af0 fixed stupid uniformisation bug Timo Philipp Gros 2017-12-13 21:04:58 +0100
  • 49a6c5f4ed Fixed docker upload in travis Matthias Volk 2017-12-13 17:51:35 +0100
  • ccbcd4ef5e Merge branch 'simpleMDPApproach' of github.com:TimoPGros/storm into simpleMDPApproach Timo Philipp Gros 2017-12-13 16:25:47 +0100
  • 95c12cf6d8 new use of FixGlynn Timo Philipp Gros 2017-12-13 16:25:29 +0100
  • 9dda579e58 slightly patched Fox-Glynn dehnert 2017-12-13 16:18:13 +0100
  • 91a9f5622f Push successful builds in travis to dockerhub Matthias Volk 2017-12-12 14:43:45 +0100
  • d8e166094f Message in cmake if ccache is disabled Matthias Volk 2017-12-12 14:37:50 +0100
  • 2d8cc1681c Fixed indentation Matthias Volk 2017-12-12 14:37:22 +0100