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

Commit Graph

  • 2b57211a98 cli: Making sure that the warning for unsupported model checking queries is only displayed in the main binary. Tim Quatmann 2020-03-24 14:51:48 +0100
  • 558078b6e9 MakePOMDPCanonic: Improved output of error message Tim Quatmann 2020-03-24 14:49:12 +0100
  • 54b912d350 storm-pomdp: better output. Tim Quatmann 2020-03-20 16:14:40 +0100
  • e76efd14d5 POMDP: Filling the statistics struct with information. Also incorporated aborting (SIGTERM, i.e. CTRL+C) Tim Quatmann 2020-03-20 15:20:02 +0100
  • 9d7b447b56 Storm-pomdp: Print if a result is not available. Tim Quatmann 2020-03-20 15:19:03 +0100
  • 7d4e8cf213 POMDP: Print the statistics from the new statistics struct. Tim Quatmann 2020-03-20 14:07:53 +0100
  • 6f3fab8e80 Added a statistics struct to the approximatePOMDP model checker Tim Quatmann 2020-03-20 14:07:23 +0100
  • 0b3945ca12 Pomdp/FormulaInformation: Added template instantiations which apparently are needed with LTO Tim Quatmann 2020-03-20 12:38:26 +0100
  • 311362d995 Removal of some more obsolete code Alexander Bork 2020-03-18 19:16:46 +0100
  • 0507da4ffa Adjusted Refinement Procedure for rewards Alexander Bork 2020-03-18 19:15:27 +0100
  • 62e3a62686 Fix for belief reward computation Alexander Bork 2020-03-18 17:41:12 +0100
  • 44fd26bd13 Implementation of exploration stopping in refinement procedure for newly added states Alexander Bork 2020-03-18 16:30:30 +0100
  • 77b1de510f Renaming of naive underapproximation value map Alexander Bork 2020-03-18 16:29:34 +0100
  • 02a325ba75 Fixed error that refinement did not stop if initial computation already yields same values for over- and under-approximation Alexander Bork 2020-03-18 15:29:37 +0100
  • 054c2a906e Fixed wrong error when over- and under-approximation values are equal Alexander Bork 2020-03-18 14:45:38 +0100
  • d28c982fbd Fix for missing initial belief ID in return struct Alexander Bork 2020-03-18 14:37:15 +0100
  • 00a89d3565 Merge remote-tracking branch 'origin/prism-pomdp' into prism-pomdp Alexander Bork 2020-03-18 14:35:04 +0100
  • 8e30e27eb9 Removal of obsolete code Alexander Bork 2020-03-18 14:34:56 +0100
  • 581e165fb9 Actually use the refinement precision.... Tim Quatmann 2020-03-18 13:59:46 +0100
  • de483cd3c1 Added missing number conversion. Tim Quatmann 2020-03-18 13:59:29 +0100
  • b3493b5888 Grid: Added cli setting to cache subsimplices. Tim Quatmann 2020-03-18 13:49:42 +0100
  • 3aaea1eb0a Added new CLI settings for GridApproximation Tim Quatmann 2020-03-18 13:45:32 +0100
  • a11ec691a9 Introduced options in the ApproximatePOMDPModelChecker. Tim Quatmann 2020-03-18 13:44:32 +0100
  • bf7f84f796 Added --check-fully-observable option to easily check the underlying MDP Tim Quatmann 2020-03-18 09:53:48 +0100
  • 5bdcb66fcb Fixes for reward formulas Tim Quatmann 2020-03-18 09:53:03 +0100
  • 24faf636d7 removed unused variables. Tim Quatmann 2020-03-18 07:01:39 +0100
  • 12f498356a Fixed help message Tim Quatmann 2020-03-18 06:53:15 +0100
  • 6c32b645c4 Fixed compilation with mathsat. Tim Quatmann 2020-03-17 09:31:00 +0100
  • 0147d57884 Merge branch 'master' into prism-pomdp Tim Quatmann 2020-03-18 06:45:06 +0100
  • 58de346bd5 Revert "Fixed compilation with mathsat." Tim Quatmann 2020-03-18 06:44:23 +0100
  • 9e0163ef9a Merge remote-tracking branch 'origin/prism-pomdp' into prism-pomdp Alexander Bork 2020-03-17 23:20:37 +0100
  • c1d0d332c1 Merge branch 'master' into prism-pomdp Sebastian Junges 2020-03-17 14:38:49 -0700
  • 01e3752d09 updated changelog Sebastian Junges 2020-03-17 13:33:15 -0700
  • 22e20e93a9 permissive strategy test should also run without mathsat Sebastian Junges 2020-03-06 13:52:32 -0800
  • 542f94babd report on gurobi library, extended libraries and prefer (empirically) newer versions over older versions Sebastian Junges 2020-03-06 12:16:19 -0800
  • c303ba361f Merge remote-tracking branch 'origin/prism-pomdp' into prism-pomdp Alexander Bork 2020-03-17 19:38:42 +0100
  • c2582058c9 Added first version of refinement with reuse of previous results Alexander Bork 2020-03-17 19:33:51 +0100
  • 27ac99806e Stopwatch: added restart() method Tim Quatmann 2020-03-17 15:12:21 +0100
  • 824c28f332 Instantiation for POMDPs in Propositional model checkers. Tim Quatmann 2020-03-17 15:11:58 +0100
  • 635fbc658a storm-pomdp: towards a more mature cli Tim Quatmann 2020-03-17 15:11:25 +0100
  • 87a4fa553b Merge branch 'master' into prism-pomdp Tim Quatmann 2020-03-17 09:34:23 +0100
  • 8b57b18201 Fixed compilation with mathsat. Tim Quatmann 2020-03-17 09:31:00 +0100
  • cc66c9d758 Storm-conv: Added a comment explaining why this executable needs its own 'setUrgentOptions' Tim Quatmann 2020-03-17 09:30:26 +0100
  • 82ad509405 storm-cli: Splitting the 'export' part from buildPreprocessExportModelWithValueTypeAndDdLib. This allows to build the model without exporting it. Tim Quatmann 2020-03-17 09:23:23 +0100
  • 5c748254a6 Cleaning up the POMDP CLI code a bit. Now supports switching to exact arithmetic with the --exact switch. Tim Quatmann 2020-03-17 09:22:19 +0100
  • 0d58ea5291 Adding missing template instantiation. Tim Quatmann 2020-03-17 09:21:22 +0100
  • 5933467670 Silenced warnings regarding member initialization in unexpected order. Tim Quatmann 2020-03-17 09:21:08 +0100
  • 4576ce7182 Merge remote-tracking branch 'origin/master' into prism-pomdp Tim Quatmann 2020-03-17 07:06:32 +0100
  • afbfd42b3a Storm version 1.5.1 Matthias Volk 2020-03-16 15:12:33 +0100
  • d605a3bf0a Use general zenodo id for complete project instead of specific release Matthias Volk 2020-03-16 15:01:07 +0100
  • 57fe5106a5 Removed printing complete matrix Matthias Volk 2020-03-16 15:00:19 +0100
  • 81356d1dc8 Jani JSONExporter: Increased precision for output. Tim Quatmann 2020-03-13 20:05:54 +0100
  • 9cc00a03a2 modernjson: Fixed compilation with GCC. Tim Quatmann 2020-03-13 18:47:06 +0100
  • 1dccab9673 JaniParser: Added missing template instantiation and other fixes. Tim Quatmann 2020-03-13 18:46:52 +0100
  • 0433469b9e Added missing template instantiation. Tim Quatmann 2020-03-13 18:20:23 +0100
  • 7b32aa968e Fixed actually using the JaniParser with rational numbers. Tim Quatmann 2020-03-13 18:03:44 +0100
  • 4fb92b200a Fix in parsing Numbers from JSON Tim Quatmann 2020-03-13 17:49:26 +0100
  • 7cbddfeef6 Updated changelog Tim Quatmann 2020-03-13 16:35:04 +0100
  • 6af6bc5472 Replaced remaining uses of modernjson::json with the new storm::json<..> Tim Quatmann 2020-03-13 16:32:09 +0100
  • 328b9c6986 Gave the JaniParser a template argument, so that we can use it to parse with doubles or with RationalNumbers. Tim Quatmann 2020-03-13 16:31:12 +0100
  • 632c9c2e1e Modified the modernjson library so that it can parse numbers as rationals. Tim Quatmann 2020-03-13 16:29:58 +0100
  • bb25d6cb10 Storm version 1.5.0 Matthias Volk 2020-03-12 16:17:49 +0100
  • 1593f39035 Updated CHANGELOG Matthias Volk 2020-03-12 16:15:24 +0100
  • c70b6baf81 Abort unif+ also in inner iterations. Store the best known solution after each completed step. Tim Quatmann 2020-03-12 09:49:15 +0100
  • 80f28e196d Print current iteration count when aborting a solver. Tim Quatmann 2020-03-12 09:47:55 +0100
  • 9fddf3858b Abort topological solvers if requested. Tim Quatmann 2020-03-12 09:47:36 +0100
  • f584bfe0d4 Updated changelog. Tim Quatmann 2020-03-11 19:10:08 +0100
  • 463766dbe0 Improved numerical stability of computation of transient probabilities in CTMCs. Tim Quatmann 2020-03-11 18:11:19 +0100
  • b5a64ba7e3 CTMC Model checker: Consider relative precision for time-bounded queries in --sound mode Tim Quatmann 2020-03-11 17:33:42 +0100
  • 71f22fef2f Added a CLI switch to perform exact model checking over finite precision floats Tim Quatmann 2020-03-11 13:40:40 +0100
  • d0b54fe6b5 Set number of printed digits in output Matthias Volk 2020-03-11 12:04:43 +0100
  • de27fa82fe Changed result output iterator for DFTs Matthias Volk 2020-03-11 12:04:00 +0100
  • 70e2263783 MarkovAutomatonCslModelCheckerTest: Prevent this test from failing in cases where z3 is installed without optimization support. Tim Quatmann 2020-03-11 11:56:59 +0100
  • 137f41abac FormulaInformation: Fixed detection of property type. Tim Quatmann 2020-03-11 11:51:32 +0100
  • 1fd052aee4 InformationCollector: Use infinite precision to determine the state domain size. Tim Quatmann 2020-03-11 11:36:36 +0100
  • 2b89da2f4b Updated decision tree used in portfolio engine. Tim Quatmann 2020-03-11 10:14:30 +0100
  • 5dcebdef93 Fixed invocation of storm without a model. Tim Quatmann 2020-03-11 10:14:06 +0100
  • 49e4bba7c1 Merge branch 'master' into qcomp2020 Tim Quatmann 2020-03-10 13:27:48 +0100
  • f4820628a5 Incorporated more features for the portfolio engine. Tim Quatmann 2020-03-10 13:09:03 +0100
  • 3b53e1e583 Implemented retrieval of jani model information with a traverser. Also determine the size of the state domain. Tim Quatmann 2020-03-10 12:07:22 +0100
  • d3ece2a2e5 Better simplification of prism commands. Tim Quatmann 2020-03-10 12:06:03 +0100
  • 0e91887ebb Queried the termination flag in a few more places. Tim Quatmann 2020-03-09 17:09:31 +0100
  • 4585f8f555 One more fix for AcyclicSolverHelper. Tim Quatmann 2020-03-09 16:20:51 +0100
  • 7766a96783 Fixes for Acylic equation solvers. Tim Quatmann 2020-03-09 15:50:07 +0100
  • bbc6f8b786 Fixed invalid memory access when applying BitVector::resize on BitVectors of length 0. Tim Quatmann 2020-03-09 15:46:31 +0100
  • 99f2344da9 Use acyclic solver in various Markov automata methods. Tim Quatmann 2020-03-09 14:00:33 +0100
  • c83721066c Use acyclic solver in reward bounded properties. Tim Quatmann 2020-03-09 14:00:09 +0100
  • 53db0b1f22 Added AcyclicMinMaxLinearEquationSolver and AcyclicLinearEquationSolver which are optimized for many calls on an acyclic model. Tim Quatmann 2020-03-09 13:10:21 +0100
  • 250a4b9b9a MdpModelChecheckerTest: added test cases for the different multiplication styles and multiplier types. Tim Quatmann 2020-03-09 13:01:47 +0100
  • 31cbe14d3c Multiplier: Added a flag to specify whether gaussSeidel style multiplications should be performed forward or backwards. Tim Quatmann 2020-03-09 13:01:10 +0100
  • d88e7e9951 Explicit header files to include all defined environments Matthias Volk 2020-03-09 13:53:15 +0100
  • 63e0d772a4 do not use the 'goal' label for internal purposes, but rather __goal__. TODO: Consider if we can do without a fresh label Sebastian Junges 2020-03-08 20:02:49 -0700
  • 5c7a6b791a fixed (merge?) mistake that yielded errors for expected rewards Sebastian Junges 2020-03-08 17:50:57 -0700
  • 14f07a2d1a Unif+: Update kappa only based on the results at the initial state Tim Quatmann 2020-03-06 16:28:59 +0100
  • dd958bcedd Changed default of the unifpluskappa Tim Quatmann 2020-03-06 16:28:11 +0100
  • 4d55dfbf07 Fixed doing non-exact model checking in portfolio engine, even if the --exact switch was set. Tim Quatmann 2020-03-06 16:27:59 +0100
  • c399c31c52 Added missing include Tim Quatmann 2020-03-06 22:12:48 +0100
  • c17a50904d Updated CHANGELOG Matthias Volk 2020-03-06 17:15:25 +0100
  • 6f62e8d402 Support abort in model building Matthias Volk 2020-03-06 17:15:07 +0100
  • 679327ee9d Merge branch 'qcomp2020' into signals Matthias Volk 2020-03-06 16:14:59 +0100