diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 098566707..2fbc60b0b 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -17,6 +17,7 @@ #include "src/utility/graph.h" #include "src/utility/counterexamples.h" #include "src/utility/solver.h" +#include "src/solver/LpSolver.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index de0d08abd..e7df544b5 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/src/modelchecker/AbstractModelChecker.cpp @@ -160,7 +160,7 @@ namespace storm { // If the probability bound is 0 or 1, is suffices to do qualitative model checking. bool qualitative = false; if (stateFormula.hasBound()) { - if (stateFormula.getBound() == storm::utility::zero() || stateFormula.getBound() == storm::utility::one()) { + if (storm::utility::isZero(stateFormula.getBound()) || storm::utility::isOne(stateFormula.getBound())) { qualitative = true; } } @@ -192,7 +192,7 @@ namespace storm { // If the reward bound is 0, is suffices to do qualitative model checking. bool qualitative = false; if (stateFormula.hasBound()) { - if (stateFormula.getBound() == storm::utility::zero()) { + if (storm::utility::isZero(stateFormula.getBound())) { qualitative = true; } } @@ -224,7 +224,7 @@ namespace storm { // If the reward bound is 0, is suffices to do qualitative model checking. bool qualitative = false; if (stateFormula.hasBound()) { - if (stateFormula.getBound() == storm::utility::zero()) { + if (storm::utility::isZero(stateFormula.getBound())) { qualitative = true; } } diff --git a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp index ea84781a4..273788e20 100644 --- a/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/HybridCtmcCslHelper.cpp @@ -45,7 +45,7 @@ namespace storm { std::unique_ptr HybridCtmcCslHelper::computeBoundedUntilProbabilities(storm::models::symbolic::Model const& model, storm::dd::Add const& rateMatrix, storm::dd::Add const& exitRateVector, storm::dd::Bdd const& phiStates, storm::dd::Bdd const& psiStates, bool qualitative, double lowerBound, double upperBound, storm::utility::solver::LinearEquationSolverFactory const& linearEquationSolverFactory) { // If the time bounds are [0, inf], we rather call untimed reachability. - if (lowerBound == storm::utility::zero() && upperBound == storm::utility::infinity()) { + if (storm::utility::isZero(lowerBound) && upperBound == storm::utility::infinity()) { return computeUntilProbabilities(model, rateMatrix, exitRateVector, phiStates, psiStates, qualitative, linearEquationSolverFactory); } @@ -60,11 +60,11 @@ namespace storm { STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNonZeroCount() << " 'maybe' states."); if (!statesWithProbabilityGreater0NonPsi.isZero()) { - if (upperBound == storm::utility::zero()) { + if (storm::utility::isZero(upperBound)) { // In this case, the interval is of the form [0, 0]. return std::unique_ptr(new SymbolicQuantitativeCheckResult(model.getReachableStates(), psiStates.toAdd())); } else { - if (lowerBound == storm::utility::zero()) { + if (storm::utility::isZero(lowerBound)) { // In this case, the interval is of the form [0, t]. // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index e4bf7883f..9fa3bac81 100644 --- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -25,7 +25,7 @@ namespace storm { uint_fast64_t numberOfStates = rateMatrix.getRowCount(); // If the time bounds are [0, inf], we rather call untimed reachability. - if (lowerBound == storm::utility::zero() && upperBound == storm::utility::infinity()) { + if (storm::utility::isZero(lowerBound) && upperBound == storm::utility::infinity()) { return computeUntilProbabilities(rateMatrix, backwardTransitions, exitRates, phiStates, psiStates, qualitative, linearEquationSolverFactory); } @@ -43,12 +43,12 @@ namespace storm { STORM_LOG_INFO("Found " << statesWithProbabilityGreater0NonPsi.getNumberOfSetBits() << " 'maybe' states."); if (!statesWithProbabilityGreater0NonPsi.empty()) { - if (upperBound == storm::utility::zero()) { + if (storm::utility::isZero(upperBound)) { // In this case, the interval is of the form [0, 0]. result = std::vector(numberOfStates, storm::utility::zero()); storm::utility::vector::setVectorValues(result, psiStates, storm::utility::one()); } else { - if (lowerBound == storm::utility::zero()) { + if (storm::utility::isZero(lowerBound)) { // In this case, the interval is of the form [0, t]. // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier. @@ -228,7 +228,7 @@ namespace storm { ValueType lambda = timeBound * uniformizationRate; // If no time can pass, the current values are the result. - if (lambda == storm::utility::zero()) { + if (storm::utility::isZero(lambda)) { return values; } diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp index 54ccc5be0..3dc58ba6a 100644 --- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp +++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp @@ -14,6 +14,7 @@ #include "src/utility/numerical.h" +#include "src/solver/MinMaxLinearEquationSolver.h" #include "src/solver/LpSolver.h" #include "src/exceptions/InvalidStateException.h" diff --git a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp index ce7c08266..8aa20c54f 100644 --- a/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp @@ -9,8 +9,7 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" -#include "src/utility/macros.h" -#include "src/utility/graph.h" +#include "src/solver/MinMaxLinearEquationSolver.h" #include "src/settings/modules/GeneralSettings.h" @@ -54,7 +53,7 @@ namespace storm { template std::unique_ptr HybridMdpPrctlModelChecker::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(pathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); std::unique_ptr leftResultPointer = this->check(pathFormula.getLeftSubformula()); std::unique_ptr rightResultPointer = this->check(pathFormula.getRightSubformula()); @@ -65,14 +64,14 @@ namespace storm { template std::unique_ptr HybridMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); return storm::modelchecker::helper::HybridMdpPrctlHelper::computeCumulativeRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } template std::unique_ptr HybridMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, boost::optional const& rewardModelName, bool qualitative, boost::optional const& optimalityType) { - STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); + STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model."); STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound."); return storm::modelchecker::helper::HybridMdpPrctlHelper::computeInstantaneousRewards(optimalityType.get() == storm::logic::OptimalityType::Minimize, this->getModel(), this->getModel().getTransitionMatrix(), rewardModelName ? this->getModel().getRewardModel(rewardModelName.get()) : this->getModel().getRewardModel(""), rewardPathFormula.getDiscreteTimeBound(), *this->linearEquationSolverFactory); } diff --git a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp index 6b564cbaf..0dcb52435 100644 --- a/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.cpp @@ -10,6 +10,7 @@ #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h" #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" +#include "src/solver/SymbolicLinearEquationSolver.h" #include "src/settings/modules/GeneralSettings.h" diff --git a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp index 044c5510b..697ce9f0c 100644 --- a/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/HybridMdpPrctlHelper.cpp @@ -13,6 +13,8 @@ #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h" #include "src/modelchecker/results/HybridQuantitativeCheckResult.h" +#include "src/solver/MinMaxLinearEquationSolver.h" + #include "src/exceptions/InvalidPropertyException.h" namespace storm { diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp index f65a834d1..33db26a60 100644 --- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp +++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp @@ -6,6 +6,9 @@ #include "src/utility/vector.h" #include "src/utility/graph.h" +#include "src/solver/MinMaxLinearEquationSolver.h" +#include "src/solver/LpSolver.h" + #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/InvalidPropertyException.h" @@ -363,7 +366,7 @@ namespace storm { std::shared_ptr solver = storm::utility::solver::getLpSolver("LRA for MEC"); solver->setModelSense(minimize ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize); - //// First, we need to create the variables for the problem. + // First, we need to create the variables for the problem. std::map stateToVariableMap; for (auto const& stateChoicesPair : mec) { std::string variableName = "h" + std::to_string(stateChoicesPair.first); diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 61ba12df0..d368ce66a 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -946,7 +946,7 @@ namespace storm { for (auto const& element : row) { // If the probability is zero, we skip this entry. - if (element.getValue() == storm::utility::zero()) { + if (storm::utility::isZero(element.getValue())) { continue; } diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp index 879192014..10c717149 100644 --- a/src/settings/modules/GeneralSettings.cpp +++ b/src/settings/modules/GeneralSettings.cpp @@ -6,7 +6,7 @@ #include "src/settings/OptionBuilder.h" #include "src/settings/ArgumentBuilder.h" #include "src/settings/Argument.h" - +#include "src/solver/SolverSelectionOptions.h" #include "src/exceptions/InvalidSettingsException.h" @@ -231,12 +231,12 @@ namespace storm { return this->getOption(timeoutOptionName).getArgumentByName("time").getValueAsUnsignedInteger(); } - GeneralSettings::EquationSolver GeneralSettings::getEquationSolver() const { + storm::solver::EquationSolverType GeneralSettings::getEquationSolver() const { std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString(); if (equationSolverName == "gmm++") { - return GeneralSettings::EquationSolver::Gmmxx; + return storm::solver::EquationSolverType::Gmmxx; } else if (equationSolverName == "native") { - return GeneralSettings::EquationSolver::Native; + return storm::solver::EquationSolverType::Native; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown equation solver '" << equationSolverName << "'."); } @@ -245,12 +245,12 @@ namespace storm { return this->getOption(eqSolverOptionName).getHasOptionBeenSet(); } - GeneralSettings::LpSolver GeneralSettings::getLpSolver() const { + storm::solver::LpSolverType GeneralSettings::getLpSolver() const { std::string lpSolverName = this->getOption(lpSolverOptionName).getArgumentByName("name").getValueAsString(); if (lpSolverName == "gurobi") { - return GeneralSettings::LpSolver::Gurobi; + return storm::solver::LpSolverType::Gurobi; } else if (lpSolverName == "glpk") { - return GeneralSettings::LpSolver::glpk; + return storm::solver::LpSolverType::Glpk; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown LP solver '" << lpSolverName << "'."); } @@ -287,12 +287,12 @@ namespace storm { return this->getOption(prismCompatibilityOptionName).getHasOptionBeenSet(); } - GeneralSettings::MinMaxTechnique GeneralSettings::getMinMaxEquationSolvingTechnique() const { + storm::solver::MinMaxTechnique GeneralSettings::getMinMaxEquationSolvingTechnique() const { std::string minMaxEquationSolvingTechnique = this->getOption(minMaxEquationSolvingTechniqueOptionName).getArgumentByName("name").getValueAsString(); if (minMaxEquationSolvingTechnique == "valueIteration") { - return GeneralSettings::MinMaxTechnique::ValueIteration; + return storm::solver::MinMaxTechnique::ValueIteration; } else if (minMaxEquationSolvingTechnique == "policyIteration") { - return GeneralSettings::MinMaxTechnique::PolicyIteration; + return storm::solver::MinMaxTechnique::PolicyIteration; } STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown min/max equation solving technique '" << minMaxEquationSolvingTechnique << "'."); } diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h index d4a6488d6..1236e5429 100644 --- a/src/settings/modules/GeneralSettings.h +++ b/src/settings/modules/GeneralSettings.h @@ -5,6 +5,12 @@ #include "src/settings/modules/ModuleSettings.h" namespace storm { + namespace solver { + enum class EquationSolverType; + enum class LpSolverType; + enum class MinMaxTechnique; + } + namespace settings { namespace modules { @@ -16,14 +22,6 @@ namespace storm { // An enumeration of all engines. enum class Engine { Sparse, Hybrid, Dd }; - // An enumeration of all available LP solvers. - enum class LpSolver { Gurobi, glpk }; - - // An enumeration of all available equation solvers. - enum class EquationSolver { Gmmxx, Native }; - - // An enumeration of all available Min/Max equation solver techniques. - enum class MinMaxTechnique { ValueIteration, PolicyIteration }; /*! * Creates a new set of general settings that is managed by the given manager. @@ -251,7 +249,7 @@ namespace storm { * * @return The selected convergence criterion. */ - EquationSolver getEquationSolver() const; + storm::solver::EquationSolverType getEquationSolver() const; /*! * Retrieves whether a equation solver has been set. @@ -265,7 +263,7 @@ namespace storm { * * @return The selected LP solver. */ - LpSolver getLpSolver() const; + storm::solver::LpSolverType getLpSolver() const; /*! * Retrieves whether the export-to-dot option was set. @@ -336,7 +334,7 @@ namespace storm { * * @return The selected min/max equation solving technique. */ - MinMaxTechnique getMinMaxEquationSolvingTechnique() const; + storm::solver::MinMaxTechnique getMinMaxEquationSolvingTechnique() const; bool check() const override; diff --git a/src/settings/modules/GlpkSettings.cpp b/src/settings/modules/GlpkSettings.cpp index 7474feb00..a459ddbb8 100644 --- a/src/settings/modules/GlpkSettings.cpp +++ b/src/settings/modules/GlpkSettings.cpp @@ -6,6 +6,7 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { @@ -34,7 +35,7 @@ namespace storm { bool GlpkSettings::check() const { if (isOutputSet() || isIntegerToleranceSet()) { - STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::glpk, "glpk is not selected as the used LP solver, so setting options for glpk has no effect."); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::solver::LpSolverType::Glpk, "glpk is not selected as the preferred LP solver, so setting options for glpk might have no effect."); } return true; diff --git a/src/settings/modules/GmmxxEquationSolverSettings.cpp b/src/settings/modules/GmmxxEquationSolverSettings.cpp index 525e369c7..fb7cbe307 100644 --- a/src/settings/modules/GmmxxEquationSolverSettings.cpp +++ b/src/settings/modules/GmmxxEquationSolverSettings.cpp @@ -7,6 +7,7 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { @@ -108,7 +109,7 @@ namespace storm { // This list does not include the precision, because this option is shared with other modules. bool optionsSet = isLinearEquationSystemMethodSet() || isPreconditioningMethodSet() || isRestartIterationCountSet() | isMaximalIterationCountSet() || isConvergenceCriterionSet(); - STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect."); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::solver::EquationSolverType::Gmmxx || !optionsSet, "gmm++ is not selected as the preferred equation solver, so setting options for gmm++ might have no effect."); return true; } diff --git a/src/settings/modules/GurobiSettings.cpp b/src/settings/modules/GurobiSettings.cpp index b669a45d3..837c631de 100644 --- a/src/settings/modules/GurobiSettings.cpp +++ b/src/settings/modules/GurobiSettings.cpp @@ -6,7 +6,7 @@ #include "src/settings/Argument.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" - +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { namespace modules { @@ -46,7 +46,7 @@ namespace storm { bool GurobiSettings::check() const { if (isOutputSet() || isIntegerToleranceSet() || isNumberOfThreadsSet()) { - STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::settings::modules::GeneralSettings::LpSolver::Gurobi, "Gurobi is not selected as the used LP solver, so setting options for Gurobi has no effect."); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getLpSolver() == storm::solver::LpSolverType::Gurobi, "Gurobi is not selected as the preferred LP solver, so setting options for Gurobi might have no effect."); } return true; diff --git a/src/settings/modules/NativeEquationSolverSettings.cpp b/src/settings/modules/NativeEquationSolverSettings.cpp index a61291503..6e64f7deb 100644 --- a/src/settings/modules/NativeEquationSolverSettings.cpp +++ b/src/settings/modules/NativeEquationSolverSettings.cpp @@ -6,7 +6,7 @@ #include "src/settings/OptionBuilder.h" #include "src/settings/ArgumentBuilder.h" #include "src/settings/Argument.h" - +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { @@ -81,7 +81,7 @@ namespace storm { // This list does not include the precision, because this option is shared with other modules. bool optionSet = isLinearEquationSystemTechniqueSet() || isMaximalIterationCountSet() || isConvergenceCriterionSet(); - STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Native || !optionSet, "Native is not selected as the equation solver, so setting options for native has no effect."); + STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::solver::EquationSolverType::Native || !optionSet, "Native is not selected as the preferred equation solver, so setting options for native might have no effect."); return true; } diff --git a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp index 1be47979a..a1a00e283 100644 --- a/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp +++ b/src/settings/modules/TopologicalValueIterationEquationSolverSettings.cpp @@ -7,6 +7,7 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/solver/SolverSelectionOptions.h" namespace storm { namespace settings { @@ -54,7 +55,7 @@ namespace storm { bool TopologicalValueIterationEquationSolverSettings::check() const { bool optionsSet = isMaximalIterationCountSet() || isPrecisionSet() || isConvergenceCriterionSet(); - STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect."); + //STORM_LOG_WARN_COND(storm::settings::generalSettings().getEquationSolver() == storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx || !optionsSet, "gmm++ is not selected as the equation solver, so setting options for gmm++ has no effect."); return true; } diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp index a92130b7e..b4357b6d4 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.cpp +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.cpp @@ -14,27 +14,24 @@ namespace storm { namespace solver { template - GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), stormMatrix(A), rowGroupIndices(A.getRowGroupIndices()) { - // Get the settings object to customize solving. - storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::gmmxxEquationSolverSettings(); - storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::generalSettings(); - - // Get appropriate settings. - precision = settings.getPrecision(); - relative = settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative; - maximalNumberOfIterations = settings.getMaximalIterationCount(); - useValueIteration = (generalSettings.getMinMaxEquationSolvingTechnique() == storm::settings::modules::GeneralSettings::MinMaxTechnique::ValueIteration); + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : + MinMaxLinearEquationSolver(A, storm::settings::gmmxxEquationSolverSettings().getPrecision(), \ + storm::settings::gmmxxEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative,\ + storm::settings::gmmxxEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique), + gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { + + } template - GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool useValueIteration, bool relative) : gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), stormMatrix(A), rowGroupIndices(A.getRowGroupIndices()), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations), useValueIteration(useValueIteration) { + GmmxxMinMaxLinearEquationSolver::GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy) : MinMaxLinearEquationSolver(A, precision, relative, maximalNumberOfIterations, trackPolicy, tech), gmmxxMatrix(storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix(A)), rowGroupIndices(A.getRowGroupIndices()) { // Intentionally left empty. } template void GmmxxMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { - if (useValueIteration) { + if (this->useValueIteration) { // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { @@ -56,18 +53,14 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations) { // Compute x' = A*x + b. gmm::mult(*gmmxxMatrix, *currentX, *multiplyResult); gmm::add(b, *multiplyResult); // Reduce the vector x by applying min/max over all nondeterministic choices. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, rowGroupIndices); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, rowGroupIndices); - } - + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, rowGroupIndices); + // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, this->precision, this->relative); @@ -99,7 +92,7 @@ namespace storm { } else { // We will use Policy Iteration to solve the given system. // We first guess an initial choice resolution which will be refined after each iteration. - std::vector::index_type> choiceVector(rowGroupIndices.size() - 1); + this->policy = std::vector(this->A.getRowGroupIndices().size() - 1); // Create our own multiplyResult for solving the deterministic sub-instances. std::vector deterministicMultiplyResult(rowGroupIndices.size() - 1); @@ -126,13 +119,13 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations) { // Take the sub-matrix according to the current choices - storm::storage::SparseMatrix submatrix = stormMatrix.selectRowsFromRowGroups(choiceVector, true); + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); submatrix.convertToEquationSystem(); - GmmxxLinearEquationSolver gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, precision, maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None, relative, 50); - storm::utility::vector::selectVectorValues(subB, choiceVector, rowGroupIndices, b); + GmmxxLinearEquationSolver gmmLinearEquationSolver(submatrix, storm::solver::GmmxxLinearEquationSolver::SolutionMethod::Gmres, this->precision, this->maximalNumberOfIterations, storm::solver::GmmxxLinearEquationSolver::Preconditioner::None, this->relative, 50); + storm::utility::vector::selectVectorValues(subB, this->policy, rowGroupIndices, b); // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); @@ -146,11 +139,8 @@ namespace storm { // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, rowGroupIndices, &choiceVector); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, rowGroupIndices, &choiceVector); - } + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, rowGroupIndices, &(this->policy)); + // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(this->precision), this->relative); @@ -199,11 +189,8 @@ namespace storm { gmm::add(*b, *multiplyResult); } - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, x, rowGroupIndices); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, x, rowGroupIndices); - } + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, x, rowGroupIndices); + } if (!multiplyResultMemoryProvided) { diff --git a/src/solver/GmmxxMinMaxLinearEquationSolver.h b/src/solver/GmmxxMinMaxLinearEquationSolver.h index 4d151d706..b34f761cb 100644 --- a/src/solver/GmmxxMinMaxLinearEquationSolver.h +++ b/src/solver/GmmxxMinMaxLinearEquationSolver.h @@ -20,7 +20,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackPolicy = false); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -31,7 +31,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool useValueIteration, bool relative = true); + GmmxxMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy = false); virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const override; @@ -41,23 +41,9 @@ namespace storm { // The (gmm++) matrix associated with this equation solver. std::unique_ptr> gmmxxMatrix; - // A reference to the original sparse matrix. - storm::storage::SparseMatrix const& stormMatrix; - // A reference to the row group indices of the original matrix. std::vector const& rowGroupIndices; - // The required precision for the iterative methods. - double precision; - - // Sets whether the relative or absolute error is to be considered for convergence detection. - bool relative; - - // The maximal number of iterations to do before iteration is aborted. - uint_fast64_t maximalNumberOfIterations; - - // Whether value iteration or policy iteration is to be used. - bool useValueIteration; }; } // namespace solver } // namespace storm diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h index 43b3f9ad5..61f26294e 100644 --- a/src/solver/LinearEquationSolver.h +++ b/src/solver/LinearEquationSolver.h @@ -15,6 +15,11 @@ namespace storm { template class LinearEquationSolver { public: + + virtual ~LinearEquationSolver() { + // Intentionally left empty. + } + /*! * Solves the equation system A*x = b. The matrix A is required to be square and have a unique solution. * The solution of the set of linear equations will be written to the vector x. Note that the matrix A has diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp new file mode 100644 index 000000000..680ee7ee0 --- /dev/null +++ b/src/solver/MinMaxLinearEquationSolver.cpp @@ -0,0 +1,27 @@ +#include "MinMaxLinearEquationSolver.h" +#include "src/settings/SettingsManager.h" +#include "src/settings/modules/GeneralSettings.h" + +#include "src/utility/macros.h" +#include "src/exceptions/NotImplementedException.h" +#include + +namespace storm { + namespace solver { + AbstractMinMaxLinearEquationSolver::AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : + precision(precision), relative(relativeError), maximalNumberOfIterations(maximalIterations), trackPolicy(trackPolicy) + { + + if(prefTech == MinMaxTechniqueSelection::FROMSETTINGS) { + useValueIteration = (storm::settings::generalSettings().getMinMaxEquationSolvingTechnique() == storm::solver::MinMaxTechnique::ValueIteration); + } else { + useValueIteration = (prefTech == MinMaxTechniqueSelection::ValueIteration); + } + } + + std::vector AbstractMinMaxLinearEquationSolver::getPolicy() const { + STORM_LOG_THROW(!useValueIteration, storm::exceptions::NotImplementedException, "Getting policies after value iteration is not yet supported!"); + return policy; + } + } +} diff --git a/src/solver/MinMaxLinearEquationSolver.h b/src/solver/MinMaxLinearEquationSolver.h index 2c31f67cb..6e6887cd8 100644 --- a/src/solver/MinMaxLinearEquationSolver.h +++ b/src/solver/MinMaxLinearEquationSolver.h @@ -2,7 +2,9 @@ #define STORM_SOLVER_MINMAXLINEAREQUATIONSOLVER_H_ #include - +#include +#include "SolverSelectionOptions.h" +#include "src/storage/sparse/StateType.h" namespace storm { namespace storage { @@ -10,6 +12,38 @@ namespace storm { } namespace solver { + /** + * Abstract base class which provides value-type independent helpers. + */ + class AbstractMinMaxLinearEquationSolver { + + public: + void setPolicyTracking(bool setToTrue=true); + + std::vector getPolicy() const; + + protected: + AbstractMinMaxLinearEquationSolver(double precision, bool relativeError, uint_fast64_t maximalIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech); + + + /// The required precision for the iterative methods. + double precision; + + /// Sets whether the relative or absolute error is to be considered for convergence detection. + bool relative; + + /// The maximal number of iterations to do before iteration is aborted. + uint_fast64_t maximalNumberOfIterations; + + /// Whether value iteration or policy iteration is to be used. + bool useValueIteration; + + /// Whether we track the policy we generate. + bool trackPolicy; + + /// + mutable std::vector policy; + }; /*! * A interface that represents an abstract nondeterministic linear equation solver. In addition to solving @@ -17,8 +51,20 @@ namespace storm { * provided. */ template - class MinMaxLinearEquationSolver { + class MinMaxLinearEquationSolver : public AbstractMinMaxLinearEquationSolver { + protected: + MinMaxLinearEquationSolver(storm::storage::SparseMatrix const& matrix, double precision, bool relativeError, uint_fast64_t maxNrIterations, bool trackPolicy, MinMaxTechniqueSelection prefTech) : + AbstractMinMaxLinearEquationSolver(precision, relativeError, maxNrIterations, trackPolicy, prefTech), + A(matrix) { + // Intentionally left empty. + } + public: + + virtual ~MinMaxLinearEquationSolver() { + // Intentionally left empty. + } + /*! * Solves the equation system x = min/max(A*x + b) given by the parameters. Note that the matrix A has * to be given upon construction time of the solver object. @@ -54,6 +100,9 @@ namespace storm { * @return The result of the repeated matrix-vector multiplication as the content of the vector x. */ virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* multiplyResult = nullptr) const = 0; + + protected: + storm::storage::SparseMatrix const& A; }; } // namespace solver diff --git a/src/solver/NativeMinMaxLinearEquationSolver.cpp b/src/solver/NativeMinMaxLinearEquationSolver.cpp index 22eb207ad..87ee3b043 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.cpp +++ b/src/solver/NativeMinMaxLinearEquationSolver.cpp @@ -14,30 +14,29 @@ namespace storm { namespace solver { template - NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : A(A) { - // Get the settings object to customize solving. - storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); - storm::settings::modules::GeneralSettings const& generalSettings = storm::settings::generalSettings(); - - // Get appropriate settings. - precision = settings.getPrecision(); - relative = settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative; - maximalNumberOfIterations = settings.getMaximalIterationCount(); - useValueIteration = (generalSettings.getMinMaxEquationSolvingTechnique() == storm::settings::modules::GeneralSettings::MinMaxTechnique::ValueIteration); + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique, bool trackPolicy) : + MinMaxLinearEquationSolver(A, storm::settings::nativeEquationSolverSettings().getPrecision(), \ + storm::settings::nativeEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative, \ + storm::settings::nativeEquationSolverSettings().getMaximalIterationCount(), trackPolicy, preferredTechnique) + { + // Intentionally left empty. } template - NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool useValueIteration, bool relative) : A(A), precision(precision), relative(relative), maximalNumberOfIterations(maximalNumberOfIterations), useValueIteration(useValueIteration) { + NativeMinMaxLinearEquationSolver::NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative, bool trackPolicy) : + MinMaxLinearEquationSolver(A, precision, \ + relative, \ + maximalNumberOfIterations, trackPolicy, tech) { // Intentionally left empty. } template void NativeMinMaxLinearEquationSolver::solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult, std::vector* newX) const { - if (useValueIteration) { + if (this->useValueIteration) { // Set up the environment for the power method. If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { - multiplyResult = new std::vector(A.getRowCount()); + multiplyResult = new std::vector(this->A.getRowCount()); multiplyResultMemoryProvided = false; } std::vector* currentX = &x; @@ -54,21 +53,17 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the // user-specified maximum number of iterations. - while (!converged && iterations < maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations) { // Compute x' = A*x + b. - A.multiplyWithVector(*currentX, *multiplyResult); + this->A.multiplyWithVector(*currentX, *multiplyResult); storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult); // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, A.getRowGroupIndices()); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, A.getRowGroupIndices()); - } - + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, this->A.getRowGroupIndices()); + // Determine whether the method converged. - converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(precision), relative); + converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(this->precision), this->relative); // Update environment variables. std::swap(currentX, newX); @@ -98,11 +93,11 @@ namespace storm { } else { // We will use Policy Iteration to solve the given system. // We first guess an initial choice resolution which will be refined after each iteration. - std::vector::index_type> choiceVector(A.getRowGroupIndices().size() - 1); + this->policy = std::vector(this->A.getRowGroupIndices().size() - 1); // Create our own multiplyResult for solving the deterministic sub-instances. - std::vector deterministicMultiplyResult(A.getRowGroupIndices().size() - 1); - std::vector subB(A.getRowGroupIndices().size() - 1); + std::vector deterministicMultiplyResult(this->A.getRowGroupIndices().size() - 1); + std::vector subB(this->A.getRowGroupIndices().size() - 1); // Check whether intermediate storage was provided and create it otherwise. bool multiplyResultMemoryProvided = true; @@ -126,13 +121,13 @@ namespace storm { // Proceed with the iterations as long as the method did not converge or reach the user-specified maximum number // of iterations. - while (!converged && iterations < maximalNumberOfIterations) { + while (!converged && iterations < this->maximalNumberOfIterations) { // Take the sub-matrix according to the current choices - storm::storage::SparseMatrix submatrix = A.selectRowsFromRowGroups(choiceVector, true); + storm::storage::SparseMatrix submatrix = this->A.selectRowsFromRowGroups(this->policy, true); submatrix.convertToEquationSystem(); NativeLinearEquationSolver nativeLinearEquationSolver(submatrix); - storm::utility::vector::selectVectorValues(subB, choiceVector, A.getRowGroupIndices(), b); + storm::utility::vector::selectVectorValues(subB, this->policy, this->A.getRowGroupIndices(), b); // Copy X since we will overwrite it std::copy(currentX->begin(), currentX->end(), newX->begin()); @@ -141,16 +136,13 @@ namespace storm { nativeLinearEquationSolver.solveEquationSystem(*newX, subB, &deterministicMultiplyResult); // Compute x' = A*x + b. This step is necessary to allow the choosing of the optimal policy for the next iteration. - A.multiplyWithVector(*newX, *multiplyResult); + this->A.multiplyWithVector(*newX, *multiplyResult); storm::utility::vector::addVectors(*multiplyResult, b, *multiplyResult); // Reduce the vector x by applying min/max over all nondeterministic choices. // Here, we capture which choice was taken in each state, thereby refining our initial guess. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, *newX, A.getRowGroupIndices(), &choiceVector); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, *newX, A.getRowGroupIndices(), &choiceVector); - } + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, *newX, this->A.getRowGroupIndices(), &(this->policy)); + // Determine whether the method converged. converged = storm::utility::vector::equalModuloPrecision(*currentX, *newX, static_cast(this->precision), this->relative); @@ -166,6 +158,7 @@ namespace storm { } else { LOG4CPLUS_WARN(logger, "Iterative solver did not converge after " << iterations << " iterations."); } + // If we performed an odd number of iterations, we need to swap the x and currentX, because the newest result // is currently stored in currentX, but x is the output vector. @@ -189,13 +182,13 @@ namespace storm { // If scratch memory was not provided, we need to create it. bool multiplyResultMemoryProvided = true; if (multiplyResult == nullptr) { - multiplyResult = new std::vector(A.getRowCount()); + multiplyResult = new std::vector(this->A.getRowCount()); multiplyResultMemoryProvided = false; } // Now perform matrix-vector multiplication as long as we meet the bound of the formula. for (uint_fast64_t i = 0; i < n; ++i) { - A.multiplyWithVector(x, *multiplyResult); + this->A.multiplyWithVector(x, *multiplyResult); // Add b if it is non-null. if (b != nullptr) { @@ -204,11 +197,8 @@ namespace storm { // Reduce the vector x' by applying min/max for all non-deterministic choices as given by the topmost // element of the min/max operator stack. - if (minimize) { - storm::utility::vector::reduceVectorMin(*multiplyResult, x, A.getRowGroupIndices()); - } else { - storm::utility::vector::reduceVectorMax(*multiplyResult, x, A.getRowGroupIndices()); - } + storm::utility::vector::reduceVectorMinOrMax(minimize, *multiplyResult, x, this->A.getRowGroupIndices()); + } if (!multiplyResultMemoryProvided) { diff --git a/src/solver/NativeMinMaxLinearEquationSolver.h b/src/solver/NativeMinMaxLinearEquationSolver.h index c3fa66b35..5e297096a 100644 --- a/src/solver/NativeMinMaxLinearEquationSolver.h +++ b/src/solver/NativeMinMaxLinearEquationSolver.h @@ -19,7 +19,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, MinMaxTechniqueSelection preferredTechnique = MinMaxTechniqueSelection::FROMSETTINGS, bool trackPolicy = false); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -30,27 +30,12 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool useValueIteration, bool relative = true); + NativeMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, MinMaxTechniqueSelection tech, bool relative = true, bool trackPolicy = false); virtual void performMatrixVectorMultiplication(bool minimize, std::vector& x, std::vector* b = nullptr, uint_fast64_t n = 1, std::vector* newX = nullptr) const override; virtual void solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; - protected: - // A reference to the matrix the gives the coefficients of the linear equation system. - storm::storage::SparseMatrix const& A; - - // The required precision for the iterative methods. - double precision; - - // Sets whether the relative or absolute error is to be considered for convergence detection. - bool relative; - - // The maximal number of iterations to do before iteration is aborted. - uint_fast64_t maximalNumberOfIterations; - - // Whether value iteration or policy iteration is to be used. - bool useValueIteration; }; } // namespace solver } // namespace storm diff --git a/src/solver/SolverSelectionOptions.cpp b/src/solver/SolverSelectionOptions.cpp new file mode 100644 index 000000000..63e56eda7 --- /dev/null +++ b/src/solver/SolverSelectionOptions.cpp @@ -0,0 +1,32 @@ +#include "src/solver/SolverSelectionOptions.h" + +namespace storm { + namespace solver { + std::string toString(MinMaxTechnique m) { + switch(m) { + case MinMaxTechnique::PolicyIteration: + return "policy"; + case MinMaxTechnique::ValueIteration: + return "value"; + } + + } + std::string toString(LpSolverType t) { + switch(t) { + case LpSolverType::Gurobi: + return "Gurobi"; + case LpSolverType::Glpk: + return "Glpk"; + } + } + + std::string toString(EquationSolverType t) { + switch(t) { + case EquationSolverType::Native: + return "Native"; + case EquationSolverType::Gmmxx: + return "Gmmxx"; + } + } + } +} diff --git a/src/solver/SolverSelectionOptions.h b/src/solver/SolverSelectionOptions.h new file mode 100644 index 000000000..cfba09a15 --- /dev/null +++ b/src/solver/SolverSelectionOptions.h @@ -0,0 +1,20 @@ + +#ifndef SOLVERSELECTIONOPTIONS_H +#define SOLVERSELECTIONOPTIONS_H + + +#include "src/utility/ExtendSettingEnumWithSelectionField.h" + +namespace storm { + namespace solver { + ExtendEnumsWithSelectionField(MinMaxTechnique, PolicyIteration, ValueIteration) + + + ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk) + ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx) + + } +} + +#endif + diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp index d3d122e12..d31a02d3e 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.cpp +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.cpp @@ -27,19 +27,12 @@ namespace storm { namespace solver { template - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : NativeMinMaxLinearEquationSolver(A) { + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A) : + NativeMinMaxLinearEquationSolver(A, storm::settings::topologicalValueIterationEquationSolverSettings().getPrecision(), \ + storm::settings::topologicalValueIterationEquationSolverSettings().getMaximalIterationCount(), MinMaxTechniqueSelection::ValueIteration, \ + storm::settings::topologicalValueIterationEquationSolverSettings().getConvergenceCriterion() == storm::settings::modules::TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative) + { // Get the settings object to customize solving. - - //storm::settings::Settings* settings = storm::settings::Settings::getInstance(); - auto settings = storm::settings::topologicalValueIterationEquationSolverSettings(); - // Get appropriate settings. - //this->maximalNumberOfIterations = settings->getOptionByLongName("maxiter").getArgument(0).getValueAsUnsignedInteger(); - //this->precision = settings->getOptionByLongName("precision").getArgument(0).getValueAsDouble(); - //this->relative = !settings->isSet("absolute"); - this->maximalNumberOfIterations = settings.getMaximalIterationCount(); - this->precision = settings.getPrecision(); - this->relative = (settings.getConvergenceCriterion() == storm::settings::modules::TopologicalValueIterationEquationSolverSettings::ConvergenceCriterion::Relative); - auto generalSettings = storm::settings::generalSettings(); this->enableCuda = generalSettings.isCudaSet(); #ifdef STORM_HAVE_CUDA @@ -48,7 +41,7 @@ namespace storm { } template - TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeMinMaxLinearEquationSolver(A, precision, maximalNumberOfIterations, relative) { + TopologicalMinMaxLinearEquationSolver::TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative) : NativeMinMaxLinearEquationSolver(A, precision, maximalNumberOfIterations, MinMaxTechniqueSelection::ValueIteration ,relative) { // Intentionally left empty. } diff --git a/src/solver/TopologicalMinMaxLinearEquationSolver.h b/src/solver/TopologicalMinMaxLinearEquationSolver.h index 4f748672c..be1b844bd 100644 --- a/src/solver/TopologicalMinMaxLinearEquationSolver.h +++ b/src/solver/TopologicalMinMaxLinearEquationSolver.h @@ -30,7 +30,7 @@ namespace storm { * * @param A The matrix defining the coefficients of the linear equation system. */ - TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); + TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A); /*! * Constructs a min/max linear equation solver with the given parameters. @@ -41,7 +41,7 @@ namespace storm { * @param relative If set, the relative error rather than the absolute error is considered for convergence * detection. */ - TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); + TopologicalMinMaxLinearEquationSolver(storm::storage::SparseMatrix const& A, double precision, uint_fast64_t maximalNumberOfIterations, bool relative = true); virtual void solveEquationSystem(bool minimize, std::vector& x, std::vector const& b, std::vector* multiplyResult = nullptr, std::vector* newX = nullptr) const override; private: diff --git a/src/storage/BitVector.cpp b/src/storage/BitVector.cpp index 9835c54dc..3e1e9bb5b 100644 --- a/src/storage/BitVector.cpp +++ b/src/storage/BitVector.cpp @@ -78,6 +78,11 @@ namespace storm { set(begin, end); } + BitVector::BitVector(uint_fast64_t length, std::vector setEntries) : BitVector(length, setEntries.begin(), setEntries.end()) + { + // Intentionally left empty. + } + BitVector::BitVector(uint_fast64_t bucketCount, uint_fast64_t bitCount) : bitCount(bitCount), bucketVector(bucketCount) { STORM_LOG_ASSERT((bucketCount << 6) == bitCount, "Bit count does not match number of buckets."); } diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h index ec4cce693..4c5e64352 100644 --- a/src/storage/BitVector.h +++ b/src/storage/BitVector.h @@ -118,6 +118,11 @@ namespace storm { template BitVector(uint_fast64_t length, InputIterator first, InputIterator last); + /*! + * Creates a bit vector that has exactly the bits set that are given by the vector + */ + BitVector(uint_fast64_t length, std::vector setEntries); + /*! * Performs a deep copy of the given bit vector. * diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp index 53277ec2d..eee581ebc 100644 --- a/src/storage/SparseMatrix.cpp +++ b/src/storage/SparseMatrix.cpp @@ -12,6 +12,7 @@ #include "src/storage/BitVector.h" #include "src/utility/constants.h" +#include "src/utility/ConstantsComparator.h" #include "src/exceptions/InvalidStateException.h" #include "src/exceptions/NotImplementedException.h" @@ -346,10 +347,10 @@ namespace storm { for (index_type row = 0; row < this->getRowCount(); ++row) { for (const_iterator it1 = this->begin(row), ite1 = this->end(row), it2 = other.begin(row), ite2 = other.end(row); it1 != ite1 && it2 != ite2; ++it1, ++it2) { // Skip over all zero entries in both matrices. - while (it1 != ite1 && it1->getValue() == storm::utility::zero()) { + while (it1 != ite1 && storm::utility::isZero(it1->getValue())) { ++it1; } - while (it2 != ite2 && it2->getValue() == storm::utility::zero()) { + while (it2 != ite2 && storm::utility::isZero(it2->getValue())) { ++it2; } if ((it1 == ite1) || (it2 == ite2)) { @@ -1065,6 +1066,17 @@ namespace storm { return sum; } + template + bool SparseMatrix::isProbabilistic() const { + storm::utility::ConstantsComparator comparator; + for(index_type row = 0; row < this->rowCount; ++row) { + if(!comparator.isOne(getRowSum(row))) { + return false; + } + } + return true; + } + template bool SparseMatrix::isSubmatrixOf(SparseMatrix const& matrix) const { // Check for matching sizes. diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h index 1dd16b3de..71fe4078e 100644 --- a/src/storage/SparseMatrix.h +++ b/src/storage/SparseMatrix.h @@ -33,6 +33,9 @@ namespace storm { // Forward declare matrix class. template class SparseMatrix; + typedef uint_fast64_t SparseMatrixIndexType; + + template class MatrixEntry { public: @@ -128,7 +131,7 @@ namespace storm { template class SparseMatrixBuilder { public: - typedef uint_fast64_t index_type; + typedef SparseMatrixIndexType index_type; typedef ValueType value_type; /*! @@ -300,7 +303,7 @@ namespace storm { friend class storm::solver::TopologicalValueIterationMinMaxLinearEquationSolver; friend class SparseMatrixBuilder; - typedef uint_fast64_t index_type; + typedef SparseMatrixIndexType index_type; typedef ValueType value_type; typedef typename std::vector>::iterator iterator; typedef typename std::vector>::const_iterator const_iterator; @@ -738,6 +741,10 @@ namespace storm { */ value_type getRowSum(index_type row) const; + /*! + * Checks for each row whether it sums to one. + */ + bool isProbabilistic() const; /*! * Checks if the current matrix is a submatrix of the given matrix, where a matrix A is called a submatrix * of B if B has no entries in position where A has none. Additionally, the matrices must be of equal size. @@ -942,6 +949,7 @@ namespace storm { // A vector indicating the row groups of the matrix. std::vector rowGroupIndices; + }; } // namespace storage diff --git a/src/storage/prism/Assignment.cpp b/src/storage/prism/Assignment.cpp index 3628c76ef..a6c8b4456 100644 --- a/src/storage/prism/Assignment.cpp +++ b/src/storage/prism/Assignment.cpp @@ -1,4 +1,5 @@ #include "Assignment.h" +#include namespace storm { namespace prism { @@ -22,6 +23,20 @@ namespace storm { return Assignment(this->getVariable(), this->getExpression().substitute(substitution).simplify(), this->getFilename(), this->getLineNumber()); } + bool Assignment::isIdentity() const { + if(this->expression.isVariable()) { + assert(this->expression.getVariables().size() == 1); + //if( variable == *(this->expression.getVariables().begin())) { + // std::cout << variable.getName() << " == " << (this->expression.getVariables().begin())->getName() << std::endl; + //} + //else { + // std::cout << "********" << variable.getName() << " != " << (this->expression.getVariables().begin())->getName() << std::endl; + //} + return variable == *(this->expression.getVariables().begin()); + } + return false; + } + std::ostream& operator<<(std::ostream& stream, Assignment const& assignment) { stream << "(" << assignment.getVariableName() << "' = " << assignment.getExpression() << ")"; return stream; diff --git a/src/storage/prism/Assignment.h b/src/storage/prism/Assignment.h index cb6006ba7..1c45a2b78 100644 --- a/src/storage/prism/Assignment.h +++ b/src/storage/prism/Assignment.h @@ -60,6 +60,13 @@ namespace storm { */ Assignment substitute(std::map const& substitution) const; + /*! + * Checks whether the assignment is an identity (lhs equals rhs) + * + * @return true iff the assignment is of the form a' = a. + */ + bool isIdentity() const; + friend std::ostream& operator<<(std::ostream& stream, Assignment const& assignment); private: diff --git a/src/storage/prism/Command.cpp b/src/storage/prism/Command.cpp index e2b1d3698..5cad634e7 100644 --- a/src/storage/prism/Command.cpp +++ b/src/storage/prism/Command.cpp @@ -1,4 +1,5 @@ #include "Command.h" +#include namespace storm { namespace prism { @@ -31,6 +32,7 @@ namespace storm { } storm::prism::Update const& Command::getUpdate(uint_fast64_t index) const { + assert(index < getNumberOfUpdates()); return this->updates[index]; } @@ -71,6 +73,20 @@ namespace storm { return true; } + Command Command::removeIdentityAssignmentsFromUpdates() const { + std::vector newUpdates; + newUpdates.reserve(this->getNumberOfUpdates()); + for (auto const& update : this->getUpdates()) { + newUpdates.emplace_back(update.removeIdentityAssignments()); + } + return copyWithNewUpdates(std::move(newUpdates)); + + } + + Command Command::copyWithNewUpdates(std::vector && newUpdates) const { + return Command(this->globalIndex, this->markovian, this->getActionIndex(), this->getActionName(), guardExpression, newUpdates, this->getFilename(), this->getLineNumber()); + } + std::ostream& operator<<(std::ostream& stream, Command const& command) { if (command.isMarkovian()) { stream << "<" << command.getActionName() << "> "; diff --git a/src/storage/prism/Command.h b/src/storage/prism/Command.h index dd8b2f9b6..658cce67d 100644 --- a/src/storage/prism/Command.h +++ b/src/storage/prism/Command.h @@ -128,6 +128,12 @@ namespace storm { friend std::ostream& operator<<(std::ostream& stream, Command const& command); + /** + * Removes identity assignments from the updates + * @return The resulting command + */ + Command removeIdentityAssignmentsFromUpdates() const; + private: // The index of the action associated with this command. uint_fast64_t actionIndex; @@ -150,6 +156,8 @@ namespace storm { // A flag indicating whether the command is labeled. bool labeled; + + Command copyWithNewUpdates(std::vector&& newUpdates) const; }; } // namespace prism diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index f398e8154..18888c646 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -802,6 +802,14 @@ namespace storm { std::vector newModules; std::vector newConstants = this->getConstants(); for (auto const& module : this->getModules()) { + // Remove identity assignments from the updates + std::vector newCommands; + for (auto const& command : module.getCommands()) { + newCommands.emplace_back(command.removeIdentityAssignmentsFromUpdates()); + } + + // Substitute Variables by Global constants if possible. + std::map booleanVars; std::map integerVars; for (auto const& variable : module.getBooleanVariables()) { @@ -811,7 +819,7 @@ namespace storm { integerVars.emplace(variable.getExpressionVariable(), variable.getInitialValueExpression()); } - for (auto const& command : module.getCommands()) { + for (auto const& command : newCommands) { // Check all updates. for (auto const& update : command.getUpdates()) { // Check all assignments. @@ -842,7 +850,7 @@ namespace storm { } } - newModules.emplace_back(module.getName(), newBVars, newIVars, module.getCommands()); + newModules.emplace_back(module.getName(), newBVars, newIVars, newCommands); for(auto const& entry : booleanVars) { newConstants.emplace_back(entry.first, entry.second); diff --git a/src/storage/prism/Update.cpp b/src/storage/prism/Update.cpp index 147e9b42e..4c3432fde 100644 --- a/src/storage/prism/Update.cpp +++ b/src/storage/prism/Update.cpp @@ -53,6 +53,17 @@ namespace storm { return Update(this->getGlobalIndex(), this->getLikelihoodExpression().substitute(substitution), newAssignments, this->getFilename(), this->getLineNumber()); } + Update Update::removeIdentityAssignments() const { + std::vector newAssignments; + newAssignments.reserve(getNumberOfAssignments()); + for(auto const& ass : this->assignments) { + if(!ass.isIdentity()) { + newAssignments.push_back(ass); + } + } + return Update(this->globalIndex, this->likelihoodExpression, newAssignments, getFilename(), getLineNumber()); + } + std::ostream& operator<<(std::ostream& stream, Update const& update) { stream << update.getLikelihoodExpression() << " : "; if (update.getAssignments().empty()) { diff --git a/src/storage/prism/Update.h b/src/storage/prism/Update.h index 1ea5470f8..7b9ebdbc1 100644 --- a/src/storage/prism/Update.h +++ b/src/storage/prism/Update.h @@ -73,6 +73,12 @@ namespace storm { * @return The resulting update. */ Update substitute(std::map const& substitution) const; + /*! + * Removes all assignments which do not change the variable. + * + * @return The resulting update. + */ + Update removeIdentityAssignments() const; friend std::ostream& operator<<(std::ostream& stream, Update const& assignment); diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp index de027d541..f55185040 100644 --- a/src/utility/ConstantsComparator.cpp +++ b/src/utility/ConstantsComparator.cpp @@ -8,22 +8,22 @@ namespace storm { namespace utility { template bool ConstantsComparator::isOne(ValueType const& value) const { - return value == one(); + return isOne(value); } template bool ConstantsComparator::isZero(ValueType const& value) const { - return value == zero(); + return isZero(value); } template bool ConstantsComparator::isEqual(ValueType const& value1, ValueType const& value2) const { return value1 == value2; } - + template bool ConstantsComparator::isConstant(ValueType const& value) const { - return true; + return isConstant(value); } template @@ -86,49 +86,7 @@ namespace storm { bool ConstantsComparator::isConstant(double const& value) const { return true; } - -#ifdef STORM_HAVE_CARL - ConstantsComparator::ConstantsComparator() { - // Intentionally left empty. - } - - bool ConstantsComparator::isOne(storm::RationalFunction const& value) const { - return value.isOne(); - } - - bool ConstantsComparator::isZero(storm::RationalFunction const& value) const { - return value.isZero(); - } - - bool ConstantsComparator::isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const { - return value1 == value2; - } - - bool ConstantsComparator::isConstant(storm::RationalFunction const& value) const { - return value.isConstant(); - } - - ConstantsComparator::ConstantsComparator() { - // Intentionally left empty. - } - - bool ConstantsComparator::isOne(storm::Polynomial const& value) const { - return value.isOne(); - } - - bool ConstantsComparator::isZero(storm::Polynomial const& value) const { - return value.isZero(); - } - - bool ConstantsComparator::isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const { - return value1 == value2; - } - - bool ConstantsComparator::isConstant(storm::Polynomial const& value) const { - return value.isConstant(); - } -#endif - + // Explicit instantiations. template class ConstantsComparator; template class ConstantsComparator; @@ -137,6 +95,7 @@ namespace storm { #ifdef STORM_HAVE_CARL template class ConstantsComparator; template class ConstantsComparator; + template class ConstantsComparator; #endif } } \ No newline at end of file diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h index d04641084..83e92ced3 100644 --- a/src/utility/ConstantsComparator.h +++ b/src/utility/ConstantsComparator.h @@ -10,7 +10,7 @@ namespace storm { class ConstantsComparator { public: // This needs to be in here, otherwise the template specializations are not used properly. - ConstantsComparator(); + ConstantsComparator() = default; bool isOne(ValueType const& value) const; @@ -21,9 +21,6 @@ namespace storm { bool isConstant(ValueType const& value) const; bool isInfinity(ValueType const& value) const; - - private: - ValueType precision; }; // For floats we specialize this class and consider the comparison modulo some predefined precision. diff --git a/src/utility/ExtendSettingEnumWithSelectionField.h b/src/utility/ExtendSettingEnumWithSelectionField.h new file mode 100644 index 000000000..997571f6e --- /dev/null +++ b/src/utility/ExtendSettingEnumWithSelectionField.h @@ -0,0 +1,28 @@ +#ifndef EXTENDSETTINGENUMWITHSELECTIONFIELD_H +#define EXTENDSETTINGENUMWITHSELECTIONFIELD_H + + + +#include +#include + + +#define ExtendEnumsWithSelectionField( NAME, ...) \ + enum class NAME : int { __VA_ARGS__ }; \ + enum class NAME##Selection : int { __VA_ARGS__, FROMSETTINGS }; \ + std::string toString(NAME); \ + inline NAME convert(NAME##Selection e) { \ + assert(e != NAME##Selection::FROMSETTINGS); \ + return static_cast< NAME >(e); \ + } \ + inline std::string toString(NAME##Selection e) { \ + if(e == NAME##Selection::FROMSETTINGS) { \ + return "[from settings]"; \ + }\ + else { \ + return toString(convert(e)); \ + } \ + } + +#endif /* EXTENDSETTINGENUMWITHSELECTIONFIELD_H */ + diff --git a/src/utility/cli.cpp b/src/utility/cli.cpp index b3867c299..4b7c2b74b 100644 --- a/src/utility/cli.cpp +++ b/src/utility/cli.cpp @@ -212,7 +212,7 @@ namespace storm { boost::optional program; if (settings.isSymbolicSet()) { std::string const& programFile = settings.getSymbolicModelFilename(); - program = storm::parser::PrismParser::parse(programFile).simplify(); + program = storm::parser::PrismParser::parse(programFile).simplify().simplify(); program->checkValidity(); } diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp index ae348ccce..1b599185d 100644 --- a/src/utility/constants.cpp +++ b/src/utility/constants.cpp @@ -25,7 +25,52 @@ namespace storm { return std::numeric_limits::infinity(); } + template + bool isOne(ValueType const& a) { + return a == one(); + } + + template + bool isZero(ValueType const& a) { + return a == zero(); + } + + template + bool isConstant(ValueType const& a) { + return true; + } + #ifdef STORM_HAVE_CARL + template<> + bool isOne(storm::RationalFunction const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::RationalFunction const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::RationalFunction const& a) { + return a.isConstant(); + } + + template<> + bool isOne(storm::Polynomial const& a) { + return a.isOne(); + } + + template<> + bool isZero(storm::Polynomial const& a) { + return a.isZero(); + } + + template<> + bool isConstant(storm::Polynomial const& a) { + return a.isConstant(); + } + template<> storm::RationalFunction infinity() { // FIXME: this does not work. @@ -65,9 +110,7 @@ namespace storm { template<> RationalFunction&& simplify(RationalFunction&& value); -#endif - -#ifdef STORM_HAVE_CARL + template<> RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) { return carl::pow(value, exponent); @@ -91,7 +134,7 @@ namespace storm { return std::move(value); } #endif - + template storm::storage::MatrixEntry simplify(storm::storage::MatrixEntry matrixEntry) { simplify(matrixEntry.getValue()); @@ -111,6 +154,10 @@ namespace storm { } // Explicit instantiations. + template bool isOne(double const& value); + template bool isZero(double const& value); + template bool isConstant(double const& value); + template double one(); template double zero(); template double infinity(); @@ -123,6 +170,10 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + template bool isOne(float const& value); + template bool isZero(float const& value); + template bool isConstant(float const& value); + template float one(); template float zero(); template float infinity(); @@ -135,6 +186,10 @@ namespace storm { template storm::storage::MatrixEntry& simplify(storm::storage::MatrixEntry& matrixEntry); template storm::storage::MatrixEntry&& simplify(storm::storage::MatrixEntry&& matrixEntry); + template bool isOne(int const& value); + template bool isZero(int const& value); + template bool isConstant(int const& value); + template int one(); template int zero(); template int infinity(); diff --git a/src/utility/constants.h b/src/utility/constants.h index f18590ef3..8f6d8149e 100644 --- a/src/utility/constants.h +++ b/src/utility/constants.h @@ -30,6 +30,15 @@ namespace storm { template ValueType infinity(); + template + bool isOne(ValueType const& a); + + template + bool isZero(ValueType const& a); + + template + bool isConstant(ValueType const& a); + template ValueType pow(ValueType const& value, uint_fast64_t exponent); diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp index 0e818456c..66927c131 100644 --- a/src/utility/solver.cpp +++ b/src/utility/solver.cpp @@ -1,9 +1,9 @@ #include "src/utility/solver.h" -#include "src/settings/SettingsManager.h" - #include "src/solver/SymbolicGameSolver.h" + +#include "src/solver/SymbolicLinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" #include "src/solver/GmmxxLinearEquationSolver.h" @@ -16,10 +16,16 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + +#include "src/exceptions/InvalidSettingsException.h" + namespace storm { namespace utility { namespace solver { + + template std::unique_ptr> SymbolicLinearEquationSolverFactory::create(storm::dd::Add const& A, storm::dd::Bdd const& allRows, std::set const& rowMetaVariables, std::set const& columnMetaVariables, std::vector> const& rowColumnMetaVariablePairs) const { return std::unique_ptr>(new storm::solver::SymbolicLinearEquationSolver(A, allRows, rowMetaVariables, columnMetaVariables, rowColumnMetaVariablePairs)); @@ -37,10 +43,10 @@ namespace storm { template std::unique_ptr> LinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - storm::settings::modules::GeneralSettings::EquationSolver equationSolver = storm::settings::generalSettings().getEquationSolver(); + storm::solver::EquationSolverType equationSolver = storm::settings::generalSettings().getEquationSolver(); switch (equationSolver) { - case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver(matrix)); - case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr>(new storm::solver::NativeLinearEquationSolver(matrix)); + case storm::solver::EquationSolverType::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver(matrix)); + case storm::solver::EquationSolverType::Native: return std::unique_ptr>(new storm::solver::NativeLinearEquationSolver(matrix)); default: return std::unique_ptr>(new storm::solver::GmmxxLinearEquationSolver(matrix)); } } @@ -76,10 +82,10 @@ namespace storm { template std::unique_ptr> MinMaxLinearEquationSolverFactory::create(storm::storage::SparseMatrix const& matrix) const { - storm::settings::modules::GeneralSettings::EquationSolver equationSolver = storm::settings::generalSettings().getEquationSolver(); + storm::solver::EquationSolverType equationSolver = storm::settings::generalSettings().getEquationSolver(); switch (equationSolver) { - case storm::settings::modules::GeneralSettings::EquationSolver::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); - case storm::settings::modules::GeneralSettings::EquationSolver::Native: return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); + case storm::solver::EquationSolverType::Gmmxx: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); + case storm::solver::EquationSolverType::Native: return std::unique_ptr>(new storm::solver::NativeMinMaxLinearEquationSolver(matrix)); default: return std::unique_ptr>(new storm::solver::GmmxxMinMaxLinearEquationSolver(matrix)); } } @@ -100,10 +106,10 @@ namespace storm { } std::unique_ptr LpSolverFactory::create(std::string const& name) const { - storm::settings::modules::GeneralSettings::LpSolver lpSolver = storm::settings::generalSettings().getLpSolver(); + storm::solver::LpSolverType lpSolver = storm::settings::generalSettings().getLpSolver(); switch (lpSolver) { - case storm::settings::modules::GeneralSettings::LpSolver::Gurobi: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); - case storm::settings::modules::GeneralSettings::LpSolver::glpk: return std::unique_ptr(new storm::solver::GlpkLpSolver(name)); + case storm::solver::LpSolverType::Gurobi: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); + case storm::solver::LpSolverType::Glpk: return std::unique_ptr(new storm::solver::GlpkLpSolver(name)); default: return std::unique_ptr(new storm::solver::GurobiLpSolver(name)); } } diff --git a/src/utility/solver.h b/src/utility/solver.h index 715ad3972..58a7d1018 100644 --- a/src/utility/solver.h +++ b/src/utility/solver.h @@ -6,17 +6,28 @@ #include "src/solver/SymbolicLinearEquationSolver.h" #include "src/solver/LinearEquationSolver.h" #include "src/solver/NativeLinearEquationSolver.h" -#include "src/solver/MinMaxLinearEquationSolver.h" -#include "src/solver/LpSolver.h" - #include "src/storage/dd/DdType.h" -#include "src/settings/modules/NativeEquationSolverSettings.h" - -#include "src/exceptions/InvalidSettingsException.h" +#include "src/utility/ExtendSettingEnumWithSelectionField.h" namespace storm { + namespace solver { + template class SymbolicGameSolver; + template class SymbolicLinearEquationSolver; + template class LinearEquationSolver; + template class MinMaxLinearEquationSolver; + class LpSolver; + } + namespace dd { + template class Add; + template class Bdd; + } + namespace expressions { + class Variable; + } + namespace utility { namespace solver { + template class SymbolicLinearEquationSolverFactory { public: diff --git a/src/utility/vector.h b/src/utility/vector.h index c695fa6d9..bd21028f9 100644 --- a/src/utility/vector.h +++ b/src/utility/vector.h @@ -350,6 +350,22 @@ namespace storm { return filter(values, fnc); } + /** + * Sum the entries from values that are set to one in the filter vector. + * @param values + * @param filter + * @return The sum of the values with a corresponding one in the filter. + */ + template + VT sum_if(std::vector const& values, storm::storage::BitVector const& filter) { + assert(values.size() >= filter.size()); + VT sum = storm::utility::zero(); + for(uint_fast64_t i : filter) { + sum += values[i]; + } + return sum; + } + /*! * Reduces the given source vector by selecting an element according to the given filter out of each row group. * @@ -434,7 +450,7 @@ namespace storm { } #endif } - + /*! * Reduces the given source vector by selecting the smallest element out of each row group. * @@ -461,6 +477,24 @@ namespace storm { reduceVector(source, target, rowGrouping, std::greater(), choices); } + /*! + * Reduces the given source vector by selecting either the smallest or the largest out of each row group. + * + * @param minimize If true, select the smallest, else select the largest. + * @param source The source vector which is to be reduced. + * @param target The target vector into which a single element from each row group is written. + * @param rowGrouping A vector that specifies the begin and end of each group of elements in the source vector. + * @param choices If non-null, this vector is used to store the choices made during the selection. + */ + template + void reduceVectorMinOrMax(bool minimize, std::vector const& source, std::vector& target, std::vector const& rowGrouping, std::vector* choices = nullptr) { + if(minimize) { + reduceVectorMin(source, target, rowGrouping, choices); + } else { + reduceVectorMax(source, target, rowGrouping, choices); + } + } + /*! * Compares the given elements and determines whether they are equal modulo the given precision. The provided flag * additionaly specifies whether the error is computed in relative or absolute terms. diff --git a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp index 706f8eef3..d187945fa 100644 --- a/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxCtmcCslModelCheckerTest.cpp @@ -13,6 +13,8 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxCtmcCslModelCheckerTest, Cluster) { diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp index d7d1b2524..224ff209c 100644 --- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" #include "src/models/sparse/StandardRewardModel.h" @@ -9,12 +10,16 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); std::shared_ptr> dtmc = abstractModel->as>(); @@ -24,34 +29,30 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("one"); - auto eventuallyFormula = std::make_shared(labelFormula); - - std::unique_ptr result = checker.check(*eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); + + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("two"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"two\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); - - result = checker.check(*eventuallyFormula); + formula = parser.parseFromString("P=? [F \"three\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - auto done = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(done); + formula = parser.parseFromString("R=? [F \"done\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(11.0/3.0, quantitativeResult4[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -61,6 +62,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; std::shared_ptr> dtmc = abstractModel->as>(); @@ -69,26 +73,23 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("observe0Greater1"); - auto eventuallyFormula = std::make_shared(labelFormula); - - std::unique_ptr result = checker.check(*eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); + + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeIGreater1"); - eventuallyFormula = std::make_shared(labelFormula); - - result = checker.check(*eventuallyFormula); + formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -98,6 +99,10 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); @@ -105,27 +110,23 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); - - std::unique_ptr result = checker.check(*eventuallyFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); + + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 20); - - result = checker.check(*boundedUntilFormula); + formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); - - result = checker.check(*reachabilityRewardFormula); + formula = parser.parseFromString("R=? [F \"elected\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.044879046, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision()); @@ -135,6 +136,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> dtmc; + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + { matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); matrixBuilder.addNextValue(0, 1, 1.); @@ -149,10 +153,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -174,10 +177,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -199,10 +201,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -215,6 +216,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> mdp; + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + { matrixBuilder = storm::storage::SparseMatrixBuilder(15, 15, 20, true); matrixBuilder.addNextValue(0, 1, 1); @@ -260,10 +264,9 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp index d607551fc..5b4a12ba7 100644 --- a/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridCtmcCslModelCheckerTest.cpp @@ -18,6 +18,8 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(GmmxxHybridCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); diff --git a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp index 5cc56d0ed..9cd259aa3 100644 --- a/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridDtmcPrctlModelCheckerTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" @@ -15,9 +16,14 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; @@ -36,40 +42,36 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("one"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("two"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"two\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"three\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - auto done = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(done); + formula = parser.parseFromString("R=? [F \"done\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); @@ -80,6 +82,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Die) { TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); @@ -90,30 +95,27 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("observe0Greater1"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.3328800375801578281, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeIGreater1"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.1522194965, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.1522194965, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); @@ -124,6 +126,9 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, Crowds) { TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; @@ -142,31 +147,27 @@ TEST(GmmxxHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::GmmxxLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 20); + formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); - result = checker.check(*boundedUntilFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("R=? [F \"elected\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp index 31ab04a6b..9cffdba66 100644 --- a/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxHybridMdpPrctlModelCheckerTest.cpp @@ -14,8 +14,9 @@ #include "src/models/symbolic/StandardRewardModel.h" #include "src/settings/SettingsManager.h" +#include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" - +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" TEST(GmmxxHybridMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 73541f562..a79be23f1 100644 --- a/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -11,6 +11,8 @@ #include "src/settings/modules/GeneralSettings.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/parser/AutoParser.h" TEST(GmmxxMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp index 96c6075b0..6e74645cb 100644 --- a/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeCtmcCslModelCheckerTest.cpp @@ -10,8 +10,8 @@ #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" - #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/modules/GeneralSettings.h" diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index c9730e795..400e3c8a8 100644 --- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/parser/FormulaParser.h" #include "src/settings/SettingMemento.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" @@ -10,12 +11,17 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/parser/AutoParser.h" TEST(SparseDtmcPrctlModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); std::shared_ptr> dtmc = abstractModel->as>(); @@ -25,34 +31,30 @@ TEST(SparseDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("one"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("two"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"two\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"three\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - auto done = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(done); + formula = parser.parseFromString("R=? [F \"done\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(3.6666650772094727, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -63,6 +65,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) { ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(8607ull, dtmc->getNumberOfStates()); @@ -70,26 +75,23 @@ TEST(SparseDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("observe0Greater1"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.33288205191646525, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeIGreater1"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.15222066094730619, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.32153900158185761, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -99,6 +101,10 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); + + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> dtmc = abstractModel->as>(); ASSERT_EQ(12400ull, dtmc->getNumberOfStates()); @@ -106,27 +112,23 @@ TEST(SparseDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 20); + formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); - result = checker.check(*boundedUntilFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.9999965911265462636, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("R=? [F \"elected\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0448979589010925, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -136,6 +138,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> dtmc; + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + { matrixBuilder = storm::storage::SparseMatrixBuilder(2, 2, 2); matrixBuilder.addNextValue(0, 1, 1.); @@ -150,10 +155,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(labelFormula); - - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -175,10 +179,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(labelFormula); - - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -200,10 +203,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(labelFormula); - - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); @@ -216,6 +218,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) { storm::storage::SparseMatrixBuilder matrixBuilder; std::shared_ptr> mdp; + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + { matrixBuilder = storm::storage::SparseMatrixBuilder(15, 15, 20, true); matrixBuilder.addNextValue(0, 1, 1); @@ -261,10 +266,9 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) { storm::modelchecker::SparseDtmcPrctlModelChecker> checker(*mdp, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory(storm::solver::NativeLinearEquationSolver::SolutionMethod::SOR, 0.9))); - auto labelFormula = std::make_shared("a"); - auto lraFormula = std::make_shared(labelFormula); - - std::unique_ptr result = std::move(checker.check(*lraFormula)); + std::shared_ptr formula = parser.parseFromString("LRA=? [\"a\"]"); + + std::unique_ptr result = std::move(checker.check(*formula)); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp index 13792718d..57b557d4e 100644 --- a/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridCtmcCslModelCheckerTest.cpp @@ -17,6 +17,8 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(NativeHybridCtmcCslModelCheckerTest, Cluster) { // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed. std::unique_ptr enablePrismCompatibility = storm::settings::mutableGeneralSettings().overridePrismCompatibilityMode(true); diff --git a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp index 688fa8a16..2262f10c9 100644 --- a/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridDtmcPrctlModelCheckerTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" #include "src/modelchecker/prctl/HybridDtmcPrctlModelChecker.h" @@ -16,9 +17,14 @@ #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; @@ -37,40 +43,36 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("one"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("two"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"two\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"three\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - auto done = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(done); + formula = parser.parseFromString("R=? [F \"done\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult4 = result->asHybridQuantitativeCheckResult(); @@ -81,6 +83,9 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Die) { TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); @@ -91,30 +96,27 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("observe0Greater1"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult1 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.33288205191646525, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeIGreater1"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.15222066094730619, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); @@ -125,6 +127,9 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, Crowds) { TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; @@ -143,31 +148,27 @@ TEST(NativeHybridDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::HybridDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::NativeLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 20); + formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); - result = checker.check(*boundedUntilFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult2 = result->asHybridQuantitativeCheckResult(); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::gmmxxEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("R=? [F \"elected\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::HybridQuantitativeCheckResult& quantitativeResult3 = result->asHybridQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp index 47508830e..50008a237 100644 --- a/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeHybridMdpPrctlModelCheckerTest.cpp @@ -16,6 +16,8 @@ #include "src/settings/modules/GeneralSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + TEST(NativeHybridMdpPrctlModelCheckerTest, Dice) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm"); diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index e4123495a..e47eaeeeb 100644 --- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -10,6 +10,8 @@ #include "src/settings/SettingsManager.h" #include "src/settings/modules/GeneralSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/parser/AutoParser.h" TEST(SparseMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp index d660862ec..b8647c7d4 100644 --- a/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp +++ b/test/functional/modelchecker/SparseDtmcEliminationModelCheckerTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/models/sparse/StandardRewardModel.h" #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" @@ -14,6 +15,9 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/die/die.tra", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/die/die.coin_flips.trans.rew"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); std::shared_ptr> dtmc = abstractModel->as>(); @@ -23,34 +27,30 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); - auto labelFormula = std::make_shared("one"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision()); - labelFormula = std::make_shared("two"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"two\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2[0], storm::settings::generalSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"three\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3[0], storm::settings::generalSettings().getPrecision()); - auto done = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(done); + formula = parser.parseFromString("R=? [F \"done\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(11.0/3.0, quantitativeResult4[0], storm::settings::generalSettings().getPrecision()); @@ -59,6 +59,9 @@ TEST(SparseDtmcEliminationModelCheckerTest, Die) { TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", ""); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); std::shared_ptr> dtmc = abstractModel->as>(); @@ -68,50 +71,37 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); - auto labelFormula = std::make_shared("observe0Greater1"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.3328800375801578281, quantitativeResult1[0], storm::settings::generalSettings().getPrecision()); - labelFormula = std::make_shared("observeIGreater1"); - eventuallyFormula = std::make_shared(labelFormula); - - result = checker.check(*eventuallyFormula); + formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult2 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.1522194965, quantitativeResult2[0], storm::settings::generalSettings().getPrecision()); - labelFormula = std::make_shared("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared(labelFormula); - - result = checker.check(*eventuallyFormula); + formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); + + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.32153724292835045, quantitativeResult3[0], storm::settings::generalSettings().getPrecision()); - labelFormula = std::make_shared("observe0Greater1"); - eventuallyFormula = std::make_shared(labelFormula); - - auto labelFormula2 = std::make_shared("observeIGreater1"); - auto eventuallyFormula2 = std::make_shared(labelFormula2); - auto conditionalFormula = std::make_shared(eventuallyFormula, eventuallyFormula2); + formula = parser.parseFromString("P=? [F \"observe0Greater1\" || F \"observeIGreater1\"]"); - result = checker.check(*conditionalFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult4 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.15330064292476167, quantitativeResult4[0], storm::settings::generalSettings().getPrecision()); - labelFormula = std::make_shared("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\" || F \"observe0Greater1\"]"); - labelFormula2 = std::make_shared("observe0Greater1"); - eventuallyFormula2 = std::make_shared(labelFormula2); - conditionalFormula = std::make_shared(eventuallyFormula, eventuallyFormula2); - - result = checker.check(*conditionalFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult5 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(0.96592521978041668, quantitativeResult5[0], storm::settings::generalSettings().getPrecision()); @@ -120,6 +110,9 @@ TEST(SparseDtmcEliminationModelCheckerTest, Crowds) { TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { std::shared_ptr> abstractModel = storm::parser::AutoParser::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.tra", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.lab", "", STORM_CPP_BASE_PATH "/examples/dtmc/synchronous_leader/leader4_8.pick.trans.rew"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + ASSERT_EQ(abstractModel->getType(), storm::models::ModelType::Dtmc); std::shared_ptr> dtmc = abstractModel->as>(); @@ -128,18 +121,16 @@ TEST(SparseDtmcEliminationModelCheckerTest, SynchronousLeader) { storm::modelchecker::SparseDtmcEliminationModelChecker> checker(*dtmc); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult1 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::generalSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("R=? [F \"elected\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); storm::modelchecker::ExplicitQuantitativeCheckResult& quantitativeResult3 = result->asExplicitQuantitativeCheckResult(); EXPECT_NEAR(1.0448979, quantitativeResult3[0], storm::settings::generalSettings().getPrecision()); diff --git a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp index 1b1071a58..82d91fd76 100644 --- a/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicDtmcPrctlModelCheckerTest.cpp @@ -1,6 +1,7 @@ #include "gtest/gtest.h" #include "storm-config.h" +#include "src/parser/FormulaParser.h" #include "src/logic/Formulas.h" #include "src/utility/solver.h" #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h" @@ -12,11 +13,16 @@ #include "src/models/symbolic/Dtmc.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + #include "src/settings/modules/GeneralSettings.h" TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; @@ -35,40 +41,36 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("one"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"one\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("two"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"two\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("three"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"three\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0/6.0, quantitativeResult3.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - auto done = std::make_shared("done"); - auto reachabilityRewardFormula = std::make_shared(done); + formula = parser.parseFromString("R=? [F \"done\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult4 = result->asSymbolicQuantitativeCheckResult(); @@ -79,6 +81,9 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Die) { TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + std::shared_ptr> model = storm::builder::DdPrismModelBuilder::translateProgram(program); EXPECT_EQ(8607ul, model->getNumberOfStates()); EXPECT_EQ(15113ul, model->getNumberOfTransitions()); @@ -89,30 +94,27 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("observe0Greater1"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"observe0Greater1\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.33288236360191303, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeIGreater1"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeIGreater1\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.15222081144084315, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("observeOnlyTrueSender"); - eventuallyFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("P=? [F \"observeOnlyTrueSender\"]"); - result = checker.check(*eventuallyFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); @@ -123,6 +125,9 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, Crowds) { TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm"); + // A parser that we use for conveniently constructing the formulas. + storm::parser::FormulaParser parser; + // Build the die model with its reward model. #ifdef WINDOWS storm::builder::DdPrismModelBuilder::Options options; @@ -141,31 +146,27 @@ TEST(SymbolicDtmcPrctlModelCheckerTest, SynchronousLeader) { storm::modelchecker::SymbolicDtmcPrctlModelChecker checker(*dtmc, std::unique_ptr>(new storm::utility::solver::SymbolicLinearEquationSolverFactory())); - auto labelFormula = std::make_shared("elected"); - auto eventuallyFormula = std::make_shared(labelFormula); + std::shared_ptr formula = parser.parseFromString("P=? [F \"elected\"]"); - std::unique_ptr result = checker.check(*eventuallyFormula); + std::unique_ptr result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult1 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(1.0, quantitativeResult1.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(1.0, quantitativeResult1.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto trueFormula = std::make_shared(true); - auto boundedUntilFormula = std::make_shared(trueFormula, labelFormula, 20); + formula = parser.parseFromString("P=? [F<=20 \"elected\"]"); - result = checker.check(*boundedUntilFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult2 = result->asSymbolicQuantitativeCheckResult(); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMin(), storm::settings::nativeEquationSolverSettings().getPrecision()); EXPECT_NEAR(0.99999989760000074, quantitativeResult2.getMax(), storm::settings::nativeEquationSolverSettings().getPrecision()); - labelFormula = std::make_shared("elected"); - auto reachabilityRewardFormula = std::make_shared(labelFormula); + formula = parser.parseFromString("R=? [F \"elected\"]"); - result = checker.check(*reachabilityRewardFormula); + result = checker.check(*formula); result->filter(storm::modelchecker::SymbolicQualitativeCheckResult(model->getReachableStates(), model->getInitialStates())); storm::modelchecker::SymbolicQuantitativeCheckResult& quantitativeResult3 = result->asSymbolicQuantitativeCheckResult(); diff --git a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp index 0642e19d2..c4a226214 100644 --- a/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp +++ b/test/functional/modelchecker/SymbolicMdpPrctlModelCheckerTest.cpp @@ -13,6 +13,8 @@ #include "src/models/symbolic/StandardRewardModel.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" + #include "src/settings/modules/GeneralSettings.h" TEST(SymbolicMdpPrctlModelCheckerTest, Dice) { diff --git a/test/functional/solver/FullySymbolicGameSolverTest.cpp b/test/functional/solver/FullySymbolicGameSolverTest.cpp index d2ea6db1c..ce9e21798 100644 --- a/test/functional/solver/FullySymbolicGameSolverTest.cpp +++ b/test/functional/solver/FullySymbolicGameSolverTest.cpp @@ -7,6 +7,7 @@ #include "src/utility/solver.h" #include "src/settings/SettingsManager.h" +#include "src/solver/SymbolicGameSolver.h" #include "src/settings/modules/NativeEquationSolverSettings.h" diff --git a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp index 5b4174e51..6c659e7b7 100644 --- a/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/GmmxxMinMaxLinearEquationSolverTest.cpp @@ -78,7 +78,7 @@ TEST(GmmxxMinMaxLinearEquationSolver, SolveWithPolicyIteration) { std::vector b = { 0.099, 0.5 }; storm::settings::modules::GmmxxEquationSolverSettings const& settings = storm::settings::gmmxxEquationSolverSettings(); - storm::solver::GmmxxMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), false, settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative); + storm::solver::GmmxxMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), storm::solver::MinMaxTechniqueSelection::PolicyIteration, settings.getConvergenceCriterion() == storm::settings::modules::GmmxxEquationSolverSettings::ConvergenceCriterion::Relative); ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::gmmxxEquationSolverSettings().getPrecision()); diff --git a/test/functional/solver/MinMaxTechniqueSelectionTest.cpp b/test/functional/solver/MinMaxTechniqueSelectionTest.cpp new file mode 100644 index 000000000..78cc8696e --- /dev/null +++ b/test/functional/solver/MinMaxTechniqueSelectionTest.cpp @@ -0,0 +1,11 @@ +#include "gtest/gtest.h" + +#include "src/solver/MinMaxLinearEquationSolver.h" + +TEST( MinMaxTechnique, Simple ) { + storm::solver::MinMaxTechniqueSelection ts = storm::solver::MinMaxTechniqueSelection::PolicyIteration; + storm::solver::MinMaxTechnique t = storm::solver::MinMaxTechnique::PolicyIteration; + ASSERT_EQ(convert(ts), t); + + +} \ No newline at end of file diff --git a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp index bb7c281c9..b83423ffe 100644 --- a/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp +++ b/test/functional/solver/NativeMinMaxLinearEquationSolverTest.cpp @@ -79,7 +79,7 @@ TEST(NativeMinMaxLinearEquationSolver, SolveWithPolicyIteration) { std::vector b = { 0.099, 0.5 }; storm::settings::modules::NativeEquationSolverSettings const& settings = storm::settings::nativeEquationSolverSettings(); - storm::solver::NativeMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), false, settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative); + storm::solver::NativeMinMaxLinearEquationSolver solver(A, settings.getPrecision(), settings.getMaximalIterationCount(), storm::solver::MinMaxTechniqueSelection::PolicyIteration, settings.getConvergenceCriterion() == storm::settings::modules::NativeEquationSolverSettings::ConvergenceCriterion::Relative); ASSERT_NO_THROW(solver.solveEquationSystem(true, x, b)); ASSERT_LT(std::abs(x[0] - 0.5), storm::settings::nativeEquationSolverSettings().getPrecision()); diff --git a/test/functional/storage/BitVectorTest.cpp b/test/functional/storage/BitVectorTest.cpp index 408c286c9..db92724fe 100644 --- a/test/functional/storage/BitVectorTest.cpp +++ b/test/functional/storage/BitVectorTest.cpp @@ -39,6 +39,21 @@ TEST(BitVectorTest, InitFromIterator) { } } +TEST(BitVectorTest, InitFromIntVector) { + std::vector valueVector = {0, 4, 10}; + storm::storage::BitVector vector(32, valueVector); + + ASSERT_EQ(32ul, vector.size()); + + for (uint_fast64_t i = 0; i < 32; ++i) { + if (i == 0 || i == 4 || i == 10) { + ASSERT_TRUE(vector.get(i)); + } else { + ASSERT_FALSE(vector.get(i)); + } + } +} + TEST(BitVectorTest, GetSet) { storm::storage::BitVector vector(32); diff --git a/test/functional/utility/VectorTest.cpp b/test/functional/utility/VectorTest.cpp new file mode 100644 index 000000000..33f3c5cfe --- /dev/null +++ b/test/functional/utility/VectorTest.cpp @@ -0,0 +1,14 @@ +#include "gtest/gtest.h" +#include "storm-config.h" +#include "src/storage/BitVector.h" +#include "src/utility/vector.h" + +TEST(VectorTest, sum_if) { + std::vector a = {1.0, 2.0, 4.0, 8.0, 16.0}; + storm::storage::BitVector f1(5, {2,4}); + storm::storage::BitVector f2(5, {3,4}); + + ASSERT_EQ(20.0, storm::utility::vector::sum_if(a, f1)); + ASSERT_EQ(24.0, storm::utility::vector::sum_if(a, f2)); + +} diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp index ea480bd22..0ecce639f 100644 --- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp @@ -2,6 +2,7 @@ #include "storm-config.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp index 1db6f796d..527dbed69 100644 --- a/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/GmmxxMdpPrctlModelCheckerTest.cpp @@ -2,6 +2,7 @@ #include "storm-config.h" #include "src/settings/SettingsManager.h" +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "src/utility/solver.h" diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp index bc0b5b563..cce9c8878 100644 --- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp @@ -2,6 +2,8 @@ #include "storm-config.h" #include "src/settings/SettingsManager.h" #include "src/settings/modules/GmmxxEquationSolverSettings.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/settings/SettingMemento.h" #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" diff --git a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp index 788f1fee6..e327910d8 100644 --- a/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp +++ b/test/performance/modelchecker/NativeMdpPrctlModelCheckerTest.cpp @@ -4,6 +4,8 @@ #include "src/settings/SettingsManager.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h" + +#include "src/settings/modules/NativeEquationSolverSettings.h" #include "src/utility/solver.h" #include "src/parser/AutoParser.h"