From 164c8225fd27ebe0d94f96a47a2fd4a6363dfcbe Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Apr 2014 14:41:27 +0200 Subject: [PATCH] Fixed some minor issues. Former-commit-id: 80f0ae4c9c91076e0987e19643d2f06f17b51aa8 --- src/adapters/ExplicitModelAdapter.h | 27 +++----- src/parser/PrismParser.cpp | 8 +-- src/parser/PrismParser.h | 2 +- .../expressions/BinaryRelationExpression.cpp | 2 +- src/storage/expressions/SimpleValuation.cpp | 64 ++++++++++++------- src/storage/expressions/SimpleValuation.h | 58 +++++++++-------- src/storage/prism/Constant.cpp | 4 ++ src/storage/prism/Constant.h | 10 +++ src/storage/prism/Program.cpp | 12 +++- test/functional/storage/ExpressionTest.cpp | 32 +++++----- 10 files changed, 127 insertions(+), 92 deletions(-) diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 0612f86e1..822ea1d12 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -336,8 +336,11 @@ namespace storm { // Only consider unlabeled commands. if (command.getActionName() != "") continue; + // Skip the command, if it is not enabled. - if (!command.getGuardExpression().evaluateAsBool(currentState)) continue; + if (!command.getGuardExpression().evaluateAsBool(currentState)) { + continue; + } result.push_back(Choice("")); Choice& choice = result.back(); @@ -521,31 +524,19 @@ namespace storm { // Initialize a queue and insert the initial state. std::queue stateQueue; - uint_fast64_t numberOfBooleanVariables = program.getNumberOfGlobalBooleanVariables(); - uint_fast64_t numberOfIntegerVariables = program.getNumberOfGlobalIntegerVariables(); - for (auto const& module : program.getModules()) { - numberOfBooleanVariables += module.getNumberOfBooleanVariables(); - numberOfIntegerVariables += module.getNumberOfIntegerVariables(); - } - StateType* initialState = new StateType(numberOfBooleanVariables, numberOfIntegerVariables, 0); - uint_fast64_t booleanIndex = 0; - uint_fast64_t integerIndex = 0; + StateType* initialState = new StateType; for (auto const& booleanVariable : program.getGlobalBooleanVariables()) { - initialState->setIdentifierIndex(booleanVariable.getName(), booleanIndex++); - initialState->setBooleanValue(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool()); + initialState->addBooleanIdentifier(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool()); } for (auto const& integerVariable : program.getGlobalIntegerVariables()) { - initialState->setIdentifierIndex(integerVariable.getName(), booleanIndex++); - initialState->setIntegerValue(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt()); + initialState->addIntegerIdentifier(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt()); } for (auto const& module : program.getModules()) { for (auto const& booleanVariable : module.getBooleanVariables()) { - initialState->setIdentifierIndex(booleanVariable.getName(), booleanIndex++); - initialState->setBooleanValue(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool()); + initialState->addBooleanIdentifier(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool()); } for (auto const& integerVariable : module.getIntegerVariables()) { - initialState->setIdentifierIndex(integerVariable.getName(), integerIndex++); - initialState->setIntegerValue(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt()); + initialState->addIntegerIdentifier(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt()); } } diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index c1a068d5c..6039c2c11 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -157,11 +157,11 @@ namespace storm { transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit(":") > plusExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3)]; transitionRewardDefinition.name("transition reward definition"); - rewardModelDefinition = (qi::lit("rewards") > qi::lit("\"") > identifier > qi::lit("\"") - > +( stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] - | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)] + rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > identifier[qi::_a = qi::_1] > qi::lit("\"")) + > +( stateRewardDefinition[phoenix::push_back(qi::_b, qi::_1)] + | transitionRewardDefinition[phoenix::push_back(qi::_c, qi::_1)] ) - >> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_1, qi::_a, qi::_b)]; + >> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)]; rewardModelDefinition.name("reward model definition"); initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesExpression, phoenix::ref(*this), qi::_1, qi::_r1)]; diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index e271b2298..3f8f17b65 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -225,7 +225,7 @@ namespace storm { qi::rule assignmentDefinition; // Rules for reward definitions. - qi::rule, std::vector>, Skipper> rewardModelDefinition; + qi::rule, std::vector>, Skipper> rewardModelDefinition; qi::rule stateRewardDefinition; qi::rule, Skipper> transitionRewardDefinition; diff --git a/src/storage/expressions/BinaryRelationExpression.cpp b/src/storage/expressions/BinaryRelationExpression.cpp index 1b00485b6..7e48c2286 100644 --- a/src/storage/expressions/BinaryRelationExpression.cpp +++ b/src/storage/expressions/BinaryRelationExpression.cpp @@ -46,7 +46,7 @@ namespace storm { void BinaryRelationExpression::printToStream(std::ostream& stream) const { stream << "(" << *this->getFirstOperand(); switch (this->getRelationType()) { - case RelationType::Equal: stream << " == "; break; + case RelationType::Equal: stream << " = "; break; case RelationType::NotEqual: stream << " != "; break; case RelationType::Greater: stream << " > "; break; case RelationType::GreaterOrEqual: stream << " >= "; break; diff --git a/src/storage/expressions/SimpleValuation.cpp b/src/storage/expressions/SimpleValuation.cpp index 7a456cb09..fb6f0088c 100644 --- a/src/storage/expressions/SimpleValuation.cpp +++ b/src/storage/expressions/SimpleValuation.cpp @@ -4,63 +4,79 @@ namespace storm { namespace expressions { - SimpleValuation::SimpleValuation(std::size_t booleanVariableCount, std::size_t integerVariableCount, std::size_t doubleVariableCount) : identifierToIndexMap(new std::unordered_map), booleanValues(booleanVariableCount), integerValues(integerVariableCount), doubleValues(doubleVariableCount) { + SimpleValuation::SimpleValuation() : booleanIdentifierToIndexMap(new std::unordered_map()), integerIdentifierToIndexMap(new std::unordered_map()), doubleIdentifierToIndexMap(new std::unordered_map()), booleanValues(), integerValues(), doubleValues() { // Intentionally left empty. } - SimpleValuation::SimpleValuation(std::shared_ptr> identifierToIndexMap, std::vector booleanValues, std::vector integerValues, std::vector doubleValues) : identifierToIndexMap(identifierToIndexMap), booleanValues(booleanValues), integerValues(integerValues), doubleValues(doubleValues) { - // Intentionally left empty. + bool SimpleValuation::operator==(SimpleValuation const& other) const { + return this->booleanIdentifierToIndexMap.get() == other.booleanIdentifierToIndexMap.get() && this->integerIdentifierToIndexMap.get() == other.integerIdentifierToIndexMap.get() && this->doubleIdentifierToIndexMap.get() == other.doubleIdentifierToIndexMap.get() && this->booleanValues == other.booleanValues && this->integerValues == other.integerValues && this->doubleValues == other.doubleValues; } - bool SimpleValuation::operator==(SimpleValuation const& other) const { - return this->identifierToIndexMap.get() == other.identifierToIndexMap.get() && this->booleanValues == other.booleanValues && this->integerValues == other.integerValues && this->doubleValues == other.doubleValues; + void SimpleValuation::addBooleanIdentifier(std::string const& name, bool initialValue) { + this->booleanIdentifierToIndexMap->emplace(name, this->booleanValues.size()); + this->booleanValues.push_back(false); } - - void SimpleValuation::setIdentifierIndex(std::string const& name, uint_fast64_t index) { - (*this->identifierToIndexMap)[name] = index; + + void SimpleValuation::addIntegerIdentifier(std::string const& name, int_fast64_t initialValue) { + this->integerIdentifierToIndexMap->emplace(name, this->integerValues.size()); + this->integerValues.push_back(initialValue); + } + + void SimpleValuation::addDoubleIdentifier(std::string const& name, double initialValue) { + this->doubleIdentifierToIndexMap->emplace(name, this->doubleValues.size()); + this->doubleValues.push_back(initialValue); } void SimpleValuation::setBooleanValue(std::string const& name, bool value) { - this->booleanValues[this->identifierToIndexMap->at(name)] = value; + this->booleanValues[this->booleanIdentifierToIndexMap->at(name)] = value; } void SimpleValuation::setIntegerValue(std::string const& name, int_fast64_t value) { - this->integerValues[this->identifierToIndexMap->at(name)] = value; + this->integerValues[this->integerIdentifierToIndexMap->at(name)] = value; } void SimpleValuation::setDoubleValue(std::string const& name, double value) { - this->doubleValues[this->identifierToIndexMap->at(name)] = value; + this->doubleValues[this->doubleIdentifierToIndexMap->at(name)] = value; } bool SimpleValuation::getBooleanValue(std::string const& name) const { - auto const& nameIndexPair = this->identifierToIndexMap->find(name); + auto const& nameIndexPair = this->booleanIdentifierToIndexMap->find(name); return this->booleanValues[nameIndexPair->second]; } int_fast64_t SimpleValuation::getIntegerValue(std::string const& name) const { - auto const& nameIndexPair = this->identifierToIndexMap->find(name); + auto const& nameIndexPair = this->integerIdentifierToIndexMap->find(name); return this->integerValues[nameIndexPair->second]; } double SimpleValuation::getDoubleValue(std::string const& name) const { - auto const& nameIndexPair = this->identifierToIndexMap->find(name); + auto const& nameIndexPair = this->doubleIdentifierToIndexMap->find(name); return this->doubleValues[nameIndexPair->second]; } std::ostream& operator<<(std::ostream& stream, SimpleValuation const& valuation) { - stream << "valuation { bool["; - for (uint_fast64_t i = 0; i < valuation.booleanValues.size() - 1; ++i) { - stream << valuation.booleanValues[i] << ", "; + stream << "valuation { bool ["; + if (!valuation.booleanValues.empty()) { + for (uint_fast64_t i = 0; i < valuation.booleanValues.size() - 1; ++i) { + stream << valuation.booleanValues[i] << ", "; + } + stream << valuation.booleanValues.back(); } - stream << valuation.booleanValues.back() << "] ints["; - for (uint_fast64_t i = 0; i < valuation.integerValues.size() - 1; ++i) { - stream << valuation.integerValues[i] << ", "; + stream << "] int ["; + if (!valuation.integerValues.empty()) { + for (uint_fast64_t i = 0; i < valuation.integerValues.size() - 1; ++i) { + stream << valuation.integerValues[i] << ", "; + } + stream << valuation.integerValues.back(); } - stream << valuation.integerValues.back() << "] double["; - for (uint_fast64_t i = 0; i < valuation.doubleValues.size() - 1; ++i) { - stream << valuation.doubleValues[i] << ", "; + stream << "] double ["; + if (!valuation.doubleValues.empty()) { + for (uint_fast64_t i = 0; i < valuation.doubleValues.size() - 1; ++i) { + stream << valuation.doubleValues[i] << ", "; + } + stream << valuation.doubleValues.back(); } - stream << valuation.doubleValues.back() << "] }"; + stream << "] }"; return stream; } diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h index 16719be00..35b74291b 100644 --- a/src/storage/expressions/SimpleValuation.h +++ b/src/storage/expressions/SimpleValuation.h @@ -16,30 +16,14 @@ namespace storm { friend class SimpleValuationPointerLess; /*! - * Creates a simple valuation that can hold the given number of boolean, integer and double variables. - * - * @param booleanVariableCount The number of boolean variables in the valuation. - * @param integerVariableCount The number of integer variables in the valuation. - * @param doubleVariableCount The number of double variables in the valuation. - */ - SimpleValuation(std::size_t booleanVariableCount, std::size_t integerVariableCount, std::size_t doubleVariableCount); - - /*! - * Creates a simple evaluation based on the given identifier to index map and value containers for the - * different types of variables. - * - * @param identifierToIndexMap A shared pointer to a mapping from identifier to their local indices in the - * value containers. - * @param booleanValues The value container for all boolean identifiers. - * @param integerValues The value container for all integer identifiers. - * @param doubleValues The value container for all double identifiers. - */ - SimpleValuation(std::shared_ptr> identifierToIndexMap, std::vector booleanValues, std::vector integerValues, std::vector doubleValues); + * Creates a simple valuation without any identifiers. + */ + SimpleValuation(); // Instantiate some constructors and assignments with their default implementations. SimpleValuation(SimpleValuation const&) = default; - SimpleValuation(SimpleValuation&&) = default; SimpleValuation& operator=(SimpleValuation const&) = default; + SimpleValuation(SimpleValuation&&) = default; SimpleValuation& operator=(SimpleValuation&&) = default; virtual ~SimpleValuation() = default; @@ -49,12 +33,28 @@ namespace storm { bool operator==(SimpleValuation const& other) const; /*! - * Sets the index of the identifier with the given name to the given value. + * Adds a boolean identifier with the given name. + * + * @param name The name of the boolean identifier to add. + * @param initialValue The initial value of the identifier. + */ + void addBooleanIdentifier(std::string const& name, bool initialValue = false); + + /*! + * Adds a integer identifier with the given name. * - * @param name The name of the identifier for which to set the index. - * @param index The new index of the identifier. + * @param name The name of the integer identifier to add. + * @param initialValue The initial value of the identifier. */ - void setIdentifierIndex(std::string const& name, uint_fast64_t index); + void addIntegerIdentifier(std::string const& name, int_fast64_t initialValue = 0); + + /*! + * Adds a double identifier with the given name. + * + * @param name The name of the double identifier to add. + * @param initialValue The initial value of the identifier. + */ + void addDoubleIdentifier(std::string const& name, double initialValue = 0); /*! * Sets the value of the boolean identifier with the given name to the given value. @@ -88,8 +88,14 @@ namespace storm { friend std::ostream& operator<<(std::ostream& stream, SimpleValuation const& valuation); private: - // A mapping of identifiers to their local indices in the value containers. - std::shared_ptr> identifierToIndexMap; + // A mapping of boolean identifiers to their local indices in the value container. + std::shared_ptr> booleanIdentifierToIndexMap; + + // A mapping of integer identifiers to their local indices in the value container. + std::shared_ptr> integerIdentifierToIndexMap; + + // A mapping of double identifiers to their local indices in the value container. + std::shared_ptr> doubleIdentifierToIndexMap; // The value container for all boolean identifiers. std::vector booleanValues; diff --git a/src/storage/prism/Constant.cpp b/src/storage/prism/Constant.cpp index 83e5f9b2a..55d08d78a 100644 --- a/src/storage/prism/Constant.cpp +++ b/src/storage/prism/Constant.cpp @@ -26,6 +26,10 @@ namespace storm { return this->expression; } + Constant Constant::substitute(std::map const& substitution) const { + return Constant(this->getConstantType(), this->getConstantName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber()); + } + std::ostream& operator<<(std::ostream& stream, Constant const& constant) { stream << "const "; switch (constant.getConstantType()) { diff --git a/src/storage/prism/Constant.h b/src/storage/prism/Constant.h index b67e1639f..06d8cbf50 100644 --- a/src/storage/prism/Constant.h +++ b/src/storage/prism/Constant.h @@ -1,6 +1,8 @@ #ifndef STORM_STORAGE_PRISM_CONSTANT_H_ #define STORM_STORAGE_PRISM_CONSTANT_H_ +#include + #include "src/storage/prism/LocatedInformation.h" #include "src/storage/expressions/Expression.h" @@ -65,6 +67,14 @@ namespace storm { */ storm::expressions::Expression const& getExpression() const; + /*! + * Substitutes all identifiers in the constant according to the given map. + * + * @param substitution The substitution to perform. + * @return The resulting constant. + */ + Constant substitute(std::map const& substitution) const; + friend std::ostream& operator<<(std::ostream& stream, Constant const& constant); private: diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index 49ebd7724..85bfc1958 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -261,10 +261,18 @@ namespace storm { Program Program::substituteConstants() const { // We start by creating the appropriate substitution std::map constantSubstitution; - for (auto const& constant : this->getConstants()) { + std::vector newConstants(this->getConstants()); + for (uint_fast64_t constantIndex = 0; constantIndex < newConstants.size(); ++constantIndex) { + auto const& constant = newConstants[constantIndex]; LOG_THROW(constant.isDefined(), storm::exceptions::InvalidArgumentException, "Cannot substitute constants in program that contains undefined constants."); + // Put the corresponding expression in the substitution. constantSubstitution.emplace(constant.getConstantName(), constant.getExpression()); + + // If there is at least one more constant to come, we substitute the costants we have so far. + if (constantIndex + 1 < newConstants.size()) { + newConstants[constantIndex + 1] = newConstants[constantIndex + 1].substitute(constantSubstitution); + } } // Now we can substitute the constants in all expressions appearing in the program. @@ -306,7 +314,7 @@ namespace storm { newLabels.emplace_back(label.substitute(constantSubstitution)); } - return Program(this->getModelType(), std::vector(), newBooleanVariables, newIntegerVariables, newFormulas, newModules, newRewardModels, this->definesInitialStatesExpression(), newInitialStateExpression, newLabels); + return Program(this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, newRewardModels, this->definesInitialStatesExpression(), newInitialStateExpression, newLabels); } std::ostream& operator<<(std::ostream& stream, Program const& program) { diff --git a/test/functional/storage/ExpressionTest.cpp b/test/functional/storage/ExpressionTest.cpp index 8bb2e4c04..0c19c5bfb 100644 --- a/test/functional/storage/ExpressionTest.cpp +++ b/test/functional/storage/ExpressionTest.cpp @@ -359,25 +359,25 @@ TEST(Expression, SimpleEvaluationTest) { ASSERT_NO_THROW(tempExpression = (intVarExpression < threeExpression || boolVarExpression) && boolConstExpression); - ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation(2, 2, 2)); - storm::expressions::SimpleValuation valuation(2, 2, 2); - ASSERT_NO_THROW(valuation.setIdentifierIndex("x", 0)); - ASSERT_NO_THROW(valuation.setIdentifierIndex("a", 1)); - ASSERT_NO_THROW(valuation.setIdentifierIndex("y", 0)); - ASSERT_NO_THROW(valuation.setIdentifierIndex("b", 1)); - ASSERT_NO_THROW(valuation.setIdentifierIndex("z", 0)); - ASSERT_NO_THROW(valuation.setIdentifierIndex("c", 1)); + ASSERT_NO_THROW(storm::expressions::SimpleValuation valuation); + storm::expressions::SimpleValuation valuation; + ASSERT_NO_THROW(valuation.addBooleanIdentifier("x")); + ASSERT_NO_THROW(valuation.addBooleanIdentifier("a")); + ASSERT_NO_THROW(valuation.addIntegerIdentifier("y")); + ASSERT_NO_THROW(valuation.addIntegerIdentifier("b")); + ASSERT_NO_THROW(valuation.addDoubleIdentifier("z")); + ASSERT_NO_THROW(valuation.addDoubleIdentifier("c")); - ASSERT_THROW(tempExpression.evaluateAsDouble(valuation), storm::exceptions::InvalidTypeException); - ASSERT_THROW(tempExpression.evaluateAsInt(valuation), storm::exceptions::InvalidTypeException); - EXPECT_FALSE(tempExpression.evaluateAsBool(valuation)); + ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); + ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); + EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); ASSERT_NO_THROW(valuation.setBooleanValue("a", true)); - EXPECT_TRUE(tempExpression.evaluateAsBool(valuation)); + EXPECT_TRUE(tempExpression.evaluateAsBool(&valuation)); ASSERT_NO_THROW(valuation.setIntegerValue("y", 3)); - EXPECT_FALSE(tempExpression.evaluateAsBool(valuation)); + EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); ASSERT_NO_THROW(tempExpression = ((intVarExpression < threeExpression).ite(trueExpression, falseExpression))); - ASSERT_THROW(tempExpression.evaluateAsDouble(valuation), storm::exceptions::InvalidTypeException); - ASSERT_THROW(tempExpression.evaluateAsInt(valuation), storm::exceptions::InvalidTypeException); - EXPECT_FALSE(tempExpression.evaluateAsBool(valuation)); + ASSERT_THROW(tempExpression.evaluateAsDouble(&valuation), storm::exceptions::InvalidTypeException); + ASSERT_THROW(tempExpression.evaluateAsInt(&valuation), storm::exceptions::InvalidTypeException); + EXPECT_FALSE(tempExpression.evaluateAsBool(&valuation)); } \ No newline at end of file