Commit Graph

  • 4ea452854f Fixes for scoring observations Tim Quatmann 2020-04-22 08:58:19 +0200
  • 7e1f5bf2ac Fixed handling of constant BE in approximation Matthias Volk 2020-04-20 20:36:06 +0200
  • 49dac54e8b Fixed typos Matthias Volk 2020-04-20 19:40:42 +0200
  • d5bcec11e3 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-04-20 12:02:45 +0200
  • 88c31b36d0 Equation system based CTMC LRA solving: For the 'inner' linear equation system solver, also set whether the solver type has been set from default. This avoids potentially using unsound/inexact equation solvers. Tim Quatmann 2020-04-20 08:09:29 +0200
  • 1a00b4d22d Merge remote-tracking branch 'origin/master' into prism-pomdp Tim Quatmann 2020-04-20 06:15:02 +0200
  • 7076a54dfb Add error checking to C style io Daniel Basgöze 2020-04-15 21:19:09 +0200
  • b7c53c080b Remove trailing whitespace Daniel Basgöze 2020-04-15 21:18:11 +0200
  • 002d9e1925 Add error checking to C style io Daniel Basgöze 2020-04-15 21:17:07 +0200
  • 1ee87a876a Remove trailing whitespace Daniel Basgöze 2020-04-15 21:16:12 +0200
  • 92f25c1fa7 Use standard integer types instead of size_t Daniel Basgöze 2020-04-03 15:37:03 +0200
  • a244b5ff67 Add assertion for an implied limitation Daniel Basgöze 2020-04-03 15:31:20 +0200
  • d62af9332b Fix bitshift overflow Daniel Basgöze 2020-04-03 15:25:10 +0200
  • 64e70c406e Replace size_t with uint64_t in bitoperations Daniel Basgöze 2020-04-02 21:09:28 +0200
  • aa0fe082d7 Document bitoperations.h Daniel Basgöze 2020-04-02 21:03:09 +0200
  • 972abfcf6f Include required headers Daniel Basgöze 2020-04-02 20:51:32 +0200
  • 4c5abe19f3 Remove unnecessary cast Daniel Basgöze 2020-04-02 20:50:44 +0200
  • be7181f9f2 Removed double include Matthias Volk 2020-04-15 14:20:25 +0200
  • 325b700c62 Explicitly set initialization order for SparseMatrix to avoid nasty segfaults Matthias Volk 2020-04-15 14:19:49 +0200
  • c1b4c3270f Fixed initialization order warnings Matthias Volk 2020-04-15 14:18:46 +0200
  • 2bda04771b Remove duplicate preprocessing Jip Spel 2020-04-15 09:19:35 +0200
  • 6d8c478378 Merge branch 'master' into almostsurepomdp Sebastian Junges 2020-04-14 22:35:05 -0700
  • 92b384c17c fix in recently introduced isSinkState Sebastian Junges 2020-04-14 22:32:52 -0700
  • c7f093575e Merge branch 'master' into almostsurepomdp Sebastian Junges 2020-04-14 18:00:55 -0700
  • b98edfb595 Merge branch 'prism-pomdp' into almostsurepomdp Sebastian Junges 2020-04-14 14:32:47 -0700
  • 5f2a598f48 remove unsound 1-state computation Sebastian Junges 2020-04-14 14:29:30 -0700
  • 6608f9f00d Fixed implementation from CCD16 Sebastian Junges 2020-04-14 14:28:14 -0700
  • 7ba3b6b8d6 Canonic POMDP in -> Canonic POMDP out Sebastian Junges 2020-04-14 14:21:50 -0700
  • e22cbdb91b support for computing the winning region or from initial state, some documentation Sebastian Junges 2020-04-14 14:01:48 -0700
  • 39bfbd5bf7 post merge fixes to interface Sebastian Junges 2020-04-14 13:56:13 -0700
  • 82978f4357 isSinkState Sebastian Junges 2020-04-14 10:34:45 -0700
  • 1ef92dee9e backbone for a simulator on top of explicit state models Sebastian Junges 2020-04-12 21:52:00 -0700
  • feebf1a24d Added scheduler export in .json Tim Quatmann 2020-04-10 16:52:28 +0200
  • 120ec74e3b Fixes for json export of choice origins and state valuations. Tim Quatmann 2020-04-10 16:49:18 +0200
  • a5ebb8b81b Export of choice origins to json Tim Quatmann 2020-04-09 21:13:54 +0200
  • 42be5537ae Added Export of state valuations to JSON Tim Quatmann 2020-04-09 21:11:41 +0200
  • 193bddbd11 add overlapping guards label via command line Sebastian Junges 2020-04-08 22:42:03 -0700
  • af8f901d4a Properly produce schedulers for models with end components. Tim Quatmann 2020-04-08 17:06:09 +0200
  • d098c2d27c graph::computeSchedulerProb1E: Only set choices if they are not defined already. Tim Quatmann 2020-04-08 17:04:32 +0200
  • 0d365ec052 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-04-08 12:32:06 +0200
  • 7ffe322e06 SparseModelMemoryProduct: Fixed incorrect computation of state-action rewards under a randomized policy. Tim Quatmann 2020-04-08 12:31:45 +0200
  • 26764137f5 Fix for --unfold-belief-mdp setting Tim Quatmann 2020-04-08 12:30:39 +0200
  • 3c5df045c1 Added a few assertions Tim Quatmann 2020-04-08 12:18:32 +0200
  • f4f9376c96 Vector: Added a method for element-wise comparison of two vectors. Tim Quatmann 2020-04-08 11:30:19 +0200
  • 03889958da Added a switch to control the size of the under-approximation via command line. Tim Quatmann 2020-04-08 11:29:37 +0200
  • 26a0544e4b BeiliefManager: Use flat_maps for beliefs and hash_maps for belief storage. Tim Quatmann 2020-04-08 10:10:34 +0200
  • fcee1d05fa Fixed an issue with dropping unexplored states. Tim Quatmann 2020-04-08 10:09:45 +0200
  • 2f020ce686 BeliefManager: Making Freudenthal happy (and fast) Tim Quatmann 2020-04-08 08:12:32 +0200
  • 937659f356 First improvement step for Freudenthal triangulation Tim Quatmann 2020-04-07 15:32:08 +0200
  • eca4dab6c0 Beliefmanager: expanding a belief now returns a vector instead of a map Tim Quatmann 2020-04-07 13:43:49 +0200
  • 26864067cf BeliefManager: Made several methods private to hide the actual BeliefType. Tim Quatmann 2020-04-07 13:04:38 +0200
  • 5cd4281133 Further output improvements. Tim Quatmann 2020-04-07 12:50:12 +0200
  • 34d6ac9fe1 Fixed computing a state limit for the under-approximation. Tim Quatmann 2020-04-07 12:44:14 +0200
  • 961baa4386 BeliefMdpExplorer: Various bugfixes for exploration restarts. Unexplored (= unreachable) states are now dropped before building the MDP since we do not get a valid MDP otherwise. Tim Quatmann 2020-04-07 12:43:33 +0200
  • c2837bb749 ApproximatePOMDPModelchecker: Improved output a bit. Tim Quatmann 2020-04-07 12:41:36 +0200
  • c3847d05af Scaling the rating of an observation with the current resolution. Tim Quatmann 2020-04-07 06:37:01 +0200
  • 6540b486e7 NotSupportedException when using drn export for symbolic models Matthias Volk 2020-04-06 14:31:47 +0200
  • c2ddea1480 First (re-) implementation of refinement. (probably needs some testing/debugging) Tim Quatmann 2020-04-03 12:41:55 +0200
  • 7982d58ef7 Combine new upper bound geq cases Jan Erik Karuc 2020-04-03 12:27:13 +0200
  • c07734d80a Handle no change after verification iterations by re-guessing Jan Erik Karuc 2020-04-03 10:39:27 +0200
  • 62c905fc58 Added basis for rewards in dropUnreachableStates() Alexander Bork 2020-04-02 20:05:00 +0200
  • 3041b881d4 Beginning of dropUnreachableStates() Alexander Bork 2020-04-01 22:34:47 +0200
  • 79641ef131 Started to make the BeliefMdpExplorer more flexible, allowing to restart the exploration Tim Quatmann 2020-04-01 15:59:31 +0200
  • 5388ed98e3 BeliefMdpExplorer: Added a few asserts so that methods can only be called in the corresponding exploration phase Tim Quatmann 2020-04-01 12:51:32 +0200
  • 71e0654498 Changed method signatures to new data structures. Tim Quatmann 2020-04-01 12:39:56 +0200
  • 37fa53c4d8 Added a command-line-switch to disable making a pomdp canonic (for prism compatibility) Tim Quatmann 2020-04-01 12:39:02 +0200
  • 52db0c1107 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-03-31 14:43:43 +0200
  • a80553a700 Removed a duplicated method in StandardRewardModel (setStateActionRewardValue did the same as setStateActionReward) Tim Quatmann 2020-03-31 14:43:35 +0200
  • 94d08d73fb Capitalized GUROBI in FindGUROBI.cmake file because it was not found on linux. Tim Quatmann 2020-03-31 14:42:38 +0200
  • 8b0e582ef4 Use the new BeliefMdpExplorer also for the underapproximation. Tim Quatmann 2020-03-31 14:16:21 +0200
  • ab26b69435 Added BeliefMdpExplorer which does most of the work when exploring (triangulated Variants of) the BeliefMdp. Tim Quatmann 2020-03-31 14:01:00 +0200
  • 37da2b4e1f Added a new model checker that allows to compute trivial (but sound) bounds on the value of POMDP states Tim Quatmann 2020-03-31 13:58:45 +0200
  • b8ac41f561 Fixed problem with stormpy by changing boost::optional arguments to const& in GSPNs Matthias Volk 2020-03-30 18:11:13 +0200
  • 41199ea5c7 Append in dot output for DDs Matthias Volk 2020-03-30 14:55:21 +0200
  • 0b552e6813 Renamed BeliefGrid to BeliefManager Tim Quatmann 2020-03-30 13:13:40 +0200
  • 87c8555312 Using the new reward functionalities of BliefGrid. This also fixes setting rewards in a wrong way (previously, the same reward was assigned to states with the same observation). Added auxiliary functions for creating properties. Tim Quatmann 2020-03-30 12:20:13 +0200
  • a3e92d2f72 Using the new reward functionalities of BliefGrid. This also fixes setting rewards in a wrong way (previously, the same reward was assigned to states with the same observation). Tim Quatmann 2020-03-30 12:18:06 +0200
  • 98bb48d3c5 BeliefGrid: Adding support for rewards. Tim Quatmann 2020-03-30 12:07:49 +0200
  • bc10fecf11 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-03-30 09:35:40 +0200
  • 743dc3e8b1 Cmake: Silence some cmake warnings that recently appear (part 2) Tim Quatmann 2020-03-30 09:01:05 +0200
  • db0caac670 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-03-30 08:38:45 +0200
  • dc7aabc2f1 Fixed moving a reference away. Tim Quatmann 2020-03-29 20:28:26 +0200
  • 1603f0569d Silenced a gcc warning. Tim Quatmann 2020-03-29 20:27:45 +0200
  • 48395f1218 Cmake: Fixed capitalization of z3 and hwloc to silence some cmake warnings that recently appear. Tim Quatmann 2020-03-29 16:11:24 +0200
  • 83fce0118c Merge branch 'prism-pomdp' into almostsurepomdp Sebastian Junges 2020-03-28 16:24:22 -0700
  • 110453146d Various fixes for under/over approximation with rewards. Tim Quatmann 2020-03-28 20:29:18 +0100
  • 3887e8a979 Fix for belief triangulation. More descriptive output for belief triangulation asserts. Tim Quatmann 2020-03-28 20:28:15 +0100
  • b3115e9395 Code polishing and re-enabled the under-approximation. Refinement should still not be possible right now. Tim Quatmann 2020-03-28 07:27:53 +0100
  • d184d67b53 Refactored under-approximation code a bit. Tim Quatmann 2020-03-28 07:24:42 +0100
  • 97842f356d Fixed beliefgrid exploration. Tim Quatmann 2020-03-28 05:20:59 +0100
  • b3796d740f Fixed confusing lower and upper result bounds for minimizing properties. Tim Quatmann 2020-03-28 05:20:06 +0100
  • 6fee61feb1 POMDP: Started to split belief logic from exploration logic. Tim Quatmann 2020-03-27 15:11:52 +0100
  • b53b6ab275 Added missing line breaks Tim Quatmann 2020-03-27 06:31:11 +0100
  • b600498d0e Better output for checking the fully observable model. Tim Quatmann 2020-03-25 14:06:19 +0100
  • a8f891aa06 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-03-25 11:06:33 +0100
  • 8c32705b99 Silenced deprecation warnings from newer versions of IntelTBB (since version 2020?). These warnings only referred to features we do not use and could be addressed by only including the relevant parts of inteltbb Tim Quatmann 2020-03-25 11:00:14 +0100
  • 7f102c915b Improved some output Tim Quatmann 2020-03-25 10:58:19 +0100
  • a8f3205d96 minor clean-up of includes Tim Quatmann 2020-03-25 08:52:08 +0100
  • 3220354187 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-03-24 15:07:02 +0100
  • 1187c0fca1 Added a CMAKE option for ThinLTO Tim Quatmann 2020-03-24 15:06:44 +0100