7035 Commits (c91033ebb178abd08b83a7e50ca58737bced10a0)
 

Author SHA1 Message Date
Tim Quatmann 01800f1590 Added string utility functions to find similar strings. 6 years ago
Tim Quatmann 80bfa6b56e Allow to quickly check a benchmark from the Quantitative Verification Benchmark Set. 6 years ago
Tim Quatmann 27c2a8ba95 Added string utility functions to find similar strings. 6 years ago
Tim Quatmann 5de1697edc Reading QVBS options from settings. 6 years ago
Tim Quatmann 6b32bd1dc3 cmake: Added option to specify a path to the qvbs benchmarks. 6 years ago
Tim Quatmann 6faf074fc5 Made sure that model::getAllParameters also returns the parameters occurring at rates. 6 years ago
Matthias Volk 12709f1625 Added parentheses to silence clang warning 6 years ago
Tim Quatmann 98ce81e86a Jani: Fixed an issue where initial expressions for unbounded variables have not been substituted correctly. 6 years ago
Tim Quatmann bc32853c28 Jani: Fixed an issue where initial expressions for unbounded variables have not been substituted correctly. 6 years ago
Tim Quatmann 40f4141b56 Jani: Allowing bounded types for constants as pointed out in GitHub issue #37 6 years ago
Tim Quatmann c6fd015e6c Picking a default SmtSolver, even if no CoreSettings are available. 6 years ago
Tim Quatmann ee6942c563 Merge branch 'quantiles_refactor' 6 years ago
Tim Quatmann 84476b7000 Fixed getSmtSolver which previously did not respect the SmtSolver selection from the settings. 6 years ago
Tim Quatmann d24f61ded6 Added tests for quantiles. 6 years ago
Tim Quatmann 1ae0200b51 Quantiles: fixed some bugs related to one or three dimensional quantile queries. 6 years ago
Tim Quatmann c40ecae2e6 Implemented quantiles for DTMCs. 6 years ago
Tim Quatmann aa3a1f5ff7 Quantiles: Improved performance by excluding already analyzed epochs from the created epochSequences 6 years ago
Tim Quatmann 971f4c8508 Quantiles: Fixed analysing epochs unnecessarily, fixed having multiple quantile formulas over the same variables. 6 years ago
Tim Quatmann c21ea2ce1f Quantiles: Bug fixes. 6 years ago
Tim Quatmann 8a72aee764 QuantileFormulas: ignore optimization direction (min/max) for quantile variables. 6 years ago
Tim Quatmann 38121c28cb quantiles: permute point entries if the order of quantile variable definitions is not the same as the order of occurrence on a cost bound. 6 years ago
TimQu e3fbb77362 JaniParser::parseFormula: Boolean connections of AtomicExpressionFormulas are now parsed as a single AtomicExpressionFormula (i.e. 'a>1 & b>2' becomes a single atomic proposition instead of having two propositions 'a>1' and 'b>2'). This reduces the number of labels that need to be considered and improves partial state space exploration for formulas such as 'P=? [F a>1 & b>2]'. 6 years ago
Tim Quatmann 746c68d039 Merge branch 'master' into quantiles_refactor 6 years ago
Tim Quatmann 004466b83f Fixed BitVector::full() for BitVectors with size 0 6 years ago
Tim Quatmann c33ac18a5a Quantiles: Fixed a precision related issue in new implementation. 6 years ago
Tim Quatmann 8ae9a6f5d6 quantiles: Further improved the implementation as in the paper 6 years ago
Tim Quatmann cde1c646d9 Started to implement the algorithm more close to the one mentioned in the paper (in particular to make things more clean and to allow more than 2 dimensions. 6 years ago
Matthias Volk aa107dc88d Merge branch 'master' into dft 6 years ago
Matthias Volk b4748064ac Warning about default dormancy factor of 1 as pointed out by Enno Ruijters 6 years ago
Matthias Volk 15bcb8afb6 Output line number for GalileoParser errors 6 years ago
Tim Quatmann a4e03ff941 Updated Changelog. We now have quantile queries. 6 years ago
Tim Quatmann 5b8ad6fbbd Merge branch 'quantiles' 6 years ago
Tim Quatmann f1abd89de1 Merge remote-tracking branch 'origin/master' into quantiles 6 years ago
TimQu 0bf9f27e31 Fixed typo and renamed a variable. 6 years ago
TimQu e89cbf2886 fixed cyclic check. 6 years ago
TimQu 88ee0bbf67 RewardUnfolding: If statistics are enabled, Log when an acyclic epoch model is found. 6 years ago
TimQu 04082fb2d6 Added a method to check whether a graph contains a cycle. 6 years ago
Matthias Volk 3c5f25fe4a Get all model parameters 6 years ago
Matthias Volk d7a22e78d0 Allow unnecessary parameters in region string 6 years ago
Sebastian Junges 6c543df537 Fix in bisimulation of MDPs, which failed if all non-absorbing states in the quotient are initial 6 years ago
Sebastian Junges 6c2262b7e8 more informative error messages during model building (for better debugging) 6 years ago
Sebastian Junges b59cbfa1de graph conditions for rewards described by rational functions with nonconstant denominators 6 years ago
Matthias Volk 8b87d79c3e Removed copy-pasted references to DFTs 6 years ago
Matthias Volk 87cd72f237 Output exception type in exception message 6 years ago
Matthias Volk 87d078f897 Output error by STORM_LOG_ERROR 6 years ago
Matthias Volk 47b2cb737d Merge branch 'master' into dft 6 years ago
Matthias Volk 04164d8b02 Fixed crucial typo in symmetry ordering 6 years ago
TimQu 5ad100e652 quantiles: Added some statistics. 6 years ago
TimQu fb7078770d rewardbounded: Various fixes. 6 years ago
TimQu dd93b1dae9 rewardbounded: Improved code structure. 6 years ago