Added a CLI switch to perform exact model checking over finite precision floats

src/storm/environment/solver/SolverEnvironment.cpp

@@ -14,8 +14,9 @@
 namespace storm {
     
     SolverEnvironment::SolverEnvironment() {
-        forceSoundness = storm::settings::getModule<storm::settings::modules::GeneralSettings>().isSoundSet();
-        forceExact = storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet();
+        auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
+        forceSoundness = generalSettings.isSoundSet();
+        forceExact = generalSettings.isExactSet() || generalSettings.isExactFinitePrecisionSet();
         linearEquationSolverType = storm::settings::getModule<storm::settings::modules::CoreSettings>().getEquationSolver();
         linearEquationSolverTypeSetFromDefault = storm::settings::getModule<storm::settings::modules::CoreSettings>().isEquationSolverSetFromDefaultValue();
     }

src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp

@@ -37,6 +37,8 @@ namespace storm {
             template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
             std::vector<ValueType> SparseCtmcCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> 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 <typename ValueType, typename RewardModelType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
             std::vector<ValueType> SparseCtmcCslHelper::computeCumulativeRewards(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> 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.");
                 

src/storm/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp

@@ -619,6 +619,8 @@ namespace storm {
             
             template <typename ValueType, typename std::enable_if<storm::NumberTraits<ValueType>::SupportsExponential, int>::type>
             std::vector<ValueType> SparseMarkovAutomatonCslHelper::computeBoundedUntilProbabilities(Environment const& env, storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRateVector, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::pair<double, double> 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) {

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 {

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.
                  *

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<storm::settings::modules::CoreSettings>().getLpSolver();
-                    if (storm::NumberTraits<ValueType>::IsExact && t != storm::solver::LpSolverType::Z3 && storm::settings::getModule<storm::settings::modules::CoreSettings>().isLpSolverSetFromDefaultValue()) {
+                    bool useExact = storm::NumberTraits<ValueType>::IsExact || storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactFinitePrecisionSet();
+                    if (useExact && t != storm::solver::LpSolverType::Z3 && storm::settings::getModule<storm::settings::modules::CoreSettings>().isLpSolverSetFromDefaultValue()) {
                         t = storm::solver::LpSolverType::Z3;
                     }
                 } else {