sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Use ValueParsen in DFTJsonParser

tempestpy_adaptions
Matthias Volk 5 years ago
parent
fba3223f63
commit
39cedc223e
5 changed files with 27 additions and 65 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 6
      src/storm-dft/api/storm-dft.h
  2. 14
      src/storm-dft/parser/DFTGalileoParser.cpp
  3. 4
      src/storm-dft/parser/DFTGalileoParser.h
  4. 41
      src/storm-dft/parser/DFTJsonParser.cpp
  5. 27
      src/storm-dft/parser/DFTJsonParser.h

6
src/storm-dft/api/storm-dft.h
View File

@ -33,8 +33,7 @@ namespace storm {
*/
template<typename ValueType>
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonString(std::string const& jsonString) {
storm::parser::DFTJsonParser<ValueType> parser;
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromString(jsonString));
return std::make_shared<storm::storage::DFT<ValueType>>(storm::parser::DFTJsonParser<ValueType>::parseJsonFromString(jsonString));
}
/*!
@ -45,8 +44,7 @@ namespace storm {
*/
template<typename ValueType>
std::shared_ptr<storm::storage::DFT<ValueType>> loadDFTJsonFile(std::string const& file) {
storm::parser::DFTJsonParser<ValueType> parser;
return std::make_shared<storm::storage::DFT<ValueType>>(parser.parseJsonFromFile(file));
return std::make_shared<storm::storage::DFT<ValueType>>(storm::parser::DFTJsonParser<ValueType>::parseJsonFromFile(file));
}
/*!

14
src/storm-dft/parser/DFTGalileoParser.cpp
View File

@ -101,7 +101,7 @@ namespace storm {
std::string name = parseName(tokens[0]);
std::vector<std::string> childNames;
for(unsigned i = 2; i < tokens.size(); ++i) {
for(size_t i = 2; i < tokens.size(); ++i) {
childNames.push_back(parseName(tokens[i]));
}
bool success = true;
@ -113,12 +113,12 @@ namespace storm {
} else if (type == "or") {
success = builder.addOrElement(name, childNames);
} else if (boost::starts_with(type, "vot")) {
unsigned threshold = storm::parser::parseNumber<unsigned>(type.substr(3));
size_t threshold = storm::parser::parseNumber<size_t>(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 = storm::parser::parseNumber<unsigned>(type.substr(0, pos));
unsigned count = storm::parser::parseNumber<unsigned>(type.substr(pos + 2));
size_t threshold = storm::parser::parseNumber<size_t>(type.substr(0, pos));
size_t count = storm::parser::parseNumber<size_t>(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") {
@ -190,7 +190,7 @@ namespace storm {
}
template<typename ValueType>
std::pair<bool, unsigned> DFTGalileoParser<ValueType>::parseNumber(std::string name, std::string& line) {
std::pair<bool, size_t> DFTGalileoParser<ValueType>::parseNumber(std::string name, std::string& line) {
// Build regex for: name=(number)
std::regex nameRegex(name + "\\s*=\\s*([[:digit:]]+)");
std::smatch match;
@ -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, storm::parser::parseNumber<unsigned>(value));
return std::make_pair(true, storm::parser::parseNumber<size_t>(value));
} else {
// No match found
return std::make_pair(false, 0);
@ -236,7 +236,7 @@ namespace storm {
}
}
// Erlang distribution
std::pair<bool, unsigned> resultNum = parseNumber("phases", line);
std::pair<bool, size_t> resultNum = parseNumber("phases", line);
if (resultNum.first) {
STORM_LOG_THROW(distribution == Distribution::None || distribution == Distribution::Exponential, storm::exceptions::WrongFormatException, "A different distribution was already defined for basic element '" << name << "' in line " << lineNo << ".");
erlangPhases = resultNum.second;

4
src/storm-dft/parser/DFTGalileoParser.h
View File

@ -72,9 +72,9 @@ namespace storm {
* @param name Name of BE.
* @param input Input line. The parsed argument will be removed from the line.
*
* @return Pair (success, value). Success is true iff the parsing was succesful. Then value contains the parsed value.
* @return Pair (success, value). Success is true iff the parsing was successful. Then value contains the parsed value.
*/
static std::pair<bool, unsigned> parseNumber(std::string name, std::string& line);
static std::pair<bool, size_t> parseNumber(std::string name, std::string& line);
enum Distribution { None, Constant, Exponential, Erlang, Weibull, LogNormal };
};

41
src/storm-dft/parser/DFTJsonParser.cpp
View File

@ -11,6 +11,7 @@
#include "storm/exceptions/NotSupportedException.h"
#include "storm/utility/macros.h"
#include "storm/utility/file.h"
#include "storm-parsers/parser/ValueParser.h"
namespace storm {
namespace parser {
@ -35,6 +36,10 @@ namespace storm {
template<typename ValueType>
storm::storage::DFT<ValueType> DFTJsonParser<ValueType>::parseJson(json const& jsonInput) {
// Init DFT builder and value parser
storm::builder::DFTBuilder<ValueType> builder;
ValueParser<ValueType> valueParser;
// Try to parse parameters
if (jsonInput.find("parameters") != jsonInput.end()) {
json parameters = jsonInput.at("parameters");
@ -42,10 +47,8 @@ namespace storm {
"Parameters only allowed when using rational functions.");
for (auto it = parameters.begin(); it != parameters.end(); ++it) {
std::string parameter = it.key();
storm::expressions::Variable var = manager->declareRationalVariable(parameter);
identifierMapping.emplace(var.getName(), var);
parser.setIdentifierMapping(identifierMapping);
STORM_LOG_TRACE("Added parameter: " << var.getName());
valueParser.addParameter(parameter);
STORM_LOG_TRACE("Added parameter: " << parameter);
}
}
@ -84,7 +87,7 @@ namespace storm {
success = builder.addOrElement(name, childNames);
} else if (type == "vot") {
std::string votThreshold = parseJsonNumber(data.at("voting"));
success = builder.addVotElement(name, boost::lexical_cast<unsigned>(votThreshold), childNames);
success = builder.addVotElement(name, storm::parser::parseNumber<size_t>(votThreshold), childNames);
} else if (type == "pand") {
success = builder.addPandElement(name, childNames);
} else if (type == "por") {
@ -98,7 +101,7 @@ namespace storm {
} else if (type == "fdep") {
success = builder.addDepElement(name, childNames, storm::utility::one<ValueType>());
} else if (type == "pdep") {
ValueType probability = parseRationalExpression(parseJsonNumber(data.at("probability")));
ValueType probability = valueParser.parseValue(parseJsonNumber(data.at("probability")));
success = builder.addDepElement(name, childNames, probability);
} else if (boost::starts_with(type, "be")) {
std::string distribution = "exp"; // Set default of exponential distribution
@ -108,8 +111,8 @@ namespace storm {
STORM_LOG_THROW(type == "be" || "be_" + distribution == type, storm::exceptions::WrongFormatException,
"BE type '" << type << "' and distribution '" << distribution << " do not agree.");
if (distribution == "exp") {
ValueType failureRate = parseRationalExpression(parseJsonNumber(data.at("rate")));
ValueType dormancyFactor = parseRationalExpression(parseJsonNumber(data.at("dorm")));
ValueType failureRate = valueParser.parseValue(parseJsonNumber(data.at("rate")));
ValueType dormancyFactor = valueParser.parseValue(parseJsonNumber(data.at("dorm")));
bool transient = false;
if (data.count("transient") > 0) {
transient = data.at("transient");
@ -178,28 +181,6 @@ namespace storm {
}
}
template<typename ValueType>
ValueType DFTJsonParser<ValueType>::parseRationalExpression(std::string const& expr) {
STORM_LOG_ASSERT(false, "Specialized method should be called.");
return 0;
}
template<>
double DFTJsonParser<double>::parseRationalExpression(std::string const& expr) {
return boost::lexical_cast<double>(expr);
}
template<>
storm::RationalFunction DFTJsonParser<storm::RationalFunction>::parseRationalExpression(std::string const& expr) {
STORM_LOG_TRACE("Translating expression: " << expr);
storm::expressions::Expression expression = parser.parseFromString(expr);
STORM_LOG_TRACE("Expression: " << expression);
storm::RationalFunction rationalFunction = evaluator.asRational(expression);
STORM_LOG_TRACE("Parsed expression: " << rationalFunction);
return rationalFunction;
}
// Explicitly instantiate the class.
template class DFTJsonParser<double>;
template class DFTJsonParser<RationalFunction>;

27
src/storm-dft/parser/DFTJsonParser.h
View File

@ -2,10 +2,6 @@
#include <map>
#include "storm/storage/expressions/ExpressionManager.h"
#include "storm-parsers/parser/ExpressionParser.h"
#include "storm/storage/expressions/ExpressionEvaluator.h"
#include "storm-dft/storage/dft/DFT.h"
#include "storm-dft/builder/DFTBuilder.h"
@ -19,32 +15,19 @@ namespace storm {
template<typename ValueType>
class DFTJsonParser {
storm::builder::DFTBuilder<ValueType> builder;
std::shared_ptr<storm::expressions::ExpressionManager> manager;
storm::parser::ExpressionParser parser;
storm::expressions::ExpressionEvaluator<ValueType> evaluator;
std::unordered_map<std::string, storm::expressions::Expression> identifierMapping;
public:
DFTJsonParser() : manager(new storm::expressions::ExpressionManager()), parser(*manager), evaluator(*manager) {
}
storm::storage::DFT<ValueType> parseJsonFromString(std::string const& jsonString);
static storm::storage::DFT<ValueType> parseJsonFromString(std::string const& jsonString);
storm::storage::DFT<ValueType> parseJsonFromFile(std::string const& filename);
static storm::storage::DFT<ValueType> parseJsonFromFile(std::string const& filename);
private:
storm::storage::DFT<ValueType> parseJson(json const& jsonInput);
std::string generateUniqueName(std::string const& name);
static storm::storage::DFT<ValueType> parseJson(json const& jsonInput);
ValueType parseRationalExpression(std::string const& expr);
static std::string generateUniqueName(std::string const& name);
std::string parseJsonNumber(json number);
static std::string parseJsonNumber(json number);
};
}
}
Write Preview
Loading…
Cancel
Save