diff --git a/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.cpp b/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.cpp new file mode 100644 index 000000000..0bbb32fba --- /dev/null +++ b/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 const& variables) : variables(variables) { + // Intentionally left empty. + } + + bool CheckIfThenElseGuardVisitor::check(storm::expressions::Expression const& expression) { + return boost::any_cast(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(expression.getThenExpression()->accept(*this, data)) || + boost::any_cast(expression.getElseExpression()->accept(*this, data)); + } + } + + boost::any CheckIfThenElseGuardVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) { + return + boost::any_cast(expression.getFirstOperand()->accept(*this, data)) || + boost::any_cast(expression.getSecondOperand()->accept(*this, data)); + } + + boost::any CheckIfThenElseGuardVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) { + return + boost::any_cast(expression.getFirstOperand()->accept(*this, data)) || + boost::any_cast(expression.getSecondOperand()->accept(*this, data)); + } + + boost::any CheckIfThenElseGuardVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) { + return + boost::any_cast(expression.getFirstOperand()->accept(*this, data)) || + boost::any_cast(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; + } + + } +} diff --git a/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.h b/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.h new file mode 100644 index 000000000..e2cac82e6 --- /dev/null +++ b/src/storm/storage/expressions/CheckIfThenElseGuardVisitor.h @@ -0,0 +1,36 @@ +#pragma once + +#include "storm/storage/expressions/ExpressionVisitor.h" +#include + +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 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 const& variables; + }; + + } +} diff --git a/src/storm/storage/expressions/Expression.cpp b/src/storm/storage/expressions/Expression.cpp index bb3dca82f..97e7046ab 100644 --- a/src/storm/storage/expressions/Expression.cpp +++ b/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 const& variables) const { + CheckIfThenElseGuardVisitor visitor(variables); + return visitor.check(*this); + } + bool Expression::isRelationalExpression() const { if (!this->isFunctionApplication()) { diff --git a/src/storm/storage/expressions/Expression.h b/src/storm/storage/expressions/Expression.h index 3d6da87c9..874a1ecda 100644 --- a/src/storm/storage/expressions/Expression.h +++ b/src/storm/storage/expressions/Expression.h @@ -253,6 +253,16 @@ namespace storm { */ bool containsVariable(std::set 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 const& variables) const; + /*! * Retrieves the base expression underlying this expression object. Note that prior to calling this, the * expression object must be properly initialized. diff --git a/src/storm/storage/prism/Command.cpp b/src/storm/storage/prism/Command.cpp index 89948d4c8..be40cd1eb 100644 --- a/src/storm/storage/prism/Command.cpp +++ b/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;