|
@ -4,6 +4,7 @@ |
|
|
#include <fstream>
|
|
|
#include <fstream>
|
|
|
#include <boost/algorithm/string.hpp>
|
|
|
#include <boost/algorithm/string.hpp>
|
|
|
#include <boost/lexical_cast.hpp>
|
|
|
#include <boost/lexical_cast.hpp>
|
|
|
|
|
|
#include <boost/algorithm/string/replace.hpp>
|
|
|
#include "storm/storage/expressions/ExpressionManager.h"
|
|
|
#include "storm/storage/expressions/ExpressionManager.h"
|
|
|
#include "storm/exceptions/NotImplementedException.h"
|
|
|
#include "storm/exceptions/NotImplementedException.h"
|
|
|
#include "storm/exceptions/FileIoException.h"
|
|
|
#include "storm/exceptions/FileIoException.h"
|
|
@ -35,6 +36,11 @@ namespace storm { |
|
|
} |
|
|
} |
|
|
} |
|
|
} |
|
|
|
|
|
|
|
|
|
|
|
template<typename ValueType> |
|
|
|
|
|
std::string DFTGalileoParser<ValueType>::parseNodeIdentifier(std::string const& name) { |
|
|
|
|
|
return boost::replace_all_copy(name, "'", "__prime__"); |
|
|
|
|
|
} |
|
|
|
|
|
|
|
|
template<typename ValueType> |
|
|
template<typename ValueType> |
|
|
void DFTGalileoParser<ValueType>::readFile(const std::string& filename) { |
|
|
void DFTGalileoParser<ValueType>::readFile(const std::string& filename) { |
|
|
// constants
|
|
|
// constants
|
|
@ -84,11 +90,11 @@ namespace storm { |
|
|
} else { |
|
|
} else { |
|
|
std::vector<std::string> tokens; |
|
|
std::vector<std::string> tokens; |
|
|
boost::split(tokens, line, boost::is_any_of(" ")); |
|
|
boost::split(tokens, line, boost::is_any_of(" ")); |
|
|
std::string name(stripQuotsFromName(tokens[0])); |
|
|
|
|
|
|
|
|
std::string name(parseNodeIdentifier(stripQuotsFromName(tokens[0]))); |
|
|
|
|
|
|
|
|
std::vector<std::string> childNames; |
|
|
std::vector<std::string> childNames; |
|
|
for(unsigned i = 2; i < tokens.size(); ++i) { |
|
|
for(unsigned i = 2; i < tokens.size(); ++i) { |
|
|
childNames.push_back(stripQuotsFromName(tokens[i])); |
|
|
|
|
|
|
|
|
childNames.push_back(parseNodeIdentifier(stripQuotsFromName(tokens[i]))); |
|
|
} |
|
|
} |
|
|
if(tokens[1] == "and") { |
|
|
if(tokens[1] == "and") { |
|
|
success = builder.addAndElement(name, childNames); |
|
|
success = builder.addAndElement(name, childNames); |
|
|