support for nonstandard predicate elimination or to-dice translation

src/storm/storage/expressions/Expression.cpp

@@ -13,6 +13,7 @@
 #include "storm/exceptions/InvalidTypeException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/utility/macros.h"
+#include "storm/storage/expressions/SimplificationVisitor.h"
 
 namespace storm {
     namespace expressions {
@@ -53,6 +54,10 @@ namespace storm {
 			return SubstitutionVisitor<std::unordered_map<Variable, Expression>>(identifierToExpressionMap).substitute(*this);
 		}
 
+		Expression Expression::substituteNonStandardPredicates() const {
+            return SimplificationVisitor().substitute(*this);
+        }
+
         bool Expression::evaluateAsBool(Valuation const* valuation) const {
             return this->getBaseExpression().evaluateAsBool(valuation);
         }

src/storm/storage/expressions/Expression.h

@@ -100,6 +100,11 @@ namespace storm {
              */
             Expression substitute(std::map<Variable, Expression> const& variableToExpressionMap) const;
 
+            /*!
+             * Eliminate nonstandard predicates from the expression.
+             * @return
+             */
+            Expression substituteNonStandardPredicates() const;
             /*!
             * Substitutes all occurrences of the variables according to the given map. Note that this substitution is
             * done simultaneously, i.e., variables appearing in the expressions that were "plugged in" are not

src/storm/storage/expressions/SimplificationVisitor.cpp

@@ -0,0 +1,171 @@
+#include <map>
+#include <unordered_map>
+#include <string>
+
+#include "storm/storage/expressions/SimplificationVisitor.h"
+#include "storm/storage/expressions/Expressions.h"
+#include "storm/storage/expressions/PredicateExpression.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+    namespace expressions {
+        SimplificationVisitor::SimplificationVisitor() {
+            // Intentionally left empty.
+        }
+
+        Expression SimplificationVisitor::substitute(Expression const &expression) {
+            return Expression(boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getBaseExpression().accept(*this, boost::none)));
+        }
+
+        boost::any SimplificationVisitor::visit(IfThenElseExpression const &expression, boost::any const &data) {
+            std::shared_ptr<BaseExpression const> conditionExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getCondition()->accept(*this, data));
+            std::shared_ptr<BaseExpression const> thenExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getThenExpression()->accept(*this, data));
+            std::shared_ptr<BaseExpression const> elseExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getElseExpression()->accept(*this, data));
+
+            // If the arguments did not change, we simply push the expression itself.
+            if (conditionExpression.get() == expression.getCondition().get() &&
+                thenExpression.get() == expression.getThenExpression().get() &&
+                elseExpression.get() == expression.getElseExpression().get()) {
+                return expression.getSharedPointer();
+            } else {
+                return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(
+                        new IfThenElseExpression(expression.getManager(), expression.getType(), conditionExpression,
+                                                 thenExpression, elseExpression)));
+            }
+        }
+
+        boost::any
+        SimplificationVisitor::visit(BinaryBooleanFunctionExpression const &expression, boost::any const &data) {
+            std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getFirstOperand()->accept(*this, data));
+            std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getSecondOperand()->accept(*this, data));
+
+            // If the arguments did not change, we simply push the expression itself.
+            if (firstExpression.get() == expression.getFirstOperand().get() &&
+                secondExpression.get() == expression.getSecondOperand().get()) {
+                return expression.getSharedPointer();
+            } else {
+                return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(
+                        new BinaryBooleanFunctionExpression(expression.getManager(), expression.getType(),
+                                                            firstExpression, secondExpression,
+                                                            expression.getOperatorType())));
+            }
+        }
+
+        boost::any
+        SimplificationVisitor::visit(BinaryNumericalFunctionExpression const &expression, boost::any const &data) {
+            std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getFirstOperand()->accept(*this, data));
+            std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getSecondOperand()->accept(*this, data));
+
+            // If the arguments did not change, we simply push the expression itself.
+            if (firstExpression.get() == expression.getFirstOperand().get() &&
+                secondExpression.get() == expression.getSecondOperand().get()) {
+                return expression.getSharedPointer();
+            } else {
+                return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(
+                        new BinaryNumericalFunctionExpression(expression.getManager(), expression.getType(),
+                                                              firstExpression, secondExpression,
+                                                              expression.getOperatorType())));
+            }
+        }
+
+        boost::any SimplificationVisitor::visit(BinaryRelationExpression const &expression, boost::any const &data) {
+            std::shared_ptr<BaseExpression const> firstExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getFirstOperand()->accept(*this, data));
+            std::shared_ptr<BaseExpression const> secondExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getSecondOperand()->accept(*this, data));
+
+            // If the arguments did not change, we simply push the expression itself.
+            if (firstExpression.get() == expression.getFirstOperand().get() &&
+                secondExpression.get() == expression.getSecondOperand().get()) {
+                return expression.getSharedPointer();
+            } else {
+                return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(
+                        new BinaryRelationExpression(expression.getManager(), expression.getType(), firstExpression,
+                                                     secondExpression, expression.getRelationType())));
+            }
+        }
+
+        boost::any SimplificationVisitor::visit(VariableExpression const &expression, boost::any const &) {
+
+            return expression.getSharedPointer();
+
+        }
+
+        boost::any
+        SimplificationVisitor::visit(UnaryBooleanFunctionExpression const &expression, boost::any const &data) {
+            std::shared_ptr<BaseExpression const> operandExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getOperand()->accept(*this, data));
+
+            // If the argument did not change, we simply push the expression itself.
+            if (operandExpression.get() == expression.getOperand().get()) {
+                return expression.getSharedPointer();
+            } else {
+                return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(
+                        new UnaryBooleanFunctionExpression(expression.getManager(), expression.getType(),
+                                                           operandExpression, expression.getOperatorType())));
+            }
+        }
+
+        boost::any
+        SimplificationVisitor::visit(UnaryNumericalFunctionExpression const &expression, boost::any const &data) {
+            std::shared_ptr<BaseExpression const> operandExpression = boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                    expression.getOperand()->accept(*this, data));
+
+            // If the argument did not change, we simply push the expression itself.
+            if (operandExpression.get() == expression.getOperand().get()) {
+                return expression.getSharedPointer();
+            } else {
+                return std::const_pointer_cast<BaseExpression const>(std::shared_ptr<BaseExpression>(
+                        new UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(),
+                                                             operandExpression, expression.getOperatorType())));
+            }
+        }
+
+        boost::any SimplificationVisitor::visit(PredicateExpression const &expression, boost::any const &data) {
+            std::vector<Expression> newExpressions;
+            for (uint64_t i = 0; i < expression.getArity(); ++i) {
+                newExpressions.emplace_back(boost::any_cast<std::shared_ptr<BaseExpression const>>(
+                        expression.getOperand(i)->accept(*this, data)));
+            }
+            std::vector<Expression> newSumExpressions;
+            for (auto const &expr : newExpressions) {
+                newSumExpressions.push_back(
+                        ite(expr, expression.getManager().integer(1), expression.getManager().integer(0)));
+            }
+
+            storm::expressions::Expression finalexpr;
+            if (expression.getPredicateType() == PredicateExpression::PredicateType::AtLeastOneOf) {
+                finalexpr = storm::expressions::sum(newSumExpressions) > expression.getManager().integer(0);
+            } else if (expression.getPredicateType() == PredicateExpression::PredicateType::AtMostOneOf) {
+                finalexpr = storm::expressions::sum(newSumExpressions) <= expression.getManager().integer(1);
+            } else if (expression.getPredicateType() == PredicateExpression::PredicateType::ExactlyOneOf) {
+                finalexpr = storm::expressions::sum(newSumExpressions) == expression.getManager().integer(1);
+            } else {
+                STORM_LOG_ASSERT(false, "Unknown predicate type.");
+            }
+            return std::const_pointer_cast<BaseExpression const>(finalexpr.getBaseExpressionPointer());
+        }
+
+
+        boost::any SimplificationVisitor::visit(BooleanLiteralExpression const &expression, boost::any const &) {
+            return expression.getSharedPointer();
+        }
+
+        boost::any SimplificationVisitor::visit(IntegerLiteralExpression const &expression, boost::any const &) {
+            return expression.getSharedPointer();
+        }
+
+        boost::any SimplificationVisitor::visit(RationalLiteralExpression const &expression, boost::any const &) {
+            return expression.getSharedPointer();
+        }
+
+    }
+}

src/storm/storage/expressions/SimplificationVisitor.h

@@ -0,0 +1,41 @@
+#pragma once
+#include <stack>
+
+#include "storm/storage/expressions/Expression.h"
+#include "storm/storage/expressions/ExpressionVisitor.h"
+
+namespace storm {
+    namespace expressions {
+        class SimplificationVisitor : public ExpressionVisitor {
+        public:
+            /*!
+             * Creates a new simplification visitor that replaces predicates by other (simpler?) predicates.
+             *
+             *  Configuration:
+             *  Currently, the visitor only replaces nonstandard predicates
+             *
+             */
+            SimplificationVisitor();
+
+            /*!
+             * Simplifies based on the configuration.
+             */
+            Expression substitute(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;
+            virtual boost::any visit(PredicateExpression const& expression, boost::any const& data) override;
+
+        protected:
+            //
+        };
+    }
+}

src/storm/storage/expressions/ToDiceStringVisitor.cpp

@@ -241,6 +241,38 @@ namespace storm {
             return boost::any();
         }
 
+        boost::any ToDiceStringVisitor::visit(PredicateExpression const& expression, boost::any const& data) {
+            auto pdt = expression.getPredicateType();
+            STORM_LOG_ASSERT(pdt == PredicateExpression::PredicateType::ExactlyOneOf || pdt == PredicateExpression::PredicateType::AtLeastOneOf || pdt == PredicateExpression::PredicateType::AtMostOneOf, "Only some predicate types are supported.");
+            stream << "(";
+            if (expression.getPredicateType() == PredicateExpression::PredicateType::ExactlyOneOf || expression.getPredicateType() == PredicateExpression::PredicateType::AtMostOneOf) {
+                stream << "(true ";
+                for (uint64_t operandi = 0; operandi < expression.getArity(); ++operandi) {
+                    for (uint64_t operandj = operandi + 1; operandj < expression.getArity(); ++operandj) {
+                        stream << "&& !(";
+                        expression.getOperand(operandi)->accept(*this, data);
+                        stream << " && ";
+                        expression.getOperand(operandj)->accept(*this, data);
+                        stream << ")";
+                    }
+                }
+                stream << ")";
+            }
+            if (expression.getPredicateType() == PredicateExpression::PredicateType::ExactlyOneOf) {
+                stream << " && ";
+            }
+            if (expression.getPredicateType() == PredicateExpression::PredicateType::ExactlyOneOf || expression.getPredicateType() == PredicateExpression::PredicateType::AtLeastOneOf) {
+                stream << "( false";
+                for (uint64_t operandj = 0; operandj < expression.getArity(); ++operandj) {
+                    stream << "|| ";
+                    expression.getOperand(operandj)->accept(*this, data);
+                }
+                stream << ")";
+            }
+            stream << ")";
+            return boost::any();
+        }
+
         boost::any ToDiceStringVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) {
             stream << (expression.getValue() ? " true " : " false ");
             return boost::any();

src/storm/storage/expressions/ToDiceStringVisitor.h

@@ -22,10 +22,12 @@ namespace storm {
             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(PredicateExpression 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::stringstream stream;
             uint64_t nrBits;

src/storm/storage/prism/Assignment.cpp

@@ -21,6 +21,10 @@ namespace storm {
         Assignment Assignment::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return Assignment(this->getVariable(), this->getExpression().substitute(substitution).simplify(), this->getFilename(), this->getLineNumber());
         }
+
+        Assignment Assignment::substituteNonStandardPredicates() const {
+           return Assignment(this->getVariable(), this->getExpression().substituteNonStandardPredicates().simplify(), this->getFilename(), this->getLineNumber());
+        }
         
         bool Assignment::isIdentity() const {
             if(this->expression.isVariable()) {

src/storm/storage/prism/Assignment.h

@@ -57,7 +57,9 @@ namespace storm {
              * @return The resulting assignment.
              */
             Assignment substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
-            
+
+            Assignment substituteNonStandardPredicates() const;
+
             /*!
              * Checks whether the assignment is an identity (lhs equals rhs)
              * 

src/storm/storage/prism/BooleanVariable.cpp

@@ -11,6 +11,10 @@ namespace storm {
         BooleanVariable BooleanVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->isObservable(), this->getFilename(), this->getLineNumber());
         }
+
+        BooleanVariable BooleanVariable::substituteNonStandardPredicates() const {
+            return BooleanVariable(this->getExpressionVariable(), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substituteNonStandardPredicates() : this->getInitialValueExpression(), this->isObservable(), this->getFilename(), this->getLineNumber());
+        }
         
         void BooleanVariable::createMissingInitialValue() {
             if (!this->hasInitialValue()) {

src/storm/storage/prism/BooleanVariable.h

@@ -34,7 +34,8 @@ namespace storm {
              * @return The resulting boolean variable.
              */
             BooleanVariable substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
-            
+            BooleanVariable substituteNonStandardPredicates() const;
+
             virtual void createMissingInitialValue() override;
             
             friend std::ostream& operator<<(std::ostream& stream, BooleanVariable const& variable);

src/storm/storage/prism/Command.cpp

@@ -56,7 +56,17 @@ namespace storm {
             
             return Command(this->getGlobalIndex(), this->isMarkovian(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substitute(substitution).simplify(), newUpdates, this->getFilename(), this->getLineNumber());
         }
-        
+
+        Command Command::substituteNonStandardPredicates() const {
+            std::vector<Update> newUpdates;
+            newUpdates.reserve(this->getNumberOfUpdates());
+            for (auto const& update : this->getUpdates()) {
+                newUpdates.emplace_back(update.substituteNonStandardPredicates());
+            }
+
+            return Command(this->getGlobalIndex(), this->isMarkovian(), this->getActionIndex(), this->getActionName(), this->getGuardExpression().substituteNonStandardPredicates().simplify(), newUpdates, this->getFilename(), this->getLineNumber());
+        }
+
         bool Command::isLabeled() const {
             return labeled;
         }

src/storm/storage/prism/Command.h

@@ -114,7 +114,8 @@ namespace storm {
              * @return The resulting command.
              */
             Command substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
-            
+
+            Command substituteNonStandardPredicates() const;
             /*!
              * Retrieves whether the command possesses a synchronization label.
              *

src/storm/storage/prism/Formula.cpp

@@ -44,6 +44,15 @@ namespace storm {
                 return Formula(this->getName(), this->getExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
             }
         }
+
+        Formula Formula::substituteNonStandardPredicates() const {
+            assert(this->getExpression().isInitialized());
+            if (hasExpressionVariable()) {
+                return Formula(this->getExpressionVariable(), this->getExpression().substituteNonStandardPredicates(), this->getFilename(), this->getLineNumber());
+            } else {
+                return Formula(this->getName(), this->getExpression().substituteNonStandardPredicates(), this->getFilename(), this->getLineNumber());
+            }
+        }
         
         std::ostream& operator<<(std::ostream& stream, Formula const& formula) {
             stream << "formula " << formula.getName() << " = " << formula.getExpression() << ";";

src/storm/storage/prism/Formula.h

@@ -92,6 +92,7 @@ namespace storm {
              * @return The resulting formula.
              */
             Formula substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+            Formula substituteNonStandardPredicates() const;
             
             friend std::ostream& operator<<(std::ostream& stream, Formula const& formula);
             

src/storm/storage/prism/IntegerVariable.cpp

@@ -21,6 +21,10 @@ namespace storm {
         IntegerVariable IntegerVariable::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substitute(substitution), this->getUpperBoundExpression().substitute(substitution), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substitute(substitution) : this->getInitialValueExpression(), this->isObservable(), this->getFilename(), this->getLineNumber());
         }
+
+        IntegerVariable IntegerVariable::substituteNonStandardPredicates() const {
+            return IntegerVariable(this->getExpressionVariable(), this->getLowerBoundExpression().substituteNonStandardPredicates(), this->getUpperBoundExpression().substituteNonStandardPredicates(), this->getInitialValueExpression().isInitialized() ? this->getInitialValueExpression().substituteNonStandardPredicates() : this->getInitialValueExpression(), this->isObservable(), this->getFilename(), this->getLineNumber());
+        }
         
         void IntegerVariable::createMissingInitialValue() {
             if (!this->hasInitialValue()) {

src/storm/storage/prism/IntegerVariable.h

@@ -57,7 +57,9 @@ namespace storm {
              * @return The resulting boolean variable.
              */
             IntegerVariable substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
-            
+
+            IntegerVariable substituteNonStandardPredicates() const;
+
             virtual void createMissingInitialValue() override;
             
             friend std::ostream& operator<<(std::ostream& stream, IntegerVariable const& variable);

src/storm/storage/prism/Label.cpp

@@ -18,6 +18,10 @@ namespace storm {
         Label Label::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return Label(this->getName(), this->getStatePredicateExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
         }
+
+        Label Label::substituteNonStandardPredicates() const {
+            return Label(this->getName(), this->getStatePredicateExpression().substituteNonStandardPredicates(), this->getFilename(), this->getLineNumber());
+        }
         
         std::ostream& operator<<(std::ostream& stream, Label const& label) {
             stream << "label \"" << label.getName() << "\" = " << label.getStatePredicateExpression() << ";";
@@ -31,5 +35,10 @@ namespace storm {
         ObservationLabel ObservationLabel::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             return ObservationLabel(this->getName(), this->getStatePredicateExpression().substitute(substitution), this->getFilename(), this->getLineNumber());
         }
+
+        ObservationLabel ObservationLabel::substituteNonStandardPredicates() const {
+            return ObservationLabel(this->getName(), this->getStatePredicateExpression().substituteNonStandardPredicates(), this->getFilename(), this->getLineNumber());
+        }
+
     } // namespace prism
 } // namespace storm

src/storm/storage/prism/Label.h

@@ -58,6 +58,7 @@ namespace storm {
              * @return The resulting label.
              */
             Label substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+            Label substituteNonStandardPredicates() const;
             
             friend std::ostream& operator<<(std::ostream& stream, Label const& label);
             
@@ -96,7 +97,7 @@ namespace storm {
             * @return The resulting label.
             */
             ObservationLabel substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
-
+            ObservationLabel substituteNonStandardPredicates() const;
         };
 
 

src/storm/storage/prism/Module.cpp

@@ -235,6 +235,28 @@ namespace storm {
             
             return Module(this->getName(), newBooleanVariables, newIntegerVariables, this->getClockVariables(), this->getInvariant(), newCommands, this->getFilename(), this->getLineNumber());
         }
+
+        Module Module::substituteNonStandardPredicates() const {
+            std::vector<BooleanVariable> newBooleanVariables;
+            newBooleanVariables.reserve(this->getNumberOfBooleanVariables());
+            for (auto const& booleanVariable : this->getBooleanVariables()) {
+                newBooleanVariables.emplace_back(booleanVariable.substituteNonStandardPredicates());
+            }
+
+            std::vector<IntegerVariable> newIntegerVariables;
+            newBooleanVariables.reserve(this->getNumberOfIntegerVariables());
+            for (auto const& integerVariable : this->getIntegerVariables()) {
+                newIntegerVariables.emplace_back(integerVariable.substituteNonStandardPredicates());
+            }
+
+            std::vector<Command> newCommands;
+            newCommands.reserve(this->getNumberOfCommands());
+            for (auto const& command : this->getCommands()) {
+                newCommands.emplace_back(command.substituteNonStandardPredicates());
+            }
+
+            return Module(this->getName(), newBooleanVariables, newIntegerVariables, this->getClockVariables(), this->getInvariant(), newCommands, this->getFilename(), this->getLineNumber());
+        }
         
         bool Module::containsVariablesOnlyInUpdateProbabilities(std::set<storm::expressions::Variable> const& undefinedConstantVariables) const {
             for (auto const& booleanVariable : this->getBooleanVariables()) {

src/storm/storage/prism/Module.h

@@ -250,7 +250,9 @@ namespace storm {
              * @return The resulting module.
              */
             Module substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
-            
+
+            Module substituteNonStandardPredicates() const;
+
             /*!
              * Checks whether the given variables only appear in the update probabilities of the module and nowhere else.
              *

src/storm/storage/prism/Program.cpp

@@ -885,7 +885,51 @@ namespace storm {
         Program Program::substituteFormulas() const {
             return substituteConstantsFormulas(false, true);
         }
-        
+
+        Program Program::substituteNonStandardPredicates() const {
+            // TODO support in constants,  initial construct, and rewards
+
+            std::vector<Formula> newFormulas;
+            newFormulas.reserve(this->getNumberOfFormulas());
+            for (auto const& oldFormula : this->getFormulas()) {
+                newFormulas.emplace_back(oldFormula.substituteNonStandardPredicates());
+            }
+
+            std::vector<BooleanVariable> newBooleanVariables;
+            newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
+            for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
+                newBooleanVariables.emplace_back(booleanVariable.substituteNonStandardPredicates());
+            }
+
+            std::vector<IntegerVariable> newIntegerVariables;
+            newBooleanVariables.reserve(this->getNumberOfGlobalIntegerVariables());
+            for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
+                newIntegerVariables.emplace_back(integerVariable.substituteNonStandardPredicates());
+            }
+
+            std::vector<Module> newModules;
+            newModules.reserve(this->getNumberOfModules());
+            for (auto const& module : this->getModules()) {
+                newModules.emplace_back(module.substituteNonStandardPredicates());
+            }
+
+
+            std::vector<Label> newLabels;
+            newLabels.reserve(this->getNumberOfLabels());
+            for (auto const& label : this->getLabels()) {
+                newLabels.emplace_back(label.substituteNonStandardPredicates());
+            }
+
+            std::vector<ObservationLabel> newObservationLabels;
+            newObservationLabels.reserve(this->getNumberOfObservationLabels());
+            for (auto const& label : this->getObservationLabels()) {
+                newObservationLabels.emplace_back(label.substituteNonStandardPredicates());
+            }
+
+            return Program(this->manager, this->getModelType(), this->getConstants(), newBooleanVariables, newIntegerVariables, newFormulas, newModules, this->getActionNameToIndexMapping(), this->getRewardModels(), newLabels, newObservationLabels, initialConstruct, this->getOptionalSystemCompositionConstruct(), prismCompatibility);
+
+        }
+
         Program Program::substituteConstantsFormulas(bool substituteConstants, bool substituteFormulas) const {
             // Formulas need to be substituted first. otherwise, constants appearing in formula expressions can not be handled properly
             if (substituteConstants && substituteFormulas) {

src/storm/storage/prism/Program.h

@@ -628,6 +628,11 @@ namespace storm {
              * @return The resulting program that only contains expressions over variables of the program (and maybe constants).
              */
             Program substituteFormulas() const;
+
+            /*!
+             * Substitutes all nonstandard predicates in expressions of the program by their defining expressions
+             */
+             Program substituteNonStandardPredicates() const;
             
             /*!
              * Substitutes all constants and/or formulas appearing in the expressions of the program by their defining expressions. For

src/storm/storage/prism/Update.cpp

@@ -75,7 +75,19 @@ namespace storm {
             // FIXME: The expression could be simplified, but 1/K (where K is an int) is then resolved to 0, which is incorrect (for probabilities).
             return Update(this->getGlobalIndex(), newLikelihoodExpression, newAssignments, this->getFilename(), this->getLineNumber());
         }
-        
+
+        Update Update::substituteNonStandardPredicates() const {
+            std::vector<Assignment> newAssignments;
+            newAssignments.reserve(this->getNumberOfAssignments());
+            for (auto const& assignment : this->getAssignments()) {
+                newAssignments.emplace_back(assignment.substituteNonStandardPredicates());
+            }
+            auto newLikelihoodExpression = this->getLikelihoodExpression().substituteNonStandardPredicates();
+            STORM_LOG_THROW(likelihoodExpression.containsVariables() || likelihoodExpression.evaluateAsRational() >= 0, storm::exceptions::IllegalArgumentException, "Substitution yielding negative probabilities in '" << this->getLikelihoodExpression() << "' are not allowed.");
+            return Update(this->getGlobalIndex(), newLikelihoodExpression, newAssignments, this->getFilename(), this->getLineNumber());
+        }
+
+
         Update Update::removeIdentityAssignments() const {
             std::vector<Assignment> newAssignments;
             newAssignments.reserve(getNumberOfAssignments());

src/storm/storage/prism/Update.h

@@ -92,6 +92,8 @@ namespace storm {
              * @return The resulting update.
              */
             Update removeIdentityAssignments() const;
+
+            Update substituteNonStandardPredicates() const;
             
             /*!
              * Simplifies the update in various ways (also removes identity assignments)