Storm 1.10.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
cli.cpp
Go to the documentation of this file.
1#include "storm/utility/cli.h"
2
3#include <boost/algorithm/string.hpp>
8
9#include <unistd.h>
10
11namespace storm {
12namespace utility {
13namespace cli {
14
16 char temp[512];
17 return (getcwd(temp, 512 - 1) ? std::string(temp) : std::string(""));
18}
19
20std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::expressions::ExpressionManager const& manager,
21 std::string const& constantDefinitionString) {
22 std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
23 std::set<storm::expressions::Variable> definedConstants;
24
25 if (!constantDefinitionString.empty()) {
26 // Parse the string that defines the undefined constants of the model and make sure that it contains exactly
27 // one value for each undefined constant of the model.
28 std::vector<std::string> definitions;
29 boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
30 for (auto& definition : definitions) {
31 boost::trim(definition);
32
33 // Check whether the token could be a legal constant definition.
34 std::size_t positionOfAssignmentOperator = definition.find('=');
35 STORM_LOG_THROW(positionOfAssignmentOperator != std::string::npos, storm::exceptions::WrongFormatException,
36 "Illegal constant definition string: syntax error.");
37
38 // Now extract the variable name and the value from the string.
39 std::string constantName = definition.substr(0, positionOfAssignmentOperator);
40 boost::trim(constantName);
41 std::string value = definition.substr(positionOfAssignmentOperator + 1);
42 boost::trim(value);
43
44 // Check whether the constant is a legal undefined constant of the program and if so, of what type it is.
45 if (manager.hasVariable(constantName)) {
46 // Get the actual constant and check whether it's in fact undefined.
47 auto const& variable = manager.getVariable(constantName);
48 STORM_LOG_THROW(definedConstants.find(variable) == definedConstants.end(), storm::exceptions::WrongFormatException,
49 "Illegally trying to define constant '" << constantName << "' twice.");
50 definedConstants.insert(variable);
51
52 if (manager.hasVariable(value)) {
53 auto const& valueVariable = manager.getVariable(value);
55 variable.getType() == valueVariable.getType(), storm::exceptions::WrongFormatException,
56 "Illegally trying to define constant '" << constantName << "' by constant '" << valueVariable.getName() << " of different type.");
57 constantDefinitions[variable] = valueVariable.getExpression();
58 } else if (variable.hasBooleanType()) {
59 if (value == "true") {
60 constantDefinitions[variable] = manager.boolean(true);
61 } else if (value == "false") {
62 constantDefinitions[variable] = manager.boolean(false);
63 } else {
64 throw storm::exceptions::WrongFormatException() << "Illegal value for boolean constant: " << value << ".";
65 }
66 } else if (variable.hasIntegerType()) {
67 int_fast64_t integerValue = std::stoll(value);
68 constantDefinitions[variable] = manager.integer(integerValue);
69 } else if (variable.hasRationalType()) {
70 try {
71 storm::RationalNumber rationalValue = storm::utility::convertNumber<storm::RationalNumber>(value);
72 constantDefinitions[variable] = manager.rational(rationalValue);
73 } catch (std::exception& e) {
74 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
75 "Illegal constant definition string '" << constantName << "=" << value << "': " << e.what());
76 }
77 }
78 } else {
79 STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
80 "Illegal constant definition string: unknown undefined constant '" << constantName << "'.");
81 }
82 }
83 }
84
85 return constantDefinitions;
86}
87
88std::vector<std::string> parseCommaSeparatedStrings(std::string const& input) {
89 std::vector<std::string> result;
90 if (!input.empty()) {
91 boost::split(result, input, boost::is_any_of(","));
92 for (auto& entry : result) {
93 boost::trim(entry);
94 }
95 }
96 return result;
97}
98
99} // namespace cli
100} // namespace utility
101} // namespace storm
This class is responsible for managing a set of typed variables and all expressions using these varia...
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
std::vector< std::string > parseCommaSeparatedStrings(std::string const &input)
Definition cli.cpp:88
std::string getCurrentWorkingDirectory()
Definition cli.cpp:15
std::map< storm::expressions::Variable, storm::expressions::Expression > parseConstantDefinitionString(storm::expressions::ExpressionManager const &manager, std::string const &constantDefinitionString)
Definition cli.cpp:20
LabParser.cpp.