Added support for parsing fractions in DRN files.

src/storm-dft/parser/DFTGalileoParser.cpp

@@ -113,12 +113,12 @@ namespace storm {
                         } else if (type == "or") {
                             success = builder.addOrElement(name, childNames);
                         } else if (boost::starts_with(type, "vot")) {
-                            unsigned threshold = NumberParser<unsigned>::parse(type.substr(3));
+                            unsigned threshold = storm::parser::parseNumber<unsigned>(type.substr(3));
                             success = builder.addVotElement(name, threshold, childNames);
                         } else if (type.find("of") != std::string::npos) {
                             size_t pos = type.find("of");
-                            unsigned threshold = NumberParser<unsigned>::parse(type.substr(0, pos));
-                            unsigned count = NumberParser<unsigned>::parse(type.substr(pos + 2));
+                            unsigned threshold = storm::parser::parseNumber<unsigned>(type.substr(0, pos));
+                            unsigned count = storm::parser::parseNumber<unsigned>(type.substr(pos + 2));
                             STORM_LOG_THROW(count == childNames.size(), storm::exceptions::WrongFormatException, "Voting gate number " << count << " does not correspond to number of children " << childNames.size() << " in line " << lineNo << ".");
                             success = builder.addVotElement(name, threshold, childNames);
                         } else if (type == "pand") {
@@ -198,7 +198,7 @@ namespace storm {
                 std::string value = match.str(1);
                 // Remove matched part
                 line = std::regex_replace(line, nameRegex, "");
-                return std::make_pair(true, NumberParser<unsigned>::parse(value));
+                return std::make_pair(true, storm::parser::parseNumber<unsigned>(value));
             } else {
                 // No match found
                 return std::make_pair(false, 0);

src/storm-parsers/parser/DirectEncodingParser.cpp

@@ -82,7 +82,7 @@ namespace storm {
                     // Parse no. of states
                     STORM_LOG_THROW(nrStates == 0, storm::exceptions::WrongFormatException, "Number states declared twice");
                     std::getline(file, line);
-                    nrStates = NumberParser<size_t>::parse(line);
+                    nrStates = parseNumber<size_t>(line);
                 } else if (line == "@model") {
                     // Parse rest of the model
                     STORM_LOG_THROW(sawType, storm::exceptions::WrongFormatException, "Type has to be declared before model.");
@@ -154,7 +154,7 @@ namespace storm {
                     } else {
                         line = "";
                     }
-                    size_t parsedId = NumberParser<size_t>::parse(curString);
+                    size_t parsedId = parseNumber<size_t>(curString);
                     STORM_LOG_ASSERT(state == parsedId, "State ids do not correspond.");
                     if (nonDeterministic) {
                         STORM_LOG_TRACE("new Row Group starts at " << row << ".");
@@ -275,7 +275,7 @@ namespace storm {
                     // New transition
                     size_t posColon = line.find(":");
                     STORM_LOG_THROW(posColon != std::string::npos, storm::exceptions::WrongFormatException, "':' not found.");
-                    size_t target = NumberParser<size_t>::parse(line.substr(2, posColon-3));
+                    size_t target = parseNumber<size_t>(line.substr(2, posColon-3));
                     std::string valueStr = line.substr(posColon+2);
                     ValueType value = valueParser.parseValue(valueStr);
                     STORM_LOG_TRACE("Transition " << row << " -> " << target << ": " << value);
@@ -302,6 +302,7 @@ namespace storm {
 
         // Template instantiations.
         template class DirectEncodingParser<double>;
+        template class DirectEncodingParser<storm::RationalNumber>;
         template class DirectEncodingParser<storm::RationalFunction>;
 
     } // namespace parser

src/storm-parsers/parser/ValueParser.cpp

@@ -18,11 +18,6 @@ namespace storm {
             STORM_LOG_TRACE("Added parameter: " << var.getName());
         }
 
-        template<>
-        double ValueParser<double>::parseValue(std::string const& value) const {
-            return NumberParser<double>::parse(value);
-        }
-
         template<>
         storm::RationalFunction ValueParser<storm::RationalFunction>::parseValue(std::string const& value) const {
             storm::RationalFunction rationalFunction = evaluator.asRational(parser.parseFromString(value));
@@ -30,8 +25,14 @@ namespace storm {
             return rationalFunction;
         }
 
+        template<typename ValueType>
+        ValueType ValueParser<ValueType>::parseValue(std::string const& value) const {
+            return parseNumber<ValueType>(value);
+        }
+        
         // Template instantiations.
         template class ValueParser<double>;
+        template class ValueParser<storm::RationalNumber>;
         template class ValueParser<storm::RationalFunction>;
         
     } // namespace parser

src/storm-parsers/parser/ValueParser.h

@@ -3,9 +3,9 @@
 
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm-parsers/parser/ExpressionParser.h"
+#include "storm/utility/constants.h"
 #include "storm/storage/expressions/ExpressionEvaluator.h"
 #include "storm/exceptions/WrongFormatException.h"
-
 namespace storm {
     namespace parser {
         /*!
@@ -45,9 +45,7 @@ namespace storm {
             std::unordered_map<std::string, storm::expressions::Expression> identifierMapping;
         };
 
-        template<typename NumberType>
-        class NumberParser {
-        public:
+        
         /*!
          * Parse number from string.
          *
@@ -55,7 +53,8 @@ namespace storm {
          *
          * @return NumberType.
          */
-            static NumberType parse(std::string const& value) {
+        template<typename NumberType>
+        inline NumberType parseNumber(std::string const& value) {
             try {
                 return boost::lexical_cast<NumberType>(value);
             }
@@ -63,7 +62,22 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse value '" << value << "' into " << typeid(NumberType).name() << ".");
             }
         }
-        };
+
+        template<>
+        inline storm::RationalNumber parseNumber(std::string const& value) {
+            return storm::utility::convertNumber<storm::RationalNumber>(value);
+        }
+
+        template<>
+        inline double parseNumber(std::string const& value) {
+            try {
+                return boost::lexical_cast<double>(value);
+            }
+            catch(boost::bad_lexical_cast &) {
+                return storm::utility::convertNumber<double>(parseNumber<storm::RationalNumber>(value));
+            }
+        }
+
 
     } // namespace parser
 } // namespace storm

src/storm/api/builder.h

@@ -148,11 +148,6 @@ namespace storm {
             return storm::parser::DirectEncodingParser<ValueType>::parseModel(drnFile);
         }
         
-        template<>
-        inline std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> buildExplicitDRNModel(std::string const&) {
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported.");
-        }
-        
         template<typename ValueType>
         std::shared_ptr<storm::models::sparse::Model<ValueType>> buildExplicitIMCAModel(std::string const&) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Exact models with direct encoding are not supported.");

src/storm/utility/constants.cpp

@@ -120,11 +120,6 @@ namespace storm {
             return static_cast<double>(number);
         }
 
-        template<>
-        double convertNumber(std::string const& value){
-            return carl::toDouble(carl::parse<storm::RationalNumber>(value));
-        }
-
         template<>
         storm::storage::sparse::state_type convertNumber(long long const& number){
             return static_cast<storm::storage::sparse::state_type>(number);
@@ -395,7 +390,11 @@ namespace storm {
         
         template<>
         ClnRationalNumber convertNumber(std::string const& number) {
-            return carl::parse<ClnRationalNumber>(number);
+            ClnRationalNumber result;
+            if (carl::try_parse<ClnRationalNumber>(number, result)) {
+                return result;
+            }
+            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unable to parse '" << number << "' as a rational number.");
         }
         
         template<>
@@ -588,7 +587,11 @@ namespace storm {
         
         template<>
         GmpRationalNumber convertNumber(std::string const& number) {
-            return carl::parse<GmpRationalNumber>(number);
+            GmpRationalNumber result;
+            if (carl::try_parse<GmpRationalNumber>(number, result)) {
+                return result;
+            }
+            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Unable to parse '" << number << "' as a rational number.");
         }
         
         template<>
@@ -863,6 +866,10 @@ namespace storm {
 
 #endif
       
+        template<>
+        double convertNumber(std::string const& value){
+            return convertNumber<double>(convertNumber<storm::RationalNumber>(value));
+        }
         
         // Explicit instantiations.