diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index 49a2a4ccd..9696d9a33 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -19,7 +19,7 @@ #include "src/ir/RewardModel.h" #include "src/ir/StateReward.h" #include "src/ir/TransitionReward.h" - +#include "src/utility/IRUtility.h" #include "src/models/AbstractModel.h" #include "src/models/Dtmc.h" #include "src/models/Ctmc.h" @@ -27,253 +27,18 @@ #include "src/models/Ctmdp.h" #include "src/models/AtomicPropositionsLabeling.h" #include "src/storage/SparseMatrix.h" -#include "src/storage/LabeledValues.h" #include "src/settings/Settings.h" #include "src/exceptions/WrongFormatException.h" -#include - #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; +using namespace storm::utility::ir; + namespace storm { namespace adapters { - - /*! - * A state of the model, i.e. a valuation of all variables. - */ - typedef std::pair, std::vector> StateType; - - /*! - * A helper class that provides the functionality to compute a hash value for states of the model. - */ - class StateHash { - public: - std::size_t operator()(StateType* state) const { - size_t seed = 0; - for (auto it : state->first) { - boost::hash_combine(seed, it); - } - for (auto it : state->second) { - boost::hash_combine(seed, it); - } - return seed; - } - }; - - /*! - * A helper class that provides the functionality to compare states of the model wrt. equality. - */ - class StateCompare { - public: - bool operator()(StateType* state1, StateType* state2) const { - return *state1 == *state2; - } - }; - - /*! - * A helper class that provides the functionality to compare states of the model wrt. the relation "<". - */ - class StateLess { - public: - bool operator()(StateType* state1, StateType* state2) const { - // Compare boolean variables. - for (uint_fast64_t i = 0; i < state1->first.size(); ++i) { - if (!state1->first.at(i) && state2->first.at(i)) { - return true; - } - } - // Then compare integer variables. - for (uint_fast64_t i = 0; i < state1->second.size(); ++i) { - if (!state1->second.at(i) && state2->second.at(i)) { - return true; - } - } - return false; - } - }; - - // A structure holding information about a particular choice. - template> - struct Choice { - public: - Choice(std::string const& actionLabel) : distribution(), actionLabel(actionLabel), choiceLabels() { - // Intentionally left empty. - } - - /*! - * Returns an iterator to the first element of this choice. - * - * @return An iterator to the first element of this choice. - */ - typename std::map::iterator begin() { - return distribution.begin(); - } - - /*! - * Returns an iterator to the first element of this choice. - * - * @return An iterator to the first element of this choice. - */ - typename std::map::const_iterator begin() const { - return distribution.cbegin(); - } - - /*! - * Returns an iterator that points past the elements of this choice. - * - * @return An iterator that points past the elements of this choice. - */ - typename std::map::iterator end() { - return distribution.end(); - } - - /*! - * Returns an iterator that points past the elements of this choice. - * - * @return An iterator that points past the elements of this choice. - */ - typename std::map::const_iterator end() const { - return distribution.cend(); - } - - /*! - * Returns an iterator to the element with the given key, if there is one. Otherwise, the iterator points to - * distribution.end(). - * - * @param value The value to find. - * @return An iterator to the element with the given key, if there is one. - */ - typename std::map::iterator find(uint_fast64_t value) { - return distribution.find(value); - } - - /*! - * Inserts the contents of this object to the given output stream. - * - * @param out The stream in which to insert the contents. - */ - friend std::ostream& operator<<(std::ostream& out, Choice const& choice) { - out << "<"; - for (auto const& stateProbabilityPair : choice.distribution) { - out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", "; - } - out << ">"; - return out; - } - - /*! - * Adds the given label to the labels associated with this choice. - * - * @param label The label to associate with this choice. - */ - void addChoiceLabel(uint_fast64_t label) { - choiceLabels.insert(label); - } - - /*! - * Adds the given label set to the labels associated with this choice. - * - * @param labelSet The label set to associate with this choice. - */ - void addChoiceLabels(std::set const& labelSet) { - for (uint_fast64_t label : labelSet) { - addChoiceLabel(label); - } - } - - /*! - * Retrieves the set of labels associated with this choice. - * - * @return The set of labels associated with this choice. - */ - std::set const& getChoiceLabels() const { - return choiceLabels; - } - - /*! - * Retrieves the action label of this choice. - * - * @return The action label of this choice. - */ - std::string const& getActionLabel() const { - return actionLabel; - } - - /*! - * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, - * yet. - * - * @param state The state for which to add the entry. - * @return A reference to the entry that is associated with the given state. - */ - ValueType& getOrAddEntry(uint_fast64_t state) { - auto stateProbabilityPair = distribution.find(state); - if (stateProbabilityPair == distribution.end()) { - distribution[state] = ValueType(); - } - return distribution.at(state); - } - - /*! - * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, - * yet. - * - * @param state The state for which to add the entry. - * @return A reference to the entry that is associated with the given state. - */ - ValueType const& getOrAddEntry(uint_fast64_t state) const { - auto stateProbabilityPair = distribution.find(state); - - if (stateProbabilityPair == distribution.end()) { - distribution[state] = ValueType(); - } - return distribution.at(state); - } - - private: - // The distribution that is associated with the choice. - std::map distribution; - - // The label of the choice. - std::string actionLabel; - - // The labels that are associated with this choice. - std::set choiceLabels; - }; - - /*! - * Adds the target state and probability to the given choice and ignores the labels. This function overloads with - * other functions to ensure the proper treatment of labels. - * - * @param choice The choice to which to add the target state and probability. - * @param state The target state of the probability. - * @param probability The probability to reach the target state in one step. - * @param labels A set of labels that is supposed to be associated with this state and probability. NOTE: this - * is ignored by this particular function but not by the overloaded functions. - */ - template - void addProbabilityToChoice(Choice& choice, uint_fast64_t state, ValueType probability, std::set const& labels) { - choice.getOrAddEntry(state) += probability; - } - - /*! - * Adds the target state and probability to the given choice and labels it accordingly. This function overloads - * with other functions to ensure the proper treatment of labels. - * - * @param choice The choice to which to add the target state and probability. - * @param state The target state of the probability. - * @param probability The probability to reach the target state in one step. - * @param labels A set of labels that is supposed to be associated with this state and probability. - */ - template - void addProbabilityToChoice(Choice>& choice, uint_fast64_t state, ValueType probability, std::set const& labels) { - auto& labeledEntry = choice.getOrAddEntry(state); - labeledEntry.addValue(probability, labels); - } - template class ExplicitModelAdapter { public: @@ -315,25 +80,6 @@ namespace storm { std::vector> choiceLabeling; }; - // A structure storing information about the used variables of the program. - struct VariableInformation { - VariableInformation() : booleanVariables(), booleanVariableToIndexMap(), integerVariables(), integerVariableToIndexMap() { - // Intentinally left empty. - } - - // List of all boolean variables. - std::vector booleanVariables; - - // A mapping of boolean variable names to their indices. - std::map booleanVariableToIndexMap; - - // List of all integer variables. - std::vector integerVariables; - - // A mapping of integer variable names to their indices. - std::map integerVariableToIndexMap; - }; - /*! * Convert the program given at construction time to an abstract model. The type of the model is the one * specified in the program. The given reward model name selects the rewards that the model will contain. @@ -346,25 +92,25 @@ namespace storm { * rewards. * @return The explicit model that was given by the probabilistic program. */ - static std::shared_ptr> translateProgram(storm::ir::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") { + static std::unique_ptr> translateProgram(storm::ir::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") { // Start by defining the undefined constants in the model. defineUndefinedConstants(program, constantDefinitionString); ModelComponents modelComponents = buildModelComponents(program, rewardModelName); - std::shared_ptr> result; + std::unique_ptr> result; switch (program.getModelType()) { case storm::ir::Program::DTMC: - result = std::shared_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Dtmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::CTMC: - result = std::shared_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Ctmc(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::MDP: - result = std::shared_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Mdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; case storm::ir::Program::CTMDP: - result = std::shared_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); + result = std::unique_ptr>(new storm::models::Ctmdp(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional>(), std::move(modelComponents.choiceLabeling))); break; default: LOG4CPLUS_ERROR(logger, "Error while creating model from probabilistic program: cannot handle this model type."); @@ -448,129 +194,7 @@ namespace storm { } return newState; } - - - /*! - * Defines the undefined constants of the given program using the given string. - * - * @param program The program in which to define the constants. - * @param constantDefinitionString A comma-separated list of constant definitions. - */ - static void defineUndefinedConstants(storm::ir::Program& program, std::string const& constantDefinitionString) { - if (!constantDefinitionString.empty()) { - // Parse the string that defines the undefined constants of the model and make sure that it contains exactly - // one value for each undefined constant of the model. - std::vector definitions; - boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); - for (auto& definition : definitions) { - boost::trim(definition); - - // Check whether the token could be a legal constant definition. - uint_fast64_t positionOfAssignmentOperator = definition.find('='); - if (positionOfAssignmentOperator == std::string::npos) { - throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error."; - } - - // Now extract the variable name and the value from the string. - std::string constantName = definition.substr(0, positionOfAssignmentOperator); - boost::trim(constantName); - std::string value = definition.substr(positionOfAssignmentOperator + 1); - boost::trim(value); - - // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. - if (program.hasUndefinedBooleanConstant(constantName)) { - if (value == "true") { - program.getUndefinedBooleanConstantExpression(constantName)->define(true); - } else if (value == "false") { - program.getUndefinedBooleanConstantExpression(constantName)->define(false); - } else { - throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; - } - } else if (program.hasUndefinedIntegerConstant(constantName)) { - try { - int_fast64_t integerValue = std::stoi(value); - program.getUndefinedIntegerConstantExpression(constantName)->define(integerValue); - } catch (std::invalid_argument const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << "."; - } catch (std::out_of_range const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << " (value too big)."; - } - } else if (program.hasUndefinedDoubleConstant(constantName)) { - try { - double doubleValue = std::stod(value); - program.getUndefinedDoubleConstantExpression(constantName)->define(doubleValue); - } catch (std::invalid_argument const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << "."; - } catch (std::out_of_range const&) { - throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big)."; - } - - } else { - throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; - } - } - } - } - - /*! - * Undefines all previously defined constants in the given program. - * - * @param program The program in which to undefine the constants. - */ - static void undefineUndefinedConstants(storm::ir::Program& program) { - for (auto const& nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) { - nameExpressionPair.second->undefine(); - } - for (auto const& nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) { - nameExpressionPair.second->undefine(); - } - for (auto const& nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) { - nameExpressionPair.second->undefine(); - } - } - - /*! - * Generates the initial state of the given program. - * - * @param program The program for which to construct the initial state. - * @param variableInformation A structure with information about the variables in the program. - * @return The initial state. - */ - static StateType* getInitialState(storm::ir::Program const& program, VariableInformation const& variableInformation) { - StateType* initialState = new StateType(); - initialState->first.resize(variableInformation.booleanVariables.size()); - initialState->second.resize(variableInformation.integerVariables.size()); - - // Start with boolean variables. - for (uint_fast64_t i = 0; i < variableInformation.booleanVariables.size(); ++i) { - // Check if an initial value is given - if (variableInformation.booleanVariables[i].getInitialValue().get() == nullptr) { - // If no initial value was given, we assume that the variable is initially false. - std::get<0>(*initialState)[i] = false; - } else { - // Initial value was given. - bool initialValue = variableInformation.booleanVariables[i].getInitialValue()->getValueAsBool(nullptr); - std::get<0>(*initialState)[i] = initialValue; - } - } - - // Now process integer variables. - for (uint_fast64_t i = 0; i < variableInformation.integerVariables.size(); ++i) { - // Check if an initial value was given. - if (variableInformation.integerVariables[i].getInitialValue().get() == nullptr) { - // No initial value was given, so we assume that the variable initially has the least value it can take. - std::get<1>(*initialState)[i] = variableInformation.integerVariables[i].getLowerBound()->getValueAsInt(nullptr); - } else { - // Initial value was given. - int_fast64_t initialValue = variableInformation.integerVariables[i].getInitialValue()->getValueAsInt(nullptr); - std::get<1>(*initialState)[i] = initialValue; - } - } - - LOG4CPLUS_DEBUG(logger, "Generated initial state."); - return initialState; - } - + /*! * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to * the lists of all states with a new id. If the state was already known, the object that is pointed to by @@ -646,59 +270,7 @@ namespace storm { } return result; } - - /*! - * Aggregates information about the variables in the program. - * - * @param program The program whose variables to aggregate. - */ - static VariableInformation createVariableInformation(storm::ir::Program const& program) { - VariableInformation result; - - uint_fast64_t numberOfIntegerVariables = 0; - uint_fast64_t numberOfBooleanVariables = 0; - - // Count number of variables. - numberOfBooleanVariables += program.getNumberOfGlobalBooleanVariables(); - numberOfIntegerVariables += program.getNumberOfGlobalIntegerVariables(); - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); - numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); - } - - // Resize the variable vectors appropriately. - result.booleanVariables.resize(numberOfBooleanVariables); - result.integerVariables.resize(numberOfIntegerVariables); - - // Create variables. - for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) { - storm::ir::BooleanVariable const& var = program.getGlobalBooleanVariable(i); - result.booleanVariables[var.getGlobalIndex()] = var; - result.booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); - } - for (uint_fast64_t i = 0; i < program.getNumberOfGlobalIntegerVariables(); ++i) { - storm::ir::IntegerVariable const& var = program.getGlobalIntegerVariable(i); - result.integerVariables[var.getGlobalIndex()] = var; - result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); - } - for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { - storm::ir::Module const& module = program.getModule(i); - - for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { - storm::ir::BooleanVariable const& var = module.getBooleanVariable(j); - result.booleanVariables[var.getGlobalIndex()] = var; - result.booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); - } - for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { - storm::ir::IntegerVariable const& var = module.getIntegerVariable(j); - result.integerVariables[var.getGlobalIndex()] = var; - result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); - } - } - - return result; - } - + static std::list> getUnlabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue& stateQueue) { std::list> result; diff --git a/src/adapters/SymbolicExpressionAdapter.h b/src/adapters/SymbolicExpressionAdapter.h index 5acb90c9c..1c1b8ca7e 100644 --- a/src/adapters/SymbolicExpressionAdapter.h +++ b/src/adapters/SymbolicExpressionAdapter.h @@ -31,12 +31,6 @@ public: return stack.top(); } - virtual void visit(storm::ir::expressions::BaseExpression* expression) { - std::cout << expression->toString() << std::endl; - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression " - << " of abstract superclass type."; - } - virtual void visit(storm::ir::expressions::BinaryBooleanFunctionExpression* expression) { expression->getLeft()->accept(this); expression->getRight()->accept(this); diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index 15d7e50bc..211baa2f1 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -14,15 +14,17 @@ namespace storm { namespace adapters { - + class Z3ExpressionAdapter : public storm::ir::expressions::ExpressionVisitor { public: /*! * Creates a Z3ExpressionAdapter over the given Z3 context. * - * @param context The Z3 context over which to build the expressions. + * @param context A reference to the Z3 context over which to build the expressions. Be careful to guarantee + * the lifetime of the context as long as the instance of this adapter is used. + * @param variableToExpressionMap A mapping from variable names to their corresponding Z3 expressions. */ - Z3ExpressionAdapter(z3::context const& context, std::map const& variableToExpressionMap) : context(context), stack(), variableToExpressionMap(variableToExpressionMap) { + Z3ExpressionAdapter(z3::context& context, std::map const& variableToExpressionMap) : context(context), stack(), variableToExpressionMap(variableToExpressionMap) { // Intentionally left empty. } @@ -32,12 +34,14 @@ namespace storm { * @param expression The expression to translate. * @return An equivalent expression for Z3. */ - z3::expr translateExpression(std::shared_ptr expression) { + z3::expr translateExpression(std::unique_ptr const& expression) { expression->accept(this); - return stack.top(); + z3::expr result = stack.top(); + stack.pop(); + return result; } - virtual void visit(BinaryBooleanFunctionExpression* expression) { + virtual void visit(ir::expressions::BinaryBooleanFunctionExpression* expression) { expression->getLeft()->accept(this); expression->getRight()->accept(this); @@ -45,7 +49,7 @@ namespace storm { stack.pop(); z3::expr leftResult = stack.top(); stack.pop(); - + switch(expression->getFunctionType()) { case storm::ir::expressions::BinaryBooleanFunctionExpression::AND: stack.push(leftResult && rightResult); @@ -56,10 +60,10 @@ namespace storm { default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; } - + } - virtual void visit(BinaryNumericalFunctionExpression* expression) { + virtual void visit(ir::expressions::BinaryNumericalFunctionExpression* expression) { expression->getLeft()->accept(this); expression->getRight()->accept(this); @@ -86,7 +90,7 @@ namespace storm { } } - virtual void visit(BinaryRelationExpression* expression) { + virtual void visit(ir::expressions::BinaryRelationExpression* expression) { expression->getLeft()->accept(this); expression->getRight()->accept(this); @@ -119,7 +123,7 @@ namespace storm { } } - virtual void visit(BooleanConstantExpression* expression) { + virtual void visit(ir::expressions::BooleanConstantExpression* expression) { if (!expression->isDefined()) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << ". Boolean constant '" << expression->getConstantName() << "' is undefined."; @@ -128,26 +132,28 @@ namespace storm { stack.push(context.bool_val(expression->getValue())); } - virtual void visit(BooleanLiteralExpression* expression) { - stack.push(context.bool_val(expression->getValueAsBool(nullptr)))); + virtual void visit(ir::expressions::BooleanLiteralExpression* expression) { + stack.push(context.bool_val(expression->getValueAsBool(nullptr))); } - virtual void visit(DoubleConstantExpression* expression) { + virtual void visit(ir::expressions::DoubleConstantExpression* expression) { if (!expression->isDefined()) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << ". Double constant '" << expression->getConstantName() << "' is undefined."; } - // FIXME: convert double value to suitable format. - stack.push(context.real_val(expression->getValue())); + std::stringstream fractionStream; + fractionStream << expression->getValue(); + stack.push(context.real_val(fractionStream.str().c_str())); } - virtual void visit(DoubleLiteralExpression* expression) { - // FIXME: convert double value to suitable format. - stack.push(context.real_val(expression->getValue())); + virtual void visit(ir::expressions::DoubleLiteralExpression* expression) { + std::stringstream fractionStream; + fractionStream << expression->getValueAsDouble(nullptr); + stack.push(context.real_val(fractionStream.str().c_str())); } - virtual void visit(IntegerConstantExpression* expression) { + virtual void visit(ir::expressions::IntegerConstantExpression* expression) { if (!expression->isDefined()) { throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " << ". Integer constant '" << expression->getConstantName() << "' is undefined."; @@ -156,11 +162,11 @@ namespace storm { stack.push(context.int_val(expression->getValue())); } - virtual void visit(IntegerLiteralExpression* expression) { - stack.push(context.int_val(expression->getValue())); + virtual void visit(ir::expressions::IntegerLiteralExpression* expression) { + stack.push(context.int_val(expression->getValueAsInt(nullptr))); } - virtual void visit(UnaryBooleanFunctionExpression* expression) { + virtual void visit(ir::expressions::UnaryBooleanFunctionExpression* expression) { expression->getChild()->accept(this); z3::expr childResult = stack.top(); @@ -175,7 +181,7 @@ namespace storm { } } - virtual void visit(UnaryNumericalFunctionExpression* expression) { + virtual void visit(ir::expressions::UnaryNumericalFunctionExpression* expression) { expression->getChild()->accept(this); z3::expr childResult = stack.top(); @@ -190,17 +196,17 @@ namespace storm { } } - virtual void visit(VariableExpression* expression) { - stack.push(variableToExpressionMap.at(expression->getVariableName()); + virtual void visit(ir::expressions::VariableExpression* expression) { + stack.push(variableToExpressionMap.at(expression->getVariableName())); } private: - z3::context context; + z3::context& context; std::stack stack; - std::map variableToExpressionMap - } - + std::map variableToExpressionMap; + }; + } // namespace adapters } // namespace storm - + #endif /* STORM_ADAPTERS_Z3EXPRESSIONADAPTER_H_ */ diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index bbd4e623b..f2b0ead6e 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -18,7 +18,8 @@ #include "z3++.h" #endif -#include "src/ir/Program.h" +#include "src/adapters/ExplicitModelAdapter.h" +#include "src/adapters/Z3ExpressionAdapter.h" #include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h" #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" @@ -158,25 +159,24 @@ namespace storm { } /*! - * Asserts cuts that rule out a lot of suboptimal solutions. + * Asserts cuts that are derived from the explicit representation of the model and rule out a lot of + * suboptimal solutions. * * @param labeledMdp The labeled MDP for which to compute 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::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, z3::context& context, z3::solver& solver) { - // Walk through the MDP and: - // identify labels enabled in initial states - // identify labels that can directly precede a given action - // identify labels that directly reach a target state - // identify labels that can directly follow a given action - // TODO: identify which labels need to synchronize + static void assertExplicitCuts(storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, z3::context& context, z3::solver& solver) { + // Walk through the MDP and + // * identify labels enabled in initial states + // * identify labels that can directly precede a given action + // * identify labels that directly reach a target state + // * identify labels that can directly follow a given action std::set initialLabels; std::map> precedingLabels; std::set targetLabels; std::map> followingLabels; - std::map> synchronizingLabels; // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); @@ -352,6 +352,47 @@ namespace storm { assertConjunction(context, solver, formulae); } + /*! + * Asserts cuts that are derived from the symbolic representation of the model and rule out a lot of + * suboptimal solutions. + * + * @param program The symbolic representation of the model in terms of a program. + * @param context The Z3 context in which to build the expressions. + * @param solver The solver to use for the satisfiability evaluation. + */ + static void assertSymbolicCuts(storm::ir::Program const& program, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, z3::context& context, z3::solver& solver) { + // TODO: + // find synchronization cuts + // find forward/backward cuts + + storm::utility::ir::VariableInformation programVariableInformation = storm::utility::ir::createVariableInformation(program); + + // Create a context and register all variables of the program with their correct type. + z3::context localContext; + std::map solverVariables; + for (auto const& booleanVariable : programVariableInformation.booleanVariables) { + solverVariables.emplace(booleanVariable.getName(), localContext.bool_const(booleanVariable.getName().c_str())); + } + for (auto const& integerVariable : programVariableInformation.integerVariables) { + solverVariables.emplace(integerVariable.getName(), localContext.int_const(integerVariable.getName().c_str())); + } + + // Now create a corresponding local solver and assert all range bounds for the integer variables. + z3::solver localSolver(localContext); + storm::adapters::Z3ExpressionAdapter expressionAdapter(localContext, solverVariables); + for (auto const& integerVariable : programVariableInformation.integerVariables) { + z3::expr lowerBound = expressionAdapter.translateExpression(integerVariable.getLowerBound()); + lowerBound = solverVariables.at(integerVariable.getName()) >= lowerBound; + localSolver.add(lowerBound); + + z3::expr upperBound = expressionAdapter.translateExpression(integerVariable.getUpperBound()); + upperBound = solverVariables.at(integerVariable.getName()) <= upperBound; + localSolver.add(upperBound); + } + + std::cout << localSolver << std::endl; + } + /*! * Asserts that the disjunction of the given formulae holds. If the content of the disjunction is empty, * this corresponds to asserting false. @@ -636,8 +677,10 @@ namespace storm { #endif public: - static std::set getMinimalCommandSet(storm::ir::Program const& program, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool checkThresholdFeasible = false) { + static std::set getMinimalCommandSet(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool checkThresholdFeasible = false) { #ifdef STORM_HAVE_Z3 + storm::utility::ir::defineUndefinedConstants(program, constantDefinitionString); + // (0) Check whether the MDP is indeed labeled. if (!labeledMdp.hasChoiceLabels()) { throw storm::exceptions::InvalidArgumentException() << "Minimal command set generation is impossible for unlabeled model."; @@ -661,7 +704,8 @@ namespace storm { assertInitialConstraints(program, labeledMdp, psiStates, context, solver, variableInformation, relevancyInformation); // (6) Add constraints that cut off a lot of suboptimal solutions. - assertCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, context, solver); + assertExplicitCuts(labeledMdp, psiStates, variableInformation, relevancyInformation, context, solver); + assertSymbolicCuts(program, variableInformation, relevancyInformation, 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. @@ -716,7 +760,8 @@ namespace storm { } std::cout << std::endl; - // (8) Return the resulting command set. + // (8) Return the resulting command set after undefining the constants. + storm::utility::ir::undefineUndefinedConstants(program); return commandSet; #else diff --git a/src/ir/expressions/BaseExpression.cpp b/src/ir/expressions/BaseExpression.cpp index 2d85dfdc9..66771d6b0 100644 --- a/src/ir/expressions/BaseExpression.cpp +++ b/src/ir/expressions/BaseExpression.cpp @@ -63,10 +63,6 @@ namespace storm { << this->getTypeName() << " because evaluation implementation is missing."; } - void BaseExpression::accept(ExpressionVisitor* visitor) { - visitor->visit(this); - } - std::string BaseExpression::getTypeName() const { switch(type) { case bool_: return std::string("bool"); diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h index 1f045f5f4..948ed9d88 100644 --- a/src/ir/expressions/BaseExpression.h +++ b/src/ir/expressions/BaseExpression.h @@ -127,7 +127,7 @@ namespace storm { * * @param visitor The visitor that is supposed to visit each node of the expression tree. */ - virtual void accept(ExpressionVisitor* visitor); + virtual void accept(ExpressionVisitor* visitor) = 0; /*! * Retrieves a string representation of the expression tree underneath the current node. diff --git a/src/ir/expressions/ExpressionVisitor.h b/src/ir/expressions/ExpressionVisitor.h index 3891fa8f3..d301e9792 100644 --- a/src/ir/expressions/ExpressionVisitor.h +++ b/src/ir/expressions/ExpressionVisitor.h @@ -28,7 +28,6 @@ namespace storm { class ExpressionVisitor { public: - virtual void visit(BaseExpression* expression) = 0; virtual void visit(BinaryBooleanFunctionExpression* expression) = 0; virtual void visit(BinaryNumericalFunctionExpression* expression) = 0; virtual void visit(BinaryRelationExpression* expression) = 0; diff --git a/src/storm.cpp b/src/storm.cpp index a1ba8ec34..80573a589 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -358,7 +358,7 @@ int main(const int argc, const char* argv[]) { storm::storage::BitVector const& finishedStates = labeledMdp->getLabeledStates("finished"); storm::storage::BitVector const& allCoinsEqual1States = labeledMdp->getLabeledStates("all_coins_equal_1"); storm::storage::BitVector targetStates = finishedStates & allCoinsEqual1States; - storm::counterexamples::SMTMinimalCommandSetGenerator::getMinimalCommandSet(program, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true); + storm::counterexamples::SMTMinimalCommandSetGenerator::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true); } } diff --git a/src/utility/IRUtility.h b/src/utility/IRUtility.h index 106032b15..63cf9519e 100644 --- a/src/utility/IRUtility.h +++ b/src/utility/IRUtility.h @@ -8,7 +8,10 @@ #ifndef STORM_UTILITY_IRUTILITY_H_ #define STORM_UTILITY_IRUTILITY_H_ -#include +#include + +#include "src/storage/LabeledValues.h" +#include "src/ir/IR.h" #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" @@ -19,6 +22,433 @@ namespace storm { namespace utility { namespace ir { + /*! + * A state of the model, i.e. a valuation of all variables. + */ + typedef std::pair, std::vector> StateType; + + /*! + * A helper class that provides the functionality to compute a hash value for states of the model. + */ + class StateHash { + public: + std::size_t operator()(StateType* state) const { + size_t seed = 0; + for (auto it : state->first) { + boost::hash_combine(seed, it); + } + for (auto it : state->second) { + boost::hash_combine(seed, it); + } + return seed; + } + }; + + /*! + * A helper class that provides the functionality to compare states of the model wrt. equality. + */ + class StateCompare { + public: + bool operator()(StateType* state1, StateType* state2) const { + return *state1 == *state2; + } + }; + + /*! + * A helper class that provides the functionality to compare states of the model wrt. the relation "<". + */ + class StateLess { + public: + bool operator()(StateType* state1, StateType* state2) const { + // Compare boolean variables. + for (uint_fast64_t i = 0; i < state1->first.size(); ++i) { + if (!state1->first.at(i) && state2->first.at(i)) { + return true; + } + } + // Then compare integer variables. + for (uint_fast64_t i = 0; i < state1->second.size(); ++i) { + if (!state1->second.at(i) && state2->second.at(i)) { + return true; + } + } + return false; + } + }; + + // A structure holding information about a particular choice. + template> + struct Choice { + public: + Choice(std::string const& actionLabel) : distribution(), actionLabel(actionLabel), choiceLabels() { + // Intentionally left empty. + } + + /*! + * Returns an iterator to the first element of this choice. + * + * @return An iterator to the first element of this choice. + */ + typename std::map::iterator begin() { + return distribution.begin(); + } + + /*! + * Returns an iterator to the first element of this choice. + * + * @return An iterator to the first element of this choice. + */ + typename std::map::const_iterator begin() const { + return distribution.cbegin(); + } + + /*! + * Returns an iterator that points past the elements of this choice. + * + * @return An iterator that points past the elements of this choice. + */ + typename std::map::iterator end() { + return distribution.end(); + } + + /*! + * Returns an iterator that points past the elements of this choice. + * + * @return An iterator that points past the elements of this choice. + */ + typename std::map::const_iterator end() const { + return distribution.cend(); + } + + /*! + * Returns an iterator to the element with the given key, if there is one. Otherwise, the iterator points to + * distribution.end(). + * + * @param value The value to find. + * @return An iterator to the element with the given key, if there is one. + */ + typename std::map::iterator find(uint_fast64_t value) { + return distribution.find(value); + } + + /*! + * Inserts the contents of this object to the given output stream. + * + * @param out The stream in which to insert the contents. + */ + friend std::ostream& operator<<(std::ostream& out, Choice const& choice) { + out << "<"; + for (auto const& stateProbabilityPair : choice.distribution) { + out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", "; + } + out << ">"; + return out; + } + + /*! + * Adds the given label to the labels associated with this choice. + * + * @param label The label to associate with this choice. + */ + void addChoiceLabel(uint_fast64_t label) { + choiceLabels.insert(label); + } + + /*! + * Adds the given label set to the labels associated with this choice. + * + * @param labelSet The label set to associate with this choice. + */ + void addChoiceLabels(std::set const& labelSet) { + for (uint_fast64_t label : labelSet) { + addChoiceLabel(label); + } + } + + /*! + * Retrieves the set of labels associated with this choice. + * + * @return The set of labels associated with this choice. + */ + std::set const& getChoiceLabels() const { + return choiceLabels; + } + + /*! + * Retrieves the action label of this choice. + * + * @return The action label of this choice. + */ + std::string const& getActionLabel() const { + return actionLabel; + } + + /*! + * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, + * yet. + * + * @param state The state for which to add the entry. + * @return A reference to the entry that is associated with the given state. + */ + ValueType& getOrAddEntry(uint_fast64_t state) { + auto stateProbabilityPair = distribution.find(state); + + if (stateProbabilityPair == distribution.end()) { + distribution[state] = ValueType(); + } + return distribution.at(state); + } + + /*! + * Retrieves the entry in the choice that is associated with the given state and creates one if none exists, + * yet. + * + * @param state The state for which to add the entry. + * @return A reference to the entry that is associated with the given state. + */ + ValueType const& getOrAddEntry(uint_fast64_t state) const { + auto stateProbabilityPair = distribution.find(state); + + if (stateProbabilityPair == distribution.end()) { + distribution[state] = ValueType(); + } + return distribution.at(state); + } + + private: + // The distribution that is associated with the choice. + std::map distribution; + + // The label of the choice. + std::string actionLabel; + + // The labels that are associated with this choice. + std::set choiceLabels; + }; + + /*! + * Adds the target state and probability to the given choice and ignores the labels. This function overloads with + * other functions to ensure the proper treatment of labels. + * + * @param choice The choice to which to add the target state and probability. + * @param state The target state of the probability. + * @param probability The probability to reach the target state in one step. + * @param labels A set of labels that is supposed to be associated with this state and probability. NOTE: this + * is ignored by this particular function but not by the overloaded functions. + */ + template + void addProbabilityToChoice(Choice& choice, uint_fast64_t state, ValueType probability, std::set const& labels) { + choice.getOrAddEntry(state) += probability; + } + + /*! + * Adds the target state and probability to the given choice and labels it accordingly. This function overloads + * with other functions to ensure the proper treatment of labels. + * + * @param choice The choice to which to add the target state and probability. + * @param state The target state of the probability. + * @param probability The probability to reach the target state in one step. + * @param labels A set of labels that is supposed to be associated with this state and probability. + */ + template + void addProbabilityToChoice(Choice>& choice, uint_fast64_t state, ValueType probability, std::set const& labels) { + auto& labeledEntry = choice.getOrAddEntry(state); + labeledEntry.addValue(probability, labels); + } + + // A structure storing information about the used variables of the program. + struct VariableInformation { + VariableInformation() : booleanVariables(), booleanVariableToIndexMap(), integerVariables(), integerVariableToIndexMap() { + // Intentinally left empty. + } + + // List of all boolean variables. + std::vector booleanVariables; + + // A mapping of boolean variable names to their indices. + std::map booleanVariableToIndexMap; + + // List of all integer variables. + std::vector integerVariables; + + // A mapping of integer variable names to their indices. + std::map integerVariableToIndexMap; + }; + + /*! + * Aggregates information about the variables in the program. + * + * @param program The program whose variables to aggregate. + * @return A structure containing information about the variables in the program. + */ + static VariableInformation createVariableInformation(storm::ir::Program const& program) { + VariableInformation result; + + uint_fast64_t numberOfIntegerVariables = 0; + uint_fast64_t numberOfBooleanVariables = 0; + + // Count number of variables. + numberOfBooleanVariables += program.getNumberOfGlobalBooleanVariables(); + numberOfIntegerVariables += program.getNumberOfGlobalIntegerVariables(); + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables(); + numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables(); + } + + // Resize the variable vectors appropriately. + result.booleanVariables.resize(numberOfBooleanVariables); + result.integerVariables.resize(numberOfIntegerVariables); + + // Create variables. + for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) { + storm::ir::BooleanVariable const& var = program.getGlobalBooleanVariable(i); + result.booleanVariables[var.getGlobalIndex()] = var; + result.booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } + for (uint_fast64_t i = 0; i < program.getNumberOfGlobalIntegerVariables(); ++i) { + storm::ir::IntegerVariable const& var = program.getGlobalIntegerVariable(i); + result.integerVariables[var.getGlobalIndex()] = var; + result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } + for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { + storm::ir::Module const& module = program.getModule(i); + + for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { + storm::ir::BooleanVariable const& var = module.getBooleanVariable(j); + result.booleanVariables[var.getGlobalIndex()] = var; + result.booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } + for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { + storm::ir::IntegerVariable const& var = module.getIntegerVariable(j); + result.integerVariables[var.getGlobalIndex()] = var; + result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex(); + } + } + + return result; + } + + /*! + * Generates the initial state of the given program. + * + * @param program The program for which to construct the initial state. + * @param variableInformation A structure with information about the variables in the program. + * @return The initial state. + */ + static StateType* getInitialState(storm::ir::Program const& program, VariableInformation const& variableInformation) { + StateType* initialState = new StateType(); + initialState->first.resize(variableInformation.booleanVariables.size()); + initialState->second.resize(variableInformation.integerVariables.size()); + + // Start with boolean variables. + for (uint_fast64_t i = 0; i < variableInformation.booleanVariables.size(); ++i) { + // Check if an initial value is given + if (variableInformation.booleanVariables[i].getInitialValue().get() == nullptr) { + // If no initial value was given, we assume that the variable is initially false. + std::get<0>(*initialState)[i] = false; + } else { + // Initial value was given. + bool initialValue = variableInformation.booleanVariables[i].getInitialValue()->getValueAsBool(nullptr); + std::get<0>(*initialState)[i] = initialValue; + } + } + + // Now process integer variables. + for (uint_fast64_t i = 0; i < variableInformation.integerVariables.size(); ++i) { + // Check if an initial value was given. + if (variableInformation.integerVariables[i].getInitialValue().get() == nullptr) { + // No initial value was given, so we assume that the variable initially has the least value it can take. + std::get<1>(*initialState)[i] = variableInformation.integerVariables[i].getLowerBound()->getValueAsInt(nullptr); + } else { + // Initial value was given. + int_fast64_t initialValue = variableInformation.integerVariables[i].getInitialValue()->getValueAsInt(nullptr); + std::get<1>(*initialState)[i] = initialValue; + } + } + + LOG4CPLUS_DEBUG(logger, "Generated initial state."); + return initialState; + } + + /*! + * Defines the undefined constants of the given program using the given string. + * + * @param program The program in which to define the constants. + * @param constantDefinitionString A comma-separated list of constant definitions. + */ + static void defineUndefinedConstants(storm::ir::Program& program, std::string const& constantDefinitionString) { + if (!constantDefinitionString.empty()) { + // Parse the string that defines the undefined constants of the model and make sure that it contains exactly + // one value for each undefined constant of the model. + std::vector definitions; + boost::split(definitions, constantDefinitionString, boost::is_any_of(",")); + for (auto& definition : definitions) { + boost::trim(definition); + + // Check whether the token could be a legal constant definition. + uint_fast64_t positionOfAssignmentOperator = definition.find('='); + if (positionOfAssignmentOperator == std::string::npos) { + throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error."; + } + + // Now extract the variable name and the value from the string. + std::string constantName = definition.substr(0, positionOfAssignmentOperator); + boost::trim(constantName); + std::string value = definition.substr(positionOfAssignmentOperator + 1); + boost::trim(value); + + // Check whether the constant is a legal undefined constant of the program and if so, of what type it is. + if (program.hasUndefinedBooleanConstant(constantName)) { + if (value == "true") { + program.getUndefinedBooleanConstantExpression(constantName)->define(true); + } else if (value == "false") { + program.getUndefinedBooleanConstantExpression(constantName)->define(false); + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << "."; + } + } else if (program.hasUndefinedIntegerConstant(constantName)) { + try { + int_fast64_t integerValue = std::stoi(value); + program.getUndefinedIntegerConstantExpression(constantName)->define(integerValue); + } catch (std::invalid_argument const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << "."; + } catch (std::out_of_range const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << " (value too big)."; + } + } else if (program.hasUndefinedDoubleConstant(constantName)) { + try { + double doubleValue = std::stod(value); + program.getUndefinedDoubleConstantExpression(constantName)->define(doubleValue); + } catch (std::invalid_argument const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << "."; + } catch (std::out_of_range const&) { + throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big)."; + } + + } else { + throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << "."; + } + } + } + } + + /*! + * Undefines all previously defined constants in the given program. + * + * @param program The program in which to undefine the constants. + */ + static void undefineUndefinedConstants(storm::ir::Program& program) { + for (auto const& nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) { + nameExpressionPair.second->undefine(); + } + for (auto const& nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) { + nameExpressionPair.second->undefine(); + } + for (auto const& nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) { + nameExpressionPair.second->undefine(); + } + } + /*! * 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