diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index be2ec770f..61c245b26 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -44,16 +44,7 @@ Module::Module(const Module& module, const std::string& moduleName, const std::m LOG4CPLUS_DEBUG(logger, "Start renaming " << module.moduleName << " to " << moduleName); // First step: Create new Variables via the adder. - for (BooleanVariable it: module.booleanVariables) { - if (renaming.count(it.getName()) > 0) { - adder->addBooleanVariable(renaming.at(it.getName()), it.getInitialValue()); - } else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!"); - } - for (IntegerVariable it: module.integerVariables) { - if (renaming.count(it.getName()) > 0) { - adder->addIntegerVariable(renaming.at(it.getName()), it.getLowerBound(), it.getUpperBound(), it.getInitialValue()); - } else LOG4CPLUS_ERROR(logger, moduleName << "." << it.getName() << " was not renamed!"); - } + adder->performRenaming(renaming); // Second step: Get all indices of variables that are produced by the renaming. for (auto it: renaming) { diff --git a/src/ir/Module.h b/src/ir/Module.h index 6e653ce47..6fbe1658e 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -24,9 +24,10 @@ namespace storm { namespace ir { struct VariableAdder { - virtual uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init) = 0; - virtual uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr init) = 0; + virtual uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper) = 0; + virtual uint_fast64_t addBooleanVariable(const std::string& name) = 0; virtual std::shared_ptr getVariable(const std::string& name) = 0; + virtual void performRenaming(const std::map& renaming) = 0; }; /*! diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index ce58bd988..c7b0b9141 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -42,7 +42,6 @@ storm::ir::Program PrismParser::parseFile(std::string const& filename) const { try { result = parse(inputFileStream, filename); } catch(std::exception& e) { - std::cerr << "Exception: " << e.what() << std::endl; // In case of an exception properly close the file before passing exception. inputFileStream.close(); throw e; @@ -91,9 +90,6 @@ storm::ir::Program PrismParser::parse(std::istream& inputStream, std::string con // Reset grammars. grammar.resetGrammars(); } catch(const qi::expectation_failure& e) { - // Reset grammars in any case. - grammar.resetGrammars(); - // If the parser expected content different than the one provided, display information // about the location of the error. const boost::spirit::classic::file_position_base& pos = e.first.get_position(); @@ -117,6 +113,9 @@ storm::ir::Program PrismParser::parse(std::istream& inputStream, std::string con msg << std::endl; std::cerr << msg.str(); + + // Reset grammars in any case. + grammar.resetGrammars(); // Now propagate exception. throw storm::exceptions::WrongFileFormatException() << msg.str(); diff --git a/src/parser/PrismParser/PrismGrammar.cpp b/src/parser/PrismParser/PrismGrammar.cpp index ac3f3dbf4..1fb3ff00e 100644 --- a/src/parser/PrismParser/PrismGrammar.cpp +++ b/src/parser/PrismParser/PrismGrammar.cpp @@ -84,14 +84,14 @@ Module PrismGrammar::createModule(const std::string name, std::vector lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids) { //std::cout << "Creating int " << name << " = " << init << std::endl; - uint_fast64_t id = this->state->addIntegerVariable(name, lower, upper, init); + uint_fast64_t id = this->state->addIntegerVariable(name, lower, upper); vars.emplace_back(id, name, lower, upper, init); varids[name] = id; this->state->localIntegerVariables_.add(name, name); } void PrismGrammar::createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids) { //std::cout << "Creating bool " << name << std::endl; - uint_fast64_t id = this->state->addBooleanVariable(name, init); + uint_fast64_t id = this->state->addBooleanVariable(name); vars.emplace_back(id, name, init); varids[name] = id; this->state->localBooleanVariables_.add(name, name); diff --git a/src/parser/PrismParser/VariableState.cpp b/src/parser/PrismParser/VariableState.cpp index dee14bcb3..3634b8954 100644 --- a/src/parser/PrismParser/VariableState.cpp +++ b/src/parser/PrismParser/VariableState.cpp @@ -23,13 +23,18 @@ std::ostream& operator<<(std::ostream& out, qi::symbols& symbols) { symbols.for_each(dump); return out; } +std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& symbols) { + SymbolDump dump(out); + symbols.for_each(dump); + return out; +} VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) { } -uint_fast64_t VariableState::addBooleanVariable(const std::string& name, const std::shared_ptr init) { +uint_fast64_t VariableState::addBooleanVariable(const std::string& name) { if (firstRun) { std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name)); LOG4CPLUS_DEBUG(logger, "Adding boolean variable " << name << " with new id " << this->nextBooleanVariableIndex); @@ -48,7 +53,7 @@ uint_fast64_t VariableState::addBooleanVariable(const std::string& name, const s } } -uint_fast64_t VariableState::addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init) { +uint_fast64_t VariableState::addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper) { if (firstRun) { std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextIntegerVariableIndex, name, lower, upper)); LOG4CPLUS_DEBUG(logger, "Adding integer variable " << name << " with new id " << this->nextIntegerVariableIndex); @@ -106,12 +111,34 @@ std::shared_ptr VariableState::getVariable(const std::string if (res != nullptr) { return *res; } else { - LOG4CPLUS_ERROR(logger, "Getting variable " << name << ", but was not found. This variable does not exist."); return std::shared_ptr(nullptr); } } } +void VariableState::performRenaming(const std::map& renaming) { + for (auto it: renaming) { + std::shared_ptr* original = this->integerVariables_.find(it.first); + if (original != nullptr) { + std::shared_ptr* next = this->integerVariables_.find(it.second); + if (next == nullptr) { + this->addIntegerVariable(it.second, (*original)->getLowerBound(), (*original)->getUpperBound()); + } + } + original = this->booleanVariables_.find(it.first); + if (original != nullptr) { + if (this->booleanVariables_.find(it.second) == nullptr) { + this->addBooleanVariable(it.second); + } + } + std::string* oldCmdName = this->commandNames_.find(it.first); + if (oldCmdName != nullptr) { + LOG4CPLUS_DEBUG(logger, "Adding new command name " << it.second << " due to module renaming."); + this->commandNames_.at(it.second) = it.second; + } + } +} + void VariableState::startModule() { this->localBooleanVariables_.clear(); this->localIntegerVariables_.clear(); diff --git a/src/parser/PrismParser/VariableState.h b/src/parser/PrismParser/VariableState.h index c4046e658..620c029ff 100644 --- a/src/parser/PrismParser/VariableState.h +++ b/src/parser/PrismParser/VariableState.h @@ -46,13 +46,15 @@ public: struct variableNamesStruct : qi::symbols { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; public: - uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr init); - uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init); + uint_fast64_t addBooleanVariable(const std::string& name); + uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper); std::shared_ptr getBooleanVariable(const std::string& name); std::shared_ptr getIntegerVariable(const std::string& name); std::shared_ptr getVariable(const std::string& name); + void performRenaming(const std::map& renaming); + void startModule(); bool isFreeIdentifier(std::string& s) const;