diff --git a/src/adapters/SymbolicModelAdapter.h b/src/adapters/SymbolicModelAdapter.h new file mode 100644 index 000000000..1cdbe7c04 --- /dev/null +++ b/src/adapters/SymbolicModelAdapter.h @@ -0,0 +1,115 @@ +/* + * SymbolicModelAdapter.h + * + * Created on: 25.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ +#define STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ + +#include "src/exceptions/WrongFileFormatException.h" + +#include "src/utility/CuddUtility.h" +#include "src/ir/expressions/ExpressionVisitor.h" + +#include "cuddObj.hh" +#include + +namespace storm { + +namespace adapters { + +class SymbolicModelAdapter { +public: + + SymbolicModelAdapter() : cuddUtility(storm::utility::cuddUtilityInstance()) { + + } + + void toMTBDD(storm::ir::Program const& program) { + LOG4CPLUS_INFO(logger, "Creating MTBDD representation for probabilistic program."); + createDecisionDiagramVariables(program); + + 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.getNumberOfCommands(); ++j) { + storm::ir::Command const& command = module.getCommand(j); + + + } + } + + LOG4CPLUS_INFO(logger, "Done creating MTBDD representation for probabilistic program."); + } + +private: + storm::utility::CuddUtility* cuddUtility; + + std::vector allDecisionDiagramVariables; + std::vector allRowDecisionDiagramVariables; + std::vector allColumnDecisionDiagramVariables; + std::vector booleanRowDecisionDiagramVariables; + std::vector integerRowDecisionDiagramVariables; + std::vector booleanColumnDecisionDiagramVariables; + std::vector integerColumnDecisionDiagramVariables; + std::unordered_map> variableToRowDecisionDiagramVariableMap; + std::unordered_map> variableToColumnDecisionDiagramVariableMap; + + void createDecisionDiagramVariables(storm::ir::Program const& program) { + 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& booleanVariable = module.getBooleanVariable(j); + + ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable(); + variableToRowDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newRowDecisionDiagramVariable); + booleanRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + + ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable(); + variableToColumnDecisionDiagramVariableMap[booleanVariable.getName()].push_back(newColumnDecisionDiagramVariable); + booleanColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + } + + for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { + storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(j); + uint_fast64_t integerRange = integerVariable.getUpperBound()->getValueAsInt(nullptr) - integerVariable.getLowerBound()->getValueAsInt(nullptr); + if (integerRange <= 0) { + throw storm::exceptions::WrongFileFormatException() << "Range of variable " + << integerVariable.getName() << " is empty or negativ."; + } + uint_fast64_t numberOfDecisionDiagramVariables = static_cast(std::ceil(std::log2(integerRange))); + + std::vector allRowDecisionDiagramVariablesForVariable; + std::vector allColumnDecisionDiagramVariablesForVariable; + for (uint_fast64_t k = 0; k < numberOfDecisionDiagramVariables; ++k) { + ADD* newRowDecisionDiagramVariable = cuddUtility->getNewAddVariable(); + allRowDecisionDiagramVariablesForVariable.push_back(newRowDecisionDiagramVariable); + integerRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + allRowDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + allDecisionDiagramVariables.push_back(newRowDecisionDiagramVariable); + + ADD* newColumnDecisionDiagramVariable = cuddUtility->getNewAddVariable(); + allColumnDecisionDiagramVariablesForVariable.push_back(newColumnDecisionDiagramVariable); + integerColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + allColumnDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + allDecisionDiagramVariables.push_back(newColumnDecisionDiagramVariable); + } + variableToRowDecisionDiagramVariableMap[integerVariable.getName()] = allRowDecisionDiagramVariablesForVariable; + variableToColumnDecisionDiagramVariableMap[integerVariable.getName()] = allColumnDecisionDiagramVariablesForVariable; + } + } + } +}; + +} // namespace adapters + +} // namespace storm + +#endif /* STORM_ADAPTERS_SYMBOLICMODELADAPTER_H_ */ diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h index 27704b64b..8324f372a 100644 --- a/src/ir/expressions/BaseExpression.h +++ b/src/ir/expressions/BaseExpression.h @@ -11,6 +11,8 @@ #include "src/exceptions/ExpressionEvaluationException.h" #include "src/exceptions/NotImplementedException.h" +#include "src/utility/CuddUtility.h" + #include #include @@ -64,6 +66,8 @@ public: << this->getTypeName() << " because evaluation implementation is missing."; } + virtual ADD* toAdd() const = 0; + virtual std::string toString() const = 0; std::string getTypeName() const { diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h index c7b5a0bdc..9c54362c2 100644 --- a/src/ir/expressions/BinaryBooleanFunctionExpression.h +++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h @@ -10,6 +10,8 @@ #include "src/ir/expressions/BaseExpression.h" +#include "src/utility/CuddUtility.h" + #include #include @@ -42,6 +44,18 @@ public: } } + virtual ADD* toAdd() const { + ADD* leftAdd = left->toAdd(); + ADD* rightAdd = right->toAdd(); + + switch(functionType) { + case AND: return new ADD(leftAdd->Times(*rightAdd)); break; + case OR: return new ADD(leftAdd->Plus(*rightAdd)); break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary operator: '" << functionType << "'."; + } + } + virtual std::string toString() const { std::stringstream result; result << left->toString(); diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h index 0d710e785..b2dd12e9c 100644 --- a/src/ir/expressions/BinaryNumericalFunctionExpression.h +++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h @@ -10,6 +10,8 @@ #include "src/ir/expressions/BaseExpression.h" +#include "src/utility/CuddUtility.h" + namespace storm { namespace ir { @@ -62,6 +64,20 @@ public: } } + virtual ADD* toAdd() const { + ADD* leftAdd = left->toAdd(); + ADD* rightAdd = right->toAdd(); + + switch(functionType) { + case PLUS: return new ADD(leftAdd->Plus(*rightAdd)); break; + case MINUS: return new ADD(leftAdd->Minus(*rightAdd)); break; + case TIMES: return new ADD(leftAdd->Times(*rightAdd)); break; + case DIVIDE: return new ADD(leftAdd->Divide(*rightAdd)); break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary operator: '" << functionType << "'."; + } + } + virtual std::string toString() const { std::string result = left->toString(); switch (functionType) { diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h index 83556fa8f..02907dfc5 100644 --- a/src/ir/expressions/BinaryRelationExpression.h +++ b/src/ir/expressions/BinaryRelationExpression.h @@ -10,6 +10,8 @@ #include "src/ir/expressions/BaseExpression.h" +#include "src/utility/CuddUtility.h" + namespace storm { namespace ir { @@ -18,7 +20,7 @@ namespace expressions { class BinaryRelationExpression : public BaseExpression { public: - enum RelationType {EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL}; + enum RelationType {EQUAL, NOT_EQUAL, LESS, LESS_OR_EQUAL, GREATER, GREATER_OR_EQUAL}; BinaryRelationExpression(std::shared_ptr left, std::shared_ptr right, RelationType relationType) : BaseExpression(bool_), left(left), right(right), relationType(relationType) { @@ -33,6 +35,7 @@ public: int_fast64_t resultRight = right->getValueAsInt(variableValues); switch(relationType) { case EQUAL: return resultLeft == resultRight; break; + case NOT_EQUAL: return resultLeft != resultRight; break; case LESS: return resultLeft < resultRight; break; case LESS_OR_EQUAL: return resultLeft <= resultRight; break; case GREATER: return resultLeft > resultRight; break; @@ -42,10 +45,27 @@ public: } } + virtual ADD* toAdd() const { + ADD* leftAdd = left->toAdd(); + ADD* rightAdd = right->toAdd(); + + switch(relationType) { + case EQUAL: return new ADD(leftAdd->Equals(*rightAdd)); break; + case NOT_EQUAL: return new ADD(leftAdd->NotEquals(*rightAdd)); break; + case LESS: return new ADD(leftAdd->LessThan(*rightAdd)); break; + case LESS_OR_EQUAL: return new ADD(leftAdd->LessThanOrEqual(*rightAdd)); break; + case GREATER: return new ADD(leftAdd->GreaterThan(*rightAdd)); break; + case GREATER_OR_EQUAL: return new ADD(leftAdd->GreaterThanOrEqual(*rightAdd)); break; + default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Unknown boolean binary operator: '" << relationType << "'."; + } + } + virtual std::string toString() const { std::string result = left->toString(); switch (relationType) { case EQUAL: result += " = "; break; + case NOT_EQUAL: result += " != "; break; case LESS: result += " < "; break; case LESS_OR_EQUAL: result += " <= "; break; case GREATER: result += " > "; break; diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h index c4a168838..b16cd5ad7 100644 --- a/src/ir/expressions/BooleanConstantExpression.h +++ b/src/ir/expressions/BooleanConstantExpression.h @@ -10,6 +10,8 @@ #include "ConstantExpression.h" +#include "src/utility/CuddUtility.h" + #include namespace storm { @@ -38,6 +40,16 @@ public: } } + virtual ADD* toAdd() const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Boolean constant '" << this->getConstantName() << "' is undefined."; + } + + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + return new ADD(*cuddUtility->getConstant(value ? 1 : 0)); + } + virtual std::string toString() const { std::string result = this->constantName; if (defined) { diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h index 55027d6cc..6b92e4b7b 100644 --- a/src/ir/expressions/BooleanLiteral.h +++ b/src/ir/expressions/BooleanLiteral.h @@ -32,6 +32,11 @@ public: return value; } + virtual ADD* toAdd() const { + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + return new ADD(*cuddUtility->getConstant(value ? 1 : 0)); + } + virtual std::string toString() const { if (value) { return std::string("true"); diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h index 573aeffd3..9e3471f19 100644 --- a/src/ir/expressions/DoubleConstantExpression.h +++ b/src/ir/expressions/DoubleConstantExpression.h @@ -35,6 +35,16 @@ public: } } + virtual ADD* toAdd() const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Double constant '" << this->getConstantName() << "' is undefined."; + } + + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + return new ADD(*cuddUtility->getConstant(value)); + } + virtual std::string toString() const { std::string result = this->constantName; if (defined) { diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h index 4963ff9c2..1f447f7fb 100644 --- a/src/ir/expressions/DoubleLiteral.h +++ b/src/ir/expressions/DoubleLiteral.h @@ -34,6 +34,11 @@ public: return value; } + virtual ADD* toAdd() const { + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + return new ADD(*cuddUtility->getConstant(value)); + } + virtual std::string toString() const { return boost::lexical_cast(value); } diff --git a/src/ir/expressions/ExpressionVisitor.h b/src/ir/expressions/ExpressionVisitor.h new file mode 100644 index 000000000..7fc05b79b --- /dev/null +++ b/src/ir/expressions/ExpressionVisitor.h @@ -0,0 +1,44 @@ +/* + * ExpressionVisitor.h + * + * Created on: 26.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ +#define STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ + +#include "Expressions.h" + +namespace storm { + +namespace ir { + +namespace expressions { + +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; + virtual void visit(BooleanConstantExpression expression) = 0; + virtual void visit(BooleanLiteral expression) = 0; + virtual void visit(ConstantExpression expression) = 0; + virtual void visit(DoubleConstantExpression expression) = 0; + virtual void visit(DoubleLiteral expression) = 0; + virtual void visit(IntegerConstantExpression expression) = 0; + virtual void visit(IntegerLiteral expression) = 0; + virtual void visit(UnaryBooleanFunctionExpression expression) = 0; + virtual void visit(UnaryNumericalFunctionExpression expression) = 0; + virtual void visit(VariableExpression expression) = 0; +}; + +} // namespace expressions + +} // namespace ir + +} // namespace storm + + +#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONVISITOR_H_ */ diff --git a/src/ir/expressions/Expressions.h b/src/ir/expressions/Expressions.h index b52474459..0de025b9f 100644 --- a/src/ir/expressions/Expressions.h +++ b/src/ir/expressions/Expressions.h @@ -2,11 +2,11 @@ * Expressions.h * * Created on: 03.01.2013 - * Author: chris + * Author: Christian Dehnert */ -#ifndef EXPRESSIONS_H_ -#define EXPRESSIONS_H_ +#ifndef STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ +#define STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ #include "BaseExpression.h" #include "BinaryBooleanFunctionExpression.h" @@ -18,8 +18,9 @@ #include "UnaryBooleanFunctionExpression.h" #include "UnaryNumericalFunctionExpression.h" #include "VariableExpression.h" +#include "ConstantExpression.h" #include "BooleanConstantExpression.h" #include "IntegerConstantExpression.h" #include "DoubleConstantExpression.h" -#endif /* EXPRESSIONS_H_ */ +#endif /* STORM_IR_EXPRESSIONS_EXPRESSIONS_H_ */ diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h index 7cb25afd9..615aa2adf 100644 --- a/src/ir/expressions/IntegerConstantExpression.h +++ b/src/ir/expressions/IntegerConstantExpression.h @@ -35,6 +35,16 @@ public: } } + virtual ADD* toAdd() const { + if (!defined) { + throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " + << "Integer constant '" << this->getConstantName() << "' is undefined."; + } + + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + return new ADD(*cuddUtility->getConstant(value)); + } + virtual std::string toString() const { std::string result = this->constantName; if (defined) { diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h index e5883e358..6399813c3 100644 --- a/src/ir/expressions/IntegerLiteral.h +++ b/src/ir/expressions/IntegerLiteral.h @@ -32,6 +32,11 @@ public: return value; } + virtual ADD* toAdd() const { + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + return new ADD(*cuddUtility->getConstant(value)); + } + virtual std::string toString() const { return boost::lexical_cast(value); } diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h index 9a924d7da..2322a323b 100644 --- a/src/ir/expressions/UnaryBooleanFunctionExpression.h +++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h @@ -37,6 +37,11 @@ public: } } + virtual ADD* toAdd() const { + ADD* childResult = child->toAdd(); + return new ADD(~(*childResult)); + } + virtual std::string toString() const { std::string result = ""; switch (functionType) { diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h index a4498aa08..3ab8fe355 100644 --- a/src/ir/expressions/UnaryNumericalFunctionExpression.h +++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h @@ -54,6 +54,13 @@ public: } } + virtual ADD* toAdd() const { + ADD* childResult = child->toAdd(); + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + ADD* result = cuddUtility->getConstant(0); + return new ADD(result->Minus(*childResult)); + } + virtual std::string toString() const { std::string result = ""; switch (functionType) { diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h index 5ef38313c..87374f080 100644 --- a/src/ir/expressions/VariableExpression.h +++ b/src/ir/expressions/VariableExpression.h @@ -10,6 +10,7 @@ #include "src/ir/expressions/BaseExpression.h" +#include #include namespace storm { @@ -20,7 +21,11 @@ namespace expressions { class VariableExpression : public BaseExpression { public: - VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName) : BaseExpression(type), index(index), variableName(variableName) { + VariableExpression(ReturnType type, uint_fast64_t index, std::string variableName, + std::shared_ptr lowerBound = std::shared_ptr(nullptr), + std::shared_ptr upperBound = std::shared_ptr(nullptr)) + : BaseExpression(type), index(index), variableName(variableName), + lowerBound(lowerBound), upperBound(upperBound) { } @@ -67,9 +72,28 @@ public: << " variable '" << variableName << "' of type double."; } + virtual ADD* toAdd() const { + storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); + + return nullptr; + + if (this->getType() == bool_) { + ADD* result = cuddUtility->getConstant(0); + //cuddUtility->addValueForEncodingOfConstant(result, 1, ) + } else { + int64_t low = lowerBound->getValueAsInt(nullptr); + int64_t high = upperBound->getValueAsInt(nullptr); + } + + return new ADD(); + } + private: uint_fast64_t index; std::string variableName; + + std::shared_ptr lowerBound; + std::shared_ptr upperBound; }; } diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 78795388e..19eed26ae 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -188,7 +188,7 @@ struct PrismParser::PrismGrammar : qi::grammar> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct(phoenix::ref(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::ref(nextBooleanVariableIndex))), qi::_a = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::bool_, phoenix::ref(nextBooleanVariableIndex), qi::_1)), phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1), phoenix::ref(nextBooleanVariableIndex) = phoenix::ref(nextBooleanVariableIndex) + 1]; booleanVariableDefinition.name("boolean variable declaration"); - integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct(phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::ref(nextIntegerVariableIndex))), qi::_a = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, phoenix::ref(nextIntegerVariableIndex), qi::_1)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), phoenix::ref(nextIntegerVariableIndex) = phoenix::ref(nextIntegerVariableIndex) + 1]; + integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";"))[phoenix::push_back(qi::_r1, phoenix::construct(phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::ref(nextIntegerVariableIndex))), qi::_a = phoenix::construct>(phoenix::new_(storm::ir::expressions::BaseExpression::int_, phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3)), phoenix::bind(integerVariables_.add, qi::_1, qi::_a), phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), phoenix::ref(nextIntegerVariableIndex) = phoenix::ref(nextIntegerVariableIndex) + 1]; integerVariableDefinition.name("integer variable declaration"); variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4)); variableDefinition.name("variable declaration"); diff --git a/src/storm.cpp b/src/storm.cpp index 35b25459d..b9fd2819f 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -140,6 +140,7 @@ void cleanUp() { if (storm::settings::instance() != nullptr) { delete storm::settings::instance(); } + delete storm::utility::cuddUtilityInstance(); } void testCheckingDie(storm::models::Dtmc& dtmc) { diff --git a/src/utility/CuddUtility.cpp b/src/utility/CuddUtility.cpp new file mode 100644 index 000000000..c9ab7aba6 --- /dev/null +++ b/src/utility/CuddUtility.cpp @@ -0,0 +1,125 @@ +/* + * CuddUtility.cpp + * + * Created on: 26.01.2013 + * Author: Christian Dehnert + */ + +#include "CuddUtility.h" +#include "src/exceptions/InvalidArgumentException.h" + +#include "log4cplus/logger.h" +#include "log4cplus/loggingmacros.h" + +extern log4cplus::Logger logger; + +#include +#include + +namespace storm { + +namespace utility { + +storm::utility::CuddUtility* storm::utility::CuddUtility::instance = nullptr; + +ADD* CuddUtility::getNewAddVariable() { + ADD* result = new ADD(manager.addVar()); + allDecisionDiagramVariables.push_back(result); + return result; +} + +ADD* CuddUtility::getAddVariable(int index) const { + return new ADD(manager.addVar(index)); +} + +ADD* CuddUtility::getConstantEncoding(uint_fast64_t constant, std::vector& variables) const { + if ((constant >> variables.size()) != 0) { + LOG4CPLUS_ERROR(logger, "Cannot create encoding for constant " << constant << " with " + << variables.size() << " variables."); + throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" + << " for constant " << constant << " with " << variables.size() + << " variables."; + } + + // Determine whether the new ADD will be rooted by the first variable or its complement. + ADD initialNode; + if ((constant & (1 << (variables.size() - 1))) != 0) { + initialNode = *variables[0]; + } else { + initialNode = ~(*variables[0]); + } + ADD* result = new ADD(initialNode); + + // Add (i.e. multiply) the other variables as well according to whether their bit is set or not. + for (uint_fast64_t i = 1; i < variables.size(); ++i) { + if ((constant & (1 << (variables.size() - i - 1))) != 0) { + *result *= *variables[i]; + } else { + *result *= ~(*variables[i]); + } + } + + return result; +} + +ADD* CuddUtility::addValueForEncodingOfConstant(ADD* add, uint_fast64_t constant, std::vector& variables, double value) const { + if ((constant >> variables.size()) != 0) { + LOG4CPLUS_ERROR(logger, "Cannot create encoding for constant " << constant << " with " + << variables.size() << " variables."); + throw storm::exceptions::InvalidArgumentException() << "Cannot create encoding" + << " for constant " << constant << " with " << variables.size() + << " variables."; + } + + // Determine whether the new ADD will be rooted by the first variable or its complement. + ADD initialNode; + if ((constant & (1 << (variables.size() - 1))) != 0) { + initialNode = *variables[0]; + } else { + initialNode = ~(*variables[0]); + } + ADD* encoding = new ADD(initialNode); + + // Add (i.e. multiply) the other variables as well according to whether their bit is set or not. + for (uint_fast64_t i = 1; i < variables.size(); ++i) { + if ((constant & (1 << (variables.size() - i - 1))) != 0) { + *encoding *= *variables[i]; + } else { + *encoding *= ~(*variables[i]); + } + } + + ADD* result = new ADD(add->Ite(manager.constant(value), *add)); + return result; +} + +ADD* CuddUtility::getConstant(double value) const { + return new ADD(manager.constant(value)); +} + +void CuddUtility::dumpDotToFile(ADD* add, std::string filename) const { + std::vector nodes; + nodes.push_back(*add); + + FILE* filePtr; + filePtr = fopen(filename.c_str(), "w"); + manager.DumpDot(nodes, 0, 0, filePtr); + fclose(filePtr); +} + +Cudd const& CuddUtility::getManager() const { + return manager; +} + +CuddUtility* cuddUtilityInstance() { + if (CuddUtility::instance != nullptr) { + CuddUtility::instance = new CuddUtility(); + } + return CuddUtility::instance; +} + +} // namespace utility + +} // namespace storm + + diff --git a/src/utility/CuddUtility.h b/src/utility/CuddUtility.h new file mode 100644 index 000000000..ae2b56bb6 --- /dev/null +++ b/src/utility/CuddUtility.h @@ -0,0 +1,57 @@ +/* + * CuddUtility.h + * + * Created on: 26.01.2013 + * Author: Christian Dehnert + */ + +#ifndef STORM_UTILITY_CUDDUTILITY_H_ +#define STORM_UTILITY_CUDDUTILITY_H_ + +#include "cuddObj.hh" + +namespace storm { + +namespace utility { + +class CuddUtility { +public: + ~CuddUtility() { + for (auto element : allDecisionDiagramVariables) { + delete element; + } + } + + ADD* getNewAddVariable(); + ADD* getAddVariable(int index) const; + + ADD* getConstantEncoding(uint_fast64_t constant, std::vector& variables) const; + + ADD* addValueForEncodingOfConstant(ADD* add, uint_fast64_t constant, std::vector& variables, double value) const; + + ADD* getConstant(double value) const; + + void dumpDotToFile(ADD* add, std::string filename) const; + + Cudd const& getManager() const; + + friend CuddUtility* cuddUtilityInstance(); + +private: + CuddUtility() : manager(0, 0), allDecisionDiagramVariables() { + + } + + Cudd manager; + std::vector allDecisionDiagramVariables; + + static CuddUtility* instance; +}; + +CuddUtility* cuddUtilityInstance(); + +} // namespace utility + +} // namespace storm + +#endif /* STORM_UTILITY_CUDDUTILITY_H_ */