diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index c9d64e9d1..15d7e50bc 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -83,7 +83,7 @@ namespace storm { break; default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; - } + } } virtual void visit(BinaryRelationExpression* expression) { diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 2d6d6381f..3e662ac2f 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -209,6 +209,17 @@ namespace storm { } assertDisjunction(context, solver, expressionVector); } + + /*! + * Asserts cuts that rule out a lot of suboptimal solutions. + * + * @param program The program for which to derive the cuts. + * @param context The Z3 context in which to build the expressions. + * @param solver The solver to use for the satisfiability evaluation. + */ + static void assertCuts(storm::ir::Program const& program, z3::context& context, z3::solver& solver) { + + } /*! * Asserts that the disjunction of the given formulae holds. @@ -396,7 +407,10 @@ namespace storm { // (5) Build the initial constraint system. assertInitialConstraints(program, labeledMdp, psiStates, context, solver, variableInformation, relevancyInformation); - // (6) Find the smallest set of commands that satisfies all constraints. If the probability of + // (6) Add constraints that cut off a lot of suboptimal solutions. + assertCuts(program, context, solver); + + // (7) Find the smallest set of commands that satisfies all constraints. If the probability of // satisfying phi until psi exceeds the given threshold, the set of labels is minimal and can be returned. // Otherwise, the current solution has to be ruled out and the next smallest solution is retrieved from // the solver. @@ -449,7 +463,7 @@ namespace storm { } std::cout << std::endl; - // (7) Return the resulting command set. + // (8) Return the resulting command set. return commandSet; #else diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h index 27d033be8..636799f0d 100644 --- a/src/ir/expressions/BaseExpression.h +++ b/src/ir/expressions/BaseExpression.h @@ -64,6 +64,13 @@ namespace storm { */ virtual ~BaseExpression(); + /*! + * Performes a deep-copy of the expression. + * + * @return A deep-copy of the expression. + */ + virtual std::shared_ptr clone() const = 0; + /*! * Copies the expression tree underneath (including) the current node and performs the provided renaming. * @@ -71,7 +78,7 @@ namespace storm { * @param variableState An object knowing about the global variable state. */ virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const = 0; - + /*! * Retrieves the value of the expression as an integer given the provided variable valuation. * diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.cpp b/src/ir/expressions/BinaryBooleanFunctionExpression.cpp index acfc392fd..0bbbd647c 100644 --- a/src/ir/expressions/BinaryBooleanFunctionExpression.cpp +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.cpp @@ -23,6 +23,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr BinaryBooleanFunctionExpression::clone() const { + return std::shared_ptr(new BinaryBooleanFunctionExpression(this->getLeft()->clone(), this->getRight()->clone(), functionType)); + } + std::shared_ptr BinaryBooleanFunctionExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType)); } diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h index 1b40cd25b..d637dd5a0 100644 --- a/src/ir/expressions/BinaryBooleanFunctionExpression.h +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h @@ -40,6 +40,8 @@ namespace storm { */ BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& binaryBooleanFunctionExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp index e3acde6fa..3cd85c5e4 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp @@ -23,6 +23,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr BinaryNumericalFunctionExpression::clone() const { + return std::shared_ptr(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(), this->getRight()->clone(), functionType)); + } + std::shared_ptr BinaryNumericalFunctionExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType)); } diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h index 34cfd4772..f4939d2a8 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.h +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h @@ -41,6 +41,8 @@ namespace storm { */ BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& binaryNumericalFunctionExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; /*! diff --git a/src/ir/expressions/BinaryRelationExpression.cpp b/src/ir/expressions/BinaryRelationExpression.cpp index bdd5cf596..af51dadb8 100644 --- a/src/ir/expressions/BinaryRelationExpression.cpp +++ b/src/ir/expressions/BinaryRelationExpression.cpp @@ -23,6 +23,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr BinaryRelationExpression::clone() const { + return std::shared_ptr(new BinaryRelationExpression(this->getLeft()->clone(), this->getRight()->clone(), relationType)); + } + std::shared_ptr BinaryRelationExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BinaryRelationExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->relationType)); } diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h index 1f0479eae..82b83fb60 100644 --- a/src/ir/expressions/BinaryRelationExpression.h +++ b/src/ir/expressions/BinaryRelationExpression.h @@ -40,6 +40,8 @@ namespace storm { */ BinaryRelationExpression(BinaryRelationExpression const& binaryRelationExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/BooleanConstantExpression.cpp b/src/ir/expressions/BooleanConstantExpression.cpp index 6b0ad2082..006e32769 100644 --- a/src/ir/expressions/BooleanConstantExpression.cpp +++ b/src/ir/expressions/BooleanConstantExpression.cpp @@ -19,6 +19,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr BooleanConstantExpression::clone() const { + return std::shared_ptr(new BooleanConstantExpression(*this)); + } + std::shared_ptr BooleanConstantExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BooleanConstantExpression(*this)); } diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h index 837c318f9..47f1b5dd7 100644 --- a/src/ir/expressions/BooleanConstantExpression.h +++ b/src/ir/expressions/BooleanConstantExpression.h @@ -33,6 +33,8 @@ namespace storm { */ BooleanConstantExpression(BooleanConstantExpression const& booleanConstantExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h deleted file mode 100644 index 3768f68f8..000000000 --- a/src/ir/expressions/BooleanLiteral.h +++ /dev/null @@ -1,62 +0,0 @@ -/* - * BooleanLiteral.h - * - * Created on: 03.01.2013 - * Author: chris - */ - -#ifndef STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_ -#define STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_ - -#include "src/ir/expressions/BaseExpression.h" - -namespace storm { -namespace ir { -namespace expressions { - -class BooleanLiteral : public BaseExpression { -public: - bool value; - - BooleanLiteral(bool value) : BaseExpression(bool_), value(value) { - - } - - virtual ~BooleanLiteral() { - - } - - virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) override { - return std::shared_ptr(new BooleanLiteral(this->value)); - } - - virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override { - return value; - } - - virtual void accept(ExpressionVisitor* visitor) override { - visitor->visit(this); - } - - virtual std::string toString() const override { - if (value) { - return std::string("true"); - } else { - return std::string("false"); - } - } - - virtual std::string dump(std::string prefix) const override { - std::stringstream result; - result << prefix << "BooleanLiteral " << this->toString() << std::endl; - return result.str(); - } -}; - -} - -} - -} - -#endif /* STORM_IR_EXPRESSIONS_BOOLEANLITERAL_H_ */ diff --git a/src/ir/expressions/BooleanLiteralExpression.cpp b/src/ir/expressions/BooleanLiteralExpression.cpp index ca01f4f7e..35708e33a 100644 --- a/src/ir/expressions/BooleanLiteralExpression.cpp +++ b/src/ir/expressions/BooleanLiteralExpression.cpp @@ -20,6 +20,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr BooleanLiteralExpression::clone() const { + return std::shared_ptr(new BooleanLiteralExpression(*this)); + } + std::shared_ptr BooleanLiteralExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new BooleanLiteralExpression(this->value)); } diff --git a/src/ir/expressions/BooleanLiteralExpression.h b/src/ir/expressions/BooleanLiteralExpression.h index 6c7d989f4..c4c6a85a1 100644 --- a/src/ir/expressions/BooleanLiteralExpression.h +++ b/src/ir/expressions/BooleanLiteralExpression.h @@ -33,6 +33,8 @@ namespace storm { */ BooleanLiteralExpression(BooleanLiteralExpression const& booleanLiteralExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual bool getValueAsBool(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/DoubleConstantExpression.cpp b/src/ir/expressions/DoubleConstantExpression.cpp index 48fab0785..3903b4b57 100644 --- a/src/ir/expressions/DoubleConstantExpression.cpp +++ b/src/ir/expressions/DoubleConstantExpression.cpp @@ -19,6 +19,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr DoubleConstantExpression::clone() const { + return std::shared_ptr(new DoubleConstantExpression(*this)); + } + std::shared_ptr DoubleConstantExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new DoubleConstantExpression(*this)); } diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h index b4f275690..cec0b23bc 100644 --- a/src/ir/expressions/DoubleConstantExpression.h +++ b/src/ir/expressions/DoubleConstantExpression.h @@ -33,6 +33,8 @@ namespace storm { */ DoubleConstantExpression(DoubleConstantExpression const& doubleConstantExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h deleted file mode 100644 index 7c66cc636..000000000 --- a/src/ir/expressions/DoubleLiteral.h +++ /dev/null @@ -1,62 +0,0 @@ -/* - * DoubleLiteral.h - * - * Created on: 03.01.2013 - * Author: chris - */ - -#ifndef STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_ -#define STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_ - -#include "src/ir/expressions/BaseExpression.h" - -#include "boost/lexical_cast.hpp" - -namespace storm { - -namespace ir { - -namespace expressions { - -class DoubleLiteral : public BaseExpression { -public: - double value; - - DoubleLiteral(double value) : BaseExpression(double_), value(value) { - - } - - virtual ~DoubleLiteral() { - - } - - virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) override { - return std::shared_ptr(new DoubleLiteral(this->value)); - } - - virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override { - return value; - } - - virtual void accept(ExpressionVisitor* visitor) override { - visitor->visit(this); - } - - virtual std::string toString() const override { - return boost::lexical_cast(value); - } - - virtual std::string dump(std::string prefix) const override { - std::stringstream result; - result << prefix << "DoubleLiteral " << this->toString() << std::endl; - return result.str(); - } -}; - -} - -} - -} - -#endif /* STORM_IR_EXPRESSIONS_DOUBLELITERAL_H_ */ diff --git a/src/ir/expressions/DoubleLiteralExpression.cpp b/src/ir/expressions/DoubleLiteralExpression.cpp index 954af88d2..b7a435051 100644 --- a/src/ir/expressions/DoubleLiteralExpression.cpp +++ b/src/ir/expressions/DoubleLiteralExpression.cpp @@ -22,6 +22,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr DoubleLiteralExpression::clone() const { + return std::shared_ptr(new DoubleLiteralExpression(*this)); + } + std::shared_ptr DoubleLiteralExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new DoubleLiteralExpression(this->value)); } diff --git a/src/ir/expressions/DoubleLiteralExpression.h b/src/ir/expressions/DoubleLiteralExpression.h index f2ff55c19..5327fbfe0 100644 --- a/src/ir/expressions/DoubleLiteralExpression.h +++ b/src/ir/expressions/DoubleLiteralExpression.h @@ -33,6 +33,8 @@ namespace storm { */ DoubleLiteralExpression(DoubleLiteralExpression const& doubleLiteralExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/IntegerConstantExpression.cpp b/src/ir/expressions/IntegerConstantExpression.cpp index bbdb5f131..b615061d7 100644 --- a/src/ir/expressions/IntegerConstantExpression.cpp +++ b/src/ir/expressions/IntegerConstantExpression.cpp @@ -19,6 +19,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr IntegerConstantExpression::clone() const { + return std::shared_ptr(new IntegerConstantExpression(*this)); + } + std::shared_ptr IntegerConstantExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new IntegerConstantExpression(*this)); } diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index d494e7700..35c9458c0 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -33,6 +33,8 @@ namespace storm { */ IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h deleted file mode 100644 index 453d6f685..000000000 --- a/src/ir/expressions/IntegerLiteral.h +++ /dev/null @@ -1,58 +0,0 @@ -/* - * IntegerLiteral.h - * - * Created on: 03.01.2013 - * Author: chris - */ - -#ifndef STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_ -#define STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_ - -#include "src/ir/expressions/BaseExpression.h" - -namespace storm { - -namespace ir { - -namespace expressions { - -class IntegerLiteral : public BaseExpression { -public: - int_fast64_t value; - - IntegerLiteral(int_fast64_t value) : BaseExpression(int_), value(value) { - } - - virtual ~IntegerLiteral() { - } - - virtual std::shared_ptr clone(const std::map& renaming, const std::map& bools, const std::map& ints) override { - return std::shared_ptr(new IntegerLiteral(this->value)); - } - - virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const override { - return value; - } - - virtual void accept(ExpressionVisitor* visitor) override { - visitor->visit(this); - } - - virtual std::string toString() const override { - return boost::lexical_cast(value); - } - - virtual std::string dump(std::string prefix) const override { - std::stringstream result; - result << prefix << "IntegerLiteral " << this->toString() << std::endl; - return result.str(); - } -}; - -} - -} - -} - -#endif /* STORM_IR_EXPRESSIONS_INTEGERLITERAL_H_ */ diff --git a/src/ir/expressions/IntegerLiteralExpression.cpp b/src/ir/expressions/IntegerLiteralExpression.cpp index 7d4f02d99..96d3f7570 100644 --- a/src/ir/expressions/IntegerLiteralExpression.cpp +++ b/src/ir/expressions/IntegerLiteralExpression.cpp @@ -22,6 +22,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr IntegerLiteralExpression::clone() const { + return std::shared_ptr(new IntegerLiteralExpression(*this)); + } + std::shared_ptr IntegerLiteralExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new IntegerLiteralExpression(this->value)); } diff --git a/src/ir/expressions/IntegerLiteralExpression.h b/src/ir/expressions/IntegerLiteralExpression.h index eeaa4d78d..9df073415 100644 --- a/src/ir/expressions/IntegerLiteralExpression.h +++ b/src/ir/expressions/IntegerLiteralExpression.h @@ -33,6 +33,8 @@ namespace storm { */ IntegerLiteralExpression(IntegerLiteralExpression const& integerLiteralExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual double getValueAsDouble(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.cpp b/src/ir/expressions/UnaryBooleanFunctionExpression.cpp index c3d57238a..6e27ba7c1 100644 --- a/src/ir/expressions/UnaryBooleanFunctionExpression.cpp +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.cpp @@ -21,6 +21,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr UnaryBooleanFunctionExpression::clone() const { + return std::shared_ptr(new UnaryBooleanFunctionExpression(this->getChild()->clone(), functionType)); + } + std::shared_ptr UnaryBooleanFunctionExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType)); } diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h index 36e8dcafd..166a036eb 100644 --- a/src/ir/expressions/UnaryBooleanFunctionExpression.h +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h @@ -39,6 +39,8 @@ namespace storm { */ UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& unaryBooleanFunctionExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; /*! diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp index 787ff4c68..aad3604b9 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp @@ -19,6 +19,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr UnaryNumericalFunctionExpression::clone() const { + return std::shared_ptr(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(), functionType)); + } + std::shared_ptr UnaryNumericalFunctionExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { return std::shared_ptr(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType)); } diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h index 59c94c7d0..1362497db 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.h +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h @@ -39,6 +39,8 @@ namespace storm { */ UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& unaryNumericalFunctionExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual int_fast64_t getValueAsInt(std::pair, std::vector> const* variableValues) const override; diff --git a/src/ir/expressions/VariableExpression.cpp b/src/ir/expressions/VariableExpression.cpp index 5cd96ce45..891417f58 100644 --- a/src/ir/expressions/VariableExpression.cpp +++ b/src/ir/expressions/VariableExpression.cpp @@ -26,6 +26,10 @@ namespace storm { // Nothing to do here. } + std::shared_ptr VariableExpression::clone() const { + return std::shared_ptr(new VariableExpression(*this)); + } + std::shared_ptr VariableExpression::clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const { // Perform the proper cloning. auto renamingPair = renaming.find(this->variableName); diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h index a66dbb573..468144b85 100644 --- a/src/ir/expressions/VariableExpression.h +++ b/src/ir/expressions/VariableExpression.h @@ -52,6 +52,8 @@ namespace storm { */ VariableExpression(VariableExpression const& variableExpression); + virtual std::shared_ptr clone() const override; + virtual std::shared_ptr clone(std::map const& renaming, storm::parser::prism::VariableState const& variableState) const override; virtual void accept(ExpressionVisitor* visitor) override; diff --git a/src/utility/IRUtility.h b/src/utility/IRUtility.h new file mode 100644 index 000000000..d26b0da61 --- /dev/null +++ b/src/utility/IRUtility.h @@ -0,0 +1,54 @@ +/* + * IRUtility.h + * + * Created on: 05.10.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_UTILITY_IRUTILITY_H_ +#define STORM_UTILITY_IRUTILITY_H_ + +#include + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +namespace storm { + namespace utility { + namespace ir { + + /*! + * Computes the weakest precondition of the given boolean expression wrt. the given updates. The weakest + * precondition is the most liberal expression that must hold in order to satisfy the given boolean + * expression after performing the updates. The updates must be disjoint in the sense that they must not + * assign an expression to a variable twice or more. + * + * @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 getWeakestPrecondition(std::shared_ptr booleanExpression, std::vector const& updates) { + std::map> 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(); + } + } + + // Copy the given expression and apply the substitution. + std::shared_ptr copiedExpression = booleanExpression->clone(); + copiedExpression->substitute(variableToExpressionMap); + + return copiedExpression; + } + + } // namespace ir + } // namespace utility +} // namespace storm + +#endif /* STORM_UTILITY_IRUTILITY_H_ */