Storm
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
ValueParser.cpp
Go to the documentation of this file.
2
3#include <boost/algorithm/string.hpp>
4#include <boost/lexical_cast.hpp>
5
11
12namespace storm {
13namespace parser {
14
15template<typename ValueType>
16ValueParser<ValueType>::ParametricData::ParametricData()
17 : manager(new storm::expressions::ExpressionManager()),
18 parser(std::make_unique<ExpressionParser>(*manager)),
19 evaluator(new storm::expressions::ExpressionEvaluator<storm::RationalFunction>(*manager)) {
20 // Set empty mapping to enable expression creation even without parameters
21 parser->setIdentifierMapping(identifierMapping);
22}
23
24template<typename ValueType>
25ValueParser<ValueType>::ParametricData::~ParametricData() = default;
26
27template<typename ValueType>
28void ValueParser<ValueType>::addParameter(std::string const& parameter) {
29 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build (Have you checked storm-pars?).");
30}
31
32template<>
33void ValueParser<storm::RationalFunction>::addParameter(std::string const& parameter) {
34 storm::expressions::Variable var = data.manager->declareRationalVariable(parameter);
35 data.identifierMapping.emplace(var.getName(), var);
36 data.parser->setIdentifierMapping(data.identifierMapping);
37 STORM_LOG_TRACE("Added parameter: " << var.getName());
38}
39
40template<>
42 storm::RationalFunction rationalFunction = data.evaluator->asRational(data.parser->parseFromString(value));
43 STORM_LOG_TRACE("Parsed expression: " << rationalFunction);
44 return rationalFunction;
45}
46
47template<typename ValueType>
48ValueType ValueParser<ValueType>::parseValue(std::string const& value) const {
49 return parseNumber<ValueType>(value);
50}
51
52template<typename NumberType>
53NumberType parseNumber(std::string const& value) {
54 NumberType result;
55 if (!parseNumber(value, result)) {
56 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Could not parse value '" << value << "' into " << typeid(NumberType).name() << ".");
57 }
58 return result;
59}
60
61bool parseDouble(std::string const& value, double& result) {
62 if (boost::conversion::try_lexical_convert(value, result)) {
63 return true;
64 } else {
65 // Try as rational number
66 storm::RationalNumber rationalResult;
67 if (parseNumber(value, rationalResult)) {
68 result = storm::utility::convertNumber<double>(rationalResult);
69 return true;
70 } else {
71 return false;
72 }
73 }
74}
75bool parseInterval(std::string const& value, storm::Interval& result) {
76 // Try whether it is a constant.
77 if (double pointResult; parseNumber(value, pointResult)) {
78 result = storm::Interval(pointResult);
79 return true;
80 }
81
82 std::string intermediate = value;
83 boost::trim(intermediate);
84 carl::BoundType leftBound;
85 carl::BoundType rightBound;
86 if (intermediate.front() == '(') {
87 leftBound = carl::BoundType::STRICT;
88 } else if (intermediate.front() == '[') {
89 leftBound = carl::BoundType::WEAK;
90 } else {
91 return false; // Expect start with '(' or '['.
92 }
93 if (intermediate.back() == ')') {
94 rightBound = carl::BoundType::STRICT;
95 } else if (intermediate.back() == ']') {
96 rightBound = carl::BoundType::WEAK;
97 } else {
98 return false; // Expected end with ')' or ']'.
99 }
100 intermediate = intermediate.substr(1, intermediate.size() - 2);
101
102 std::vector<std::string> words;
103 boost::split(words, intermediate, boost::is_any_of(","));
104 if (words.size() != 2) {
105 return false; // Did not find exactly one comma.
106 }
107 double leftVal, rightVal;
108 boost::trim(words[0]);
109 if (!parseNumber(words[0], leftVal)) {
110 return false; // lower value of interval invalid.
111 }
112 boost::trim(words[1]);
113 if (!parseNumber(words[1], rightVal)) {
114 return false; // upper value of interval invalid.
115 }
116 result = storm::Interval(leftVal, leftBound, rightVal, rightBound);
117 return true;
118}
119
120template<typename NumberType>
121bool parseNumber(std::string const& value, NumberType& result) {
122 if constexpr (std::is_same_v<NumberType, double>) {
123 return parseDouble(value, result);
124 } else if constexpr (std::is_same_v<NumberType, storm::RationalNumber>) {
125 return carl::try_parse(value, result);
126 } else if constexpr (std::is_same_v<NumberType, storm::Interval>) {
127 return parseInterval(value, result);
128 } else {
129 return boost::conversion::try_lexical_convert(value, result);
130 }
131}
132
133// Template instantiations.
134template class ValueParser<double>;
135template class ValueParser<storm::RationalNumber>;
136template class ValueParser<storm::RationalFunction>;
137template class ValueParser<storm::Interval>;
138
139template std::size_t parseNumber<std::size_t>(std::string const&);
140
141} // namespace parser
142} // namespace storm
Variable declareRationalVariable(std::string const &name, bool auxiliary=false)
Declares a new rational variable with a name that must not yet exist and its corresponding type.
std::string const & getName() const
Retrieves the name of the variable.
Definition Variable.cpp:46
Parser for values according to their ValueType.
Definition ValueParser.h:23
#define STORM_LOG_TRACE(message)
Definition logging.h:17
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
NumberType parseNumber(std::string const &value)
Parse number from string.
bool parseDouble(std::string const &value, double &result)
bool parseInterval(std::string const &value, storm::Interval &result)
SettingsManager const & manager()
Retrieves the settings manager.
LabParser.cpp.
Definition cli.cpp:18
carl::Interval< double > Interval
carl::RationalFunction< Polynomial, true > RationalFunction