Browse Source

Towards adding more cuts to MaxSAT-based minimal command counterexamples. Some fixes here and there along the way.

Former-commit-id: 15ea8544fd
tempestpy_adaptions
dehnert 11 years ago
parent
commit
b6ff62e689
  1. 450
      src/adapters/ExplicitModelAdapter.h
  2. 6
      src/adapters/SymbolicExpressionAdapter.h
  3. 68
      src/adapters/Z3ExpressionAdapter.h
  4. 71
      src/counterexamples/SMTMinimalCommandSetGenerator.h
  5. 4
      src/ir/expressions/BaseExpression.cpp
  6. 2
      src/ir/expressions/BaseExpression.h
  7. 1
      src/ir/expressions/ExpressionVisitor.h
  8. 2
      src/storm.cpp
  9. 432
      src/utility/IRUtility.h

450
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 <boost/algorithm/string.hpp>
#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<bool>, std::vector<int_fast64_t>> 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<bool>(seed, it);
}
for (auto it : state->second) {
boost::hash_combine<int_fast64_t>(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<typename ValueType, typename KeyType=uint_fast64_t, typename Compare=std::less<uint_fast64_t>>
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<KeyType, ValueType>::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<KeyType, ValueType>::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<KeyType, ValueType>::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<KeyType, ValueType>::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<KeyType, ValueType>::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<ValueType> 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<uint_fast64_t> 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<uint_fast64_t> 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<KeyType, ValueType, Compare> distribution;
// The label of the choice.
std::string actionLabel;
// The labels that are associated with this choice.
std::set<uint_fast64_t> 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<typename ValueType>
void addProbabilityToChoice(Choice<ValueType>& choice, uint_fast64_t state, ValueType probability, std::set<uint_fast64_t> 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<typename ValueType>
void addProbabilityToChoice(Choice<storm::storage::LabeledValues<ValueType>>& choice, uint_fast64_t state, ValueType probability, std::set<uint_fast64_t> const& labels) {
auto& labeledEntry = choice.getOrAddEntry(state);
labeledEntry.addValue(probability, labels);
}
template<typename ValueType>
class ExplicitModelAdapter {
public:
@ -315,25 +80,6 @@ namespace storm {
std::vector<std::set<uint_fast64_t>> 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<storm::ir::BooleanVariable> booleanVariables;
// A mapping of boolean variable names to their indices.
std::map<std::string, uint_fast64_t> booleanVariableToIndexMap;
// List of all integer variables.
std::vector<storm::ir::IntegerVariable> integerVariables;
// A mapping of integer variable names to their indices.
std::map<std::string, uint_fast64_t> 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<storm::models::AbstractModel<ValueType>> translateProgram(storm::ir::Program program, std::string const& constantDefinitionString = "", std::string const& rewardModelName = "") {
static std::unique_ptr<storm::models::AbstractModel<ValueType>> 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<storm::models::AbstractModel<ValueType>> result;
std::unique_ptr<storm::models::AbstractModel<ValueType>> result;
switch (program.getModelType()) {
case storm::ir::Program::DTMC:
result = std::shared_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Dtmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
case storm::ir::Program::CTMC:
result = std::shared_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmc<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
case storm::ir::Program::MDP:
result = std::shared_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Mdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
break;
case storm::ir::Program::CTMDP:
result = std::shared_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(modelComponents.choiceLabeling)));
result = std::unique_ptr<storm::models::AbstractModel<ValueType>>(new storm::models::Ctmdp<ValueType>(std::move(modelComponents.transitionMatrix), std::move(modelComponents.stateLabeling), std::move(modelComponents.nondeterministicChoiceIndices), rewardModelName != "" ? std::move(modelComponents.stateRewards) : boost::optional<std::vector<ValueType>>(), rewardModelName != "" ? std::move(modelComponents.transitionRewardMatrix) : boost::optional<storm::storage::SparseMatrix<ValueType>>(), 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<std::string> 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<Choice<ValueType>> getUnlabeledTransitions(storm::ir::Program const& program, StateInformation& stateInformation, VariableInformation const& variableInformation, uint_fast64_t stateIndex, std::queue<uint_fast64_t>& stateQueue) {
std::list<Choice<ValueType>> result;

6
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);

68
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<std::string, z3::expr> const& variableToExpressionMap) : context(context), stack(), variableToExpressionMap(variableToExpressionMap) {
Z3ExpressionAdapter(z3::context& context, std::map<std::string, z3::expr> 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<storm::ir::expressions::BaseExpression> expression) {
z3::expr translateExpression(std::unique_ptr<storm::ir::expressions::BaseExpression> 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<z3::expr> stack;
std::map<std::string, z3::expr> variableToExpressionMap
}
std::map<std::string, z3::expr> variableToExpressionMap;
};
} // namespace adapters
} // namespace storm
#endif /* STORM_ADAPTERS_Z3EXPRESSIONADAPTER_H_ */

71
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<T> 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<T> 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<uint_fast64_t> initialLabels;
std::map<uint_fast64_t, std::set<uint_fast64_t>> precedingLabels;
std::set<uint_fast64_t> targetLabels;
std::map<uint_fast64_t, std::set<uint_fast64_t>> followingLabels;
std::map<uint_fast64_t, std::set<uint_fast64_t>> synchronizingLabels;
// Get some data from the MDP for convenient access.
storm::storage::SparseMatrix<T> 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<std::string, z3::expr> 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<uint_fast64_t> getMinimalCommandSet(storm::ir::Program const& program, storm::models::Mdp<T> const& labeledMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool checkThresholdFeasible = false) {
static std::set<uint_fast64_t> getMinimalCommandSet(storm::ir::Program program, std::string const& constantDefinitionString, storm::models::Mdp<T> 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

4
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");

2
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.

1
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;

2
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<double>::getMinimalCommandSet(program, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true);
storm::counterexamples::SMTMinimalCommandSetGenerator<double>::getMinimalCommandSet(program, constants, *labeledMdp, storm::storage::BitVector(labeledMdp->getNumberOfStates(), true), targetStates, 0.3, true);
}
}

432
src/utility/IRUtility.h

@ -8,7 +8,10 @@
#ifndef STORM_UTILITY_IRUTILITY_H_
#define STORM_UTILITY_IRUTILITY_H_
#include <src/ir/IR.h>
#include <boost/algorithm/string.hpp>
#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<bool>, std::vector<int_fast64_t>> 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<bool>(seed, it);
}
for (auto it : state->second) {
boost::hash_combine<int_fast64_t>(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<typename ValueType, typename KeyType=uint_fast64_t, typename Compare=std::less<uint_fast64_t>>
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<KeyType, ValueType>::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<KeyType, ValueType>::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<KeyType, ValueType>::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<KeyType, ValueType>::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<KeyType, ValueType>::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<ValueType> 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<uint_fast64_t> 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<uint_fast64_t> 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<KeyType, ValueType, Compare> distribution;
// The label of the choice.
std::string actionLabel;
// The labels that are associated with this choice.
std::set<uint_fast64_t> 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<typename ValueType>
void addProbabilityToChoice(Choice<ValueType>& choice, uint_fast64_t state, ValueType probability, std::set<uint_fast64_t> 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<typename ValueType>
void addProbabilityToChoice(Choice<storm::storage::LabeledValues<ValueType>>& choice, uint_fast64_t state, ValueType probability, std::set<uint_fast64_t> 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<storm::ir::BooleanVariable> booleanVariables;
// A mapping of boolean variable names to their indices.
std::map<std::string, uint_fast64_t> booleanVariableToIndexMap;
// List of all integer variables.
std::vector<storm::ir::IntegerVariable> integerVariables;
// A mapping of integer variable names to their indices.
std::map<std::string, uint_fast64_t> 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<std::string> 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

Loading…
Cancel
Save