Commit Graph

  • 47ac26eb02 JaniScopeChanger: Fixed segfault and incorrect detection for variable accesses (GitHub issue #70) Tim Quatmann 2020-05-22 15:31:16 +0200
  • 52b1b8158e Merge remote-tracking branch 'refs/remotes/origin/master' Tim Quatmann 2020-05-22 13:24:13 +0200
  • aae44a3b4b Fixed error message that appeared when using jit. Tim Quatmann 2020-05-22 13:22:40 +0200
  • bf3b70cedf Travis: update Linux docker versions and remove one build stage Matthias Volk 2020-05-21 16:46:08 +0200
  • c09c31be6a Enable pragmas in eigen.h only for GCC 9 Matthias Volk 2020-05-21 16:45:21 +0200
  • 7b6101c220 Updated list of ignored warnings for Eigen Matthias Volk 2020-05-21 13:36:26 +0200
  • 57e42a16de Eigen Patch: Silence a warning regarding unused variable. Tim Quatmann 2020-05-20 15:54:25 +0200
  • ee0e90462f Fixed incorrect result of canHandleStatic for multi-objective formulas for MDP in hybrid engine and MA in sparse engine. Tim Quatmann 2020-05-20 15:47:03 +0200
  • 74f7cd17ea Changed the target directory for the downloaded Eigen headers so that they are now located within the build folder (hopefully avoiding conflicts with multiple build-folders). Made the include path for the Eigen headers more unique, so we no longer use the headers at /urs/include/ instead. Tim Quatmann 2020-05-20 15:17:43 +0200
  • 121589541d Removed old Eigen Sources. Tim Quatmann 2020-05-19 14:05:07 +0200
  • d72f1270e4 Added some documentation for steps on how to update a resource. Tim Quatmann 2020-05-19 14:03:37 +0200
  • 9ba293d760 Fixed trailing whitespace error when applying the Eigen patch. Tim Quatmann 2020-05-19 11:56:08 +0200
  • 9f1487392e We now avoid the renaming of 'Eigen' to 'StormEigen' as this is (hopefully) not needed anymore. Tim Quatmann 2020-05-19 10:36:49 +0200
  • 739ef0b8b4 Updated Eigen version. This fixes issue #77 We also now clone Eigen from the eigen git and perform a patch step. This makes updating the eigen versions more easy in the future. Tim Quatmann 2020-05-19 10:35:31 +0200
  • dd7dc4b797 Towards allowing CLN numbers for RationalNumbers again. Tim Quatmann 2020-05-18 11:21:13 +0200
  • bdcd181458 updated changelog Tim Quatmann 2020-05-12 17:21:00 +0200
  • 28437b089a Merge branch 'master' into almostsurepomdp Sebastian Junges 2020-05-14 11:04:30 -0700
  • a649968a62 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Sebastian Junges 2020-05-14 10:42:32 -0700
  • b6fcdefbbb Merge branch 'prism-pomdp' Tim Quatmann 2020-05-12 16:39:44 +0200
  • e560c7f57c Added some INFO output to check why there is no refinement fixpoint. Tim Quatmann 2020-05-11 13:38:49 +0200
  • ee350ca384 Use same precision as BeliefValueType when dealing with triangulation resolutions. Tim Quatmann 2020-05-11 13:38:24 +0200
  • 92aa029bc5 Removed debug output Tim Quatmann 2020-05-11 10:23:03 +0200
  • 55c4408c6a Storing the observation resolutions as a float so that we can increase the resolution more accurately with a non-integer factor Tim Quatmann 2020-05-11 10:01:18 +0200
  • 2f2a007896 Implemented 'guessing' of initial pomdp schedulers for multiple guesses Tim Quatmann 2020-05-11 09:37:10 +0200
  • 005e23d5d5 two fixes after encoding from non-empty winning regions Sebastian Junges 2020-05-10 18:28:52 -0700
  • 972332810b cosmetic changes, better output, some assertions Sebastian Junges 2020-05-10 18:27:57 -0700
  • 556a884e74 use target state to initialise winning region, better timers and slight improvements in partial scheduler extension Sebastian Junges 2020-05-10 18:27:14 -0700
  • f00a208e9c validate whether a winning region is maximal Sebastian Junges 2020-05-10 18:24:29 -0700
  • d3c593fe74 set validation level from command line Sebastian Junges 2020-05-08 17:25:36 -0700
  • a1f50253d9 compact output of winning region Sebastian Junges 2020-05-08 17:23:50 -0700
  • 2500cc0cd2 Fixed computation of relative gap for special cases (in particular l=u=0) Tim Quatmann 2020-05-08 07:58:25 +0200
  • a95f65cc27 Explicit fall-through Matthias Volk 2020-05-06 18:14:24 +0200
  • ac9fc7b99c Fixed permutations for more than 32 bits by using correct bit-shift Matthias Volk 2020-05-06 17:47:32 +0200
  • 121b082139 Added missing break; statements Matthias Volk 2020-05-06 17:46:30 +0200
  • c039b817ef Removed unused variable + dependent code Matthias Volk 2020-05-06 17:46:03 +0200
  • 6355e07a0c Fix fall-through by using assert Matthias Volk 2020-05-06 17:45:35 +0200
  • 1f67ecb9c7 Merge branch 'master' into dft_bdd_bugfix Matthias Volk 2020-05-06 14:45:09 +0200
  • 896d409602 Implemented simple (but incomplete) check to display whether the belief MDP is finite. Tim Quatmann 2020-05-06 12:44:16 +0200
  • 1766bc385e POMDP Approximation: Use relative gap Tim Quatmann 2020-05-06 10:10:16 +0200
  • fcbce6052c Fixed getting invalid bounds if we abort during the initial approximation step. Tim Quatmann 2020-05-06 10:09:46 +0200
  • 2ebb5e8383 Fixed detection of fixpoints. Tim Quatmann 2020-05-05 14:40:39 +0200
  • 703bdc4eb9 Changed strategy of the dynamic triangulation approach such that the number of "missed" probabilities is minimized Tim Quatmann 2020-05-05 14:39:46 +0200
  • 6ee2ed8550 Merge remote-tracking branch 'origin/master' into prism-pomdp Tim Quatmann 2020-05-05 13:02:38 +0200
  • 71c410a3be Added settings to switch between different triangulation modes. Tim Quatmann 2020-05-05 13:00:52 +0200
  • fa10087fba Implemented triangulation in a more dynamic way. Tim Quatmann 2020-05-05 13:00:26 +0200
  • cc5faee9c0 Fixed initial size threshold for over-approx. Tim Quatmann 2020-05-04 14:35:35 +0200
  • 2ac1c73076 Change default initial resolution to 3 Tim Quatmann 2020-05-04 14:35:15 +0200
  • ab95e7d08b BeliefManager: organized stored beliefs in buckets (beliefs with the same observation belong in the same bucket) Tim Quatmann 2020-05-04 14:34:56 +0200
  • f263d9a39f Remove OVI hm debug elements Jan Erik Karuc 2020-05-03 15:30:05 +0200
  • e6f1c573c4 recent changes added Sebastian Junges 2020-05-02 20:48:34 -0700
  • 10253b25f2 removed xerces-c source from storm. If xerces-c is unavailable, storm will build everything as before, but storm-gspn will not be able to load gspns in XML format. Sebastian Junges 2020-05-02 18:42:02 -0700
  • b915a15758 Merge branch 'dirty' into almostsurepomdp Sebastian Junges 2020-05-02 18:57:15 -0700
  • cd51a7125c Merge branch 'master' into almostsurepomdp Sebastian Junges 2020-05-02 18:57:06 -0700
  • 0a5717aee7 lowlevel storing/loading bitvectors from a string (without any error handling, that is). Helpful to store bitvecots in python Sebastian Junges 2020-05-02 18:56:33 -0700
  • 356eb0b3b1 fix debugging assistance code that is no longer valid when you compute multiple counterexamples Sebastian Junges 2020-05-02 18:55:38 -0700
  • e9e9b15cb1 store/load winning region to file Sebastian Junges 2020-05-02 18:54:39 -0700
  • b2e7c5d5ed various changes to allow restarting and more finegrained selection of switch-and-finish-with-policy Sebastian Junges 2020-05-02 18:51:13 -0700
  • 43bb70e93d bugfix where the wrong successor variables where selected Sebastian Junges 2020-05-02 18:49:34 -0700
  • 5783719c05 add a validator to the winning region search Sebastian Junges 2020-05-02 18:47:43 -0700
  • 93e7bac668 Fix bitshift overflow Daniel Basgöze 2020-05-02 01:56:36 +0200
  • 6f476ef079 belief exploration: Improved fixpoint detection for over-approx Tim Quatmann 2020-05-01 20:43:46 +0200
  • ddec9ce740 ApproximatePomdpModelchecker: Fixed output a little. Tim Quatmann 2020-05-01 16:53:40 +0200
  • 778a4fc71b Added temporary function to apply no-change hm results on lower bound Jan Erik Karuc 2020-04-30 21:12:50 +0200
  • 06941e7c48 Setting 'dft-statistics' prints information about intermediate approximation results Matthias Volk 2020-04-30 17:38:23 +0200
  • 1a1664e350 Updated .gitignore Matthias Volk 2020-04-30 16:46:07 +0200
  • a61ea32aea Fixed some GCC warnings Matthias Volk 2020-04-30 16:41:39 +0200
  • d3c8093e0f Removed unnecessary semicolons Matthias Volk 2020-04-30 16:41:06 +0200
  • f45db73afe Support coloured output for GCC Matthias Volk 2020-04-30 16:38:45 +0200
  • a187a299af Merge branch 'master' into prism-pomdp Tim Quatmann 2020-04-30 15:38:17 +0200
  • 5a221acbd0 Multi-objective model checking: Fixed incorrect computations for some models with end components. (Github Issue #75) Tim Quatmann 2020-04-30 15:38:08 +0200
  • 08c60bcb3d Added OVISolverSettings to storm-pomdp Tim Quatmann 2020-04-27 14:30:50 +0200
  • c0ac9814e1 allow for graph-analysis and sat-based analysis interleaving, and restarting sat-based solver when advantageous Sebastian Junges 2020-04-29 17:07:56 -0700
  • ea73e246a7 A new qualitative reachability analysis for POMDPs/prob1max, based on graphs (sound but incomplete). Sebastian Junges 2020-04-28 12:10:36 -0700
  • 7504f6f315 Improved statistics output for refinements, added detection of fixpoints TimQu 2020-04-28 08:28:39 +0200
  • 5a76f7355d Fixed an issue with refinement of under-approximation Tim Quatmann 2020-04-27 12:38:45 +0200
  • 16ad9d3a83 fixed storm-pomdp output a little. Tim Quatmann 2020-04-27 12:38:24 +0200
  • 96309e1f11 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-04-27 11:39:14 +0200
  • 4eed592811 --timeout now just sends a SIGALRM signal (which can be catched by the signal handler). Tim Quatmann 2020-04-27 11:39:07 +0200
  • 8b4595042e Only do iteration output if the result bound improved. Handle integer overflows for the observation resolution. Tim Quatmann 2020-04-24 08:58:50 +0200
  • a5774cf2bd Merge branch 'master' into almostsurepomdp Sebastian Junges 2020-04-23 16:00:22 -0700
  • 4930908942 new version of containsVariable, with better performance and somewhat better to debug Sebastian Junges 2020-04-23 15:57:16 -0700
  • 91cad8164f trace outputs towards debugging the JaniScopeChanger Sebastian Junges 2020-04-23 15:54:19 -0700
  • e4a4214fc4 towards more helpful output when POMDP is not canonical Sebastian Junges 2020-04-23 15:52:36 -0700
  • 0e97647d9e canonic POMDPs are now annotated with the state valuations and the choice labellings Sebastian Junges 2020-04-23 15:52:06 -0700
  • 5277139640 first version of a generator for belief support MDPs Sebastian Junges 2020-04-23 15:49:43 -0700
  • 94c87a9926 first version of query interface that is more accessible than the winning region itself Sebastian Junges 2020-04-23 15:49:19 -0700
  • 86ece9d324 cleaning code Sebastian Junges 2020-04-23 15:48:37 -0700
  • 43220759f4 Implemented a time limit for exploration. Tim Quatmann 2020-04-23 11:59:43 +0200
  • e81b8f1622 BeliefManager: fixed a few assertion conditions Tim Quatmann 2020-04-23 11:57:56 +0200
  • c91c98f2de Pomdp: Fixing result output with exact numbers Tim Quatmann 2020-04-23 11:56:55 +0200
  • 1763f0c582 Making sure that we only store the best bounds found so far. Also added some output for the resulting values in each iteration. Tim Quatmann 2020-04-23 09:08:02 +0200
  • fa624d2a20 Introduced new settings for controlling the refinement strategy and whether to produce only upper and/or lower bounds Tim Quatmann 2020-04-23 08:27:21 +0200
  • 2d94e77f2a Only display the bound that was requested. Tim Quatmann 2020-04-23 06:30:53 +0200
  • 6dd50575f9 New 'belief-exploration' setting (replaces gridapproximation setting) Tim Quatmann 2020-04-23 06:08:37 +0200
  • 37490a8eca Started to integrate new refinement options. Tim Quatmann 2020-04-22 16:16:26 +0200
  • 45f9c66602 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-04-22 13:53:08 +0200
  • a728c01322 BitVector: Fixed an issue with the move assignment operator. The 'other' BitVector was left in an invalid state. Tim Quatmann 2020-04-22 13:52:58 +0200
  • 75d792e987 Implemented refinement heuristic. Tim Quatmann 2020-04-22 13:51:18 +0200
  • 45832d3de3 BeliefMdpExplorer: Implemented extraction of optimal scheduler choices and reachable states under these choices Tim Quatmann 2020-04-22 12:12:05 +0200
  • 61215e4b24 Over-Approximation: Taking current values as new lower/upper bounds for next refinement step. Tim Quatmann 2020-04-22 09:06:28 +0200