Added new settings and environment module for time-bounded settings.

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>;

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();
     }

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;
       

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;
+    }
+
+}

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;
+    };
+}
+

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>();

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();
+            }
+
+        }
+    }
+}

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;
+            };
+            
+        }
+    }
+}

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:

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)