diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp index df56b6bc5..a8998a715 100644 --- a/src/ir/Module.cpp +++ b/src/ir/Module.cpp @@ -38,7 +38,7 @@ Module::Module(std::string const& moduleName, this->collectActions(); } -Module::Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap, std::shared_ptr const& adder) +Module::Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap, std::shared_ptr const& variableState) : moduleName(newModuleName), booleanVariableToLocalIndexMap(oldModule.booleanVariableToLocalIndexMap), integerVariableToLocalIndexMap(oldModule.integerVariableToLocalIndexMap) { LOG4CPLUS_TRACE(logger, "Start renaming " << oldModule.getName() << " to " << moduleName << "."); @@ -51,8 +51,8 @@ Module::Module(Module const& oldModule, std::string const& newModuleName, std::m LOG4CPLUS_ERROR(logger, "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed."); throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << moduleName << "." << booleanVariable.getName() << " was not renamed."; } else { - this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, adder->getNextGlobalBooleanVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap); - adder->addBooleanVariable(renamingPair->second); + this->booleanVariables.emplace_back(booleanVariable, renamingPair->second, variableState->getNextGlobalBooleanVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap); + variableState->addBooleanVariable(renamingPair->second); } } // Now do the same for the integer variables. @@ -63,8 +63,8 @@ Module::Module(Module const& oldModule, std::string const& newModuleName, std::m LOG4CPLUS_ERROR(logger, "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed."); throw storm::exceptions::InvalidArgumentException() << "Integer variable " << moduleName << "." << integerVariable.getName() << " was not renamed."; } else { - this->integerVariables.emplace_back(integerVariable, renamingPair->second, adder->getNextGlobalIntegerVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap); - adder->addIntegerVariable(renamingPair->second); + this->integerVariables.emplace_back(integerVariable, renamingPair->second, variableState->getNextGlobalIntegerVariableIndex(), renaming, booleanVariableToIndexMap, integerVariableToIndexMap); + variableState->addIntegerVariable(renamingPair->second); } } diff --git a/src/ir/Module.h b/src/ir/Module.h index 08c0dcefc..b57b9e70d 100644 --- a/src/ir/Module.h +++ b/src/ir/Module.h @@ -14,43 +14,16 @@ #include #include +#include "VariableStateInterface.h" #include "BooleanVariable.h" #include "IntegerVariable.h" -#include "expressions/VariableExpression.h" #include "Command.h" +#include "expressions/VariableExpression.h" namespace storm { namespace ir { - struct VariableAdder { - /*! - * Adds an integer variable with the given name, lower and upper bound. - * - * @param name The name of the boolean variable to add. - */ - uint_fast64_t addBooleanVariable(std::string const& name) = 0; - - /*! - * Adds an integer variable with the given name, lower and upper bound. - * - * @param name The name of the integer variable to add. - * @param lower The lower bound of the integer variable. - * @param upper The upper bound of the integer variable. - */ - uint_fast64_t addIntegerVariable(std::string const& name) = 0; - - /*! - * Retrieves the next free (global) index for a boolean variable. - */ - uint_fast64_t getNextGlobalBooleanVariableIndex() const = 0; - - /*! - * Retrieves the next free (global) index for a integer variable. - */ - uint_fast64_t getNextGlobalIntegerVariableIndex() const = 0; - }; - /*! * A class representing a module. */ @@ -92,7 +65,7 @@ public: * @param adder An instance of the VariableAdder interface that keeps track of all the variables in the probabilistic * program. */ - Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap, std::shared_ptr const& adder); + Module(Module const& oldModule, std::string const& newModuleName, std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap, std::shared_ptr const& variableState); /*! * Retrieves the number of boolean variables in the module. diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h index 54bebce72..fa7cfc6c1 100644 --- a/src/ir/expressions/VariableExpression.h +++ b/src/ir/expressions/VariableExpression.h @@ -8,11 +8,13 @@ #ifndef VARIABLEEXPRESSION_H_ #define VARIABLEEXPRESSION_H_ -#include "src/ir/expressions/BaseExpression.h" - #include #include +#include "src/ir/VariableStateInterface.h" +#include "BaseExpression.h" +#include "src/exceptions/InvalidArgumentException.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -25,32 +27,41 @@ namespace expressions { class VariableExpression : public BaseExpression { public: - VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName, - std::shared_ptr lowerBound = std::shared_ptr(nullptr), - std::shared_ptr upperBound = std::shared_ptr(nullptr)) - : BaseExpression(type), index(index), variableName(variableName), - lowerBound(lowerBound), upperBound(upperBound) { + VariableExpression(ReturnType type, std::string variableName) : BaseExpression(type), localIndex(0), globalIndex(0), variableName(variableName) { + // Nothing to do here. + } + + VariableExpression(ReturnType type, uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string variableName) + : BaseExpression(type), localIndex(localIndex), globalIndex(globalIndex), variableName(variableName) { + // Nothing to do here. } + + VariableExpression(VariableExpression const& oldExpression, std::string const& newName, uint_fast64_t newGlobalIndex) + : BaseExpression(oldExpression.getType()), localIndex(oldExpression.localIndex), globalIndex(newGlobalIndex), variableName(newName) { + // Nothing to do here. + } virtual ~VariableExpression() { + // Nothing to do here. } - virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) { - std::shared_ptr lower = this->lowerBound, upper = this->upperBound; - if (lower != nullptr) lower = lower->clone(renaming, bools, ints); - if (upper != nullptr) upper = upper->clone(renaming, bools, ints); - if (renaming.count(this->variableName) > 0) { - std::string newName = renaming.at(this->variableName); + virtual std::shared_ptr clone(std::map const& renaming, std::shared_ptr const& variableState) { + // Perform the proper cloning. + } + + virtual std::shared_ptr clone(std::map const& renaming, std::map const& booleanVariableToIndexMap, std::map const& integerVariableToIndexMap) { + auto renamingPair = renaming.find(this->variableName); + if (renamingPair != renaming.end()) { if (this->getType() == bool_) { - return std::shared_ptr(new VariableExpression(bool_, bools.at(newName), newName, lower, upper)); + return std::shared_ptr(new VariableExpression(bool_, this->localIndex, booleanVariableToIndexMap.at(renamingPair->second), renamingPair->second)); } else if (this->getType() == int_) { - return std::shared_ptr(new VariableExpression(int_, ints.at(newName), newName, lower, upper)); + return std::shared_ptr(new VariableExpression(int_, this->localIndex, integerVariableToIndexMap.at(renamingPair->second), renamingPair->second)); } else { - LOG4CPLUS_ERROR(logger, "ERROR: Renaming variable " << this->variableName << " that is neither bool nor int."); - return std::shared_ptr(nullptr); + LOG4CPLUS_ERROR(logger, "Renaming variable " << this->variableName << " that is neither bool nor int."); + throw storm::exceptions::InvalidArgumentException() << "Renaming variable " << this->variableName << " that is neither bool nor int."; } } else { - return std::shared_ptr(new VariableExpression(this->getType(), this->index, this->variableName, lower, upper)); + return std::shared_ptr(new VariableExpression(this->getType(), this->localIndex, this->globalIndex, this->variableName)); } } @@ -67,14 +78,6 @@ public: virtual std::string dump(std::string prefix) const { std::stringstream result; result << prefix << this->variableName << " " << index << std::endl; - if (this->lowerBound != nullptr) { - result << prefix << "lower bound" << std::endl; - result << this->lowerBound->dump(prefix + "\t"); - } - if (this->upperBound != nullptr) { - result << prefix << "upper bound" << std::endl; - result << this->upperBound->dump(prefix + "\t"); - } return result.str(); } @@ -84,7 +87,7 @@ public: } if (variableValues != nullptr) { - return variableValues->second[index]; + return variableValues->second[globalIndex]; } else { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" << " involving variables without variable values."; @@ -97,7 +100,7 @@ public: } if (variableValues != nullptr) { - return variableValues->first[index]; + return variableValues->first[globalIndex]; } else { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression" << " involving variables without variable values."; @@ -117,24 +120,18 @@ public: return variableName; } - std::shared_ptr const& getLowerBound() const { - return lowerBound; + uint_fast64_t getLocalVariableIndex() const { + return this->localIndex; } - - std::shared_ptr const& getUpperBound() const { - return upperBound; - } - - uint_fast64_t getVariableIndex() const { - return this->index; + + uint_fast64_t getGlobalVariableIndex() const { + return this->globalIndex; } private: - uint_fast64_t index; + uint_fast64_t localIndex; + uint_fast64_t globalIndex; std::string variableName; - - std::shared_ptr lowerBound; - std::shared_ptr upperBound; }; } diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 736fce64a..79459f3e7 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -5,6 +5,11 @@ * Author: chris */ +// Needed for file IO. +#include +#include +#include + #include "PrismGrammar.h" #include "src/utility/OsDetection.h" @@ -18,11 +23,6 @@ #include "src/parser/prismparser/IdentifierGrammars.h" #include "src/parser/prismparser/VariableState.h" -// Needed for file IO. -#include -#include -#include - #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -41,37 +41,39 @@ void dump(const std::string& s) { std::cerr << "Dump: " << s << std::endl; } -std::shared_ptr PrismGrammar::addIntegerConstant(const std::string& name, const std::shared_ptr value) { +std::shared_ptr PrismGrammar::addIntegerConstant(std::string const& name, std::shared_ptr const& value) { this->state->integerConstants_.add(name, value); this->state->allConstantNames_.add(name, name); return value; } -void PrismGrammar::addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping) { +void PrismGrammar::addLabel(std::string const& name, std::shared_ptr const& value, std::map>& nameToExpressionMap) { this->state->labelNames_.add(name, name); - mapping[name] = value; + nameToExpressionMap[name] = value; } -void PrismGrammar::addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { - //std::cout << "Adding int assignment for " << variable << std::endl; + +void PrismGrammar::addIntegerAssignment(std::string const& variable, std::shared_ptr const& value, std::map& variableToAssignmentMap) { this->state->assignedLocalIntegerVariables_.add(variable, variable); - mapping[variable] = Assignment(variable, value); + variableToAssignmentMap[variable] = Assignment(variable, value); } -void PrismGrammar::addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping) { - //std::cout << "Adding bool assignment for " << variable << std::endl; + +void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr const& value, std::map& variableToAssigmentMap) { this->state->assignedLocalBooleanVariables_.add(variable, variable); - mapping[variable] = Assignment(variable, value); + variableToAssigmentMap[variable] = Assignment(variable, value); } -Module PrismGrammar::renameModule(const std::string& name, const std::string& oldname, std::map& mapping) { + +Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map& renaming) { this->state->moduleNames_.add(name, name); Module* old = this->moduleMap_.find(oldname); if (old == nullptr) { - LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldname << " does not exist!"); - throw "Renaming module failed"; + LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldName << " does not exist."); + throw storm::exceptions::InvalidArgumentException() << "Renaming module failed: module " << oldName << " does not exist."; } - Module res(*old, name, mapping, this->state); + Module res(*old, newName, renaming, this->state); this->moduleMap_.at(name) = res; return res; } + Module PrismGrammar::createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands) { this->state->moduleNames_.add(name, name); Module res(name, bools, ints, boolids, intids, commands); @@ -80,14 +82,12 @@ 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); 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); vars.emplace_back(id, name, init); varids[name] = id; diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index a512befb9..6aeb0282e 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -47,8 +47,21 @@ class PrismGrammar : public qi::grammar< >, Skipper> { public: + /*! + * Default constructor that creates an empty and functional grammar. + */ PrismGrammar(); + + /*! + * Puts all sub-grammars into the mode for performing the second run. A two-run model was chosen + * because modules can involve variables that are only declared afterwards, so the first run + * creates all variables and the second one tries to parse the full model. + */ void prepareForSecondRun(); + + /*! + * Resets all sub-grammars, i.e. puts them into an initial state. + */ void resetGrammars(); private: @@ -122,15 +135,88 @@ private: storm::parser::prism::modelTypeStruct modelType_; storm::parser::prism::relationalOperatorStruct relations_; - std::shared_ptr addIntegerConstant(const std::string& name, const std::shared_ptr value); - void addLabel(const std::string& name, std::shared_ptr value, std::map>& mapping); - void addBoolAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); - void addIntAssignment(const std::string& variable, std::shared_ptr value, std::map& mapping); - Module renameModule(const std::string& name, const std::string& oldname, std::map& mapping); - Module createModule(const std::string name, std::vector& bools, std::vector& ints, std::map& boolids, std::map intids, std::vector commands); - - void createIntegerVariable(const std::string name, std::shared_ptr lower, std::shared_ptr upper, std::shared_ptr init, std::vector& vars, std::map& varids); - void createBooleanVariable(const std::string name, std::shared_ptr init, std::vector& vars, std::map& varids); + /*! + * Adds a constant of type integer with the given name and value. + * + * @param name The name of the constant. + * @param value An expression definining the value of the constant. + */ + std::shared_ptr addIntegerConstant(std::string const& name, std::shared_ptr const& value); + + /*! + * Adds a label with the given name and expression to the given label-to-expression map. + * + * @param name The name of the label. + * @param expression The expression associated with the label. + * @param nameToExpressionMap The map to which the label is added. + */ + void addLabel(std::string const& name, std::shared_ptr const& value, std::map>& nameToExpressionMap); + + /*! + * Adds a boolean assignment for the given variable with the given expression and adds it to the + * provided variable-to-assignment map. + * + * @param variable The name of the variable that the assignment targets. + * @param expression The expression that is assigned to the variable. + * @param variableToAssignmentMap The map to which the assignment is added. + */ + void addBooleanAssignment(std::string const& variable, std::shared_ptr const& expression, std::map& variableToAssignmentMap); + + /*! + * Adds a boolean assignment for the given variable with the given expression and adds it to the + * provided variable-to-assignment map. + * + * @param variable The name of the variable that the assignment targets. + * @param expression The expression that is assigned to the variable. + * @param variableToAssignmentMap The map to which the assignment is added. + */ + void addIntegerAssignment(std::string const& variable, std::shared_ptr const& value, std::map& variableToAssignmentMap); + + /*! + * Creates a module by renaming, i.e. takes the module given by the old name, creates a new module + * with the given name which renames all identifiers according to the given mapping. + * + * @param name The name of the new module. + * @param oldName The name of the module that is to be copied (modulo renaming). + * @param renaming A mapping from identifiers to their new names. + */ + Module renameModule(std::string const& name, std::string const& oldName, std::map& renaming); + + /*! + * Creates a new module with the given name, boolean and integer variables and commands. + * + * @param name The name of the module to create. + * @param booleanVariables The boolean variables of the module. + * @param integerVariables The integer variables of the module. + * @param booleanVariableToLocalIndexMap A mapping of boolean variables to module-local indices. + * @param integerVariableToLocalIndexMap A mapping of boolean variables to module-local indices. + * @param commands The commands associated with this module. + */ + Module createModule(std::string const& name, std::vector const& booleanVariables, std::vector const& integerVariables, std::map const& booleanVariableToLocalIndexMap, std::map integerVariableToLocalIndexMap, std::vector const& commands); + + /*! + * Creates an integer variable with the given name, domain and initial value and adds it to the + * provided list of integer variables and the given mappings. + * + * @param name The name of the integer variable. + * @param lower The expression that defines the lower bound of the domain. + * @param upper The expression that defines the upper bound of the domain. + * @param init The expression that defines the initial value of the variable. + * @param integerVariableToLocalIndexMap A mapping of integer variables to local indices. + * @param integerVariableToGlobalIndexMap A mapping of integer variables to global indices. + */ + void createIntegerVariable(std::string const& name, std::shared_ptr const& lower, std::shared_ptr const& upper, std::shared_ptr const& init, std::vector& integerVariables, std::map& integerVariableToLocalIndexMap, std::map& integerVariableToGlobalIndexMap); + + /*! + * Creates an boolean variable with the given name and initial value and adds it to the + * provided list of boolean variables and the given mappings. + * + * @param name The name of the boolean variable. + * @param init The expression that defines the initial value of the variable. + * @param booleanVariableToLocalIndexMap A mapping of boolean variables to local indices. + * @param booleanVariableToGlobalIndexMap A mapping of boolean variables to global indices. + */ + void createBooleanVariable(std::string const& name, std::shared_ptr const& init, std::vector& booleanVariables, std::map& booleanVariableToLocalIndexMap, std::map& booleanVariableToGlobalIndexMap); }; diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp index 29feb025b..c0e57237c 100644 --- a/src/parser/prismparser/VariableState.cpp +++ b/src/parser/prismparser/VariableState.cpp @@ -31,10 +31,18 @@ std::ostream& operator<<(std::ostream& out, VariableState::variableNamesStruct& } -VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0) { +VariableState::VariableState(bool firstRun) : firstRun(firstRun), keywords(), nextLocalBooleanVariableIndex(0), nextLocalIntegerVariableIndex(0), nextGlobalBooleanVariableIndex(0), nextGlobalIntegerVariableIndex(0) { // Nothing to do here. } +uint_fast64_t VariableState::getNextLocalBooleanVariableIndex() const { + return this->nextLocalBooleanVariableIndex; +} + +uint_fast64_t VariableState::getNextLocalIntegerVariableIndex() const { + return this->nextLocalIntegerVariableIndex; +} + uint_fast64_t VariableState::getNextGlobalBooleanVariableIndex() const { return this->nextGlobalBooleanVariableIndex; } @@ -43,17 +51,18 @@ uint_fast64_t VariableState::getNextGlobalIntegerVariableIndex() const { return this->nextGlobalIntegerVariableIndex; } -uint_fast64_t VariableState::addBooleanVariable(std::string const& name) { +std::pair VariableState::addBooleanVariable(std::string const& name) { if (firstRun) { LOG4CPLUS_TRACE(logger, "Adding boolean variable " << name << " with new id " << this->nextGlobalBooleanVariableIndex << "."); - this->booleanVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextGlobalBooleanVariableIndex, name))); + this->booleanVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextLocalBooleanVariableIndex, this->nextGlobalBooleanVariableIndex, name))); this->booleanVariableNames_.add(name, name); ++this->nextGlobalBooleanVariableIndex; - return this->nextGlobalBooleanVariableIndex - 1; + ++this->nextLocalBooleanVariableIndex; + return std::make_pair(this->nextLocalBooleanVariableIndex - 1, this->nextGlobalBooleanVariableIndex - 1); } else { - std::shared_ptr res = this->booleanVariables_.at(name); - if (res != nullptr) { - return res->getVariableIndex(); + std::shared_ptr variableExpression = this->booleanVariables_.at(name); + if (variableExpression != nullptr) { + return std::make_pair(variableExpression->getLocalVariableIndex(), variableExpression->getGlobalVariableIndex()); } else { LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; @@ -61,17 +70,18 @@ uint_fast64_t VariableState::addBooleanVariable(std::string const& name) { } } -uint_fast64_t VariableState::addIntegerVariable(std::string const& name) { +std::pair VariableState::addIntegerVariable(std::string const& name) { if (firstRun) { LOG4CPLUS_TRACE(logger, "Adding integer variable " << name << " with new id " << this->nextGlobalIntegerVariableIndex << "."); - this->integerVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextGlobalIntegerVariableIndex, name))); + this->integerVariables_.add(name, std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextLocalIntegerVariableIndex, this->nextGlobalIntegerVariableIndex, name))); this->integerVariableNames_.add(name, name); ++this->nextGlobalIntegerVariableIndex; - return this->nextGlobalIntegerVariableIndex - 1; + ++this->nextLocalIntegerVariableIndex; + return std::make_pair(this->nextLocalIntegerVariableIndex, this->nextGlobalIntegerVariableIndex - 1); } else { - std::shared_ptr res = this->integerVariables_.at(name); - if (res != nullptr) { - return res->getVariableIndex(); + std::shared_ptr variableExpression = this->integerVariables_.at(name); + if (variableExpression != nullptr) { + return std::make_pair(variableExpression->getLocalVariableIndex(), variableExpression->getGlobalVariableIndex()); } else { LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; @@ -79,14 +89,14 @@ uint_fast64_t VariableState::addIntegerVariable(std::string const& name) { } } -std::shared_ptr VariableState::getBooleanVariableExpression(std::string const& name) { - std::shared_ptr* res = this->booleanVariables_.find(name); - if (res != nullptr) { - return *res; +std::shared_ptr VariableState::getBooleanVariableExpression(std::string const& name) const { + std::shared_ptr* variableExpression = this->booleanVariables_.find(name); + if (variableExpression != nullptr) { + return *variableExpression; } else { if (firstRun) { LOG4CPLUS_TRACE(logger, "Trying to retrieve boolean variable " << name << " that was not yet created; returning dummy instead."); - return std::shared_ptr(BaseExpression::bool_, 0, name); + return std::shared_ptr(new VariableExpression(BaseExpression::bool_, name)); } else { LOG4CPLUS_ERROR(logger, "Boolean variable " << name << " does not exist."); throw storm::exceptions::InvalidArgumentException() << "Boolean variable " << name << " does not exist."; @@ -94,14 +104,14 @@ std::shared_ptr VariableState::getBooleanVariableExpression( } } -std::shared_ptr VariableState::getIntegerVariableExpression(std::string const& name) { - std::shared_ptr* res = this->integerVariables_.find(name); - if (res != nullptr) { - return *res; +std::shared_ptr VariableState::getIntegerVariableExpression(std::string const& name) const { + std::shared_ptr* variableExpression = this->integerVariables_.find(name); + if (variableExpression != nullptr) { + return *variableExpression; } else { if (firstRun) { LOG4CPLUS_TRACE(logger, "Trying to retrieve integer variable " << name << " that was not yet created; returning dummy instead."); - return std::shared_ptr(BaseExpression::int_, 0, name); + return std::shared_ptr(new VariableExpression(BaseExpression::int_, name)); } else { LOG4CPLUS_ERROR(logger, "Integer variable " << name << " does not exist."); throw storm::exceptions::InvalidArgumentException() << "Integer variable " << name << " does not exist."; @@ -109,10 +119,10 @@ std::shared_ptr VariableState::getIntegerVariableExpression( } } -std::shared_ptr VariableState::getVariableExpression(std::string const& name) { - std::shared_ptr* res = this->integerVariables_.find(name); - if (res != nullptr) { - return *res; +std::shared_ptr VariableState::getVariableExpression(std::string const& name) const { + std::shared_ptr* variableExpression = this->integerVariables_.find(name); + if (variableExpression != nullptr) { + return *variableExpression; } LOG4CPLUS_ERROR(logger, "Variable " << name << " does not exist."); throw storm::exceptions::InvalidArgumentException() << "Variable " << name << " does not exist."; @@ -121,6 +131,8 @@ std::shared_ptr VariableState::getVariableExpression(std::st void VariableState::clearLocalVariables() { this->localBooleanVariables_.clear(); this->localIntegerVariables_.clear(); + this->nextLocalBooleanVariableIndex = 0; + this->nextLocalIntegerVariableIndex = 0; } bool VariableState::isFreeIdentifier(std::string const& identifier) const { diff --git a/src/parser/prismparser/VariableState.h b/src/parser/prismparser/VariableState.h index 953f46d2b..60ff2772b 100644 --- a/src/parser/prismparser/VariableState.h +++ b/src/parser/prismparser/VariableState.h @@ -27,10 +27,18 @@ template std::ostream& operator<<(std::ostream& out, qi::symbols& symbols); /*! - * This class contains the state that is needed during the parsing of a prism model. + * This class contains the internal state that is needed for parsing a PRISM model. */ struct VariableState : public storm::ir::VariableAdder { + /*! + * Creates a new variable state object. By default, this object will be set to a state in which + * it is ready for performing a first run on some input. The first run creates all variables + * while the second one checks for the correct usage of variables in expressions. + * + * @param firstRun If set, this object will be in a state ready for performing the first run. If + * set to false, this object will assume that it has all variable data already. + */ VariableState(bool firstRun = true); /*! @@ -43,6 +51,30 @@ struct VariableState : public storm::ir::VariableAdder { */ keywordsStruct keywords; + /*! + * Internal counter for the local index of the next new boolean variable. + */ + uint_fast64_t nextLocalBooleanVariableIndex; + + /*! + * Retrieves the next free local index for a boolean variable. + * + * @return The next free local index for a boolean variable. + */ + uint_fast64_t getNextLocalBooleanVariableIndex() const; + + /*! + * Internal counter for the local index of the next new integer variable. + */ + uint_fast64_t nextLocalIntegerVariableIndex; + + /*! + * Retrieves the next free global index for a integer variable. + * + * @return The next free global index for a integer variable. + */ + uint_fast64_t getNextLocalIntegerVariableIndex() const; + /*! * Internal counter for the index of the next new boolean variable. */ @@ -81,17 +113,17 @@ struct VariableState : public storm::ir::VariableAdder { * Adds a new boolean variable with the given name. * * @param name The name of the variable. - * @return The global index of the variable. + * @return A pair containing the local and global index of the variable. */ - uint_fast64_t addBooleanVariable(std::string const& name); + std::pair addBooleanVariable(std::string const& name); /*! * Adds a new integer variable with the given name. * * @param name The name of the variable. - * @return The global index of the variable. + * @return A pair containing the local and global index of the variable. */ - uint_fast64_t addIntegerVariable(std::string const& name); + std::pair addIntegerVariable(std::string const& name); /*! * Retrieves the variable expression for the boolean variable with the given name. @@ -99,7 +131,7 @@ struct VariableState : public storm::ir::VariableAdder { * @param name The name of the boolean variable for which to retrieve the variable expression. * @return The variable expression for the boolean variable with the given name. */ - std::shared_ptr getBooleanVariableExpression(std::string const& name); + std::shared_ptr getBooleanVariableExpression(std::string const& name) const; /*! * Retrieves the variable expression for the integer variable with the given name. @@ -107,7 +139,7 @@ struct VariableState : public storm::ir::VariableAdder { * @param name The name of the integer variable for which to retrieve the variable expression. * @return The variable expression for the integer variable with the given name. */ - std::shared_ptr getIntegerVariableExpression(std::string const& name); + std::shared_ptr getIntegerVariableExpression(std::string const& name) const; /*! * Retrieve the variable expression for the variable with the given name. @@ -115,7 +147,7 @@ struct VariableState : public storm::ir::VariableAdder { * @param name The name of the variable for which to retrieve the variable expression. * @return The variable expression for the variable with the given name. */ - std::shared_ptr getVariableExpression(std::string const& name); + std::shared_ptr getVariableExpression(std::string const& name) const; /*! * Clears all local variables. diff --git a/src/parser/prismparser/VariableStateInterface.h b/src/parser/prismparser/VariableStateInterface.h new file mode 100644 index 000000000..d6489cb34 --- /dev/null +++ b/src/parser/prismparser/VariableStateInterface.h @@ -0,0 +1,69 @@ +/* + * VariableStateInterface.h + * + * Created on: 10.06.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_VARIABLESTATEINTERFACE_H_ +#define STORM_IR_VARIABLESTATEINTERFACE_H_ + +namespace storm { +namespace ir { + +struct VariableStateInterface { + /*! + * Adds an integer variable with the given name, lower and upper bound. + * + * @param name The name of the boolean variable to add. + */ + virtual uint_fast64_t addBooleanVariable(std::string const& name) = 0; + + /*! + * Adds an integer variable with the given name, lower and upper bound. + * + * @param name The name of the integer variable to add. + * @param lower The lower bound of the integer variable. + * @param upper The upper bound of the integer variable. + */ + virtual uint_fast64_t addIntegerVariable(std::string const& name) = 0; + + /*! + * Retrieves the variable expression for the boolean variable with the given name. + * + * @param name The name of the boolean variable for which to retrieve the variable expression. + * @return The variable expression for the boolean variable with the given name. + */ + std::shared_ptr getBooleanVariableExpression(std::string const& name) const = 0; + + /*! + * Retrieves the variable expression for the integer variable with the given name. + * + * @param name The name of the integer variable for which to retrieve the variable expression. + * @return The variable expression for the integer variable with the given name. + */ + std::shared_ptr getIntegerVariableExpression(std::string const& name) const = 0; + + /*! + * Retrieve the variable expression for the variable with the given name. + * + * @param name The name of the variable for which to retrieve the variable expression. + * @return The variable expression for the variable with the given name. + */ + std::shared_ptr getVariableExpression(std::string const& name) const = 0; + + /*! + * Retrieves the next free (global) index for a boolean variable. + */ + virtual uint_fast64_t getNextGlobalBooleanVariableIndex() const = 0; + + /*! + * Retrieves the next free (global) index for a integer variable. + */ + virtual uint_fast64_t getNextGlobalIntegerVariableIndex() const = 0; +}; + +} // namespace ir +} // namespace storm + +#endif /* STORM_IR_VARIABLESTATEINTERFACE_H_ */ \ No newline at end of file