diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index b96a0b823..ffda5e219 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -1,5 +1,6 @@
#include "src/parser/PrismParser.h"
#include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm {
@@ -7,7 +8,7 @@ namespace storm {
storm::prism::Program PrismParser::parse(std::string const& filename, bool typeCheck) {
// Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in);
- LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file " << filename << ".");
+ LOG_THROW(inputFileStream.good(), storm::exceptions::WrongFormatException, "Unable to read from file '" << filename << "'.");
storm::prism::Program result;
@@ -264,7 +265,7 @@ namespace storm {
}
bool PrismParser::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) {
- LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::WrongFormatException, "Program must not define two initial constructs.");
+ LOG_THROW(!globalProgramInformation.hasInitialStatesExpression, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Program must not define two initial constructs.");
if (globalProgramInformation.hasInitialStatesExpression) {
return false;
}
@@ -277,7 +278,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1.ite(e2, e3);
+ try {
+ return e1.ite(e2, e3);
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -285,7 +290,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1.implies(e2);
+ try {
+ return e1.implies(e2);
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -293,7 +302,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 || e2;
+ try {
+ return e1 || e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -301,7 +314,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 && e2;
+ try{
+ return e1 && e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -309,7 +326,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 > e2;
+ try {
+ return e1 > e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -317,7 +338,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 >= e2;
+ try {
+ return e1 >= e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -325,7 +350,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 < e2;
+ try {
+ return e1 < e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -333,7 +362,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 <= e2;
+ try {
+ return e1 <= e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -341,10 +374,14 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
- return e1.iff(e2);
- } else {
- return e1 == e2;
+ try {
+ if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
+ return e1.iff(e2);
+ } else {
+ return e1 == e2;
+ }
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
@@ -353,10 +390,14 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
- return e1 ^ e2;
- } else {
- return e1 != e2;
+ try {
+ if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
+ return e1 ^ e2;
+ } else {
+ return e1 != e2;
+ }
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
@@ -365,7 +406,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 + e2;
+ try {
+ return e1 + e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -373,7 +418,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 - e2;
+ try {
+ return e1 - e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -381,7 +430,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 * e2;
+ try {
+ return e1 * e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -389,7 +442,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1 / e2;
+ try {
+ return e1 / e2;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -397,7 +454,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return !e1;
+ try {
+ return !e1;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -405,7 +466,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return -e1;
+ try {
+ return -e1;
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -450,7 +515,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return storm::expressions::Expression::minimum(e1, e2);
+ try {
+ return storm::expressions::Expression::minimum(e1, e2);
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -458,7 +527,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return storm::expressions::Expression::maximum(e1, e2);
+ try {
+ return storm::expressions::Expression::maximum(e1, e2);
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -466,7 +539,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1.floor();
+ try {
+ return e1.floor();
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -474,7 +551,11 @@ namespace storm {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
- return e1.ceil();
+ try {
+ return e1.ceil();
+ } catch (storm::exceptions::InvalidTypeException const& e) {
+ LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
+ }
}
}
@@ -483,14 +564,14 @@ namespace storm {
return storm::expressions::Expression::createFalse();
} else {
storm::expressions::Expression const* expression = this->identifiers_.find(identifier);
- LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Undeclared identifier '" << identifier << "'.");
+ LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
return *expression;
}
}
storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
+ LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename());
@@ -498,7 +579,7 @@ namespace storm {
storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
+ LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename());
@@ -506,7 +587,7 @@ namespace storm {
storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
+ LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename());
@@ -514,7 +595,7 @@ namespace storm {
storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
+ LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename());
@@ -522,7 +603,7 @@ namespace storm {
storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
+ LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename());
@@ -530,7 +611,7 @@ namespace storm {
storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << newConstant << "'.");
+ LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
}
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename());
@@ -538,7 +619,7 @@ namespace storm {
storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << formulaName << "'.");
+ LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'.");
this->identifiers_.add(formulaName, expression);
}
return storm::prism::Formula(formulaName, expression, this->getFilename());
@@ -576,7 +657,7 @@ namespace storm {
storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'.");
+ LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
}
return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename());
@@ -584,7 +665,7 @@ namespace storm {
storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
if (!this->secondRun) {
- LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Duplicate identifier '" << variableName << "'.");
+ LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
}
return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
@@ -598,19 +679,19 @@ namespace storm {
storm::prism::Module PrismParser::createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const {
// Check whether the module to rename actually exists.
auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName);
- LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "No module named '" << oldModuleName << "' to rename.");
+ LOG_THROW(moduleIndexPair != globalProgramInformation.moduleToIndexMap.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": No module named '" << oldModuleName << "' to rename.");
storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
if (!this->secondRun) {
// Register all (renamed) variables for later use.
for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
- LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed.");
+ LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createBooleanVariable(renamingPair->second));
}
for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
- LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed.");
+ LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createIntegerVariable(renamingPair->second));
}
@@ -634,7 +715,7 @@ namespace storm {
std::vector<storm::prism::BooleanVariable> booleanVariables;
for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
- LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Boolean variable '" << variable.getName() << " was not renamed.");
+ LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
}
@@ -643,7 +724,7 @@ namespace storm {
std::vector<storm::prism::IntegerVariable> integerVariables;
for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName());
- LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Integer variable '" << variable.getName() << " was not renamed.");
+ LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
}
@@ -676,7 +757,7 @@ namespace storm {
++globalProgramInformation.currentCommandIndex;
}
- return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, this->getFilename());
+ return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, oldModuleName, renaming);
}
}
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index b5013eee8..3312768c3 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -189,7 +189,6 @@ namespace storm {
qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition;
// Rules for parsing the program header.
-
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedIntegerConstantDefinition;
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index f17e1bc12..d7b3fb572 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -2,10 +2,15 @@
#include "src/exceptions/ExceptionMacros.h"
#include "src/exceptions/OutOfRangeException.h"
#include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/InvalidAccessException.h"
namespace storm {
namespace prism {
- Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap() {
+ Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename, uint_fast64_t lineNumber) : Module(moduleName, booleanVariables, integerVariables, commands, "", std::map<std::string, std::string>(), filename, lineNumber) {
+ // Intentionally left empty.
+ }
+
+ Module::Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename, uint_fast64_t lineNumber) : LocatedInformation(filename, lineNumber), moduleName(moduleName), booleanVariables(booleanVariables), booleanVariableToIndexMap(), integerVariables(integerVariables), integerVariableToIndexMap(), commands(commands), actions(), actionsToCommandIndexMap(), renamedFromModule(renamedFromModule), renaming(renaming) {
// Initialize the internal mappings for fast information retrieval.
this->createMappings();
}
@@ -71,6 +76,20 @@ namespace storm {
return actionEntry != this->actions.end();
}
+ bool Module::isRenamedFromModule() const {
+ return this->renamedFromModule != "";
+ }
+
+ std::string const& Module::getBaseModule() const {
+ LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve base module of module that was not created by renaming.");
+ return this->renamedFromModule;
+ }
+
+ std::map<std::string, std::string> const& Module::getRenaming() const {
+ LOG_THROW(this->isRenamedFromModule(), storm::exceptions::InvalidAccessException, "Unable to retrieve renaming of module that was not created by renaming.");
+ return this->renaming;
+ }
+
std::set<uint_fast64_t> const& Module::getCommandIndicesByAction(std::string const& action) const {
auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action);
if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) {
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index f4fd21f29..1031cbf27 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -2,6 +2,7 @@
#define STORM_STORAGE_PRISM_MODULE_H_
#include <set>
+#include <map>
#include <string>
#include <vector>
#include <memory>
@@ -28,7 +29,22 @@ namespace storm {
* @param lineNumber The line number in which the module is defined.
*/
Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& filename = "", uint_fast64_t lineNumber = 0);
-
+
+ /*!
+ * Creates a module with the given name, variables and commands that is marked as being renamed from the
+ * given module with the given renaming.
+ *
+ * @param moduleName The name of the module.
+ * @param booleanVariables The boolean variables defined by the module.
+ * @param integerVariables The integer variables defined by the module.
+ * @param commands The commands of the module.
+ * @param renamedFromModule The name of the module from which this module was renamed.
+ * @param renaming The renaming of identifiers used to create this module.
+ * @param filename The filename in which the module is defined.
+ * @param lineNumber The line number in which the module is defined.
+ */
+ Module(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, std::string const& renamedFromModule, std::map<std::string, std::string> const& renaming, std::string const& filename = "", uint_fast64_t lineNumber = 0);
+
// Create default implementations of constructors/assignment.
Module() = default;
Module(Module const& other) = default;
@@ -133,6 +149,29 @@ namespace storm {
*/
bool hasAction(std::string const& action) const;
+ /*!
+ * Retrieves whether this module was created from another module via renaming.
+ *
+ * @return True iff the module was created via renaming.
+ */
+ bool isRenamedFromModule() const;
+
+ /*!
+ * If the module was created via renaming, this method retrieves the name of the module that was used as the
+ * in the base in the renaming process.
+ *
+ * @return The name of the module from which this module was created via renaming.
+ */
+ std::string const& getBaseModule() const;
+
+ /*!
+ * If the module was created via renaming, this method returns the applied renaming of identifiers used for
+ * the renaming process.
+ *
+ * @return A mapping of identifiers to new identifiers that was used in the renaming process.
+ */
+ std::map<std::string, std::string> const& getRenaming() const;
+
/*!
* Retrieves the indices of all commands within this module that are labelled by the given action.
*
@@ -188,6 +227,12 @@ namespace storm {
// A map of actions to the set of commands labeled with this action.
std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap;
+
+ // This string indicates whether and from what module this module was created via renaming.
+ std::string renamedFromModule;
+
+ // If the module was created by renaming, this mapping contains the provided renaming of identifiers.
+ std::map<std::string, std::string> renaming;
};
} // namespace prism