Fixed some minor issues.

Former-commit-id: 80f0ae4c9c

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<ValueType>(""));
                         Choice<ValueType>& choice = result.back();
@@ -521,31 +524,19 @@ namespace storm {
                 
                 // Initialize a queue and insert the initial state.
                 std::queue<uint_fast64_t> 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());
                     }
                 }
         

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)];

src/parser/PrismParser.h

@@ -225,7 +225,7 @@ namespace storm {
             qi::rule<Iterator, storm::prism::Assignment(), Skipper> assignmentDefinition;
             
             // Rules for reward definitions.
-            qi::rule<Iterator, storm::prism::RewardModel(), qi::locals<std::vector<storm::prism::StateReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition;
+            qi::rule<Iterator, storm::prism::RewardModel(), qi::locals<std::string, std::vector<storm::prism::StateReward>, std::vector<storm::prism::TransitionReward>>, Skipper> rewardModelDefinition;
             qi::rule<Iterator, storm::prism::StateReward(), Skipper> stateRewardDefinition;
             qi::rule<Iterator, storm::prism::TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
             

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;

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<std::string, uint_fast64_t>), booleanValues(booleanVariableCount), integerValues(integerVariableCount), doubleValues(doubleVariableCount) {
+        SimpleValuation::SimpleValuation() : booleanIdentifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>()), integerIdentifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>()), doubleIdentifierToIndexMap(new std::unordered_map<std::string, uint_fast64_t>()), booleanValues(), integerValues(), doubleValues() {
             // Intentionally left empty.
         }
         
-        SimpleValuation::SimpleValuation(std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> identifierToIndexMap, std::vector<bool> booleanValues, std::vector<int_fast64_t> integerValues, std::vector<double> 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::addIntegerIdentifier(std::string const& name, int_fast64_t initialValue) {
+            this->integerIdentifierToIndexMap->emplace(name, this->integerValues.size());
+            this->integerValues.push_back(initialValue);
         }
         
-        void SimpleValuation::setIdentifierIndex(std::string const& name, uint_fast64_t index) {
-            (*this->identifierToIndexMap)[name] = index;
+        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 [";
+            if (!valuation.booleanValues.empty()) {
                 for (uint_fast64_t i = 0; i < valuation.booleanValues.size() - 1; ++i) {
                     stream << valuation.booleanValues[i] << ", ";
                 }
-            stream << valuation.booleanValues.back() << "] ints[";
+                stream << valuation.booleanValues.back();
+            }
+            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() << "] double[";
+                stream << valuation.integerValues.back();
+            }
+            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;
         }

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.
+             * Creates a simple valuation without any identifiers.
             */
-            SimpleValuation(std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> identifierToIndexMap, std::vector<bool> booleanValues, std::vector<int_fast64_t> integerValues, std::vector<double> doubleValues);
+            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 identifier for which to set the index.
-             * @param index The new index of the identifier.
+             * @param name The name of the boolean identifier to add.
+             * @param initialValue The initial value of the identifier.
              */
-            void setIdentifierIndex(std::string const& name, uint_fast64_t index);
+            void addBooleanIdentifier(std::string const& name, bool initialValue = false);
+            
+            /*!
+             * Adds a integer identifier with the given name.
+             *
+             * @param name The name of the integer identifier to add.
+             * @param initialValue The initial value of the identifier.
+             */
+            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<std::unordered_map<std::string, uint_fast64_t>> identifierToIndexMap;
+            // A mapping of boolean identifiers to their local indices in the value container.
+            std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> booleanIdentifierToIndexMap;
+            
+            // A mapping of integer identifiers to their local indices in the value container.
+            std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> integerIdentifierToIndexMap;
+            
+            // A mapping of double identifiers to their local indices in the value container.
+            std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> doubleIdentifierToIndexMap;
             
             // The value container for all boolean identifiers.
             std::vector<bool> booleanValues;

src/storage/prism/Constant.cpp

@@ -26,6 +26,10 @@ namespace storm {
             return this->expression;
         }
         
+        Constant Constant::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+            return Constant(this->getConstantType(), this->getConstantName(), this->getExpression().substitute<std::map>(substitution), this->getFilename(), this->getLineNumber());
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Constant const& constant) {
             stream << "const ";
             switch (constant.getConstantType()) {

src/storage/prism/Constant.h

@@ -1,6 +1,8 @@
 #ifndef STORM_STORAGE_PRISM_CONSTANT_H_
 #define STORM_STORAGE_PRISM_CONSTANT_H_
 
+#include <map>
+
 #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<std::string, storm::expressions::Expression> const& substitution) const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Constant const& constant);
             
         private:

src/storage/prism/Program.cpp

@@ -261,10 +261,18 @@ namespace storm {
         Program Program::substituteConstants() const {
             // We start by creating the appropriate substitution
             std::map<std::string, storm::expressions::Expression> constantSubstitution;
-            for (auto const& constant : this->getConstants()) {
+            std::vector<Constant> 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<Constant>(), 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) {

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_THROW(tempExpression.evaluateAsDouble(valuation), storm::exceptions::InvalidTypeException);
-    ASSERT_THROW(tempExpression.evaluateAsInt(valuation), storm::exceptions::InvalidTypeException);
-    EXPECT_FALSE(tempExpression.evaluateAsBool(valuation));
+    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_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));
 }