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

Commit Graph

  • 7c535cca84 Fixed upcasting of Exceptions in PrismParser. Tim Quatmann 2019-11-05 16:26:35 +0100
  • d1f4e111b1 DetSchedsLpChecker: Do not assume Gurobi as LPSolver. Tim Quatmann 2019-11-05 16:24:44 +0100
  • f8754c0f50 LPSolvers: Allowing premature termination by specifying a mip gap. Fixes for incremental solving with Z3Lpsolver. Tim Quatmann 2019-11-05 16:11:18 +0100
  • 20fe90a527 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-11-05 12:54:45 +0100
  • 32c5a6f9da Added return statement Matthias Volk 2019-11-05 12:49:23 +0100
  • 0bbbb2f6fb glpk: fixes for incremental solving Tim Quatmann 2019-11-05 12:41:19 +0100
  • 4ee31063a4 Removed double whitespaces in outputs Matthias Volk 2019-10-31 21:23:44 +0100
  • 78d99328b6 PrismParser: Making module renaming a LocatedInformation so we can properly store the line number of it. Also silenced a warning related to virtual destructors Tim Quatmann 2019-11-04 19:20:55 +0100
  • 6041e60aca more work on incremental support for glpk Tim Quatmann 2019-11-04 19:16:18 +0100
  • 1323c099dd Test for incremental LP solving. Tim Quatmann 2019-11-04 16:35:00 +0100
  • 078eb86c48 GLPK: added support for incremental solving Tim Quatmann 2019-11-04 15:52:54 +0100
  • 83832c990a Merge branch 'master' into deterministicScheds Tim Quatmann 2019-11-04 15:50:47 +0100
  • fb22c3fe68 Tests: Illegal synchronized writes are now detected already during parsing. The corresponding test case has thus been moved. Tim Quatmann 2019-11-04 15:50:07 +0100
  • afda2eb2a0 .gitignore: added files in l3pp/.git Tim Quatmann 2019-11-04 15:47:44 +0100
  • d67f1b4898 cmake: Fixed compilation of shipped glpk under mac os Tim Quatmann 2019-11-04 15:46:22 +0100
  • 6008f489e2 bumped version of shipped glpk Tim Quatmann 2019-11-04 15:45:51 +0100
  • cad5ed26d9 Merge branch 'master' into deterministicScheds Tim Quatmann 2019-11-04 14:08:48 +0100
  • 6dd6c502e7 Prism: Error upon synchronized write to global variable. Tim Quatmann 2019-11-04 13:06:14 +0100
  • 3db50f570d PrismProgram: Correctly set line numbers for renamed modules. Tim Quatmann 2019-11-04 12:10:13 +0100
  • 632d7ee2fc Merge branch 'prism-parser-improvements' Tim Quatmann 2019-11-04 09:23:18 +0100
  • 4f36e7e431 Check if counterexample exists for k-shortest path Matthias Volk 2019-10-31 20:05:26 +0100
  • 5f3065ec5a PrismParser: Check for expression type. Support for formulas in arbitrary order. TimQu 2019-10-30 19:42:11 +0100
  • 48e98119d5 Merge branch 'master' into prism-parser-improvements TimQu 2019-10-29 23:09:37 +0100
  • 013695a6ce Fixed compile issue: boost::split seems to need an lvalue for the input string. TimQu 2019-10-29 23:09:20 +0100
  • 734cb2d456 PrismParser: Allow Formula assignments in random order. TimQu 2019-10-29 23:07:36 +0100
  • ddff929cbd Scheduler extraction is only supported for quantitative checks Matthias Volk 2019-10-29 21:17:24 +0100
  • d4199b544d Merge branch 'master' into prism-parser-improvements Tim Quatmann 2019-10-29 21:15:13 +0100
  • 12ef18a239 PrismParser: Various improvements of error output. Support for using formulas before they were declared. Tim Quatmann 2019-10-29 21:12:21 +0100
  • bf735f0b00 Fixed doxygen issue with old cmake version (issue #55) Matthias Volk 2019-10-29 20:22:44 +0100
  • b0abbb5088 Support for k-shortest path counterexamples Matthias Volk 2019-10-29 18:42:50 +0100
  • bb71c078fa Export to dot format allows for maximal line width in state labels and valuations Matthias Volk 2019-10-29 16:54:30 +0100
  • 11f89de9e8 Added preprocessing to reduce the POMDP state space before analysis Alexander Bork 2019-10-29 10:30:40 +0100
  • 9a5a6d72c6 Moved some cex code into counterexample module Matthias Volk 2019-10-28 22:39:16 +0100
  • 6a77ce210a Moved setting nofixdl to build settings Matthias Volk 2019-10-28 18:41:12 +0100
  • 2c46b38130 Updated CHANGELOG Matthias Volk 2019-10-28 14:03:30 +0100
  • b8991ca4bf Fixed compile issue due to merge Matthias Volk 2019-10-24 12:37:57 +0200
  • e4e069a98c Slight refactoring of transformations Matthias Volk 2019-10-23 18:50:21 +0200
  • fab86e8823 DFT wellformedness check can be performed stricter as precondition for analysis Matthias Volk 2019-10-23 18:46:00 +0200
  • 1767c40f2d Refactored FDEPConflictFinder Matthias Volk 2019-10-22 18:13:08 +0200
  • fb81571da5 Silenced some more compiler warnings Matthias Volk 2019-10-22 13:18:03 +0200
  • 38c7762254 Added missing include to fix compilation issue on Linux Matthias Volk 2019-10-24 10:47:00 +0200
  • cbecc6d192 Merge branch 'master' into deterministicScheds TimQu 2019-10-23 21:02:31 +0200
  • 9438d56ab3 added cli option for transforming continuous time models to discrete time. TimQu 2019-10-23 21:02:18 +0200
  • b07acd0e3f deterministicScheds: changed setting to --purescheds and added memory pattern 'counter' TimQu 2019-10-23 20:59:45 +0200
  • 48bddc29b7 NondeterministicMemoryProduct: Disabled support for Markov automata since Nondeterminism was added to Markovian states. TimQu 2019-10-23 20:43:54 +0200
  • 22a19d68ba Fixed an issue with multi-objective model checking preprocessor not correctly preserving reachability rewards TimQu 2019-10-23 20:42:39 +0200
  • 4c1958c245 Fixed some compiler warnings Matthias Volk 2019-10-22 11:19:54 +0200
  • 179c46570b Added missing file Jip Spel 2019-10-22 11:14:25 +0200
  • 4b8664c521 Added reward under-approximation Alexander Bork 2019-10-22 10:30:50 +0200
  • e89b743f65 Update changelog Jip Spel 2019-10-21 16:41:03 +0200
  • 5c1d597292 Add line for changelog Jip Spel 2019-10-21 13:48:31 +0200
  • a3d7c4c3f2 Merge branch 'master' into storm-pars-analysis-monotonicity Jip Spel 2019-10-21 12:30:00 +0200
  • bb439d076b DetScheds: Fixed wrong computation of the number of schedulers. TimQu 2019-10-18 15:03:04 +0200
  • f119e3d4c7 Added reward over-approximation Alexander Bork 2019-10-18 11:32:36 +0200
  • 4c8395c3b1 Speedup of probability approximation Alexander Bork 2019-10-18 11:25:03 +0200
  • 0e04cfc883 Merge branch 'master' into storm-pars-analysis-monotonicity Jip Spel 2019-10-17 11:17:16 +0200
  • ed3fa3f82b Fix TODOs Jip Spel 2019-10-17 11:14:31 +0200
  • 382747c70f Merge branch 'master' into deterministicScheds TimQu 2019-10-17 09:59:10 +0200
  • de5b9368c4 Bumping Gurobi version TimQu 2019-10-17 09:58:58 +0200
  • 97a857f8ef Merge branch 'master' into deterministicScheds TimQu 2019-10-17 09:46:18 +0200
  • 0842cb1bd7 DdJaniModelBuilder: adding source locations to guards to correctly track action fragments writing global variables dehnert 2019-10-15 20:51:01 +0200
  • a39f297b8c Fix OrderTest and add assert in Order Jip Spel 2019-10-15 14:47:41 +0200
  • f98250968c Fix checking monotonicity on samples Jip Spel 2019-10-15 14:38:48 +0200
  • 5fbb47d525 Merge branch 'master' into storm-pars-analysis-monotonicity Jip Spel 2019-10-14 13:08:31 +0200
  • c1de1e7747 Merge branch 'master' of https://srv-i2.informatik.rwth-aachen.de/scm/git/storm Matthias Volk 2019-10-14 10:09:52 +0200
  • f6d9a6ac02 Changed datatype used in POMDP analysis from RationalNumber to double for better comparision of approximation speeds with PRISM Alexander Bork 2019-10-11 11:02:35 +0200
  • 5de96cc170 Modified implementation to speed up the subsimplex computation Alexander Bork 2019-10-11 10:59:45 +0200
  • 959a2c2400 Added ability to use an MDP for the underapproximation Alexander Bork 2019-10-11 10:57:30 +0200
  • 4784e1e1c9 Cmake: Temporarily disabled stack checks for current AppleClang. Tim Quatmann 2019-10-10 13:17:54 +0200
  • 555fd90536 Silenced a few warnings. Tim Quatmann 2019-10-10 13:17:15 +0200
  • 60e78dd438 cmake: Do not search for CLN if it is not needed. Tim Quatmann 2019-10-10 10:14:27 +0200
  • d61d1bd3fe Fixed type uintX -> uintX_t Tim Quatmann 2019-10-10 10:13:59 +0200
  • cb00c21db2 Fixed type uintX -> uintX_t Tim Quatmann 2019-10-10 10:13:08 +0200
  • 8d99ae4f4c Added some more trace output for sound value iteration. Tim Quatmann 2019-10-04 12:12:22 +0200
  • 3698b79130 Added missing TransformationSettings for storm-pars Matthias Volk 2019-10-07 17:18:22 +0200
  • 2c80eb518a Fixed output of properties in the prism syntax. TimQu 2019-10-07 16:04:43 +0200
  • 404ec63f6c storm-conv: Added support for transformations on prism programs (such as flattening of modules). TimQu 2019-10-07 14:52:58 +0200
  • 3bd910f42b Added timing and caching of subsimplex computation results Alexander Bork 2019-10-01 17:11:49 +0200
  • d814942997 Working version of under-approximation Alexander Bork 2019-09-25 14:17:39 +0200
  • c0075f1cc4 Removed unused variable Matthias Volk 2019-09-23 12:23:37 +0200
  • c715874339 Merge from dftFDEP Matthias Volk 2019-09-22 20:28:34 +0200
  • d9f4c0037f Merge branch 'master' into dft Matthias Volk 2019-09-20 11:52:54 +0200
  • a0d8c959e4 Changed SEND_ERROR to FATAL_ERROR in CMakeLists for resources Matthias Volk 2019-09-19 14:00:18 +0200
  • 2bc79e6e07 Refactoring to include a list of all generated beliefs Alexander Bork 2019-09-18 17:13:39 +0200
  • 74cfecd011 Working version of over-approximation Alexander Bork 2019-09-11 17:46:13 +0200
  • 7f9ad39d34 First version for the over-approximation of POMDP reachability Alexander Bork 2019-09-11 13:18:59 +0200
  • b15ba29d9e Disable search for boost-cmake Matthias Volk 2019-09-09 14:42:37 +0200
  • 28f8c9d821 Fix as proposed by Lord Hobborg in Issue 53 Sebastian Junges 2019-08-27 17:05:33 +0200
  • 8b77f7f6d6 Added placeholders to DRN format Matthias Volk 2019-08-22 21:19:32 +0200
  • 7a8b32399c Issue warning if max memory of Sylvan is ignored Matthias Volk 2019-08-21 18:35:40 +0200
  • 3fa0b5aabb Fixed issue in Sylvan where large numbers were not recognized as powers of 2. Matthias Volk 2019-08-21 18:32:13 +0200
  • 49ca253ccc Cleanup Alexander Bork 2019-08-16 12:21:24 +0200
  • 584dc6caa7 Fixed error that matrix dimensions were to small if last columns have only 0 entries Alexander Bork 2019-08-09 13:33:13 +0200
  • 3473a930a2 Added hint towards uniquefailedbe flag in error message Alexander Bork 2019-08-09 13:09:48 +0200
  • 2ec921a683 Added support for constantly failed BEs in the model generation Alexander Bork 2019-08-07 18:08:27 +0200
  • a257071346 Added option to transform a DFT to only use one unique constantly failed BE Alexander Bork 2019-08-07 17:10:47 +0200
  • 628331fda3 Fixed error that SMT solver was always used in the FDEP conflict search Alexander Bork 2019-08-07 16:30:21 +0200
  • 4c20495a20 Adjusted tests to removal of mandatory state space reduction Alexander Bork 2019-08-07 16:28:52 +0200
  • 541e582934 Added support for BEs with probabilities in Galileo parser Alexander Bork 2019-08-07 12:57:25 +0200
  • 56a206ea5c Fixed segfaults in reward parsing of DRN Matthias Volk 2019-08-05 22:04:49 +0200