diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp index 01591b4ee..ca2599389 100644 --- a/src/storm/environment/solver/SolverEnvironment.cpp +++ b/src/storm/environment/solver/SolverEnvironment.cpp @@ -14,8 +14,9 @@ namespace storm { SolverEnvironment::SolverEnvironment() { - forceSoundness = storm::settings::getModule().isSoundSet(); - forceExact = storm::settings::getModule().isExactSet(); + auto generalSettings = storm::settings::getModule(); + forceSoundness = generalSettings.isSoundSet(); + forceExact = generalSettings.isExactSet() || generalSettings.isExactFinitePrecisionSet(); linearEquationSolverType = storm::settings::getModule().getEquationSolver(); linearEquationSolverTypeSetFromDefault = storm::settings::getModule().isEquationSolverSetFromDefaultValue(); } diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index e163e0c02..ae8dc0bfc 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -37,6 +37,8 @@ namespace storm { template ::SupportsExponential, int>::type> std::vector SparseCtmcCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound) { + STORM_LOG_THROW(!env.solver().isForceExact(), storm::exceptions::InvalidOperationException, "Exact computations not possible for bounded until probabilities."); + uint_fast64_t numberOfStates = rateMatrix.getRowCount(); // If the time bounds are [0, inf], we rather call untimed reachability. @@ -257,6 +259,8 @@ namespace storm { template ::SupportsExponential, int>::type> std::vector SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRateVector, RewardModelType const& rewardModel, double timeBound) { + STORM_LOG_THROW(!env.solver().isForceExact(), storm::exceptions::InvalidOperationException, "Exact computations not possible for cumulative expected rewards."); + // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); diff --git a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 0ce9d485f..438181fe9 100644 --- a/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -619,6 +619,8 @@ namespace storm { template ::SupportsExponential, int>::type> std::vector SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal&& goal, storm::storage::SparseMatrix const& transitionMatrix, std::vector const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair const& boundsPair) { + STORM_LOG_THROW(!env.solver().isForceExact(), storm::exceptions::InvalidOperationException, "Exact computations not possible for bounded until probabilities."); + // Choose the applicable method auto method = env.solver().timeBounded().getMaMethod(); if (method == storm::solver::MaBoundedReachabilityMethod::Imca) { diff --git a/src/storm/settings/modules/GeneralSettings.cpp b/src/storm/settings/modules/GeneralSettings.cpp index aa4407d69..b21e35c74 100644 --- a/src/storm/settings/modules/GeneralSettings.cpp +++ b/src/storm/settings/modules/GeneralSettings.cpp @@ -45,7 +45,8 @@ namespace storm { .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file from which to read the configuration.").addValidatorString(ArgumentValidatorFactory::createExistingFileValidator()).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, bisimulationOptionName, false, "Sets whether to perform bisimulation minimization.").setShortName(bisimulationOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, parametricOptionName, false, "Sets whether to enable parametric model checking.").setIsAdvanced().build()); - this->addOption(storm::settings::OptionBuilder(moduleName, exactOptionName, false, "Sets whether to enable exact model checking.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exactOptionName, false, "Sets whether to enable exact model checking.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("valuetype", "The kind of datatype used to represent numeric values").setDefaultValueString("rationals").makeOptional().addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"rationals", "floats"})).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, soundOptionName, false, "Sets whether to force sound model checking.").build()); } @@ -90,7 +91,11 @@ namespace storm { } bool GeneralSettings::isExactSet() const { - return this->getOption(exactOptionName).getHasOptionBeenSet(); + return this->getOption(exactOptionName).getHasOptionBeenSet() && this->getOption(exactOptionName).getArgumentByName("valuetype").getValueAsString() == "rationals"; + } + + bool GeneralSettings::isExactFinitePrecisionSet() const { + return this->getOption(exactOptionName).getHasOptionBeenSet() && this->getOption(exactOptionName).getArgumentByName("valuetype").getValueAsString() == "floats"; } bool GeneralSettings::isSoundSet() const { diff --git a/src/storm/settings/modules/GeneralSettings.h b/src/storm/settings/modules/GeneralSettings.h index 209cedfe0..25d434692 100644 --- a/src/storm/settings/modules/GeneralSettings.h +++ b/src/storm/settings/modules/GeneralSettings.h @@ -93,12 +93,19 @@ namespace storm { bool isParametricSet() const; /*! - * Retrieves whether the option enabling exact model checking is set. + * Retrieves whether the option enabling exact model checking is set and we should use infinite precision rationals. * * @return True iff the option was set. */ bool isExactSet() const; + /*! + * Retrieves whether the option enabling exact model checking is set. + * + * @return True iff the option was set. + */ + bool isExactFinitePrecisionSet() const; + /*! * Retrieves whether the option forcing soundnet is set. * diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp index e944d4bd6..248f2e92d 100644 --- a/src/storm/utility/solver.cpp +++ b/src/storm/utility/solver.cpp @@ -15,6 +15,7 @@ #include "storm/solver/MathsatSmtSolver.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" +#include "storm/settings/modules/GeneralSettings.h" #include "storm/utility/NumberTraits.h" #include "storm/exceptions/InvalidSettingsException.h" @@ -29,7 +30,8 @@ namespace storm { storm::solver::LpSolverType t; if (solvT == storm::solver::LpSolverTypeSelection::FROMSETTINGS) { t = storm::settings::getModule().getLpSolver(); - if (storm::NumberTraits::IsExact && t != storm::solver::LpSolverType::Z3 && storm::settings::getModule().isLpSolverSetFromDefaultValue()) { + bool useExact = storm::NumberTraits::IsExact || storm::settings::getModule().isExactFinitePrecisionSet(); + if (useExact && t != storm::solver::LpSolverType::Z3 && storm::settings::getModule().isLpSolverSetFromDefaultValue()) { t = storm::solver::LpSolverType::Z3; } } else {