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

Commit Graph

  • 8b2b0008da The stack check issue has been fixed in newer AppleClang versions. Thus, we no longer have to disable stack checks for AppleClang 11.0.3 or higher. TimQu 2020-07-15 09:51:00 +0200
  • 5b7bc4319a
         Missing pragma once Matthias Volk 2020-07-13 15:05:16 +0200
  • 3282bf895c more support for the modulo expression Sebastian Junges 2020-07-12 21:58:19 -0700
  • d76bcc4d10 pPOMDP support Sebastian Junges 2020-07-09 23:00:10 -0700
  • 62757e28f7 parametric pomdps? Sebastian Junges 2020-07-09 22:00:26 -0700
  • b84ada827a expression to dice Sebastian Junges 2020-07-07 20:08:30 -0700
  • cf3bfc3d2d simulator presents rewards for efficiency Sebastian Junges 2020-06-18 12:26:51 -0700
  • ceab2c4985 update changelog Sebastian Junges 2020-06-13 18:17:41 -0700
  • 9c33cec3b6
         Added mising include Matthias Volk 2020-06-14 16:38:19 +0200
  • 3a70c68d45 dd-based reachability exploration reports number of iterations in return value Sebastian Junges 2020-06-13 18:10:44 -0700
  • bb200fe9f4 simplify prism programs now also simplifies labels Sebastian Junges 2020-06-13 18:10:06 -0700
  • b901a1b308 fix for the binary pomdp transformer: labels are now attached to auxiliary states as well Sebastian Junges 2020-06-13 18:09:22 -0700
  • 4350ea72d7 Simplifying expressions with iff and implies a bit more Sebastian Junges 2020-06-09 14:30:43 -0700
  • 7d4bb545f6 Export option STORM_HAVE_XERCES for stormpy Matthias Volk 2020-06-10 16:15:05 +0200
  • f1462bfda7 Cmake: added a comment that the stack check issue seems to be resolved in more recent clang versions (but still not in the one that comes with the command line tools right now) Tim Quatmann 2020-06-10 15:55:37 +0200
  • 0791fc723e renamed files Sebastian Junges 2020-06-04 22:28:43 -0700
  • 0cb0ca8a48 Storm version 1.6.0 Matthias Volk 2020-06-08 16:11:49 +0200
  • a7f847d4e1 KnownProbabilityTransformer: Removed output of model info to std::cout Tim Quatmann 2020-06-08 15:57:05 +0200
  • 5536cda902 BeliefExplorationModelCheckerTest: added refuel test case Tim Quatmann 2020-06-08 15:53:38 +0200
  • 1313e3c096 BeliefExplorationModelCheckerTest: added maze2 test case Tim Quatmann 2020-06-08 15:37:32 +0200
  • 5076ff00c6 Removind debug output. Tim Quatmann 2020-06-08 15:37:03 +0200
  • cc4379130f BeliefExplorationPomdpModelCheckerTest: More tests and testing of preprocessed models. Tim Quatmann 2020-06-08 14:34:02 +0200
  • 2ed1813b39 Cleaner code and checks for GlobalPomdpSelfLoopEliminator Tim Quatmann 2020-06-08 12:03:41 +0200
  • f4a3ceb60e Skipping tests that fail for z3 version 4.8.8 (Issue reported at https://github.com/Z3Prover/z3/issues/4465) Tim Quatmann 2020-06-08 10:06:49 +0200
  • eeeb3df4f8 Added some tests for BeliefExplorationPomdpModelChecker and made the testing more sensible towards very imprecise results Tim Quatmann 2020-06-05 16:52:28 +0200
  • 31c39d1dc7 storm-pomdp: Cleaned up output of belief exploration. Use --verbose to restore it. Tim Quatmann 2020-06-05 16:50:35 +0200
  • 08f82d44f1 Renamed ApproximatePOMDPModelchecker to BeliefExplorationPomdpModelChecker Tim Quatmann 2020-06-04 15:39:54 +0200
  • 67bcafe5e1 storm-pomdp: Cleaned up includes of BeliefManager and BeliefMdpExplorer. Tim Quatmann 2020-06-04 15:32:14 +0200
  • 073d2affa4 api/verification: Added a missing include Tim Quatmann 2020-06-04 15:24:57 +0200
  • 74c2f83110 Separated header and logic for struct in BeliefMdpExplorer Alexander Bork 2020-06-01 23:49:31 +0200
  • 1cce958e12 Separated header and logic for BeliefMdpExplorer Alexander Bork 2020-06-01 23:41:57 +0200
  • 8b7ab24d66 Moved struct functions to cpp-file Alexander Bork 2020-06-01 22:39:50 +0200
  • 4f61ab422e Separated BeliefManager header and logic Alexander Bork 2020-06-01 21:16:43 +0200
  • 4f5d54c310 Fixed error message. Tim Quatmann 2020-06-04 15:01:57 +0200
  • 202c25c3db Added first working test case Tim Quatmann 2020-06-04 15:01:41 +0200
  • 5aa3610f2e Model building: Set automatically building choice labels and origins within the BuilderOptions (previously, this was done in the cli code) Tim Quatmann 2020-06-04 14:53:53 +0200
  • e9ab8e65d4 model building: Fixed correctly setting the number of reserved bits for unbounded state variables from the cli option Tim Quatmann 2020-06-04 14:51:25 +0200
  • ae9360af03 Use the new MakeStateSetObservationClosed transformer for the belief-exploration based pomdp model checker Tim Quatmann 2020-06-04 14:00:59 +0200
  • 8c38333dd1 Added transformer that can make a given set of states (e.g. goal states) observation closed. Tim Quatmann 2020-06-04 14:00:19 +0200
  • 764b6c9a3b Added small pomdp example. Tim Quatmann 2020-06-04 13:57:06 +0200
  • c7d167fda3 Delete accidentally pushed makefiles. Tim Quatmann 2020-06-04 09:03:13 +0200
  • c788ec430d First version of test frame work for belief exploration. Tim Quatmann 2020-06-04 09:02:26 +0200
  • cd4ad03f37 Added output 'DEBUG BUILD' in case storm is running in debug mode. Tim Quatmann 2020-06-03 10:18:34 +0200
  • 55c71a8297 Updated .gitignore to recent changes Tim Quatmann 2020-06-03 10:13:55 +0200
  • 70d10bd037 Moved generated file `storm-version.cpp` to build folder. Moved version information to new library `storm-version-info` (addressing Github issue #78) Tim Quatmann 2020-06-03 10:13:39 +0200
  • c9ef222a7f somewhat improved counting of winning region sizes Sebastian Junges 2020-06-02 19:45:00 -0700
  • 3a206784a3 better logging Sebastian Junges 2020-06-02 19:44:27 -0700
  • ad39b23c1c StateValuations: Added class to conveniently iterate over the variable-value assignments of a given state Tim Quatmann 2020-06-02 14:17:46 +0200
  • a7b6e00e88 builderoptions no longer implicitly takes settings from buildersettings Sebastian Junges 2020-05-30 18:44:50 -0700
  • d71e70da42 build-all-labels for building all labels without building everything, and renamed build-overlapping-guards-label and build-out-of-bounds-state Sebastian Junges 2020-05-30 18:41:02 -0700
  • c4c680438f fix exporting POMDPs with rewards & observations Sebastian Junges 2020-05-29 23:19:17 -0700
  • 9d35eab33e fix warning regarding hash Sebastian Junges 2020-05-29 23:16:29 -0700
  • 390a2ada04 remove test file that should not have been committed Sebastian Junges 2020-05-29 09:47:03 -0700
  • 5b103579f2 Fixed building state valuations for transient variables of a jani model. Tim Quatmann 2020-05-29 09:09:31 +0200
  • 34a226a582 more mature storing and loading of winning regions Sebastian Junges 2020-05-28 19:50:56 -0700
  • 0eec9e56da better error message when a colon cannot be found in the drn file Sebastian Junges 2020-05-28 19:50:12 -0700
  • 65fab09931 comments in the model are now also allowed Sebastian Junges 2020-05-28 19:49:42 -0700
  • e2b0855208 hashing POMDPs Sebastian Junges 2020-05-28 13:16:24 -0700
  • 009a60df5c fix in hash computation Sebastian Junges 2020-05-27 12:58:59 -0700
  • 48a3b5a927 Optimizing original OVI & Switch for comparing minswap methods Jan Erik Karuc 2020-05-28 20:59:42 +0200
  • bff888a97e Renaming min upper aux method setting Jan Erik Karuc 2020-05-28 20:58:58 +0200
  • 6cfb2be36d Preparation for minimum upper and aux benchmarking Jan Erik Karuc 2020-05-28 18:37:09 +0200
  • 90ade051c2 Added CMAKE option STORM_LOAD_QVBS to automatically download the quantitative verification benchmark set Tim Quatmann 2020-05-28 14:24:09 +0200
  • a07f6068af fixed some strange bug ( why did it even work? ) in counterexample generation for upper-bounded probabilities Sebastian Junges 2020-05-27 12:16:39 -0700
  • 2fa2ea1283 a first version of sparse model hashing Sebastian Junges 2020-05-26 22:29:29 -0700
  • d1b34e3572 changelog updated with storm-pomdp change Sebastian Junges 2020-05-26 15:57:46 -0700
  • 4942e362db transformation preserve canonicity, and this is now set explicitly. (Opt-out rather than opt-in might be more convenient, but also more dangerous...) Sebastian Junges 2020-05-26 15:56:33 -0700
  • 8f9e81f61f less means less or equal in cmake. :/ Sebastian Junges 2020-05-26 15:43:41 -0700
  • ec7198bf07 xerces-c macos fix for version 3.2.3 and newer Sebastian Junges 2020-05-26 11:14:50 -0700
  • 1658b98a26 report xerces-c version Sebastian Junges 2020-05-26 11:14:22 -0700
  • 574cb1918d Merge remote-tracking branch 'refs/remotes/origin/master' Tim Quatmann 2020-05-26 09:39:59 +0200
  • 9981df3f92 Z3LpSolver: Removed exception that was thrown by accident. Tim Quatmann 2020-05-26 09:39:15 +0200
  • 4bcb541866 pmc simplifications are disabled by default, can be switched on via option Sebastian Junges 2020-05-25 21:32:01 -0700
  • 1a6f2e6fba --io:nodrnplaceholders Sebastian Junges 2020-05-25 17:01:53 -0700
  • 1a2a4c1a8e Merge branch 'master' into almostsurepomdp Sebastian Junges 2020-05-25 12:12:49 -0700
  • 3b68059e2b Hiding the StateValuation object of a single state. Tim Quatmann 2020-05-25 17:38:26 +0200
  • adfdf8c572 Refactored state valuations. They now store values for transient jani variables and do not store values for constants (solving Github issue #73) Tim Quatmann 2020-05-25 16:38:58 +0200
  • 3a86cc4391 CompressedState: Added a method to create a human readable string out of the state. Added a method to "uncompress" by extracting all values into corresponding value vectors Tim Quatmann 2020-05-25 16:34:20 +0200
  • 5733072898 TransientVariableInformation: Flagging a few getters const Tim Quatmann 2020-05-25 16:32:34 +0200
  • ab93422fa0 Changed default dd library from `cudd` to `sylvan` (cf. Github issue #71) Tim Quatmann 2020-05-25 09:40:01 +0200
  • cdfbe8d4bb from pomdp to pmc now preserves state valuations Sebastian Junges 2020-05-24 22:21:55 -0700
  • 55b344c560 but state valuations as comments into drn Sebastian Junges 2020-05-24 22:21:21 -0700
  • f23efb9eb2 split pomdp settings into toparametric settings for the UAI18 stuff Sebastian Junges 2020-05-24 22:20:34 -0700
  • 669ffc52d2 reworked the interface to qualitative analysis of POMDPs Sebastian Junges 2020-05-24 11:23:23 -0700
  • a90a82d271 better performance when only looking for a winning policy Sebastian Junges 2020-05-24 11:21:44 -0700
  • 498067816d fix stupid mistake that made subsequent searches mostly unsat by setting scheduler var to wrong value Sebastian Junges 2020-05-24 11:19:27 -0700
  • 53800c2145 major improvements by introducing real-valued ranking and various related fixes Sebastian Junges 2020-05-24 11:18:42 -0700
  • 34fce002cb compute size of winning region Sebastian Junges 2020-05-24 11:15:14 -0700
  • eca148cee0 graph-based analysis improved, and cleaning outputs Sebastian Junges 2020-05-24 11:13:34 -0700
  • a7f05847ac better info message if an engine does not support a model Sebastian Junges 2020-05-24 11:07:51 -0700
  • 2de8c94fd9 flatsets to string Sebastian Junges 2020-05-24 11:07:31 -0700
  • 08cb25c28c to be sure: z3model by const reference Sebastian Junges 2020-05-24 11:07:16 -0700
  • c2f5eb9ce0 do not export reward model if we find a counterexample for a probability property Sebastian Junges 2020-05-24 11:05:00 -0700
  • 5937a764b8 debug output now only appears with log level Sebastian Junges 2020-05-24 11:04:24 -0700
  • 22c644b42c more trace messages in counterexample generation Sebastian Junges 2020-05-24 11:03:30 -0700
  • ee2351ede3 fix logic for including xercesc on macos Sebastian Junges 2020-05-24 11:02:54 -0700
  • 235f335579 typo Sebastian Junges 2020-05-24 11:02:30 -0700
  • fc49b32979 Merge branch 'master' into almostsurepomdp Sebastian Junges 2020-05-24 10:49:00 -0700
  • 890dca30cf Nativepolytope: When intersecting, check easy cases where one of the polytopes are universal first. This also prevents that an internal Eigen assertion is raised in cases where an empty and a non-empty matrix are concatenated (somehow only relevant for gcc 9.3 in debug mode...). Tim Quatmann 2020-05-22 18:58:06 +0200
  • ae2b63ca07 Eigenadapter: changed Returntype of digits10 to match the NumTraits interface Tim Quatmann 2020-05-22 18:54:22 +0200