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

If a module is renamed from some other module, this is now kept track of in the respective PRISM classes. 

Former-commit-id: c07e25ac55
main
dehnert 12 years ago
parent
82836f1ad1
commit
873d80cd2d
4 changed files with 191 additions and 47 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 117
      src/parser/PrismParser.cpp
  2. 1
      src/parser/PrismParser.h
  3. 21
      src/storage/prism/Module.cpp
  4. 45
      src/storage/prism/Module.h

117
src/parser/PrismParser.cpp
View File

@ -1,5 +1,6 @@
#include "src/parser/PrismParser.h" #include "src/parser/PrismParser.h"
#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
namespace storm { namespace storm {
@ -7,7 +8,7 @@ namespace storm {
storm::prism::Program PrismParser::parse(std::string const& filename, bool typeCheck) { storm::prism::Program PrismParser::parse(std::string const& filename, bool typeCheck) {
// Open file and initialize result. // Open file and initialize result.
std::ifstream inputFileStream(filename, std::ios::in); 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; storm::prism::Program result;
@ -264,7 +265,7 @@ namespace storm {
} }
bool PrismParser::addInitialStatesExpression(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation) { 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) { if (globalProgramInformation.hasInitialStatesExpression) {
return false; return false;
} }
@ -277,7 +278,11 @@ namespace storm {
if (!this->secondRun) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1.ite(e2, e3); 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1.implies(e2); 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1 || e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try{
return e1 && e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1 > e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1 >= e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1 < e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1 <= e2; 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,11 +374,15 @@ namespace storm {
if (!this->secondRun) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
return e1.iff(e2); return e1.iff(e2);
} else { } else {
return e1 == e2; 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,11 +390,15 @@ namespace storm {
if (!this->secondRun) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) { if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
return e1 ^ e2; return e1 ^ e2;
} else { } else {
return e1 != e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1 + e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1 - e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1 * e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1 / e2; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return !e1; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return -e1; 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return storm::expressions::Expression::minimum(e1, e2); 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return storm::expressions::Expression::maximum(e1, e2); 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1.floor(); 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) { if (!this->secondRun) {
return storm::expressions::Expression::createFalse(); return storm::expressions::Expression::createFalse();
} else { } else {
try {
return e1.ceil(); 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(); return storm::expressions::Expression::createFalse();
} else { } else {
storm::expressions::Expression const* expression = this->identifiers_.find(identifier); 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; return *expression;
} }
} }
storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const { storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
if (!this->secondRun) { 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)); this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
} }
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename()); 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 { storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
if (!this->secondRun) { 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)); this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
} }
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename()); 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 { storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
if (!this->secondRun) { 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)); this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
} }
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename()); 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 { storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) { 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)); this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanConstant(newConstant));
} }
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename()); 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 { storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) { 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)); this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerConstant(newConstant));
} }
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename()); 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 { storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
if (!this->secondRun) { 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)); this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleConstant(newConstant));
} }
return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename()); 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 { storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const {
if (!this->secondRun) { 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); this->identifiers_.add(formulaName, expression);
} }
return storm::prism::Formula(formulaName, expression, this->getFilename()); 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 { storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
if (!this->secondRun) { 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)); this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
} }
return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename()); 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 { 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) { 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)); this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
} }
return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename()); 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 { 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. // Check whether the module to rename actually exists.
auto const& moduleIndexPair = globalProgramInformation.moduleToIndexMap.find(oldModuleName); 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]; storm::prism::Module const& moduleToRename = globalProgramInformation.modules[moduleIndexPair->second];
if (!this->secondRun) { if (!this->secondRun) {
// Register all (renamed) variables for later use. // Register all (renamed) variables for later use.
for (auto const& variable : moduleToRename.getBooleanVariables()) { for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); 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)); this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createBooleanVariable(renamingPair->second));
} }
for (auto const& variable : moduleToRename.getIntegerVariables()) { for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); 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)); this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createIntegerVariable(renamingPair->second));
} }
@ -634,7 +715,7 @@ namespace storm {
std::vector<storm::prism::BooleanVariable> booleanVariables; std::vector<storm::prism::BooleanVariable> booleanVariables;
for (auto const& variable : moduleToRename.getBooleanVariables()) { for (auto const& variable : moduleToRename.getBooleanVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); 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))); 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; std::vector<storm::prism::IntegerVariable> integerVariables;
for (auto const& variable : moduleToRename.getIntegerVariables()) { for (auto const& variable : moduleToRename.getIntegerVariables()) {
auto const& renamingPair = renaming.find(variable.getName()); 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))); 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; ++globalProgramInformation.currentCommandIndex;
} }
return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, this->getFilename());
return storm::prism::Module(newModuleName, booleanVariables, integerVariables, commands, oldModuleName, renaming);
} }
} }

1
src/parser/PrismParser.h
View File

@ -189,7 +189,6 @@ namespace storm {
qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition; qi::rule<Iterator, storm::prism::Program::ModelType(), Skipper> modelTypeDefinition;
// Rules for parsing the program header. // Rules for parsing the program header.
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedConstantDefinition; qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedBooleanConstantDefinition; qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedBooleanConstantDefinition;
qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedIntegerConstantDefinition; qi::rule<Iterator, storm::prism::Constant(), Skipper> undefinedIntegerConstantDefinition;

21
src/storage/prism/Module.cpp
View File

@ -2,10 +2,15 @@
#include "src/exceptions/ExceptionMacros.h" #include "src/exceptions/ExceptionMacros.h"
#include "src/exceptions/OutOfRangeException.h" #include "src/exceptions/OutOfRangeException.h"
#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidAccessException.h"
namespace storm { namespace storm {
namespace prism { 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. // Initialize the internal mappings for fast information retrieval.
this->createMappings(); this->createMappings();
} }
@ -71,6 +76,20 @@ namespace storm {
return actionEntry != this->actions.end(); 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 { std::set<uint_fast64_t> const& Module::getCommandIndicesByAction(std::string const& action) const {
auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action); auto actionsCommandSetPair = this->actionsToCommandIndexMap.find(action);
if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) { if (actionsCommandSetPair != this->actionsToCommandIndexMap.end()) {

45
src/storage/prism/Module.h
View File

@ -2,6 +2,7 @@
#define STORM_STORAGE_PRISM_MODULE_H_ #define STORM_STORAGE_PRISM_MODULE_H_
#include <set> #include <set>
#include <map>
#include <string> #include <string>
#include <vector> #include <vector>
#include <memory> #include <memory>
@ -29,6 +30,21 @@ namespace storm {
*/ */
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); 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. // Create default implementations of constructors/assignment.
Module() = default; Module() = default;
Module(Module const& other) = default; Module(Module const& other) = default;
@ -133,6 +149,29 @@ namespace storm {
*/ */
bool hasAction(std::string const& action) const; 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. * 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. // A map of actions to the set of commands labeled with this action.
std::map<std::string, std::set<uint_fast64_t>> actionsToCommandIndexMap; 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 } // namespace prism

Write Preview
Loading…
Cancel
Save