Sampling the corners of the region

Former-commit-id: 510b727c32

src/modelchecker/reachability/SparseDtmcRegionModelChecker.cpp

@@ -28,10 +28,41 @@ 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), checkResult(RegionCheckResult::UNKNOWN) {
-            // Intentionally left empty.
             //todo: check whether both mappings map the same variables
         }
 
+        template<typename ParametricType, typename ConstantType>        
+        void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::setUnSatPoint(std::map<VariableType, BoundType> const& unSatPoint) {
+            this->unSatPoint = unSatPoint;
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getUnSatPoint() const {
+            return unSatPoint;
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::setSatPoint(std::map<VariableType, BoundType> const& satPoint) {
+            this->satPoint = satPoint;
+        }
+
+        template<typename ParametricType, typename ConstantType>
+        std::map<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType, typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getSatPoint() const {
+            return satPoint;
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::setCheckResult(RegionCheckResult checkResult) {
+            this->checkResult = checkResult;
+        }
+
+        template<typename ParametricType, typename ConstantType>        
+        typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::RegionCheckResult SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getCheckResult() const {
+            return checkResult;
+        }
+
+      
+                
         template<typename ParametricType, typename ConstantType>
         std::set<typename SparseDtmcRegionModelChecker<ParametricType, ConstantType>::VariableType> SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getVariables() const{
             std::set<VariableType> result;
@@ -84,7 +115,7 @@ namespace storm {
         }
 
         template<typename ParametricType, typename ConstantType>
-        std::string SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getCheckResultAsString() const {
+        std::string SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::checkResultToString() const {
             switch (this->checkResult) {
                 case RegionCheckResult::UNKNOWN:
                     return "unknown";
@@ -100,7 +131,7 @@ namespace storm {
         }
             
         template<typename ParametricType, typename ConstantType>
-        std::string SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::getRegionAsString() const {
+        std::string SparseDtmcRegionModelChecker<ParametricType, ConstantType>::ParameterRegion::toString() const {
             std::stringstream regionstringstream;
             for(auto var : this->getVariables()){
                 regionstringstream << storm::utility::regions::convertNumber<SparseDtmcRegionModelChecker<ParametricType, ConstantType>::BoundType,double>(this->getLowerBound(var));
@@ -197,14 +228,14 @@ namespace storm {
             std::chrono::high_resolution_clock::time_point timeInitialStateEliminationStart = std::chrono::high_resolution_clock::now();
             // eliminate all states with only constant outgoing transitions
             //TODO: maybe also states with constant incoming tranistions. THEN the ordering of the eliminated states does matter.
-            eliminateStatesConstSucc(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->oneStepProbabilities, this->initialState);
+            eliminateStatesConstSucc(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->oneStepProbabilities, this->hasOnlyLinearFunctions, this->initialState);
             STORM_LOG_DEBUG("Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl);
             std::cout << "Eliminated " << subsystem.size() - subsystem.getNumberOfSetBits() << " of " << subsystem.size() << " states that had constant outgoing transitions." << std::endl;
             //eliminate the remaining states to get the reachability probability function
             this->sparseTransitions = flexibleTransitions.getSparseMatrix();
             this->sparseBackwardTransitions = this->sparseTransitions.transpose();
             this->reachProbFunction = computeReachProbFunction(this->subsystem, this->flexibleTransitions, this->flexibleBackwardTransitions, this->sparseTransitions, this->sparseBackwardTransitions, this->oneStepProbabilities, this->initialState);
-            std::cout << std::endl <<"the resulting reach prob function is " << std::endl << this->reachProbFunction << std::endl << std::endl;
+      //      std::cout << std::endl <<"the resulting reach prob function is " << std::endl << this->reachProbFunction << std::endl << std::endl;
             std::chrono::high_resolution_clock::time_point timeInitialStateEliminationEnd = std::chrono::high_resolution_clock::now();
             
             //some information for statistics...
@@ -220,20 +251,27 @@ namespace storm {
                 FlexibleMatrix& flexTransitions,
                 FlexibleMatrix& flexBackwardTransitions,
                 std::vector<ParametricType>& oneStepProbs,
+                bool& allFunctionsAreLinear,
                 storm::storage::sparse::state_type const& initialState) {
             
             //temporarily unselect the initial state to skip it.
             subsys.set(initialState, false);
             
+            allFunctionsAreLinear=true;
+            
             boost::optional<std::vector<ParametricType>> missingStateRewards;
             for (auto const& state : subsys) {
                 bool onlyConstantOutgoingTransitions=true;
-                for(auto const& entry : flexTransitions.getRow(state)){
+                for(auto& entry : flexTransitions.getRow(state)){
                     if(!this->parametricTypeComparator.isConstant(entry.getValue())){
                         onlyConstantOutgoingTransitions=false;
-                        break;
+                        allFunctionsAreLinear &= storm::utility::regions::functionIsLinear<ParametricType>(entry.getValue());
                     }
                 }
+                if(!this->parametricTypeComparator.isConstant(oneStepProbs[state])){
+                    onlyConstantOutgoingTransitions=false;
+                    allFunctionsAreLinear &= storm::utility::regions::functionIsLinear<ParametricType>(oneStepProbs[state]);
+                }
                 if(onlyConstantOutgoingTransitions){
                     this->eliminationModelChecker.eliminateState(flexTransitions, oneStepProbs, state, flexBackwardTransitions, missingStateRewards);
                     subsys.set(state,false);
@@ -301,6 +339,128 @@ namespace storm {
             
             return workingCopyOneStepProbs[initState];
         }
+        
+
+
+
+        template<typename ParametricType, typename ConstantType>
+        void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkRegion(ParameterRegion& region) {
+            std::chrono::high_resolution_clock::time_point timeCheckRegionStart = std::chrono::high_resolution_clock::now();
+            ++this->numOfCheckedRegions;
+            
+            STORM_LOG_THROW(this->probabilityOperatorFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to analyze a region although no property has been specified" );
+            STORM_LOG_DEBUG("Analyzing the region " << region.toString());
+            
+            //switches for the different steps.
+            bool doSampling=true;
+            bool doApproximation=this->hasOnlyLinearFunctions; // this approach is only correct if the model has only linear functions
+            bool doSubsystemSmt=false; //this->hasOnlyLinearFunctions;  // this approach is only correct if the model has only linear functions
+            bool doFullSmt=false; //true;
+            
+            std::chrono::high_resolution_clock::time_point timeSamplingStart = std::chrono::high_resolution_clock::now();
+            if(doSampling){
+                STORM_LOG_DEBUG("Testing Sample points...");
+                if(testSamplePoints(region)){
+                    ++this->numOfRegionsSolvedThroughSampling;
+                    STORM_LOG_DEBUG("Result '" << region.checkResultToString() <<"' obtained through sampling.");
+                    doApproximation=false;
+                    doSubsystemSmt=false;
+                    doFullSmt=false;
+                }
+            }
+            std::chrono::high_resolution_clock::time_point timeSamplingEnd = std::chrono::high_resolution_clock::now();
+            
+            std::chrono::high_resolution_clock::time_point timeApproximationStart = std::chrono::high_resolution_clock::now();
+            if(doApproximation){
+                STORM_LOG_WARN("Approximation approach not yet implemented");
+            }
+            std::chrono::high_resolution_clock::time_point timeApproximationEnd = std::chrono::high_resolution_clock::now();
+            
+            std::chrono::high_resolution_clock::time_point timeSubsystemSmtStart = std::chrono::high_resolution_clock::now();
+            if(doSubsystemSmt){
+                STORM_LOG_WARN("SubsystemSmt approach not yet implemented");
+            }
+            std::chrono::high_resolution_clock::time_point timeSubsystemSmtEnd = std::chrono::high_resolution_clock::now();
+            
+            std::chrono::high_resolution_clock::time_point timeFullSmtStart = std::chrono::high_resolution_clock::now();
+            if(doFullSmt){
+                STORM_LOG_WARN("FullSmt approach not yet implemented");
+            }
+            std::chrono::high_resolution_clock::time_point timeFullSmtEnd = std::chrono::high_resolution_clock::now();
+            
+            
+            
+            //some information for statistics...
+            std::chrono::high_resolution_clock::time_point timeCheckRegionEnd = std::chrono::high_resolution_clock::now();
+            this->timeCheckRegion = timeCheckRegionEnd-timeCheckRegionStart;
+            this->timeSampling = timeSamplingEnd - timeSamplingStart;
+            this->timeApproximation = timeApproximationEnd - timeApproximationStart;
+            this->timeSubsystemSmt = timeSubsystemSmtEnd - timeSubsystemSmtStart;
+            this->timeFullSmt = timeFullSmtEnd - timeFullSmtStart;
+            
+        }
+
+        template<typename ParametricType, typename ConstantType>
+        void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkRegions(std::vector<ParameterRegion>& regions) {
+            for(auto& region : regions){
+                this->checkRegion(region);
+            }
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::testSamplePoints(ParameterRegion& region) {
+
+            auto samplingPoints = region.getVerticesOfRegion(region.getVariables()); //only test the 4 corner points (for now)
+            
+            bool regionHasSatPoint = !region.getSatPoint().empty();
+            bool regionHasUnSatPoint = !region.getUnSatPoint().empty();
+            for (auto const& point : samplingPoints){
+                // check whether the property is satisfied or not at the given point
+                if(this->valueIsInBoundOfFormula(storm::utility::regions::evaluateFunction<ParametricType, ConstantType>(this->reachProbFunction, point))){
+                    if (!regionHasSatPoint){
+                        region.setSatPoint(point);
+                        regionHasSatPoint=true;
+                        if(regionHasUnSatPoint){
+                            region.setCheckResult(RegionCheckResult::INCONCLUSIVE);
+                            return true;
+                        }
+                    }
+                }
+                else{
+                    if (!regionHasUnSatPoint){
+                        region.setUnSatPoint(point);
+                        regionHasUnSatPoint=true;
+                        if(regionHasSatPoint){
+                            region.setCheckResult(RegionCheckResult::INCONCLUSIVE);
+                            return true;
+                        }
+                    }
+                }
+            }
+            return false;
+        }
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
+        
         
         
         
@@ -584,7 +744,7 @@ namespace storm {
         }
         
         template<>
-        bool SparseDtmcRegionModelChecker<storm::RationalFunction, double>::checkRegion(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions){
+        bool SparseDtmcRegionModelChecker<storm::RationalFunction, double>::checkRegionOld(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions){
             //Note: this is an 'experimental' implementation
             
             std::chrono::high_resolution_clock::time_point timeStart = std::chrono::high_resolution_clock::now();
@@ -754,13 +914,14 @@ namespace storm {
         }
 
         template<typename ParametricType, typename ConstantType>
-        bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkRegion(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions){
+        bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::checkRegionOld(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions){
             STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Region check is not supported for this type");
         }
         
         template<typename ParametricType, typename ConstantType>
         template<typename ValueType>
         bool SparseDtmcRegionModelChecker<ParametricType, ConstantType>::valueIsInBoundOfFormula(ValueType value){
+            STORM_LOG_THROW(this->probabilityOperatorFormula!=nullptr, storm::exceptions::InvalidStateException, "Tried to compare a value to the bound of a formula, but no formula specified.");
             double valueAsDouble = storm::utility::regions::convertNumber<ValueType, double>(value);
             switch (this->probabilityOperatorFormula->getComparisonType()) {
                 case storm::logic::ComparisonType::Greater:
@@ -779,17 +940,30 @@ namespace storm {
         template<typename ParametricType, typename ConstantType>
         void SparseDtmcRegionModelChecker<ParametricType, ConstantType>::printStatisticsToStream(std::ostream& outstream) {
             
+            if(this->probabilityOperatorFormula==nullptr){
+                outstream << "Statistic Region Model Checker Statistics Error: No formula specified." << std::endl; 
+                return;
+            }
+            
             std::chrono::milliseconds timePreprocessingInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timePreprocessing);
             std::chrono::milliseconds timeInitialStateEliminationInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(this->timeInitialStateElimination);
             
             std::chrono::high_resolution_clock::duration timeOverall = timePreprocessing; // + ...
             std::chrono::milliseconds timeOverallInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(timeOverall);
             
-            outstream << std::endl << "Statistics Region Model Checker:" << std::endl;
+            std::size_t subsystemTransitions = this->sparseTransitions.getNonzeroEntryCount();
+            for(auto const& transition : this->oneStepProbabilities){
+                if(!this->parametricTypeComparator.isZero(transition)){
+                    ++subsystemTransitions;
+                }
+            }
+            
+            outstream << std::endl << "Statistics Region Model Checker Statistics:" << std::endl;
             outstream << "-----------------------------------------------" << std::endl;
             outstream << "Model: " << this->model.getNumberOfStates() << " states, " << this->model.getNumberOfTransitions() << " transitions." << std::endl;
-            outstream << "Reduced model: " << this->subsystem.getNumberOfSetBits() << " states, " << this->sparseTransitions.getEntryCount() << "transitions" << std::endl;
+            outstream << "Reduced model: " << this->subsystem.getNumberOfSetBits() << " states, " << subsystemTransitions << "transitions" << std::endl;
             outstream << "Formula: " << *this->probabilityOperatorFormula << std::endl;
+            outstream << "All occuring functions in the model are " << (this->hasOnlyLinearFunctions ? "" : "not") << " linear" << std::endl;
             outstream << "Number of checked regions: " << this->numOfCheckedRegions << std::endl;
             outstream << "Running times:" << std::endl;
             outstream << "  " << timeOverallInMilliseconds.count() << "ms overall" << std::endl;

src/modelchecker/reachability/SparseDtmcRegionModelChecker.h

@@ -37,13 +37,6 @@ namespace storm {
 
                 ParameterRegion(std::map<VariableType, BoundType> lowerBounds, std::map<VariableType, BoundType> upperBounds);
                 
-                void setCheckResult(RegionCheckResult checkResult) {
-                    this->checkResult = checkResult;
-                }
-
-                RegionCheckResult getCheckResult() const {
-                    return checkResult;
-                }
                 
                 
                 std::set<VariableType> getVariables() const;
@@ -59,14 +52,46 @@ namespace storm {
                  */
                 std::vector<std::map<VariableType, BoundType>> getVerticesOfRegion(std::set<VariableType> const& consideredVariables) const;
                 
-                std::string getCheckResultAsString() const;
-                std::string getRegionAsString() const;
+                //returns the currently set check result as a string
+                std::string checkResultToString() const;
+                
+                //returns the region as string in the format 0.3<=p<=0.4,0.2<=q<=0.5;
+                std::string toString() const;
+                
+                void setCheckResult(RegionCheckResult checkResult);
+                RegionCheckResult getCheckResult() const;
+                
+                /*!
+                 * Sets a point in the region for which the considered property is not satisfied. 
+                 */
+                void setUnSatPoint(std::map<VariableType, BoundType> const& unSatPoint);
+                
+                /*!
+                 * Retrieves a point in the region for which is considered property is not satisfied.
+                 * If such a point is not known, the returned map is empty.
+                 */
+                std::map<VariableType, BoundType> getUnSatPoint() const;
+                
+                
+                /*!
+                 * Sets a point in the region for which the considered property is satisfied. 
+                 */
+                void setSatPoint(std::map<VariableType, BoundType> const& satPoint);
+                
+                /*!
+                 * Retrieves a point in the region for which is considered property is satisfied.
+                 * If such a point is not known, the returned map is empty.
+                 */
+                std::map<VariableType, BoundType> getSatPoint() const;
                 
             private:
                 
                 std::map<VariableType, BoundType> const lowerBounds;
                 std::map<VariableType, BoundType> const upperBounds;
                 RegionCheckResult checkResult;
+                std::map<VariableType, BoundType> satPoint;
+                std::map<VariableType, BoundType> unSatPoint;
+                
                 
             };
             
@@ -87,11 +112,32 @@ namespace storm {
              */
             void specifyFormula(storm::logic::Formula const& formula);
 
+            /*!
+             * Checks whether the given formula holds for all parameters that lie in the given region.
+             * Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.unSatPoint will be set.
+             * 
+             * @note A formula has to be specified first.
+             * 
+             * @param region The considered region
+             * 
+             */
+            void checkRegion(ParameterRegion& region);
+            
+            /*!
+             * Checks for every given region whether the specified formula holds for all parameters that lie in that region.
+             * Sets the region checkresult accordingly. Moreover, region.satPoint and/or an region.unSatPoint will be set.
+             * 
+             * @note A formula has to be specified first.
+             * 
+             * @param region The considered region
+             */
+            void checkRegions(std::vector<ParameterRegion>& regions);
+            
             /*!
              * Checks whether the given formula holds for all possible parameters that satisfy the given parameter regions
              * ParameterRegions should contain all parameters.
              */
-            bool checkRegion(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions);
+            bool checkRegionOld(storm::logic::Formula const& formula, std::vector<ParameterRegion> parameterRegions);
             
             /*!
              * Prints statistical information (mostly running times) to the given stream.
@@ -142,12 +188,16 @@ namespace storm {
             template <typename ValueType>
             bool valueIsInBoundOfFormula(ValueType value);
             
-            //eliminates all states for which the outgoing transitions are constant.
+            /*!
+             * eliminates all states for which the outgoing transitions are constant.
+             * Also checks whether the non constant functions are linear
+             */
             void eliminateStatesConstSucc(
                     storm::storage::BitVector& subsys,
                     FlexibleMatrix& flexTransitions,
                      FlexibleMatrix& flexBackwardTransitions,
                     std::vector<ParametricType>& oneStepProbs,
+                    bool& allFunctionsAreLinear,
                     storm::storage::sparse::state_type const& initState
             );
             
@@ -163,6 +213,14 @@ namespace storm {
             );
             
             
+            /*!
+             * Checks the value of the function at some sampling points within the given region
+             * may set the satPoint and unSatPoint of the regions if they are not yet specified and such points are found
+             * may also change the regioncheckresult of the region
+             * 
+             * @return true if an unsat point as well as a sat point has been found during the process
+             */
+            bool testSamplePoints(ParameterRegion& region);
             
             
             
@@ -195,6 +253,8 @@ namespace storm {
             storm::storage::sparse::state_type initialState;
             // the set of states that have not been eliminated
             storm::storage::BitVector subsystem;
+            // a flag that is true if there are only linear functions at transitions of the model
+            bool hasOnlyLinearFunctions;
             
             // The  function for the reachability probability in the initial state 
             ParametricType reachProbFunction;
@@ -202,8 +262,18 @@ namespace storm {
             
             // runtimes and other information for statistics. 
             uint_fast64_t numOfCheckedRegions;
+            uint_fast64_t numOfRegionsSolvedThroughSampling;
+            uint_fast64_t numOfRegionsSolvedThroughApproximation;
+            uint_fast64_t numOfRegionsSolvedThroughSubsystemSmt;
+            uint_fast64_t numOfRegionsSolvedThroughFullSmt;
+            
             std::chrono::high_resolution_clock::duration timePreprocessing;
             std::chrono::high_resolution_clock::duration timeInitialStateElimination;
+            std::chrono::high_resolution_clock::duration timeCheckRegion;
+            std::chrono::high_resolution_clock::duration timeSampling;
+            std::chrono::high_resolution_clock::duration timeApproximation;
+            std::chrono::high_resolution_clock::duration timeSubsystemSmt;
+            std::chrono::high_resolution_clock::duration timeFullSmt;
         };
         
     } // namespace modelchecker

src/utility/cli.h

@@ -480,18 +480,14 @@ namespace storm {
                     storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction, double> modelchecker(*dtmc);
                     if (modelchecker.canHandle(*formula.get())) {
                         modelchecker.specifyFormula(*formula.get());
+                        modelchecker.checkRegions(regions);
                     }
                     else {
                         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric region check engine currently does not support this property.");
                     }
-                    
-                    auto result = modelchecker.checkRegion(*formula.get(), regions);
                     std::cout << "... done." << std::endl;
-                    if (!result){
-                        std::cout << "The result of one or more regions is still unknown." << std::endl;    
-                    }
                     for(auto const& reg : regions){
-                        std::cout << reg.getRegionAsString() << "      Result: " << reg.getCheckResultAsString() << std::endl;
+                        std::cout << reg.toString() << "      Result: " << reg.checkResultToString() << std::endl;
                     }
                     modelchecker.printStatisticsToStream(std::cout);
                     

src/utility/regions.cpp

@@ -131,9 +131,9 @@ namespace storm {
                 return number;
             }
             
-            template<typename SourceType, typename TargetType>
-            TargetType convertNumber(SourceType const& number, bool const& roundDown, double const& precision){
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "number conversion between the given types not implemented");
+            template<>
+            cln::cl_RA convertNumber<cln::cl_RA, cln::cl_RA>(cln::cl_RA const& number, bool const& roundDown, double const& precision){
+                return number;
             }
                        
             
@@ -144,32 +144,45 @@ namespace storm {
                 return var;
             }
                       
-            template<typename VariableType>
-            VariableType getVariableFromString(std::string variableString){
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Variable from String not implemented for this type");
-            }
-            
             template<>
             std::string getVariableName<storm::Variable>(storm::Variable variable){
                 return carl::VariablePool::getInstance().getName(variable);
             }
                         
-            template<typename VariableType>
-            std::string getVariableName(VariableType variable){
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "VariableName from Variable not implemented for this type");
+            template<>
+            typename storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction,double>::BoundType evaluateFunction<storm::RationalFunction, double>(
+                    storm::RationalFunction const& function, 
+                    std::map<typename storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction,double>::VariableType,
+                             typename storm::modelchecker::SparseDtmcRegionModelChecker<storm::RationalFunction,double>::BoundType> const& point){
+                return function.evaluate(point);
+            }
+            
+            template<>
+            bool functionIsLinear<storm::RationalFunction>(storm::RationalFunction const& function){
+                // Note: At this moment there is no function in carl for rationalFunctions.
+                // We therefore check whether the numerator is linear and the denominator constant.
+                // We simplify the function to (hopefully) avoid wrong answers for situations like x^2/x
+                storm::utility::simplify(function);
+                bool result=(function.nominator().isLinear() && function.denominator().isConstant());
+                STORM_LOG_WARN_COND(result, "The function " << function << "is not considered as linear.");
+                return result;
             }
             
             //explicit instantiations
+       template double convertNumber<double, double>(double const& number, bool const& roundDown, double const& precision);
+       
 #ifdef STORM_HAVE_CARL
        template class RegionParser<storm::RationalFunction, double>;
        
        template storm::RationalFunction convertNumber<double, storm::RationalFunction>(double const& number, bool const& roundDown, double const& precision);
        template storm::RationalFunction::CoeffType convertNumber<double, storm::RationalFunction::CoeffType>(double const& number, bool const& roundDown, double const& precision);
        template double convertNumber<cln::cl_RA, double>(storm::RationalFunction::CoeffType const& number, bool const& roundDown, double const& precision);
-       template double convertNumber<double, double>(double const& number, bool const& roundDown, double const& precision);
+       template cln::cl_RA convertNumber<cln::cl_RA, cln::cl_RA>(cln::cl_RA const& number, bool const& roundDown, double const& precision);
        
        template storm::Variable getVariableFromString<storm::Variable>(std::string variableString);
        template std::string getVariableName<storm::Variable>(storm::Variable variable);
+       
+       template bool functionIsLinear<storm::RationalFunction>(storm::RationalFunction const& function);
 #endif 
         }
     }

src/utility/regions.h

@@ -97,6 +97,16 @@ namespace storm {
              */
             template<typename VariableType>
             std::string getVariableName(VariableType variable);
+            
+            template<typename ParametricType, typename ConstantType>
+            typename storm::modelchecker::SparseDtmcRegionModelChecker<ParametricType,ConstantType>::BoundType evaluateFunction(ParametricType const& function, std::map<typename storm::modelchecker::SparseDtmcRegionModelChecker<ParametricType,ConstantType>::VariableType, typename storm::modelchecker::SparseDtmcRegionModelChecker<ParametricType,ConstantType>::BoundType> const& point);
+            
+            /*!
+             * Returns true if the function is rational. Note that the function might be simplified.
+             */
+            template<typename ParametricType>
+            bool functionIsLinear(ParametricType const& function);
+            
         }
     }
 }