diff --git a/src/storm/environment/SubEnvironment.cpp b/src/storm/environment/SubEnvironment.cpp
index c42e21c93..8e5a23e83 100644
--- a/src/storm/environment/SubEnvironment.cpp
+++ b/src/storm/environment/SubEnvironment.cpp
@@ -9,6 +9,7 @@
#include "storm/environment/solver/GmmxxSolverEnvironment.h"
#include "storm/environment/solver/NativeSolverEnvironment.h"
#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
+#include "storm/environment/solver/TimeBoundedSolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/environment/solver/MultiplierEnvironment.h"
#include "storm/environment/solver/GameSolverEnvironment.h"
@@ -65,6 +66,7 @@ namespace storm {
template class SubEnvironment<GmmxxSolverEnvironment>;
template class SubEnvironment<NativeSolverEnvironment>;
template class SubEnvironment<LongRunAverageSolverEnvironment>;
+ template class SubEnvironment<TimeBoundedSolverEnvironment>;
template class SubEnvironment<MinMaxSolverEnvironment>;
template class SubEnvironment<MultiplierEnvironment>;
template class SubEnvironment<GameSolverEnvironment>;
diff --git a/src/storm/environment/solver/SolverEnvironment.cpp b/src/storm/environment/solver/SolverEnvironment.cpp
index 07a02aca1..9825d926b 100644
--- a/src/storm/environment/solver/SolverEnvironment.cpp
+++ b/src/storm/environment/solver/SolverEnvironment.cpp
@@ -1,6 +1,7 @@
#include "storm/environment/solver/SolverEnvironment.h"
#include "storm/environment/solver/LongRunAverageSolverEnvironment.h"
+#include "storm/environment/solver/TimeBoundedSolverEnvironment.h"
#include "storm/environment/solver/MinMaxSolverEnvironment.h"
#include "storm/environment/solver/MultiplierEnvironment.h"
#include "storm/environment/solver/EigenSolverEnvironment.h"
@@ -38,6 +39,14 @@ namespace storm {
return longRunAverageSolverEnvironment.get();
}
+ TimeBoundedSolverEnvironment& SolverEnvironment::timeBounded() {
+ return timeBoundedSolverEnvironment.get();
+ }
+
+ TimeBoundedSolverEnvironment const& SolverEnvironment::timeBounded() const {
+ return timeBoundedSolverEnvironment.get();
+ }
+
MinMaxSolverEnvironment& SolverEnvironment::minMax() {
return minMaxSolverEnvironment.get();
}
diff --git a/src/storm/environment/solver/SolverEnvironment.h b/src/storm/environment/solver/SolverEnvironment.h
index 26ac33fea..4f0a88869 100644
--- a/src/storm/environment/solver/SolverEnvironment.h
+++ b/src/storm/environment/solver/SolverEnvironment.h
@@ -15,6 +15,7 @@ namespace storm {
class GmmxxSolverEnvironment;
class NativeSolverEnvironment;
class LongRunAverageSolverEnvironment;
+ class TimeBoundedSolverEnvironment;
class MinMaxSolverEnvironment;
class MultiplierEnvironment;
class GameSolverEnvironment;
@@ -34,6 +35,8 @@ namespace storm {
NativeSolverEnvironment const& native() const;
LongRunAverageSolverEnvironment& lra();
LongRunAverageSolverEnvironment const& lra() const;
+ TimeBoundedSolverEnvironment& timeBounded();
+ TimeBoundedSolverEnvironment const& timeBounded() const;
MinMaxSolverEnvironment& minMax();
MinMaxSolverEnvironment const& minMax() const;
MultiplierEnvironment& multiplier();
@@ -60,6 +63,7 @@ namespace storm {
SubEnvironment<GameSolverEnvironment> gameSolverEnvironment;
SubEnvironment<TopologicalSolverEnvironment> topologicalSolverEnvironment;
SubEnvironment<LongRunAverageSolverEnvironment> longRunAverageSolverEnvironment;
+ SubEnvironment<TimeBoundedSolverEnvironment> timeBoundedSolverEnvironment;
SubEnvironment<MinMaxSolverEnvironment> minMaxSolverEnvironment;
SubEnvironment<MultiplierEnvironment> multiplierEnvironment;
diff --git a/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp b/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp
new file mode 100644
index 000000000..743474e4b
--- /dev/null
+++ b/src/storm/environment/solver/TimeBoundedSolverEnvironment.cpp
@@ -0,0 +1,60 @@
+#include "storm/environment/solver/TimeBoundedSolverEnvironment.h"
+
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/TimeBoundedSolverSettings.h"
+#include "storm/utility/constants.h"
+#include "storm/utility/macros.h"
+
+namespace storm {
+
+ TimeBoundedSolverEnvironment::TimeBoundedSolverEnvironment() {
+ auto const& tbSettings = storm::settings::getModule<storm::settings::modules::TimeBoundedSolverSettings>();
+ maMethod = tbSettings.getMaMethod();
+ maMethodSetFromDefault = tbSettings.isMaMethodSetFromDefaultValue();
+ precision = storm::utility::convertNumber<storm::RationalNumber>(tbSettings.getPrecision());
+ relative = tbSettings.isRelativePrecision();
+ unifPlusKappa = tbSettings.getUnifPlusKappa();
+ }
+
+ TimeBoundedSolverEnvironment::~TimeBoundedSolverEnvironment() {
+ // Intentionally left empty
+ }
+
+ storm::solver::MaBoundedReachabilityMethod const& TimeBoundedSolverEnvironment::getMaMethod() const {
+ return maMethod;
+ }
+
+ bool const& TimeBoundedSolverEnvironment::isMaMethodSetFromDefault() const {
+ return maMethodSetFromDefault;
+ }
+
+ void TimeBoundedSolverEnvironment::setMaMethod(storm::solver::MaBoundedReachabilityMethod value, bool isSetFromDefault) {
+ maMethod = value;
+ maMethodSetFromDefault = isSetFromDefault;
+ }
+
+ storm::RationalNumber const& TimeBoundedSolverEnvironment::getPrecision() const {
+ return precision;
+ }
+
+ void TimeBoundedSolverEnvironment::setPrecision(storm::RationalNumber value) {
+ precision = value;
+ }
+
+ bool const& TimeBoundedSolverEnvironment::getRelativeTerminationCriterion() const {
+ return relative;
+ }
+
+ void TimeBoundedSolverEnvironment::setRelativeTerminationCriterion(bool value) {
+ relative = value;
+ }
+
+ storm::RationalNumber const& TimeBoundedSolverEnvironment::getUnifPlusKappa() const {
+ return unifPlusKappa;
+ }
+
+ void TimeBoundedSolverEnvironment::setUnifPlusKappa(storm::RationalNumber value) {
+ unifPlusKappa = value;
+ }
+
+}
diff --git a/src/storm/environment/solver/TimeBoundedSolverEnvironment.h b/src/storm/environment/solver/TimeBoundedSolverEnvironment.h
new file mode 100644
index 000000000..ddf1d8321
--- /dev/null
+++ b/src/storm/environment/solver/TimeBoundedSolverEnvironment.h
@@ -0,0 +1,36 @@
+#pragma once
+
+#include "storm/environment/solver/SolverEnvironment.h"
+#include "storm/solver/SolverSelectionOptions.h"
+
+namespace storm {
+
+ class TimeBoundedSolverEnvironment {
+ public:
+
+ TimeBoundedSolverEnvironment();
+ ~TimeBoundedSolverEnvironment();
+
+ storm::solver::MaBoundedReachabilityMethod const& getMaMethod() const;
+ bool const& isMaMethodSetFromDefault() const;
+ void setMaMethod(storm::solver::MaBoundedReachabilityMethod value, bool isSetFromDefault = false);
+
+ storm::RationalNumber const& getPrecision() const;
+ void setPrecision(storm::RationalNumber value);
+ bool const& getRelativeTerminationCriterion() const;
+ void setRelativeTerminationCriterion(bool value);
+
+ storm::RationalNumber const& getUnifPlusKappa() const;
+ void setUnifPlusKappa(storm::RationalNumber value);
+
+ private:
+ storm::solver::MaBoundedReachabilityMethod maMethod;
+ bool maMethodSetFromDefault;
+
+ storm::RationalNumber precision;
+ bool relative;
+
+ storm::RationalNumber unifPlusKappa;
+ };
+}
+
diff --git a/src/storm/settings/SettingsManager.cpp b/src/storm/settings/SettingsManager.cpp
index 8e278fecb..4824ce135 100644
--- a/src/storm/settings/SettingsManager.cpp
+++ b/src/storm/settings/SettingsManager.cpp
@@ -32,6 +32,7 @@
#include "storm/settings/modules/GurobiSettings.h"
#include "storm/settings/modules/Smt2SmtSolverSettings.h"
#include "storm/settings/modules/TopologicalEquationSolverSettings.h"
+#include "storm/settings/modules/TimeBoundedSolverSettings.h"
#include "storm/settings/modules/ExplorationSettings.h"
#include "storm/settings/modules/ResourceSettings.h"
#include "storm/settings/modules/AbstractionSettings.h"
@@ -657,6 +658,7 @@ namespace storm {
storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::EliminationSettings>();
storm::settings::addModule<storm::settings::modules::LongRunAverageSolverSettings>();
+ storm::settings::addModule<storm::settings::modules::TimeBoundedSolverSettings>();
storm::settings::addModule<storm::settings::modules::MinMaxEquationSolverSettings>();
storm::settings::addModule<storm::settings::modules::GameSolverSettings>();
storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
diff --git a/src/storm/settings/modules/TimeBoundedSolverSettings.cpp b/src/storm/settings/modules/TimeBoundedSolverSettings.cpp
new file mode 100644
index 000000000..88b323c8f
--- /dev/null
+++ b/src/storm/settings/modules/TimeBoundedSolverSettings.cpp
@@ -0,0 +1,62 @@
+#include "storm/settings/modules/TimeBoundedSolverSettings.h"
+
+#include "storm/settings/Option.h"
+#include "storm/settings/ArgumentBuilder.h"
+#include "storm/settings/OptionBuilder.h"
+
+#include "storm/utility/macros.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ const std::string TimeBoundedSolverSettings::moduleName = "timebounded";
+
+ const std::string TimeBoundedSolverSettings::maMethodOptionName = "mamethod";
+ const std::string TimeBoundedSolverSettings::precisionOptionName = "precision";
+ const std::string TimeBoundedSolverSettings::absoluteOptionName = "absolute";
+ const std::string TimeBoundedSolverSettings::unifPlusKappaOptionName = "kappa";
+
+ TimeBoundedSolverSettings::TimeBoundedSolverSettings() : ModuleSettings(moduleName) {
+ std::vector<std::string> maMethods = {"imca", "unifplus"};
+ this->addOption(storm::settings::OptionBuilder(moduleName, maMethodOptionName, false, "The method to use to solve bounded reachability queries on MAs.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the method to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(maMethods)).setDefaultValueString("unifplus").build()).build());
+
+ this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The precision used for detecting convergence of iterative methods.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to achieve.").setDefaultValueDouble(1e-06).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+
+ this->addOption(storm::settings::OptionBuilder(moduleName, absoluteOptionName, false, "Sets whether the relative or the absolute error is considered for detecting convergence.").setIsAdvanced().build());
+
+ this->addOption(storm::settings::OptionBuilder(moduleName, unifPlusKappaOptionName, false, "The truncation factor used in unifPlus.").setIsAdvanced().addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("kappa", "The factor").setDefaultValueDouble(0.1).addValidatorDouble(ArgumentValidatorFactory::createDoubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+
+ }
+
+ bool TimeBoundedSolverSettings::isPrecisionSet() const {
+ return this->getOption(precisionOptionName).getHasOptionBeenSet();
+ }
+
+ double TimeBoundedSolverSettings::getPrecision() const {
+ return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+ }
+
+ bool TimeBoundedSolverSettings::isRelativePrecision() const {
+ return !this->getOption(absoluteOptionName).getHasOptionBeenSet();
+ }
+
+ storm::solver::MaBoundedReachabilityMethod TimeBoundedSolverSettings::getMaMethod() const {
+ std::string techniqueAsString = this->getOption(maMethodOptionName).getArgumentByName("name").getValueAsString();
+ if (techniqueAsString == "imca") {
+ return storm::solver::MaBoundedReachabilityMethod::Imca;
+ }
+ return storm::solver::MaBoundedReachabilityMethod::UnifPlus;
+ }
+
+ bool TimeBoundedSolverSettings::isMaMethodSetFromDefaultValue() const {
+ return !this->getOption(maMethodOptionName).getArgumentByName("name").getHasBeenSet() || this->getOption(maMethodOptionName).getArgumentByName("name").wasSetFromDefaultValue();
+ }
+
+ double TimeBoundedSolverSettings::getUnifPlusKappa() const {
+ return this->getOption(unifPlusKappaOptionName).getArgumentByName("kappa").getValueAsDouble();
+ }
+
+ }
+ }
+}
diff --git a/src/storm/settings/modules/TimeBoundedSolverSettings.h b/src/storm/settings/modules/TimeBoundedSolverSettings.h
new file mode 100644
index 000000000..8140da9ce
--- /dev/null
+++ b/src/storm/settings/modules/TimeBoundedSolverSettings.h
@@ -0,0 +1,66 @@
+#pragma once
+
+#include "storm-config.h"
+#include "storm/settings/modules/ModuleSettings.h"
+
+#include "storm/solver/SolverSelectionOptions.h"
+
+namespace storm {
+ namespace settings {
+ namespace modules {
+
+ /*!
+ * This class represents the min/max solver settings.
+ */
+ class TimeBoundedSolverSettings : public ModuleSettings {
+ public:
+
+ TimeBoundedSolverSettings();
+
+ /*!
+ * Retrieves whether solving technique for time bounded reachability on Markov Automata has been set from its default value.
+ */
+ bool isMaMethodSetFromDefaultValue() const;
+
+ /*!
+ * Retrieves the selected solving technique for time bounded reachability on Markov Automata.
+ */
+ storm::solver::MaBoundedReachabilityMethod getMaMethod() const;
+
+ /*!
+ * Retrieves whether the precision has been set.
+ *
+ * @return True iff the precision has been set.
+ */
+ bool isPrecisionSet() const;
+
+ /*!
+ * Retrieves the precision that is used for detecting convergence.
+ *
+ * @return The precision to use for detecting convergence.
+ */
+ double getPrecision() const;
+
+ /*!
+ * Retrieves whether the convergence criterion has been set to relative or absolute.
+ */
+ bool isRelativePrecision() const;
+
+ /*!
+ * Retrieves the truncation factor used for unifPlus
+ */
+ double getUnifPlusKappa() const;
+
+ // The name of the module.
+ static const std::string moduleName;
+
+ private:
+ static const std::string maMethodOptionName;
+ static const std::string precisionOptionName;
+ static const std::string absoluteOptionName;
+ static const std::string unifPlusKappaOptionName;
+ };
+
+ }
+ }
+}
diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp
index f635b5a38..2b913c2ae 100644
--- a/src/storm/solver/SolverSelectionOptions.cpp
+++ b/src/storm/solver/SolverSelectionOptions.cpp
@@ -60,6 +60,16 @@ namespace storm {
return "invalid";
}
+ std::string toString(MaBoundedReachabilityMethod m) {
+ switch(m) {
+ case MaBoundedReachabilityMethod::Imca:
+ return "imca";
+ case MaBoundedReachabilityMethod::UnifPlus:
+ return "unifplus";
+ }
+ return "invalid";
+ }
+
std::string toString(LpSolverType t) {
switch(t) {
case LpSolverType::Gurobi:
diff --git a/src/storm/solver/SolverSelectionOptions.h b/src/storm/solver/SolverSelectionOptions.h
index d21262099..e6d38274b 100644
--- a/src/storm/solver/SolverSelectionOptions.h
+++ b/src/storm/solver/SolverSelectionOptions.h
@@ -10,6 +10,7 @@ namespace storm {
ExtendEnumsWithSelectionField(MultiplierType, Native, Gmmxx)
ExtendEnumsWithSelectionField(GameMethod, PolicyIteration, ValueIteration)
ExtendEnumsWithSelectionField(LraMethod, LinearProgramming, ValueIteration, GainBiasEquations, LraDistributionEquations)
+ ExtendEnumsWithSelectionField(MaBoundedReachabilityMethod, Imca, UnifPlus)
ExtendEnumsWithSelectionField(LpSolverType, Gurobi, Glpk, Z3)
ExtendEnumsWithSelectionField(EquationSolverType, Native, Gmmxx, Eigen, Elimination, Topological)