no hardcoded regions anymore

Former-commit-id: ca137c1f6b

src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp

@@ -30,7 +30,7 @@ namespace storm {
         
         
         template<typename ParametricType, typename ConstantType>
-        SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, BoundType> lowerBounds, std::map<VariableType, BoundType> upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds) {
+        SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::ParameterRegion(std::map<VariableType, BoundType> lowerBounds, std::map<VariableType, BoundType> upperBounds) : lowerBounds(lowerBounds), upperBounds(upperBounds), checkResult(RegionCheckResult::UNKNOWN) {
             // Intentionally left empty.
             //todo: check whether both mappings map the same variables
         }
@@ -96,41 +96,31 @@ namespace storm {
         }
         
         template<typename ParametricType, typename ConstantType>
-        //Todo adapt
         bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::canHandle(storm::logic::Formula const& formula) const {
-            if (formula.isProbabilityOperatorFormula()) {
-                storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
-                return this->canHandle(probabilityOperatorFormula.getSubformula());
-            } else if (formula.isRewardOperatorFormula()) {
-                storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
-                return this->canHandle(rewardOperatorFormula.getSubformula());
-            } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) {
-                if (formula.isUntilFormula()) {
-                    storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula();
-                    if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) {
-                        return true;
-                    }
-                } else if (formula.isEventuallyFormula()) {
-                    storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula();
-                    if (eventuallyFormula.getSubformula().isPropositionalFormula()) {
-                        return true;
-                    }
-                }
-            } else if (formula.isReachabilityRewardFormula()) {
-                storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula();
-                if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) {
-                    return true;
-                }
-            } else if (formula.isConditionalPathFormula()) {
-                storm::logic::ConditionalPathFormula conditionalPathFormula = formula.asConditionalPathFormula();
-                if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) {
-                    return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula());
-                }
-            } else if (formula.isPropositionalFormula()) {
-                return true;
+             //for simplicity we only support state formulas with eventually (e.g. P<0.5 [ F "target" ])
+            if(!formula.isStateFormula()){
+                STORM_LOG_DEBUG("Region Model Checker could not handle formula " << formula << " Reason: expected a stateFormula");
+                return false;
+            }
+            if(!formula.asStateFormula().isProbabilityOperatorFormula()){
+                STORM_LOG_DEBUG("Region Model Checker could not handle formula " << formula << " Reason: expected a probabilityOperatorFormula");
+                return false;
             }
-            return false;
+            storm::logic::ProbabilityOperatorFormula const& probOpForm=formula.asStateFormula().asProbabilityOperatorFormula();
+            if(!probOpForm.hasBound()){
+                STORM_LOG_DEBUG("Region Model Checker could not handle formula " << formula << " Reason: The formula has no bound");
+                return false;
+            }
+            if(!probOpForm.getSubformula().asPathFormula().isEventuallyFormula()){
+                STORM_LOG_DEBUG("Region Model Checker could not handle formula " << formula << " Reason: expected an eventually subformula");
+                return false;
+            }
+            return true;
         }
+            
+            
+            
+            
         
         template<>
         std::pair<storm::storage::SparseMatrix<double>,std::vector<boost::container::flat_set<uint_fast64_t>>> SparseDtmcRegionModelChecker<storm::RationalFunction, double>::instantiateFlexibleMatrix(FlexibleMatrix const& matrix, std::vector<std::map<storm::Variable, storm::RationalFunction::CoeffType>> const& substitutions, storm::storage::BitVector const& filter, bool addSinkState, std::vector<storm::RationalFunction> const& oneStepProbabilities, bool addSelfLoops) const {

src/modelchecker/reachability/SparseDtmcRegionModelChecker.h

@@ -22,6 +22,8 @@ namespace storm {
             typedef typename std::conditional<(std::is_same<ParametricType,storm::RationalFunction>::value), storm::Variable,std::nullptr_t>::type VariableType;
             typedef typename std::conditional<(std::is_same<ParametricType,storm::RationalFunction>::value), storm::RationalFunction::CoeffType,std::nullptr_t>::type BoundType;
             
+            enum class RegionCheckResult { UNKNOWN, ALLSAT, ALLUNSAT, INCONCLUSIVE};
+            
             class ParameterRegion{
             public:
                 
@@ -44,6 +46,7 @@ namespace storm {
                 
                 std::map<VariableType, BoundType> const lowerBounds;
                 std::map<VariableType, BoundType> const upperBounds;
+                RegionCheckResult checkResult;
                 
             };
             
@@ -53,7 +56,7 @@ namespace storm {
 
             /*!
              * Checks whether the given formula holds for all possible parameters that satisfy the given parameter regions
-             * ParameterRegions should contain all parameters (not mentioned parameters are assumed to be arbitrary reals)
+             * ParameterRegions should contain all parameters.
              */
             bool checkRegion(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions);
         private:

src/parser/MappedFile.h

@@ -51,7 +51,7 @@ namespace storm {
 
 			/*!
 			 * Tests whether the given file exists and is readable.
-			 *
+			 *qi
 			 * @param filename Path and name of the file to be tested.
 			 * @return True iff the file exists and is readable.
 			 */

src/settings/SettingsManager.cpp

@@ -30,6 +30,7 @@ namespace storm {
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::Smt2SmtSolverSettings(*this)));
 			this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::TopologicalValueIterationEquationSolverSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::ParametricSettings(*this)));
+            this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::RegionSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::SparseDtmcEliminationModelCheckerSettings(*this)));
         }
         
@@ -523,6 +524,10 @@ namespace storm {
         storm::settings::modules::ParametricSettings const& parametricSettings() {
             return dynamic_cast<storm::settings::modules::ParametricSettings const&>(manager().getModule(storm::settings::modules::ParametricSettings::moduleName));
         }
+        
+        storm::settings::modules::RegionSettings const& regionSettings() {
+            return dynamic_cast<storm::settings::modules::RegionSettings const&>(manager().getModule(storm::settings::modules::RegionSettings::moduleName));
+        }
 
         storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings() {
             return dynamic_cast<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const&>(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName));

src/settings/SettingsManager.h

@@ -30,6 +30,7 @@
 #include "src/settings/modules/GurobiSettings.h"
 #include "src/settings/modules/Smt2SmtSolverSettings.h"
 #include "src/settings/modules/ParametricSettings.h"
+#include "src/settings/modules/RegionSettings.h"
 #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
 #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
 
@@ -333,6 +334,13 @@ namespace storm {
          * @return An object that allows accessing the settings for parameteric model checking.
          */
         storm::settings::modules::ParametricSettings const& parametricSettings();
+        
+        /*!
+         * Retrieves the settings for parametric region model checking.
+         *
+         * @return An object that allows accessing the settings for parametric region model checking.
+         */
+        storm::settings::modules::RegionSettings const& regionSettings();
 
         /* Retrieves the settings of the elimination-based DTMC model checker.
          *

src/settings/modules/RegionSettings.cpp

@@ -0,0 +1,50 @@
+#include "src/settings/modules/RegionSettings.h"
+
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string RegionSettings::moduleName = "region";
+            const std::string RegionSettings::regionfileOptionName = "regionfile";
+            const std::string RegionSettings::regionsOptionName = "regions";
+            
+            RegionSettings::RegionSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, regionfileOptionName, true, "Specifies the regions via a file. Format: 0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file from which to read the regions.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, regionsOptionName, true, "Specifies the regions via command line. Format: '0.3<=p<=0.4,0.2<=q<=0.5; 0.6<=p<=0.7,0.8<=q<=0.9'")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("regions", "The considered regions.").build()).build());
+            }
+            
+           
+            
+            bool RegionSettings::isRegionFileSet() const{
+                return this->getOption(regionfileOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string RegionSettings::getRegionFilePath() const{
+                return this->getOption(regionfileOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool RegionSettings::isRegionsSet() const{
+                return this->getOption(regionsOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string RegionSettings::getRegionsFromCmdLine() const{
+                return this->getOption(regionsOptionName).getArgumentByName("regions").getValueAsString();
+            }
+            
+            bool RegionSettings::check() const{
+                if(isRegionsSet() && isRegionFileSet()){
+                    STORM_LOG_ERROR("Regions specified twice: via command line AND via file.");
+                    return false;
+                }
+                return true;
+            }
+            
+            
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm

src/settings/modules/RegionSettings.h

@@ -0,0 +1,64 @@
+#ifndef STORM_SETTINGS_MODULES_REGIONSETTINGS_H_
+#define STORM_SETTINGS_MODULES_REGIONSETTINGS_H_
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+
+            /*!
+             * This class represents the settings for parametric region model checking.
+             */
+            class RegionSettings : public ModuleSettings {
+            public:
+                /**
+                 * A type for saving the Solving Strategy.
+                 * 
+                 */
+                //enum class SolvingStrategy { ... };
+
+                /*!
+                 * Creates a new set of parametric region model checking settings that is managed by the given manager.
+                 *
+                 * @param settingsManager The responsible manager.
+                 */
+                RegionSettings(storm::settings::SettingsManager& settingsManager);
+
+                /*!
+                 * Retrieves whether the regions are specified in a file.
+                 * @return  True iff the regions are specified in a file.
+                 */
+                bool isRegionFileSet() const;
+                
+                /*!
+                 * Returns the file in which the regions are specified.
+                 */
+                std::string getRegionFilePath() const;
+
+                /*!
+                 * Retrieves whether the regions are specified as cmd line parameter
+                 * @return  True iff the regions are specified as cmd line parameter
+                 */
+                bool isRegionsSet() const;
+                
+                /*!
+                 * Returns the regions that are specified as cmd line parameter
+                 */
+                std::string getRegionsFromCmdLine() const;
+
+                
+                bool check() const override;
+
+                const static std::string moduleName;
+
+            private:
+                const static std::string regionfileOptionName;
+                const static std::string regionsOptionName;
+            };
+
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_REGIONSETTINGS_H_ */

src/utility/cli.h

@@ -473,16 +473,13 @@ namespace storm {
                 STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs.");
                 std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
                 
-                std::cout << std::endl << "Model checking property: " << *formula << " ...";
-                //do we want to check for a parameter region?
                 if(settings.isParametricRegionSet()){
-                    std::cout << std::endl;
-                    //experimental implementation! check some hardcoded region
+                    std::cout << std::endl << "Model checking property: " << *formula << " for all parameters in the given regions." << std::endl;
                     
-                    std::vector<storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction,double>::ParameterRegion> regions=storm::utility::regions::RegionParser<storm::RationalFunction, double>::parseMultipleRegions("0.78<=pL<=0.82,0.78<=pK<=0.82; 0.3<=pL<=0.5,0.1<=pK<=0.7;0.6<=pL<=0.7,0.8<=pK<=0.9");                    
+                    auto regions=storm::utility::regions::RegionParser<storm::RationalFunction, double>::getRegionsFromSettings();                    
                     
                     storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
-                    bool result = modelchecker.checkRegion(*formula.get(), regions);
+                    auto result = modelchecker.checkRegion(*formula.get(), regions);
                     std::cout << "... done." << std::endl;
                     if (result){
                     std::cout << "the property holds for all parameters in the given region" << std::endl;
@@ -490,9 +487,9 @@ namespace storm {
                     std::cout << "the property does NOT hold for all parameters in the given region" << std::endl;
                     }
                     
-                    
                 }else{
-                    //just obtain the resulting rational function
+                    // obtain the resulting rational function
+                    std::cout << std::endl << "Model checking property: " << *formula << " ...";
                     std::unique_ptr<storm::modelchecker::CheckResult> result;
 
                     storm::modelchecker::SparseDtmcEliminationModelChecker<storm::RationalFunction> modelchecker(*dtmc);

src/utility/regions.cpp

@@ -11,6 +11,8 @@
 #include "src/exceptions/NotImplementedException.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "adapters/CarlAdapter.h"
+#include "exceptions/InvalidSettingsException.h"
+#include "parser/MappedFile.h"
 
 namespace storm {
     namespace utility{
@@ -45,7 +47,9 @@ namespace storm {
                 
                 VariableType var = getVariableFromString<VariableType>(parameter);
                 BoundType lb = convertNumber<double, BoundType>(lowerBound, true, actualPrecision);
+                STORM_LOG_WARN_COND((lowerBound==convertNumber<BoundType, double>(lb, true, actualPrecision)), "The lower bound of '"<< parameterBoundsString << "' could not be parsed accurately. Increase precision?");
                 BoundType ub = convertNumber<double, BoundType>(upperBound, false, actualPrecision);
+                STORM_LOG_WARN_COND((upperBound==convertNumber<BoundType, double>(ub, true, actualPrecision)), "The upper bound of '"<< parameterBoundsString << "' could not be parsed accurately. Increase precision?");
                 lowerBounds.emplace(std::make_pair(var, lb));  
                 upperBounds.emplace(std::make_pair(var, ub));
                 std::cout << "parsed bounds " << parameterBoundsString << ": lb=" << lowerBound << " ub=" << upperBound << " param='" << parameter << "' precision=" << actualPrecision << std::endl;
@@ -59,10 +63,7 @@ namespace storm {
                 std::vector<std::string> parameterBounds;
                 boost::split(parameterBounds, regionString, boost::is_any_of(","));
                 for(auto const& parameterBound : parameterBounds){
-                    std::cout << "parsing a parameter bound" << std::endl;
                     RegionParser<ParametricType, ConstantType>::parseParameterBounds(lowerBounds, upperBounds, parameterBound, actualPrecision);
-                    std::cout << "created a parameter bound. lower bound has size" << lowerBounds.size() << std::endl;
-                    std::cout << "parsing a param bound is done" << std::endl;
                 }
                 return ParameterRegion(lowerBounds, upperBounds);
             }
@@ -74,28 +75,43 @@ namespace storm {
                 std::vector<std::string> regionsStrVec;
                 boost::split(regionsStrVec, regionsString, boost::is_any_of(";"));
                 for(auto const& regionStr : regionsStrVec){
-                    std::cout << "parsing a region" << std::endl;
+                    if(!std::all_of(regionStr.begin(),regionStr.end(),isspace)){ //skip this string if it only consists of space
                     result.emplace_back(RegionParser<ParametricType, ConstantType>::parseRegion(regionStr, actualPrecision));
-                    std::cout << "parsing a region is done" << std::endl;
+                    }
                 }
                 return result;
             }
             
+            template<typename ParametricType, typename ConstantType>
+            std::vector<typename RegionParser<ParametricType, ConstantType>::ParameterRegion> RegionParser<ParametricType, ConstantType>::getRegionsFromSettings(double precision){
+                STORM_LOG_THROW(storm::settings::regionSettings().isRegionsSet() || storm::settings::regionSettings().isRegionFileSet(), storm::exceptions::InvalidSettingsException, "Tried to obtain regions from the settings but no regions are specified.");
+                STORM_LOG_THROW(!(storm::settings::regionSettings().isRegionsSet() && storm::settings::regionSettings().isRegionFileSet()), storm::exceptions::InvalidSettingsException, "Regions are specified via file AND cmd line. Only one option is allowed.");
+                
+                std::string regionsString;
+                if(storm::settings::regionSettings().isRegionsSet()){
+                    regionsString = storm::settings::regionSettings().getRegionsFromCmdLine();
+                }
+                else{
+                    //if we reach this point we can assume that the region is given as a file.
+                    STORM_LOG_THROW(storm::parser::MappedFile::fileExistsAndIsReadable(storm::settings::regionSettings().getRegionFilePath().c_str()), storm::exceptions::InvalidSettingsException, "The path to the file in which the regions are specified is not valid.");
+                    storm::parser::MappedFile mf(storm::settings::regionSettings().getRegionFilePath().c_str());
+                    regionsString = std::string(mf.getData(),mf.getDataSize());
+                }
+                return RegionParser<ParametricType, ConstantType>::parseMultipleRegions(regionsString,precision);
+            }
+            
+            
             template<>
             storm::RationalFunction::CoeffType convertNumber<double, storm::RationalFunction::CoeffType>(double const& number, bool const& roundDown, double const& precision){
                 double actualPrecision = (precision==0.0 ? storm::settings::generalSettings().getPrecision() : precision);
                 uint_fast64_t denominator = 1.0/actualPrecision;
                 uint_fast64_t numerator;
                 if(roundDown){
-                    numerator= number*denominator; //this will always round down if necessary
+                    numerator= number*denominator; //this will always round down
                 } else{
-                    numerator = number*denominator*10; //*10 to look whether we have to round up
-                    if(numerator%10>0){
-                        numerator+=10;
-                    }
-                    numerator/=10;
+                    numerator = std::ceil(number*denominator);
                 }
-                storm::RationalFunction::CoeffType result=numerator;
+                storm::RationalFunction::CoeffType result(numerator);
                 result = result/denominator;
                 return result;
             }

src/utility/regions.h

@@ -65,6 +65,16 @@ namespace storm {
                         std::string const& regionsString,
                         double precision=0.0);
             
+
+                /*
+                 * Retrieves the regions that are specified in the settings.
+                 * The numbers are parsed as doubles and then converted to SparseDtmcRegionModelChecker::Boundtype.
+                 * According to the given precision, the lower bound may be rounded down and the upper bound may be rounded up.
+                 * If no precision is given, the one from the settings is used.
+                 * 
+                 */
+                static std::vector<ParameterRegion> getRegionsFromSettings(double precision=0.0);
+            
             };