Several fixes for the IR. Weakest precondition computation is now supported for IR expressions.

Former-commit-id: 00387e59fc

src/adapters/ExplicitModelAdapter.h

@@ -703,7 +703,7 @@ namespace storm {
                 std::list<Choice<ValueType>> result;
                 
                 StateType const* currentState = stateInformation.reachableStates[stateIndex];
-                
+
                 // Iterate over all modules.
                 for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
                     storm::ir::Module const& module = program.getModule(i);
@@ -757,7 +757,7 @@ namespace storm {
                 for (std::string const& action : program.getActions()) {
                     StateType const* currentState = stateInformation.reachableStates[stateIndex];
                     boost::optional<std::vector<std::list<storm::ir::Command>>> optionalActiveCommandLists = getActiveCommandsByAction(program, currentState, action);
-                    
+                                        
                     // Only process this action label, if there is at least one feasible solution.
                     if (optionalActiveCommandLists) {
                         std::vector<std::list<storm::ir::Command>> const& activeCommandList = optionalActiveCommandLists.get();

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -20,6 +20,8 @@
 #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
 
+#include "src/utility/IRUtility.h"
+
 namespace storm {
     namespace counterexamples {
         
@@ -218,7 +220,7 @@ namespace storm {
              * @param solver The solver to use for the satisfiability evaluation.
              */
             static void assertCuts(storm::ir::Program const& program, z3::context& context, z3::solver& solver) {
-                
+                // TODO.
             }
 
             /*!

src/ir/Program.cpp

@@ -77,7 +77,7 @@ namespace storm {
         Program::Program(Program const& otherProgram) : modelType(otherProgram.modelType), globalBooleanVariables(otherProgram.globalBooleanVariables),
         globalIntegerVariables(otherProgram.globalIntegerVariables), globalBooleanVariableToIndexMap(otherProgram.globalBooleanVariableToIndexMap),
         globalIntegerVariableToIndexMap(otherProgram.globalIntegerVariableToIndexMap), modules(otherProgram.modules), rewards(otherProgram.rewards),
-        actionsToModuleIndexMap(), variableToModuleIndexMap() {
+        actions(otherProgram.actions), actionsToModuleIndexMap(), variableToModuleIndexMap() {
             // Perform deep-copy of the maps.
             for (auto const& booleanUndefinedConstant : otherProgram.booleanUndefinedConstantExpressions) {
                 this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second));
@@ -102,6 +102,7 @@ namespace storm {
                 this->globalIntegerVariableToIndexMap = otherProgram.globalIntegerVariableToIndexMap;
                 this->modules = otherProgram.modules;
                 this->rewards = otherProgram.rewards;
+                this->actions = otherProgram.actions;
                 this->actionsToModuleIndexMap = otherProgram.actionsToModuleIndexMap;
                 this->variableToModuleIndexMap = otherProgram.variableToModuleIndexMap;
                 

src/ir/expressions/BaseExpression.cpp

@@ -26,6 +26,16 @@ namespace storm {
                 // Nothing to do here.
             }
             
+            std::unique_ptr<BaseExpression> BaseExpression::substitute(std::unique_ptr<BaseExpression>&& expression, std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
+                BaseExpression* result = expression->performSubstitution(substitution);
+                
+                if (result != expression.get()) {
+                    return std::unique_ptr<BaseExpression>(result);
+                } else {
+                    return std::move(expression);
+                }
+            }
+            
             int_fast64_t BaseExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
                 if (type != int_) {
                     throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
@@ -70,6 +80,10 @@ namespace storm {
                 return type;
             }
             
+            BaseExpression* BaseExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
+                return this;
+            }
+            
         } // namespace expressions
     } // namespace ir
 } // namespace storm

src/ir/expressions/BaseExpression.h

@@ -33,8 +33,11 @@ namespace storm {
              * The base class for all expressions.
              */
             class BaseExpression {
-                
             public:
+                // Forward declare friend classes to allow access to substitute.
+                friend class BinaryExpression;
+                friend class UnaryExpression;
+
                 /*!
                  * Each node in an expression tree has a uniquely defined type from this enum.
                  */
@@ -78,7 +81,17 @@ namespace storm {
                  * @param variableState An object knowing about the global variable state.
                  */
                 virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const = 0;
-                                
+                
+                /*!
+                 * Performs the given substitution by replacing each variable in the given expression that is a key in
+                 * the map by a copy of the mapped expression.
+                 *
+                 * @param expression The expression in which to perform the substitution.
+                 * @param substitution The substitution to apply.
+                 * @return The resulting expression.
+                 */
+                static std::unique_ptr<BaseExpression> substitute(std::unique_ptr<BaseExpression>&& expression, std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution);
+                
                 /*!
                  * Retrieves the value of the expression as an integer given the provided variable valuation.
                  *
@@ -137,6 +150,16 @@ namespace storm {
                  */
                 ReturnType getType() const;
                 
+            protected:
+                /*!
+                 * Performs the given substitution on the expression, i.e. replaces all variables whose names are keys
+                 * of the map by a copy of the expression they are associated with in the map. This is intended as a helper
+                 * function for substitute.
+                 *
+                 * @param substitution The substitution to perform
+                 */
+                virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution);
+                
             private:
                 // The type to which this node evaluates.
                 ReturnType type;

src/ir/expressions/BinaryExpression.cpp

@@ -20,6 +20,25 @@ namespace storm {
                 // Nothing to do here.
             }
 
+            BaseExpression* BinaryExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
+                // Get the new left successor recursively.
+                BaseExpression* newLeftSuccessor = left->performSubstitution(substitution);
+                
+                // If the left successor changed, we need to update it. If it did not change, this must not be executed,
+                // because assigning to the unique_ptr will destroy the current successor immediately.
+                if (newLeftSuccessor != left.get()) {
+                    left = std::unique_ptr<BaseExpression>(newLeftSuccessor);
+                }
+                
+                // Now do the same thing for the right successor.
+                BaseExpression* newRightSuccessor = right->performSubstitution(substitution);
+                if (newRightSuccessor != right.get()) {
+                    right = std::unique_ptr<BaseExpression>(newRightSuccessor);
+                }
+            
+                return this;
+            }
+            
             std::unique_ptr<BaseExpression> const& BinaryExpression::getLeft() const {
                 return left;
             }

src/ir/expressions/BinaryExpression.h

@@ -33,7 +33,7 @@ namespace storm {
                  * @param binaryExpression The expression to copy.
                  */
                 BinaryExpression(BinaryExpression const& binaryExpression);
-                
+                                
                 /*!
                  * Retrieves the left child of the expression node.
                  *
@@ -48,6 +48,9 @@ namespace storm {
                  */
                 std::unique_ptr<BaseExpression> const& getRight() const;
                 
+            protected:
+                virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) override;
+                
             private:
                 // The left child of the binary expression.
                 std::unique_ptr<BaseExpression> left;

src/ir/expressions/UnaryExpression.cpp

@@ -23,6 +23,17 @@ namespace storm {
                 return child;
             }
             
+            BaseExpression* UnaryExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
+                BaseExpression* newChild = child->performSubstitution(substitution);
+                
+                // Only update the child if it changed, because otherwise the child gets destroyed.
+                if (newChild != child.get()) {
+                    child = std::unique_ptr<BaseExpression>(newChild);
+                }
+                
+                return this;
+            }
+            
         } // namespace expressions
     } // namespace ir
 } // namespace storm

src/ir/expressions/UnaryExpression.h

@@ -39,6 +39,9 @@ namespace storm {
                  * @return The child of the expression node.
                  */
                 std::unique_ptr<BaseExpression> const& getChild() const;
+
+            protected:
+                virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) override;
                 
             private:
                 // The left child of the unary expression.

src/ir/expressions/VariableExpression.cpp

@@ -48,6 +48,20 @@ namespace storm {
                 }
             }
             
+            BaseExpression* VariableExpression::performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) {
+                // If the name of the variable is a key of the map, we need to replace it.
+                auto substitutionIterator = substitution.find(variableName);
+                
+                if (substitutionIterator != substitution.end()) {
+                    std::unique_ptr<BaseExpression> expressionClone = substitutionIterator->second.get().clone();
+                    BaseExpression* rawPointer = expressionClone.release();
+                    return rawPointer;
+                } else {
+                    // Otherwise, we don't need to replace anything.
+                    return this;
+                }
+            }
+            
             void VariableExpression::accept(ExpressionVisitor* visitor) {
                 visitor->visit(this);
             }

src/ir/expressions/VariableExpression.h

@@ -55,7 +55,7 @@ namespace storm {
                 virtual std::unique_ptr<BaseExpression> clone() const override;
                 
 				virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
-				
+				            
 				virtual void accept(ExpressionVisitor* visitor) override;
 				
 				virtual std::string toString() const override;
@@ -79,7 +79,10 @@ namespace storm {
                  * @return The global index of the variable.
                  */
 				uint_fast64_t getGlobalVariableIndex() const;
-				
+				            
+            protected:
+                virtual BaseExpression* performSubstitution(std::map<std::string, std::reference_wrapper<BaseExpression>> const& substitution) override;
+                
 			private:
                 // The global index of the variable.
 				uint_fast64_t globalIndex;

src/parser/prismparser/PrismGrammar.cpp

@@ -93,7 +93,7 @@ namespace storm {
             void PrismGrammar::createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
                 uint_fast64_t id = this->state->addIntegerVariable(name);
                 uint_fast64_t newLocalIndex = this->state->nextLocalIntegerVariableIndex;
-                vars.emplace_back(newLocalIndex, id, name, lower->clone(), upper->clone(), init->clone());
+                vars.emplace_back(newLocalIndex, id, name, lower != nullptr ? lower->clone() : nullptr, upper != nullptr ? upper->clone() : nullptr, init != nullptr ? init->clone() : nullptr);
                 varids[name] = newLocalIndex;
                 ++this->state->nextLocalIntegerVariableIndex;
                 this->state->localIntegerVariables_.add(name, name);
@@ -105,7 +105,7 @@ namespace storm {
             void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
                 uint_fast64_t id = this->state->addBooleanVariable(name);
                 uint_fast64_t newLocalIndex = this->state->nextLocalBooleanVariableIndex;
-                vars.emplace_back(newLocalIndex, id, name, init->clone());
+                vars.emplace_back(newLocalIndex, id, name, init != nullptr ? init->clone() : nullptr);
                 varids[name] = newLocalIndex;
                 ++this->state->nextLocalBooleanVariableIndex;
                 this->state->localBooleanVariables_.add(name, name);
@@ -125,7 +125,7 @@ namespace storm {
             }
             Update PrismGrammar::createUpdate(std::shared_ptr<BaseExpression> const& likelihood, std::map<std::string, Assignment> const& bools, std::map<std::string, Assignment> const& ints) {
                 this->state->nextGlobalUpdateIndex++;
-                return Update(this->state->getNextGlobalUpdateIndex() - 1, likelihood->clone(), bools, ints);
+                return Update(this->state->getNextGlobalUpdateIndex() - 1, likelihood != nullptr ? likelihood->clone() : nullptr, bools, ints);
             }
             Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::vector<Update> const& updates) {
                 this->state->nextGlobalCommandIndex++;

src/utility/IRUtility.h

@@ -8,7 +8,7 @@
 #ifndef STORM_UTILITY_IRUTILITY_H_
 #define STORM_UTILITY_IRUTILITY_H_
 
-#include <IR.h>
+#include <src/ir/IR.h>
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
@@ -28,23 +28,21 @@ namespace storm {
              * @param expression The expression for which to build the weakest precondition.
              * @param update The update with respect to which to compute the weakest precondition.
              */
-            std::shared_ptr<storm::ir::expressions::BaseExpression> getWeakestPrecondition(std::shared_ptr<storm::ir::expressions::BaseExpression> booleanExpression, std::vector<storm::ir::Update> const& updates) {
-                std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> variableToExpressionMap;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> getWeakestPrecondition(std::unique_ptr<storm::ir::expressions::BaseExpression> const& booleanExpression, std::vector<storm::ir::Update> const& updates) {
+                std::map<std::string, std::reference_wrapper<storm::ir::expressions::BaseExpression>> variableToExpressionMap;
                 
                 // Construct the full substitution we need to perform later.
                 for (auto const& update : updates) {
-                    for (uint_fast64_t assignmentIndex = 0; assignmentIndex < update.getNumberOfAssignments(); ++assignmentIndex) {
-                        storm::ir::Assignment const& update.getAssignment(assignmentIndex);
-                        
-                        variableToExpressionMap[assignment.getVariableName()] = assignment.getExpression();
+                    for (auto const& variableAssignmentPair : update.getBooleanAssignments()) {
+                        variableToExpressionMap.emplace(variableAssignmentPair.first, *variableAssignmentPair.second.getExpression());
+                    }
+                    for (auto const& variableAssignmentPair : update.getIntegerAssignments()) {
+                        variableToExpressionMap.emplace(variableAssignmentPair.first, *variableAssignmentPair.second.getExpression());
                     }
                 }
                 
                 // Copy the given expression and apply the substitution.
-                std::shared_ptr<storm::ir::expressions::BaseExpression> copiedExpression = booleanExpression->clone();
-                copiedExpression->substitute(variableToExpressionMap);
-                
-                return copiedExpression;
+                return storm::ir::expressions::BaseExpression::substitute(booleanExpression->clone(), variableToExpressionMap);
             }
             
         } // namespace ir