Commit Graph

  • 743b01f00a add badges for zenodo and version Sebastian Junges 2019-12-19 11:07:31 +0100
  • 8d3254b8d0 Use boost::bimap for the belief space <-> state space mapping Alexander Bork 2019-12-17 14:36:34 +0100
  • c64591ffb3 Merge remote-tracking branch 'origin/prism-pomdp' into prism-pomdp Alexander Bork 2019-12-17 10:53:44 +0100
  • 0facf4a572 Preparation work for the implementation of the refinement procedure Alexander Bork 2019-12-17 10:52:56 +0100
  • bb0b14bfa2 oops. missed a brace Sebastian Junges 2019-12-15 18:28:57 +0100
  • 5f747214b1 Merge branch 'prism-pomdp' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm into prism-pomdp Sebastian Junges 2019-12-15 18:09:56 +0100
  • fe2dcfc975 better dot output for pomdp models Sebastian Junges 2019-12-15 18:04:31 +0100
  • 5bbf54cb78 make everything compile again, add/fix method for memless strategy search (CCD16) and towards iterative search Sebastian Junges 2019-12-15 18:03:58 +0100
  • add8193dd4 Removed duplicate makeOptional() Matthias Volk 2019-12-13 16:16:42 +0100
  • ba6358c3fa Set optional arguments for settings Matthias Volk 2019-12-13 16:09:00 +0100
  • 3f717202cd Fixed handling of optional arguments. Matthias Volk 2019-12-13 16:01:00 +0100
  • 32371c44d4 Updated documentation for new release Matthias Volk 2019-12-13 15:35:21 +0100
  • cf8337583b Storm version 1.4.1 Matthias Volk 2019-12-13 14:29:18 +0100
  • 94b93f013c Added option to stop approximation space exploration early if difference between over- and under-approximation is under a given threshold Alexander Bork 2019-12-13 14:24:36 +0100
  • b1bb7872fd Parsing integers as long long ints (instead of ints) to fix github issue #60. TimQu 2019-12-10 14:51:34 +0100
  • f416cc8291 Added flag to toggle caching of subsimplex and lambda values Alexander Bork 2019-12-10 12:23:26 +0100
  • aca676a0a5 Added model generation and checking for initial approximation bounds Alexander Bork 2019-12-09 09:48:09 +0100
  • be3cffe8ba Write output monotonicity checking to user-specified file Jip Spel 2019-12-06 11:27:28 +0100
  • 419013025b Fixed reduction to state-based rewards for CTMCs in Dd engine. When action rewards are reduced to state rewards, they have to be multiplied with the exit rate. TimQu 2019-12-05 12:28:58 +0100
  • bc85e6742e Fixed parsing of RationalFunctions if no parameters are given Matthias Volk 2019-12-03 18:25:02 +0100
  • 6fb9f7e743 Warn if property could not be checked on DFT Matthias Volk 2019-12-03 17:28:33 +0100
  • 1de76b36c8 Updated steps for new release Matthias Volk 2019-12-03 17:27:59 +0100
  • 267291ea90 Updated Changelog Tim Quatmann 2019-12-03 18:05:58 +0100
  • 3912d59a3b Added kanban model for LRA test Tim Quatmann 2019-12-03 18:05:40 +0100
  • 62dc50035c Removed a test case that is not relevant anymore. Tim Quatmann 2019-12-03 18:05:20 +0100
  • ea04f6dcd2 Fixes for LRA computation. Tim Quatmann 2019-12-03 14:29:29 +0100
  • 4418422ea8 merge -- but code is not working atm Sebastian Junges 2019-12-03 17:30:49 +0100
  • 86506e2b25 Added LRA distribution equation system for computing the LRA of a BSCC. Fixes in the gain/bias characterization. Tim Quatmann 2019-12-03 13:55:58 +0100
  • f9f845bb79 Separated LRA tests from CTMC tests and added a testcase for LRA Rewards Tim Quatmann 2019-12-03 13:46:51 +0100
  • 6110a677f5 More environments checked in Lra Dtmc test. Tim Quatmann 2019-12-03 13:46:24 +0100
  • 068c1b3ea6 Removed obsolete settings Tim Quatmann 2019-12-03 10:58:25 +0100
  • 324eb23cdd Using new LRA environment Tim Quatmann 2019-12-03 10:56:57 +0100
  • 7a026922b7 Added LRA Environment Tim Quatmann 2019-12-03 10:55:46 +0100
  • 7017fc1ab0 Added LRA settings. Tim Quatmann 2019-12-03 10:55:14 +0100
  • bcd193dd57 Implemented Value iteration based LRA computation for CTMCs. Tim Quatmann 2019-12-02 13:53:23 +0100
  • aa38fec527 Merge branch 'master' into prism-pomdp Sebastian Junges 2019-11-29 18:18:18 +0100
  • d919a2d6ee Merge branch 'prism-pomdp' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm into prism-pomdp Sebastian Junges 2019-11-29 18:17:28 +0100
  • 77c63f4c12 SAT based zerostate analysis: work in progress Sebastian Junges 2019-11-29 18:17:24 +0100
  • 1ccdabd7b2 DdJaniModelBuilder: Fixed an "Unexpected edge type" exception occurring if there are unsatisfiable Markovian guards. TimQu 2019-11-29 17:58:40 +0100
  • 8992b70da3 Made Value Iteration its own function to reduce duplicate code Alexander Bork 2019-11-29 15:08:16 +0100
  • fe81e0d7cf Smaller touch-ups (Removal of unused code, pass-by-reference) Alexander Bork 2019-11-29 13:59:43 +0100
  • 877c15ed43 Removed obsolete function to create transition matrices from a data structure not used anymore Alexander Bork 2019-11-29 13:41:36 +0100
  • b7b213571d Refactoring of underapproximation procedures to reduce code duplication Alexander Bork 2019-11-29 13:27:49 +0100
  • 8f81958268 Refactoring of reachability reward and probability methods to reduce code duplication Alexander Bork 2019-11-26 12:33:20 +0100
  • 4664b4244b Refactoring of on-the-fly computation to reduce code duplication Alexander Bork 2019-11-26 11:01:22 +0100
  • c6902e0ca7 Added reward MDP generation for the overapproximation Alexander Bork 2019-11-25 11:08:07 +0100
  • c663edbd85 Added generation of an MDP for the over-approximation in the on-the-fly state exploration Alexander Bork 2019-11-22 16:29:29 +0100
  • bbd3ec7287 Fix of wrong MDP underapproximation Alexander Bork 2019-11-22 16:21:54 +0100
  • e28203fbb8 Added option to merge labels of eliminated states into existing states Alexander Bork 2019-11-15 10:11:35 +0100
  • 2c80acd121 Prepared Changelog for next entries Matthias Volk 2019-11-14 15:20:41 +0100
  • 97be2f9df0 Storm version 1.4.0 Matthias Volk 2019-11-14 15:02:11 +0100
  • bf0ec34024 Skipping more tests in case of oldish z3 version. Tim Quatmann 2019-11-13 20:25:38 +0100
  • d245f65649 Fixed Testcase for replacing of unassigned variables. Tim Quatmann 2019-11-13 20:23:48 +0100
  • 2b55302a4b Testcase for replacing of unassigned variables. Tim Quatmann 2019-11-13 19:04:26 +0100
  • f4135fbd14 ToJaniConverter: Fixed detection of accessing modules of variables: The likelihood expression was not taken into account before. Tim Quatmann 2019-11-13 18:42:46 +0100
  • 9128318ced storm-conv: Added an option to replace variables without assignment by constants. Tim Quatmann 2019-11-13 17:54:51 +0100
  • 1536edb99f Jani: Check if a variable is never used as the lvalue of an assignment. If yes, (and if the variable has a known initial value), we replace the variable by a constant. Tim Quatmann 2019-11-13 17:53:44 +0100
  • 729dda163d Fixed export in DRN format: parameters could occur multiple times Matthias Volk 2019-11-13 17:04:12 +0100
  • f86864f9bc Skipping tests that trigger bugs in some older versions of z3. Tim Quatmann 2019-11-12 19:28:12 +0100
  • 7028198989 Revised documentation Matthias Volk 2019-11-12 14:18:11 +0100
  • 61c1ec8537 Check for Zeno cycles in MA Matthias Volk 2019-11-12 14:12:29 +0100
  • ab94b630c1 Removed .gitignore Matthias Volk 2019-11-12 13:22:28 +0100
  • 13b0f6e421 Updated Changelog Matthias Volk 2019-11-12 11:39:09 +0100
  • 32e3661bd2 Fix adding same state twice to Order Jip Spel 2019-11-12 10:59:32 +0100
  • c955d8203a Tests: Silencing a warning. TimQu 2019-11-11 19:34:16 +0100
  • 7339f487a9 Fixed BUILD_BYPRODUCTS for Ninja Matthias Volk 2019-11-11 17:21:05 +0100
  • 8bb9ad3b64 tests: Print STORM_LOG_ERRORs Tim Quatmann 2019-11-11 15:43:38 +0100
  • 99991d344e utility/initialize: Added a function to read the current loglevel. Tim Quatmann 2019-11-11 15:42:15 +0100
  • 1a21674ab0 Tests: Silencing some "EXPECT_THROW" test cases since error messages are expected here. Tim Quatmann 2019-11-11 14:00:02 +0100
  • 9e1c7820b3 Fixed typo. Tim Quatmann 2019-11-11 13:28:43 +0100
  • 9328332789 Moving a newer test case to the correct location. Tim Quatmann 2019-11-11 13:28:29 +0100
  • 7000dc6ff0 Removing old prctl locations Tim Quatmann 2019-11-11 13:27:58 +0100
  • b55f828251 Merge branch 'branch' Tim Quatmann 2019-11-11 13:19:18 +0100
  • b24d224691 tests: Enabled logging output while running test-cases. Tim Quatmann 2019-11-11 13:14:18 +0100
  • 553100b555 Replaced TYPED_TEST_CASE with TYPED_TEST_SUITE since the former is deprecated. Tim Quatmann 2019-11-11 11:09:51 +0100
  • b320eb38d2 z3LpSolverTest: Skipping a test if not supported by installed z3 version. Tim Quatmann 2019-11-11 10:58:46 +0100
  • a4954332a3 incremented gtest version. Tim Quatmann 2019-11-11 10:55:43 +0100
  • 98e3ac5ad7 integrated new gtest version in cmake. Tim Quatmann 2019-11-11 10:39:44 +0100
  • a145818e4d updated gtest version Tim Quatmann 2019-11-11 10:38:44 +0100
  • b9c0af6628 Added on-the-fly belief grid generation for rewards Alexander Bork 2019-11-08 11:43:09 +0100
  • 68539592f2 Modelchecker-Prctl removed from original split Darknety 2019-11-08 11:31:26 +0100
  • 6e1238b10b Modelchecker-Prctl tests split Darknety 2019-11-08 10:57:55 +0100
  • 21e417bdac Added on-the-fly belief grid generation to avoid computations for unreachable beliefs Alexander Bork 2019-11-08 10:55:13 +0100
  • bc52aa86ca Added procedure to repeat probability computation with higher resolution Alexander Bork 2019-11-08 10:48:55 +0100
  • a65c445243 Avoid multiple computation of size in subsimplex computation Alexander Bork 2019-11-08 10:20:49 +0100
  • 7afc47f354 Fixed wrong size of stateLabeling if no probability 0 states were found Alexander Bork 2019-11-08 10:14:43 +0100
  • 9fabb01478 GlpkLpSolver: No exception if an integer solution exceeds the integer tolerance. (Just print an error). Tim Quatmann 2019-11-07 15:45:10 +0100
  • 654f705d2e DetSchedsLpChecker: Glpk does not allow point intervals as bounds for variables. Tim Quatmann 2019-11-07 15:37:50 +0100
  • aa620f73f6 Travis: use newer Linux versions Matthias Volk 2019-11-07 13:18:38 +0100
  • a0e68a9d22 MultiObjectiveSchedRestModelCheckerTest: The test should not be executed if the installed z3 version is too old for optimization. Tim Quatmann 2019-11-07 12:56:55 +0100
  • 1807775c6c Removed test of SparseModelNondeterministicTransitionBasedMemoryProduct which is no longer in use. TimQu 2019-11-06 16:36:38 +0100
  • b8b6dab6db Modelchecker test split Jan Karuc 2019-11-06 16:07:28 +0100
  • bba5c65afb The MultiObjectiveSchedRestModelCheckerTest now also works without Gurobi. TimQu 2019-11-06 12:52:57 +0100
  • d8338676ff Delete unused files. TimQu 2019-11-06 12:52:27 +0100
  • 3881ae73f2 glpk: Fixed pop()ing for the case where no constraints have to be deleted. Tim Quatmann 2019-11-06 15:24:19 +0100
  • c977a1f5fa Fix for detecting infeasible models in glpk. Tim Quatmann 2019-11-05 17:48:49 +0100
  • 293fec426e Flagged several options as advanced. Tim Quatmann 2019-11-05 16:58:26 +0100
  • 175a1d8686 Updated changelog. Tim Quatmann 2019-11-05 16:58:08 +0100
  • f01577eacd Merge branch 'deterministicScheds' Tim Quatmann 2019-11-05 16:32:28 +0100
  • b7cd16df68 Updated Changelog Tim Quatmann 2019-11-05 16:29:47 +0100