Add check that undefined constants / parameters do not appear in the 'if' part of IfThenElseExpressions

src/storm/storage/expressions/CheckIfThenElseGuardVisitor.cpp

@@ -0,0 +1,71 @@
+#include "storm/storage/expressions/CheckIfThenElseGuardVisitor.h"
+
+#include "storm/storage/expressions/Expressions.h"
+
+namespace storm {
+    namespace expressions {
+        
+        CheckIfThenElseGuardVisitor::CheckIfThenElseGuardVisitor(std::set<storm::expressions::Variable> const& variables) : variables(variables) {
+            // Intentionally left empty.
+        }
+
+        bool CheckIfThenElseGuardVisitor::check(storm::expressions::Expression const& expression) {
+            return boost::any_cast<bool>(expression.accept(*this, boost::none));
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
+            // check whether the 'if' condition depends on one of the variables
+            if (expression.getCondition()->toExpression().containsVariable(variables)) {
+                return true;
+            } else {
+                // recurse
+                return
+                    boost::any_cast<bool>(expression.getThenExpression()->accept(*this, data)) ||
+                    boost::any_cast<bool>(expression.getElseExpression()->accept(*this, data));
+            }
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            return
+                boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, data)) ||
+                boost::any_cast<bool>(expression.getSecondOperand()->accept(*this, data));
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            return
+                boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, data)) ||
+                boost::any_cast<bool>(expression.getSecondOperand()->accept(*this, data));
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
+            return
+                boost::any_cast<bool>(expression.getFirstOperand()->accept(*this, data)) ||
+                boost::any_cast<bool>(expression.getSecondOperand()->accept(*this, data));
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(VariableExpression const& expression, boost::any const&) {
+            return false;
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            return expression.getOperand()->accept(*this, data);
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            return expression.getOperand()->accept(*this, data);
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) {
+            return false;
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(IntegerLiteralExpression const& expression, boost::any const&) {
+            return false;
+        }
+        
+        boost::any CheckIfThenElseGuardVisitor::visit(RationalLiteralExpression const& expression, boost::any const&) {
+            return false;
+        }
+        
+    }
+}

src/storm/storage/expressions/CheckIfThenElseGuardVisitor.h

@@ -0,0 +1,36 @@
+#pragma once
+
+#include "storm/storage/expressions/ExpressionVisitor.h"
+#include <set>
+
+namespace storm {
+    namespace expressions {
+
+        class Expression;
+        class Variable;
+
+        // Visits all sub-expressions and returns true if any of them is an IfThenElseExpression
+        // where the 'if' part depends on one of the variables in the set passed in the constructor.
+        class CheckIfThenElseGuardVisitor : public ExpressionVisitor {
+        public:
+            CheckIfThenElseGuardVisitor(std::set<storm::expressions::Variable> const& variables);
+
+            bool check(storm::expressions::Expression const& expression);
+
+            virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
+            virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
+
+        private:
+            std::set<storm::expressions::Variable> const& variables;
+        };
+
+    }
+}

src/storm/storage/expressions/Expression.cpp

@@ -7,6 +7,7 @@
 #include "storm/storage/expressions/LinearityCheckVisitor.h"
 #include "storm/storage/expressions/SyntacticalEqualityCheckVisitor.h"
 #include "storm/storage/expressions/ChangeManagerVisitor.h"
+#include "storm/storage/expressions/CheckIfThenElseGuardVisitor.h"
 #include "storm/storage/expressions/Expressions.h"
 #include "storm/exceptions/InvalidTypeException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
@@ -118,6 +119,12 @@ namespace storm {
             std::set_intersection(variables.begin(), variables.end(), appearingVariables.begin(), appearingVariables.end(), std::inserter(intersection, intersection.begin()));
             return !intersection.empty();
         }
+
+        bool Expression::containsVariableInITEGuard(std::set<storm::expressions::Variable> const& variables) const {
+            CheckIfThenElseGuardVisitor visitor(variables);
+            return visitor.check(*this);
+        }
+
         
         bool Expression::isRelationalExpression() const {
             if (!this->isFunctionApplication()) {

src/storm/storage/expressions/Expression.h

@@ -253,6 +253,16 @@ namespace storm {
              */
             bool containsVariable(std::set<storm::expressions::Variable> const& variables) const;
             
+
+            /*!
+             * Retrieves whether the expression contains any of the given variables in the
+             * 'if' part of any sub-IfThenElseExpressions.
+             *
+             * @param variables The variables to search for.
+             * @return True iff any of the variables appear in the 'if' part of an ITE-expression.
+             */
+            bool containsVariableInITEGuard(std::set<storm::expressions::Variable> const& variables) const;
+
             /*!
              * Retrieves the base expression underlying this expression object. Note that prior to calling this, the
              * expression object must be properly initialized.

src/storm/storage/prism/Command.cpp

@@ -67,6 +67,11 @@ namespace storm {
                         return false;
                     }
                 }
+
+                // check likelihood, undefined constants may not occur in 'if' part of IfThenElseExpression
+                if (update.getLikelihoodExpression().containsVariableInITEGuard(undefinedConstantVariables)) {
+                    return false;
+                }
             }
             
             return true;