From 429c91ff138a606e21334cb6874d634ae2f40da4 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 1 Aug 2019 15:27:34 +0200
Subject: [PATCH] Added support for parsing fractions in DRN files.

---
 src/storm-dft/parser/DFTGalileoParser.cpp     |  8 +--
 .../parser/DirectEncodingParser.cpp           |  7 +--
 src/storm-parsers/parser/ValueParser.cpp      | 13 ++---
 src/storm-parsers/parser/ValueParser.h        | 50 ++++++++++++-------
 src/storm/api/builder.h                       |  5 --
 src/storm/utility/constants.cpp               | 23 ++++++---
 6 files changed, 62 insertions(+), 44 deletions(-)

diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp
index 8d44637f9..2461fb9cb 100644
--- a/src/storm-dft/parser/DFTGalileoParser.cpp
+++ b/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);
diff --git a/src/storm-parsers/parser/DirectEncodingParser.cpp b/src/storm-parsers/parser/DirectEncodingParser.cpp
index 46519f81c..a34bbdb35 100644
--- a/src/storm-parsers/parser/DirectEncodingParser.cpp
+++ b/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
diff --git a/src/storm-parsers/parser/ValueParser.cpp b/src/storm-parsers/parser/ValueParser.cpp
index 918c89bac..7f35fc86f 100644
--- a/src/storm-parsers/parser/ValueParser.cpp
+++ b/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,9 +25,15 @@ 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
 } // namespace storm
diff --git a/src/storm-parsers/parser/ValueParser.h b/src/storm-parsers/parser/ValueParser.h
index 626857a3e..768be44ad 100644
--- a/src/storm-parsers/parser/ValueParser.h
+++ b/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,25 +45,39 @@ namespace storm {
             std::unordered_map<std::string, storm::expressions::Expression> identifierMapping;
         };
 
+        
+        /*!
+         * Parse number from string.
+         *
+         * @param value String containing the value.
+         *
+         * @return NumberType.
+         */
         template<typename NumberType>
-        class NumberParser {
-        public:
-            /*!
-             * Parse number from string.
-             *
-             * @param value String containing the value.
-             *
-             * @return NumberType.
-             */
-            static NumberType parse(std::string const& value) {
-                try {
-                    return boost::lexical_cast<NumberType>(value);
-                }
-                catch(boost::bad_lexical_cast &) {
-                    STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse value '" << value << "' into " << typeid(NumberType).name() << ".");
-                }
+        inline NumberType parseNumber(std::string const& value) {
+            try {
+                return boost::lexical_cast<NumberType>(value);
             }
-        };
+            catch(boost::bad_lexical_cast &) {
+                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
diff --git a/src/storm/api/builder.h b/src/storm/api/builder.h
index f1520aed4..5fc7898ee 100644
--- a/src/storm/api/builder.h
+++ b/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.");
diff --git a/src/storm/utility/constants.cpp b/src/storm/utility/constants.cpp
index a5e1c14f5..eeff62ad3 100644
--- a/src/storm/utility/constants.cpp
+++ b/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<>
@@ -862,7 +865,11 @@ namespace storm {
         }
 
 #endif
-        
+      
+        template<>
+        double convertNumber(std::string const& value){
+            return convertNumber<double>(convertNumber<storm::RationalNumber>(value));
+        }
         
         // Explicit instantiations.