diff --git a/src/adapters/DdExpressionAdapter.cpp b/src/adapters/DdExpressionAdapter.cpp index 955a94970..65e82f765 100644 --- a/src/adapters/DdExpressionAdapter.cpp +++ b/src/adapters/DdExpressionAdapter.cpp @@ -9,17 +9,17 @@ namespace storm { namespace adapters { template - SymbolicExpressionAdapter::SymbolicExpressionAdapter(storm::dd::DdManager const& ddManager, std::map const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) { + DdExpressionAdapter::DdExpressionAdapter(storm::dd::DdManager const& ddManager, std::map const& variableMapping) : ddManager(ddManager), variableMapping(variableMapping) { // Intentionally left empty. } template - storm::dd::Dd SymbolicExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { + storm::dd::Dd DdExpressionAdapter::translateExpression(storm::expressions::Expression const& expression) { return boost::any_cast>(expression.accept(*this)); } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::IfThenElseExpression const& expression) { storm::dd::Dd elseDd = boost::any_cast>(expression.getElseExpression()->accept(*this)); storm::dd::Dd thenDd = boost::any_cast>(expression.getThenExpression()->accept(*this)); storm::dd::Dd conditionDd = boost::any_cast>(expression.getCondition()->accept(*this)); @@ -27,7 +27,7 @@ namespace storm { } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression) { storm::dd::Dd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); storm::dd::Dd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); @@ -54,7 +54,7 @@ namespace storm { } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression) { storm::dd::Dd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); storm::dd::Dd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); @@ -86,10 +86,10 @@ namespace storm { } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::BinaryRelationExpression const& expression) { storm::dd::Dd leftResult = boost::any_cast>(expression.getFirstOperand()->accept(*this)); storm::dd::Dd rightResult = boost::any_cast>(expression.getSecondOperand()->accept(*this)); - + storm::dd::Dd result; switch (expression.getRelationType()) { case storm::expressions::BinaryRelationExpression::RelationType::Equal: @@ -116,14 +116,14 @@ namespace storm { } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::VariableExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::VariableExpression const& expression) { auto const& variablePair = variableMapping.find(expression.getVariable()); STORM_LOG_THROW(variablePair != variableMapping.end(), storm::exceptions::InvalidArgumentException, "Cannot translate the given expression, because it contains th variable '" << expression.getVariableName() << "' for which no DD counterpart is known."); return ddManager.getIdentity(variablePair->second); } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression) { storm::dd::Dd result = boost::any_cast>(expression.getOperand()->accept(*this)); switch (expression.getOperatorType()) { @@ -136,7 +136,7 @@ namespace storm { } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression) { storm::dd::Dd result = boost::any_cast>(expression.getOperand()->accept(*this)); switch (expression.getOperatorType()) { @@ -151,22 +151,22 @@ namespace storm { } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::BooleanLiteralExpression const& expression) { return ddManager.getConstant(expression.getValue()); } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::IntegerLiteralExpression const& expression) { return ddManager.getConstant(expression.getValue()); } template - boost::any SymbolicExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { + boost::any DdExpressionAdapter::visit(storm::expressions::DoubleLiteralExpression const& expression) { return ddManager.getConstant(expression.getValue()); } // Explicitly instantiate the symbolic expression adapter - template class SymbolicExpressionAdapter; + template class DdExpressionAdapter; } // namespace adapters } // namespace storm diff --git a/src/adapters/DdExpressionAdapter.h b/src/adapters/DdExpressionAdapter.h index a41d0993c..6eaff65a8 100644 --- a/src/adapters/DdExpressionAdapter.h +++ b/src/adapters/DdExpressionAdapter.h @@ -12,9 +12,9 @@ namespace storm { namespace adapters { template - class SymbolicExpressionAdapter : public storm::expressions::ExpressionVisitor { + class DdExpressionAdapter : public storm::expressions::ExpressionVisitor { public: - SymbolicExpressionAdapter(storm::dd::DdManager const& ddManager, std::map const& variableMapping); + DdExpressionAdapter(storm::dd::DdManager const& ddManager, std::map const& variableMapping); storm::dd::Dd translateExpression(storm::expressions::Expression const& expression); diff --git a/src/adapters/SymbolicExpressionAdapter.h b/src/adapters/SymbolicExpressionAdapter.h deleted file mode 100644 index 1c1b8ca7e..000000000 --- a/src/adapters/SymbolicExpressionAdapter.h +++ /dev/null @@ -1,228 +0,0 @@ -/* - * SymbolicExpressionAdapter.h - * - * Created on: 27.01.2013 - * Author: Christian Dehnert - */ - -#ifndef STORM_ADAPTERS_SYMBOLICEXPRESSIONADAPTER_H_ -#define STORM_ADAPTERS_SYMBOLICEXPRESSIONADAPTER_H_ - -#include "src/ir/expressions/ExpressionVisitor.h" -#include "src/exceptions/ExpressionEvaluationException.h" - -#include "cuddObj.hh" - -#include -#include - -namespace storm { - -namespace adapters { - -class SymbolicExpressionAdapter : public storm::ir::expressions::ExpressionVisitor { -public: - SymbolicExpressionAdapter(storm::ir::Program const& program, std::unordered_map>& variableToDecisionDiagramVariableMap) : program(program), stack(), variableToDecisionDiagramVariableMap(variableToDecisionDiagramVariableMap) { - - } - - ADD* translateExpression(std::unique_ptr const& expression) { - expression->accept(this); - return stack.top(); - } - - virtual void visit(storm::ir::expressions::BinaryBooleanFunctionExpression* expression) { - expression->getLeft()->accept(this); - expression->getRight()->accept(this); - - ADD* rightResult = stack.top(); - stack.pop(); - ADD* leftResult = stack.top(); - stack.pop(); - - switch(expression->getFunctionType()) { - case storm::ir::expressions::BinaryBooleanFunctionExpression::AND: - stack.push(new ADD(leftResult->Times(*rightResult))); - break; - case storm::ir::expressions::BinaryBooleanFunctionExpression::OR: - stack.push(new ADD(leftResult->Plus(*rightResult))); - break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; - } - - // delete leftResult; - // delete rightResult; - } - - virtual void visit(storm::ir::expressions::BinaryNumericalFunctionExpression* expression) { - expression->getLeft()->accept(this); - expression->getRight()->accept(this); - - ADD* rightResult = stack.top(); - stack.pop(); - ADD* leftResult = stack.top(); - stack.pop(); - - switch(expression->getFunctionType()) { - case storm::ir::expressions::BinaryNumericalFunctionExpression::PLUS: - stack.push(new ADD(leftResult->Plus(*rightResult))); - break; - case storm::ir::expressions::BinaryNumericalFunctionExpression::MINUS: - stack.push(new ADD(leftResult->Minus(*rightResult))); - break; - case storm::ir::expressions::BinaryNumericalFunctionExpression::TIMES: - stack.push(new ADD(leftResult->Times(*rightResult))); - break; - case storm::ir::expressions::BinaryNumericalFunctionExpression::DIVIDE: - stack.push(new ADD(leftResult->Divide(*rightResult))); - break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getFunctionType() << "'."; - } - } - - virtual void visit(storm::ir::expressions::BinaryRelationExpression* expression) { - expression->getLeft()->accept(this); - expression->getRight()->accept(this); - - ADD* rightResult = stack.top(); - stack.pop(); - ADD* leftResult = stack.top(); - stack.pop(); - - switch(expression->getRelationType()) { - case storm::ir::expressions::BinaryRelationExpression::EQUAL: - stack.push(new ADD(leftResult->Equals(*rightResult))); - break; - case storm::ir::expressions::BinaryRelationExpression::NOT_EQUAL: - stack.push(new ADD(leftResult->NotEquals(*rightResult))); - break; - case storm::ir::expressions::BinaryRelationExpression::LESS: - stack.push(new ADD(leftResult->LessThan(*rightResult))); - break; - case storm::ir::expressions::BinaryRelationExpression::LESS_OR_EQUAL: - stack.push(new ADD(leftResult->LessThanOrEqual(*rightResult))); - break; - case storm::ir::expressions::BinaryRelationExpression::GREATER: - stack.push(new ADD(leftResult->GreaterThan(*rightResult))); - break; - case storm::ir::expressions::BinaryRelationExpression::GREATER_OR_EQUAL: - stack.push(new ADD(leftResult->GreaterThanOrEqual(*rightResult))); - break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean binary operator: '" << expression->getRelationType() << "'."; - } - } - - virtual void visit(storm::ir::expressions::BooleanConstantExpression* expression) { - if (!expression->isDefined()) { - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Boolean constant '" << expression->getConstantName() << "' is undefined."; - } - - storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); - stack.push(new ADD(*cuddUtility->getConstant(expression->getValue() ? 1 : 0))); - } - - virtual void visit(storm::ir::expressions::BooleanLiteralExpression* expression) { - storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); - stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsBool(nullptr) ? 1 : 0))); - } - - virtual void visit(storm::ir::expressions::DoubleConstantExpression* expression) { - if (expression->isDefined()) { - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Double constant '" << expression->getConstantName() << "' is undefined."; - } - - storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); - stack.push(new ADD(*cuddUtility->getConstant(expression->getValue()))); - } - - virtual void visit(storm::ir::expressions::DoubleLiteralExpression* expression) { - storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); - stack.push(new ADD(*cuddUtility->getConstant(expression->getValueAsDouble(nullptr)))); - } - - virtual void visit(storm::ir::expressions::IntegerConstantExpression* expression) { - if (!expression->isDefined()) { - throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Integer constant '" << expression->getConstantName() << "' is undefined."; - } - - storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); - stack.push(new ADD(*cuddUtility->getConstant(static_cast(expression->getValue())))); - } - - virtual void visit(storm::ir::expressions::IntegerLiteralExpression* expression) { - storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); - stack.push(new ADD(*cuddUtility->getConstant(static_cast(expression->getValueAsInt(nullptr))))); - } - - virtual void visit(storm::ir::expressions::UnaryBooleanFunctionExpression* expression) { - expression->getChild()->accept(this); - - ADD* childResult = stack.top(); - stack.pop(); - - switch (expression->getFunctionType()) { - case storm::ir::expressions::UnaryBooleanFunctionExpression::NOT: - stack.push(new ADD(~(*childResult))); - break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown boolean unary operator: '" << expression->getFunctionType() << "'."; - } - } - - virtual void visit(storm::ir::expressions::UnaryNumericalFunctionExpression* expression) { - expression->getChild()->accept(this); - - ADD* childResult = stack.top(); - stack.pop(); - - storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); - ADD* result = cuddUtility->getConstant(0); - switch(expression->getFunctionType()) { - case storm::ir::expressions::UnaryNumericalFunctionExpression::MINUS: - stack.push(new ADD(result->Minus(*childResult))); - break; - default: throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: " - << "Unknown numerical unary operator: '" << expression->getFunctionType() << "'."; - } - - } - - virtual void visit(storm::ir::expressions::VariableExpression* expression) { - storm::utility::CuddUtility* cuddUtility = storm::utility::cuddUtilityInstance(); - - std::vector const& variables = variableToDecisionDiagramVariableMap[expression->getVariableName()]; - - ADD* result = cuddUtility->getConstant(0); - if (expression->getType() == storm::ir::expressions::BaseExpression::bool_) { - cuddUtility->setValueAtIndex(result, 1, variables, 1); - } else { - storm::ir::Module const& module = program.getModule(program.getModuleIndexForVariable(expression->getVariableName())); - storm::ir::IntegerVariable const& integerVariable = module.getIntegerVariable(expression->getVariableName()); - int64_t low = integerVariable.getLowerBound()->getValueAsInt(nullptr); - int64_t high = integerVariable.getUpperBound()->getValueAsInt(nullptr); - - for (int_fast64_t i = low; i <= high; ++i) { - cuddUtility->setValueAtIndex(result, i - low, variables, static_cast(i)); - } - } - - stack.push(result); - } - -private: - storm::ir::Program const& program; - std::stack stack; - std::unordered_map>& variableToDecisionDiagramVariableMap; -}; - -} // namespace adapters - -} // namespace storm - -#endif /* STORM_ADAPTERS_SYMBOLICEXPRESSIONADAPTER_H_ */ diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp index 3214a1e42..cf6e42fb5 100644 --- a/src/builder/DdPrismModelBuilder.cpp +++ b/src/builder/DdPrismModelBuilder.cpp @@ -1,16 +1,16 @@ #include "src/builder/DdPrismModelBuilder.h" -#include "src/adapters/DdExpressionAdapter.h" #include "src/storage/dd/CuddDd.h" #include "src/storage/dd/CuddDdManager.h" #include "src/settings/SettingsManager.h" +#include "src/exceptions/InvalidStateException.h" + #include "src/utility/prism.h" #include "src/utility/math.h" -#include "src/utility/macros.h" namespace storm { - namespace adapters { + namespace builder { template DdPrismModelBuilder::Options::Options() : buildRewards(false), rewardModelName(), constantDefinitions() { @@ -48,6 +48,440 @@ namespace storm { } } + template + storm::dd::Dd DdPrismModelBuilder::createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Update const& update) { + storm::dd::Dd updateDd = generationInfo.manager->getOne(); + + // Iterate over all assignments (boolean and integer) and build the DD for it. + std::vector assignments = update.getAssignments(); + std::set assignedVariables; + for (auto const& assignment : assignments) { + // Record the variable as being written. + STORM_LOG_TRACE("Assigning to variable " << generationInfo.variableToRowMetaVariableMap.at(assignment.getVariable()).getName()); + assignedVariables.insert(generationInfo.variableToRowMetaVariableMap.at(assignment.getVariable())); + + // Translate the written variable. + auto const& primedMetaVariable = generationInfo.variableToColumnMetaVariableMap.at(assignment.getVariable()); + storm::dd::Dd writtenVariable = generationInfo.manager->getIdentity(primedMetaVariable); + + // Translate the expression that is being assigned. + storm::dd::Dd updateExpression = generationInfo.rowExpressionAdapter->translateExpression(assignment.getExpression()); + + // Combine the update expression with the guard. + storm::dd::Dd result = updateExpression * guard; + + // Combine the variable and the assigned expression. + result = result.equals(writtenVariable); + result *= guard; + + // Restrict the transitions to the range of the written variable. + result = result * generationInfo.manager->getRange(primedMetaVariable); + + updateDd *= result; + } + + // FIXME: global boolean variables cause problems. They cannot be added here, because then synchronization goes wrong. +// for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalBooleanVariables().size(); ++i) { +// storm::prism::BooleanVariable const& booleanVariable = generationInfo.program.getGlobalBooleanVariables().at(i); +// if (update.getAssignmentMapping().find(booleanVariable.getName()) == update.getAssignmentMapping().end()) { +// // Multiply identity matrix +// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(booleanVariable.getName()); +// } +// } +// +// // All unused global integer variables do not change +// for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalIntegerVariables().size(); ++i) { +// storm::prism::IntegerVariable const& integerVariable = generationInfo.program.getGlobalIntegerVariables().at(i); +// if (update.getAssignmentMapping().find(integerVariable.getName()) == update.getAssignmentMapping().end()) { +// // Multiply identity matrix +// updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(integerVariable.getName()); +// } +// } + + // All unassigned boolean variables need to keep their value. + for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { + if (assignedVariables.find(booleanVariable.getExpressionVariable()) == assignedVariables.end()) { + storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(booleanVariable.getExpressionVariable()); + STORM_LOG_TRACE("Multiplying identity of variable " << booleanVariable.getName()); + updateDd *= generationInfo.variableToIdentityMap.at(booleanVariable.getExpressionVariable()); + } + } + + // All unassigned integer variables need to keep their value. + for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { + storm::expressions::Variable const& metaVariable = generationInfo.variableToRowMetaVariableMap.at(integerVariable.getExpressionVariable()); + if (assignedVariables.find(metaVariable) == assignedVariables.end()) { + STORM_LOG_TRACE("Multiplying identity of variable " << integerVariable.getName()); + updateDd *= generationInfo.variableToIdentityMap.at(integerVariable.getExpressionVariable()); + } + } + + return updateDd; + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command) { + STORM_LOG_TRACE("Translating guard " << command.getGuardExpression()); + storm::dd::Dd guardDd = generationInfo.rowExpressionAdapter->translateExpression(command.getGuardExpression()); + STORM_LOG_WARN_COND(!guardDd.isZero(), "The guard '" << command.getGuardExpression() << "' is unsatisfiable."); + + if (!guardDd.isZero()) { + storm::dd::Dd commandDd = generationInfo.manager->getZero(); + for (storm::prism::Update const& update : command.getUpdates()) { + storm::dd::Dd updateDd = createUpdateDecisionDiagram(generationInfo, module, guardDd, update); + + STORM_LOG_WARN_COND(!updateDd.isZero(), "Update '" << update << "' does not have any effect."); + + double p = update.getLikelihoodExpression().evaluateAsDouble(); + updateDd *= generationInfo.manager->getConstant(p); + + commandDd += updateDd; + } + + return ActionDecisionDiagram(guardDd, guardDd * commandDd); + } else { + return ActionDecisionDiagram(*generationInfo.manager); + } + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, boost::optional synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset) { + std::vector commandDds; + for (storm::prism::Command const& command : module.getCommands()) { + + // Determine whether the command is relevant for the selected action. + bool relevant = (!synchronizationActionIndex && !command.isLabeled()) || (synchronizationActionIndex && command.getActionIndex() == synchronizationActionIndex.get()); + + if (!relevant) { + continue; + } + + // At this point, the command is known to be relevant for the action. + commandDds.push_back(createCommandDecisionDiagram(generationInfo, module, command)); + } + + ActionDecisionDiagram result(*generationInfo.manager); + if (!commandDds.empty()) { + switch (generationInfo.program.getModelType()){ + case storm::prism::Program::ModelType::DTMC: + result = combineCommandsToActionDTMC(generationInfo, commandDds); + break; + case storm::prism::Program::ModelType::MDP: + result = combineCommandsToActionMDP(generationInfo, commandDds, nondeterminismVariableOffset); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot translate model of this type."); + } + } + + return result; + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector const& commandDds) { + storm::dd::Dd allGuards = generationInfo.manager->getZero(); + storm::dd::Dd allCommands = generationInfo.manager->getZero(); + storm::dd::Dd temporary; + + for (auto const& commandDd : commandDds) { + // Check for overlapping guards. + temporary = commandDd.guardDd * allGuards; + STORM_LOG_WARN_COND(temporary.isZero(), "Guard of a command overlaps with previous guards."); + + allGuards += commandDd.guardDd; + allCommands += commandDd.guardDd * commandDd.transitionsDd; + } + + return ActionDecisionDiagram(allGuards, allCommands); + } + + template + storm::dd::Dd DdPrismModelBuilder::encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value) { + storm::dd::Dd result = generationInfo.manager->getOne(); + + std::map metaVariableNameToValueMap; + for (uint_fast64_t i = nondeterminismVariableOffset; i < nondeterminismVariableOffset + numberOfBinaryVariables; ++i) { + if (value & (1ull << (numberOfBinaryVariables - i - 1))) { + metaVariableNameToValueMap.emplace(generationInfo.nondeterminismMetaVariables[i], 1); + } + else { + metaVariableNameToValueMap.emplace(generationInfo.nondeterminismMetaVariables[i], 0); + } + } + + result.setValue(metaVariableNameToValueMap, 1); + return result; + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector const& commandDds, uint_fast64_t nondeterminismVariableOffset) { + storm::dd::Dd allGuards = generationInfo.manager->getZero(); + storm::dd::Dd allCommands = generationInfo.manager->getZero(); + + // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state. + storm::dd::Dd sumOfGuards = generationInfo.manager->getZero(); + for (auto const& commandDd : commandDds) { + sumOfGuards += commandDd.guardDd; + allGuards = allGuards || commandDd.guardDd; + } + uint_fast64_t maxChoices = static_cast(sumOfGuards.getMax()); + + // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism. + if (maxChoices == 0) { + return ActionDecisionDiagram(*generationInfo.manager); + } else if (maxChoices == 1) { + // Sum up all commands. + for (auto const& commandDd : commandDds) { + // FIXME: necessary to multiply with guard again? + allCommands += commandDd.guardDd * commandDd.transitionsDd; + } + return ActionDecisionDiagram(sumOfGuards, allCommands); + } else { + // Calculate number of required variables to encode the nondeterminism. + uint_fast64_t numberOfBinaryVariables = static_cast(std::ceil(storm::utility::math::log2(maxChoices))); + + storm::dd::Dd equalsNumberOfChoicesDd = generationInfo.manager->getZero(); + std::vector> choiceDds(maxChoices, generationInfo.manager->getZero()); + std::vector> remainingDds(maxChoices, generationInfo.manager->getZero()); + + for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) { + // Determine the set of states with exactly currentChoices choices. + equalsNumberOfChoicesDd = sumOfGuards.equals(generationInfo.manager->getConstant(static_cast(currentChoices))); + + // If there is no such state, continue with the next possible number of choices. + if (equalsNumberOfChoicesDd.isZero()) { + continue; + } + + // Reset the previously used intermediate storage. + for (uint_fast64_t j = 0; j < currentChoices; ++j) { + choiceDds[j] = generationInfo.manager->getZero(); + remainingDds[j] = equalsNumberOfChoicesDd; + } + + for (std::size_t j = 0; j < commandDds.size(); ++j) { + // Check if command guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices + // choices such that one outgoing choice is given by the j-th command. + storm::dd::Dd guardChoicesIntersection = commandDds[j].guardDd && equalsNumberOfChoicesDd; + + // If there is no such state, continue with the next command. + if (guardChoicesIntersection.isZero()) { + continue; + } + + // Split the currentChoices nondeterministic choices. + for (uint_fast64_t k = 0; k < currentChoices; ++k) { + // Calculate the overlapping part of command guard and the remaining DD. + storm::dd::Dd remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k]; + + // Check if we can add some overlapping parts to the current index + if (!remainingGuardChoicesIntersection.isZero()) { + // Remove overlapping parts from the remaining DD. + remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection; + + // Combine the overlapping part of the guard with command updates and add it to the resulting DD. + choiceDds[k] += remainingGuardChoicesIntersection * commandDds[j].transitionsDd; + } + + // Remove overlapping parts from the command guard DD + guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection; + + // If the guard DD has become equivalent to false, we can stop here. + if (guardChoicesIntersection.isZero()) { + break; + } + } + } + + // Add the meta variables that encode the nondeterminisim to the different choices. + for (uint_fast64_t j = 0; j < currentChoices; ++j) { + allCommands += encodeChoice(generationInfo, nondeterminismVariableOffset, numberOfBinaryVariables, j) * choiceDds[j]; + } + + // Delete currentChoices out of overlapping DD + sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd); + } + + return ActionDecisionDiagram(allGuards, allCommands, nondeterminismVariableOffset + numberOfBinaryVariables); + } + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) { + return ActionDecisionDiagram(action1.guardDd * action2.guardDd, action1.transitionsDd * action2.transitionsDd, std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables)); + } + + template + typename DdPrismModelBuilder::ActionDecisionDiagram DdPrismModelBuilder::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2, storm::dd::Dd const& identityDd1, storm::dd::Dd const& identityDd2) { + storm::dd::Dd action1Extended = action1.transitionsDd * identityDd2; + storm::dd::Dd action2Extended = action2.transitionsDd * identityDd1; + + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { + return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1Extended + action2Extended, 0); + } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + if (action1.transitionsDd.isZero()) { + return ActionDecisionDiagram(action2.guardDd, action2Extended, action2.numberOfUsedNondeterminismVariables); + } else if (action2.transitionsDd.isZero()) { + return ActionDecisionDiagram(action1.guardDd, action1Extended, action1.numberOfUsedNondeterminismVariables); + } + + // Bring both choices to the same number of variables that encode the nondeterminism. + uint_fast64_t numberOfUsedNondeterminismVariables = std::max(action1.numberOfUsedNondeterminismVariables, action2.numberOfUsedNondeterminismVariables); + if (action1.numberOfUsedNondeterminismVariables > action2.numberOfUsedNondeterminismVariables) { + storm::dd::Dd nondeterminisimEncoding = generationInfo.manager->getOne(); + + for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables + 1; i <= action1.numberOfUsedNondeterminismVariables; ++i) { + nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0); + } + action2Extended *= nondeterminisimEncoding; + } else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) { + storm::dd::Dd nondeterminisimEncoding = generationInfo.manager->getOne(); + + for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables + 1; i <= action2.numberOfUsedNondeterminismVariables; ++i) { + nondeterminisimEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0); + } + action1Extended *= nondeterminisimEncoding; + } + + // Add a new variable that resolves the nondeterminism between the two choices. + storm::dd::Dd combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables + 1], 1).ite(action2Extended, action1Extended); + + return ActionDecisionDiagram(action1.guardDd || action2.guardDd, combinedTransitions, numberOfUsedNondeterminismVariables + 1); + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type."); + } + } + + template + typename DdPrismModelBuilder::ModuleDecisionDiagram DdPrismModelBuilder::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap) { + // Start by creating the action DD for the independent action. + ActionDecisionDiagram independentActionDd = createActionDecisionDiagram(generationInfo, module, boost::optional(), 0); + + // Create module DD for all synchronizing actions of the module. + std::map actionIndexToDdMap; + for (auto const& actionIndex : module.getActionIndices()) { + actionIndexToDdMap.emplace(actionIndex, createActionDecisionDiagram(generationInfo, module, actionIndex, synchronizingActionToOffsetMap.at(actionIndex))); + } + + return ModuleDecisionDiagram(independentActionDd, actionIndexToDdMap, generationInfo.moduleToIdentityMap.at(module.getName())); + } + + template + storm::dd::Dd DdPrismModelBuilder::createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module) { + // If the model is an MDP, we need to encode the nondeterminism using additional variables. + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { + storm::dd::Dd result = generationInfo.manager->getZero(); + + // First, determine the maximal variable index that is used. + uint_fast64_t numberOfUsedNondeterminismVariables = module.independentAction.numberOfUsedNondeterminismVariables; + for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { + numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, synchronizingAction.second.numberOfUsedNondeterminismVariables); + } + + // Now make all actions use the same amount of nondeterminism variables. + + // Add variables to independent action DD. + storm::dd::Dd nondeterminismEncoding = generationInfo.manager->getOne(); + for (uint_fast64_t i = module.independentAction.numberOfUsedNondeterminismVariables + 1; i <= numberOfUsedNondeterminismVariables; ++i) { + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0); + } + result = module.independentAction.transitionsDd * nondeterminismEncoding; + + // Add variables to synchronized action DDs. + std::map> synchronizingActionToDdMap; + for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { + nondeterminismEncoding = generationInfo.manager->getOne(); + for (uint_fast64_t i = synchronizingAction.second.numberOfUsedNondeterminismVariables + 1; i <= numberOfUsedNondeterminismVariables; ++i) { + nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0); + } + synchronizingActionToDdMap.emplace(synchronizingAction.first, synchronizingAction.second.transitionsDd * nondeterminismEncoding); + } + + // Add variables for synchronization. + storm::dd::Dd synchronization = generationInfo.manager->getOne(); + for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0); + } + result *= synchronization; + + for (auto& synchronizingAction : synchronizingActionToDdMap) { + synchronization = generationInfo.manager->getOne(); + + for (uint_fast64_t i = 0; i < generationInfo.synchronizationMetaVariables.size(); ++i) { + if (i == synchronizingAction.first) { + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 1); + } else { + synchronization *= generationInfo.manager->getEncoding(generationInfo.synchronizationMetaVariables[i], 0); + } + } + + synchronizingAction.second *= synchronization; + } + + // Now, we can simply add all synchronizing actions to the result. + for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { + result += synchronizingAction.second.transitionsDd; + } + + return result; + } else { + // Simply add all actions. + storm::dd::Dd result = module.independentAction.transitionsDd; + for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) { + result += synchronizingAction.second.transitionsDd; + } + return result; + } + } + + template + storm::dd::Dd DdPrismModelBuilder::createSystemDecisionDiagram(GenerationInformation& generationInfo) { + // Create the initial offset mapping. + std::map synchronizingActionToOffsetMap; + for (auto const& actionIndex : generationInfo.program.getActionIndices()) { + synchronizingActionToOffsetMap[actionIndex] = 0; + } + + // Start by creating DDs for the first module. + ModuleDecisionDiagram system = createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(0), synchronizingActionToOffsetMap); + + // No translate module by module and combine it with the system created thus far. + for (uint_fast64_t i = 1; i < generationInfo.program.getNumberOfModules(); ++i) { + storm::prism::Module const& currentModule = generationInfo.program.getModule(i); + + // Update the offset index. + for (auto const& actionIndex : generationInfo.program.getActionIndices()) { + synchronizingActionToOffsetMap[actionIndex] = system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables; + } + + ModuleDecisionDiagram nextModule = createModuleDecisionDiagram(generationInfo, currentModule, synchronizingActionToOffsetMap); + + // Combine the non-synchronizing action. + system.independentAction = combineUnsynchronizedActions(generationInfo, system.independentAction, nextModule.independentAction, system.identity, nextModule.identity); + + // Combine synchronizing actions. + for (auto const& actionIndex : currentModule.getActionIndices()) { + if (system.hasSynchronizingAction(actionIndex)) { + system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex]); + } else { + system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineUnsynchronizedActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], nextModule.synchronizingActionToDecisionDiagramMap[actionIndex], system.identity, nextModule.identity); + } + } + + // Combine identity matrices. + system.identity = system.identity * nextModule.identity; + } + + storm::dd::Dd result = createSystemFromModule(generationInfo, system); + + // For DTMCs, we normalize each row to 1 (to account for non-determinism). + if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) { + result = result / result.sumAbstract(generationInfo.columnMetaVariables); + } + + return result; + } + template void DdPrismModelBuilder::translateProgram(storm::prism::Program const& program, Options const& options) { // There might be nondeterministic variables. In that case the program must be prepared before translating. @@ -62,56 +496,42 @@ namespace storm { // Start by initializing the structure used for storing all information needed during the model generation. // In particular, this creates the meta variables used to encode the model. -// GenerationInformation generationInfo(preparedProgram); + GenerationInformation generationInfo(preparedProgram); -// LOG4CPLUS_INFO(logger, "Creating MTBDD representation for probabilistic program."); -// -// // There might be nondeterministic variables. In that case the program must be prepared before translating. -// storm::prism::Program preparedProgram = program.defineUndefinedConstants(std::map()); -// preparedProgram = preparedProgram.substituteConstants(); -// -// // Initialize the structure used for storing all information needed during the model generation. -// GenerationInformation generationInfo(preparedProgram); -// -// // Initial state DD -// storm::dd::Dd initialStateDd = generationInfo.manager->getZero(); -// initialStateDd = getInitialStateDecisionDiagram(generationInfo); -// -// // System DD -// storm::dd::Dd systemDd = generationInfo.manager->getZero(); -// -// // Reachable states DD -// storm::dd::Dd reachableStatesDd = generationInfo.manager->getOne(); -// -// // Initialize the clock. -// auto clock = std::chrono::high_resolution_clock::now(); -// -// // Create system DD -// systemDd = createSystemDecisionDiagramm(generationInfo); -// std::cout << "Built transition matrix in " << std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - clock).count() << "ms." << std::endl; -// -// //manager->triggerReordering(); -// -// // Get all reachable states -// if (!storm::settings::adapterSettings().isNoReachSet()){ -// reachableStatesDd = performReachability(generationInfo, systemDd, initialStateDd); -// // Reduce transition matrix -// systemDd = systemDd * reachableStatesDd; -// } -// -// // Fix deadlocks -// if (!storm::settings::adapterSettings().isNoDeadlockSet()){ -// systemDd = findDeadlocks(generationInfo, systemDd, reachableStatesDd); -// } + auto clock = std::chrono::high_resolution_clock::now(); + storm::dd::Dd transitionMatrix = createSystemDecisionDiagram(generationInfo); + std::cout << "Built transition matrix in " << std::chrono::duration_cast(std::chrono::high_resolution_clock::now() - clock).count() << "ms." << std::endl; + transitionMatrix.exportToDot("trans.dot"); + std::cout << "num transitions: " << transitionMatrix.getNonZeroCount() << std::endl; + + storm::dd::Dd initialStates = createInitialStatesDecisionDiagram(generationInfo); + std::cout << "initial states: " << initialStates.getNonZeroCount() << std::endl; + + + } + + template + storm::dd::Dd DdPrismModelBuilder::createInitialStatesDecisionDiagram(GenerationInformation& generationInfo) { + storm::dd::Dd initialStates = generationInfo.rowExpressionAdapter->translateExpression(generationInfo.program.getInitialConstruct().getInitialStatesExpression()); + + for (auto const& metaVariable : generationInfo.rowMetaVariables) { + initialStates *= generationInfo.manager->getRange(metaVariable); + } + + return initialStates; + } + +// template +// storm::dd::Dd DdPrismModelBuilder::performReachability(GenerationInformation& generationInfo, storm::dd::Dd const& initialStates, storm::dd::Dd const& transitions) { +// storm::dd::Dd reachableStates = initialStates; // -// // System DD with only 0/1 leaves -// storm::dd::Dd systemBdd = systemDd.notZero(); +// // Copy current state +// storm::dd::Dd newReachableStates = reachableStates; // -// // Get all abstract variables (MDP) // std::set abstractVariables = std::set(); // -// if (program.getModelType() == storm::prism::Program::ModelType::MDP) { +// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { // for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { // // Synchronizing variables // if (systemDd.containsMetaVariable("sync" + std::to_string(i))) { @@ -126,221 +546,65 @@ namespace storm { // } // } // -// // Create state labeling -// std::unordered_map> labelToStateDdMap; -// storm::dd::Dd temporary; -// for (auto const& label : program.getLabels()) { -// // Translate Labeling into Expression and further into DD -// temporary = storm::adapters::SymbolicExpressionAdapter::translateExpression(label.getStatePredicateExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager, false); -// temporary = temporary * reachableStatesDd; -// labelToStateDdMap.insert(std::make_pair(label.getName(), temporary)); -// } -// -// // Create model -// std::shared_ptr> model; -// switch (program.getModelType()){ -// case storm::prism::Program::ModelType::DTMC: -// model = std::shared_ptr>(std::make_shared>(std::move(systemDd), -// std::move(systemBdd), std::move(initialStateDd), std::move(reachableStatesDd), -// std::move(generationInfo.rewardDds.first), std::move(generationInfo.rewardDds.second), std::move(generationInfo.manager->getZero()), -// std::move(generationInfo.rowMetaVariableNames), std::move(generationInfo.columnMetaVariableNames), std::move(generationInfo.metaVariablePairs), -// std::move(generationInfo.allSynchronizingActions), std::move(abstractVariables), std::move(generationInfo.manager), std::move(labelToStateDdMap))); -// break; -// case storm::prism::Program::ModelType::MDP: -// model = std::shared_ptr>(std::make_shared>(std::move(systemDd), -// std::move(systemBdd), std::move(initialStateDd), std::move(reachableStatesDd), -// std::move(generationInfo.rewardDds.first), std::move(generationInfo.rewardDds.second), std::move(generationInfo.transitionActionDd), -// std::move(generationInfo.rowMetaVariableNames), std::move(generationInfo.columnMetaVariableNames), std::move(generationInfo.metaVariablePairs), -// std::move(generationInfo.allSynchronizingActions), std::move(abstractVariables), std::move(generationInfo.manager), std::move(labelToStateDdMap))); -// break; -// default: -// STORM_LOG_ASSERT(false, "Illegal model type."); -// } -// -// LOG4CPLUS_INFO(logger, "Done creating MTBDD representation for probabilistic preparedProgram."); -// LOG4CPLUS_INFO(logger, "MTBDD: " << systemDd.getNodeCount() << " nodes, " << systemDd.getLeafCount() << " leaves, " << generationInfo.manager->getNumberOfMetaVariables() << " variables."); -// return model; - } - -// template -// void SymbolicModelAdapter::GenerationInformation::addDecisionDiagramVariables() { -// -// uint_fast64_t numberOfSynchronizingActions = allSynchronizingActions.size(); -// -// // Add synchronizing variables -// for (uint_fast64_t i = 0; i < numberOfSynchronizingActions; ++i) { -// manager->addMetaVariable("sync" + std::to_string(i), 0, 1); -// } -// -// // Add nondet. variables ( number of modules + number of commands) -// numberOfNondetVariables = program.getModules().size(); -// for (uint_fast64_t i = 0; i < program.getModules().size(); ++i) { -// numberOfNondetVariables += program.getModule(i).getCommands().size(); -// } -// -// for (uint_fast64_t i = numberOfNondetVariables; i > 0; --i) { -// manager->addMetaVariable("nondet" + std::to_string(i), 0, 1); -// } -// -// std::vector newVariables; -// -// // Global Boolean Variables -// for (uint_fast64_t j = 0; j < program.getGlobalBooleanVariables().size(); ++j) { -// storm::prism::BooleanVariable const& booleanVariable = program.getGlobalBooleanVariables().at(j); -// -// // Add row and column meta variable -// manager->addMetaVariable(booleanVariable.getName(), 0, 1); -// -// rowMetaVariableNames.insert(booleanVariable.getName()); -// columnMetaVariableNames.insert(booleanVariable.getName() + "'"); -// -// // Create pair (column,row) -// std::pair variablePair(booleanVariable.getName() + "'", booleanVariable.getName()); -// metaVariablePairs.push_back(variablePair); -// } +// // Create system BDD +// storm::dd::Dd systemBdd = systemDd.notZero(); // -// // Global Integer Variables -// for (uint_fast64_t j = 0; j < program.getGlobalIntegerVariables().size(); ++j) { -// storm::prism::IntegerVariable const& integerVariable = program.getGlobalIntegerVariables().at(j); -// -// int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); -// int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); -// -// // Add row and column meta variable -// manager->addMetaVariable(integerVariable.getName(), low, high); -// -// rowMetaVariableNames.insert(integerVariable.getName()); -// columnMetaVariableNames.insert(integerVariable.getName() + "'"); -// -// // Create pair (column,row) -// std::pair variablePair(integerVariable.getName() + "'", integerVariable.getName()); -// metaVariablePairs.push_back(variablePair); +// // For MDPs, we need to abstract from the nondeterminism variables, but we can do so prior to the +// // reachability analysis. +// if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) { +// // Abstract from synchronizing and nondet. variables (MDPs) +// systemBdd = systemBdd.existsAbstract(abstractVariables); // } // -// // Add boolean and integer variables -// for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { -// storm::prism::Module const& module = program.getModule(i); -// -// // Boolean Variables -// for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { -// storm::prism::BooleanVariable const& booleanVariable = module.getBooleanVariables().at(j); -// -// // Add row and column meta variable -// manager->addMetaVariable(booleanVariable.getName(), 0, 1); -// -// rowMetaVariableNames.insert(booleanVariable.getName()); -// columnMetaVariableNames.insert(booleanVariable.getName() + "'"); -// -// // Create pair (column,row) -// std::pair variablePair(booleanVariable.getName() + "'", booleanVariable.getName()); -// metaVariablePairs.push_back(variablePair); -// } -// -// // Integer Variables -// for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { -// storm::prism::IntegerVariable const& integerVariable = module.getIntegerVariables().at(j); -// -// int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); -// int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); -// -// // Add row and column meta variable -// manager->addMetaVariable(integerVariable.getName(), low, high); -// -// rowMetaVariableNames.insert(integerVariable.getName()); -// columnMetaVariableNames.insert(integerVariable.getName() + "'"); -// -// // Create pair (column,row) -// std::pair variablePair(integerVariable.getName() + "'", integerVariable.getName()); -// metaVariablePairs.push_back(variablePair); -// } -// } +// // Initialize variables and choose option +// bool changed; +// int iter = 0; +// int option = storm::settings::adapterSettings().getReachabilityMethod(); // -// std::cout << "Variable Ordering: "; -// for(auto x: manager->getDdVariableNames()){ -// std::cout << x << ","; -// } -// std::cout << std::endl; -// std::cout << std::endl; -// } -// -// template -// void SymbolicModelAdapter::GenerationInformation::createIdentityDecisionDiagrams() { +// //TODO: Name reachability options. +// std::cout << "Reachability option: " << option << std::endl; // -// // Global Boolean variables -// for (uint_fast64_t j = 0; j < program.getGlobalBooleanVariables().size(); ++j) { -// storm::prism::BooleanVariable const & booleanVariable = program.getGlobalBooleanVariables().at(j); -// -// storm::dd::Dd identity = manager->getZero(); -// -// // f(0)=0 leads to 1 -// identity.setValue(booleanVariable.getName(), 0, booleanVariable.getName() + "'", 0, 1); -// // f(1)=1 leads to 1 -// identity.setValue(booleanVariable.getName(), 1, booleanVariable.getName() + "'", 1, 1); +// if (option == 3 || option == 4){ // -// variableToIdentityDecisionDiagramMap.insert(std::make_pair(booleanVariable.getName(), identity)); -// } -// -// // Global Integer variables -// for (uint_fast64_t j = 0; j < program.getGlobalIntegerVariables().size(); ++j) { -// storm::prism::IntegerVariable const& integerVariable = program.getGlobalIntegerVariables().at(j); -// storm::dd::Dd identity = manager->getZero(); +// S = storm::dd::Dd(initialStateDd); +// U = storm::dd::Dd(initialStateDd); // -// int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); -// int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); +// generationInfo.globalSystemDds.independentActionDd.commandsDd = generationInfo.globalSystemDds.independentActionDd.commandsDd.notZero(); +// generationInfo.globalSystemDds.independentActionDd.commandsDd = generationInfo.globalSystemDds.independentActionDd.commandsDd.existsAbstract(abstractVariables); // -// for (int_fast64_t i = low; i <= high; ++i) { -// // f(i)=i leads to 1 -// identity.setValue(integerVariable.getName(), i, integerVariable.getName() + "'", i, 1); +// for (uint_fast64_t i = 0; i < generationInfo.allSynchronizingActions.size(); ++i) { +// generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd = generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd.notZero(); +// generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd = generationInfo.globalSystemDds.synchronizingActionDds[i].commandsDd.existsAbstract(abstractVariables); // } -// -// variableToIdentityDecisionDiagramMap.insert(std::make_pair(integerVariable.getName(), identity)); // } // -// -// for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) { -// storm::prism::Module const& module = program.getModule(i); -// -// // Module identity matrix -// storm::dd::Dd moduleIdentity = manager->getOne(); -// -// // Boolean variables -// for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) { -// storm::prism::BooleanVariable const& booleanVariable = module.getBooleanVariables().at(j); +// // Perform updates until nothing changes +// do { +// if (option == 1){ +// iter++; +// changed = true; // -// storm::dd::Dd identity = manager->getZero(); +// newReachableStates = newReachableStates * systemBdd; // -// // f(0)=0 leads to 1 -// identity.setValue(booleanVariable.getName(), 0, booleanVariable.getName() + "'", 0, 1); -// // f(1)=1 leads to 1 -// identity.setValue(booleanVariable.getName(), 1, booleanVariable.getName() + "'", 1, 1); +// // Abstract from row meta variables +// newReachableStates = newReachableStates.existsAbstract(generationInfo.rowMetaVariableNames); // -// variableToIdentityDecisionDiagramMap.insert(std::make_pair(booleanVariable.getName(), identity)); -// moduleIdentity = moduleIdentity * identity; -// } -// -// // Integer variables -// for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) { -// storm::prism::IntegerVariable const& integerVariable = module.getIntegerVariables().at(j); -// storm::dd::Dd identity = manager->getZero(); +// // Swap column variables to row variables +// newReachableStates.swapVariables(generationInfo.metaVariablePairs); // -// int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); -// int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); +// newReachableStates = newReachableStates * (!reachableStates); // -// for (int_fast64_t i = low; i <= high; ++i) { -// // f(i)=i leads to 1 -// identity.setValue(integerVariable.getName(), i, integerVariable.getName() + "'", i, 1); +// // Check if something has changed +// if (newReachableStates.isZero()) { +// changed = false; // } // -// variableToIdentityDecisionDiagramMap.insert(std::make_pair(integerVariable.getName(), identity)); -// moduleIdentity = moduleIdentity * identity; -// } -// -// // Create module identity matrix -// moduleToIdentityDecisionDiagramMap.insert(std::make_pair(module.getName(), moduleIdentity)); -// } -// +// // Update reachableStates DD +// reachableStates = reachableStates + newReachableStates; +// +// // } -// + // template // storm::dd::Dd SymbolicModelAdapter::createSystemDecisionDiagramm(GenerationInformation & generationInfo){ // @@ -436,7 +700,7 @@ namespace storm { // // return systemTransitionMatrix; // } -// +// // template // SystemComponentDecisionDiagram SymbolicModelAdapter::combineSystem(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram systemDds){ // @@ -683,45 +947,6 @@ namespace storm { // return systemComponentDd; // } // -// template -// ModuleDecisionDiagram SymbolicModelAdapter::combineCommandsDTMC(std::shared_ptr> const & manager, uint_fast64_t numberOfCommands, std::vector> const& commandDds, std::vector> const & guardDds){ -// -// // Module DD -// ModuleDecisionDiagram moduleDd; -// -// // Initialize DDs -// storm::dd::Dd guardRangeDd = manager->getZero(); -// storm::dd::Dd commandsDd = manager->getZero(); -// storm::dd::Dd temporary = manager->getZero(); -// -// for (uint_fast64_t i = 0; i < numberOfCommands; ++i) { -// -// // Check guard -// if (guardDds[i].isZero()) continue; -// -// // Check for overlapping guards -// temporary = guardDds[i] * guardRangeDd; -// if (!(temporary.isZero())) { -// LOG4CPLUS_WARN(logger, "Overlapping guard in command " << (i + 1) << "."); -// } -// -// // Sum up all guards -// guardRangeDd = guardRangeDd + guardDds[i]; -// -// // Create command DD (multiply guard and updates) -// temporary = guardDds[i] * commandDds[i]; -// -// // Sum up all command DDs -// commandsDd = commandsDd + temporary; -// } -// -// moduleDd.guardDd = guardRangeDd; -// moduleDd.commandsDd = commandsDd; -// moduleDd.usedNondetVariables = 0; -// -// return moduleDd; -// } -// // // TODO // std::map getMetaVariableMapping(std::vector metaVariables, uint_fast64_t value){ // @@ -735,7 +960,7 @@ namespace storm { // metaVariableNameToValueMap.insert(std::make_pair(metaVariables[i], 0)); // } // } -// +// // return metaVariableNameToValueMap; // } // @@ -886,7 +1111,7 @@ namespace storm { // // // Translate guard // guardDds[j] = storm::adapters::SymbolicExpressionAdapter::translateExpression(command.getGuardExpression().getBaseExpressionPointer(), generationInfo.program, generationInfo.manager); -// +// // if (guardDds[j].isZero()){ // LOG4CPLUS_WARN(logger, "A guard is unsatisfiable."); // } @@ -948,7 +1173,7 @@ namespace storm { // // return commandDd; // } -// +// // template // storm::dd::Dd SymbolicModelAdapter::createUpdateDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Update const& update){ // @@ -977,7 +1202,7 @@ namespace storm { // // updateDd = updateDd * result; // } -// +// // // All unused global boolean variables do not change // for (uint_fast64_t i = 0; i < generationInfo.program.getGlobalBooleanVariables().size(); ++i) { // storm::prism::BooleanVariable const& booleanVariable = generationInfo.program.getGlobalBooleanVariables().at(i); @@ -1013,7 +1238,7 @@ namespace storm { // updateDd = updateDd * generationInfo.variableToIdentityDecisionDiagramMap.at(integerVariable.getName()); // } // } -// +// // return updateDd; // } // diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h index 03283d55d..fa9ebf150 100644 --- a/src/builder/DdPrismModelBuilder.h +++ b/src/builder/DdPrismModelBuilder.h @@ -7,9 +7,10 @@ #include "src/logic/Formulas.h" #include "src/storage/prism/Program.h" #include "src/adapters/DdExpressionAdapter.h" +#include "src/utility/macros.h" namespace storm { - namespace adapters { + namespace builder { template class DdPrismModelBuilder { @@ -63,10 +64,21 @@ namespace storm { private: // This structure can store the decision diagrams representing a particular action. struct ActionDecisionDiagram { - ActionDecisionDiagram(storm::dd::DdManager const& manager) : guardDd(manager.getZero()), transitionsDd(manager.getZero()), numberOfUsedNondeterminismVariables(0) { + ActionDecisionDiagram() : guardDd(), transitionsDd(), numberOfUsedNondeterminismVariables(0) { // Intentionally left empty. } + ActionDecisionDiagram(storm::dd::DdManager const& manager, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(manager.getZero()), transitionsDd(manager.getZero()), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { + // Intentionally left empty. + } + + ActionDecisionDiagram(storm::dd::Dd guardDd, storm::dd::Dd transitionsDd, uint_fast64_t numberOfUsedNondeterminismVariables = 0) : guardDd(guardDd), transitionsDd(transitionsDd), numberOfUsedNondeterminismVariables(numberOfUsedNondeterminismVariables) { + // Intentionally left empty. + } + + ActionDecisionDiagram(ActionDecisionDiagram const& other) = default; + ActionDecisionDiagram& operator=(ActionDecisionDiagram const& other) = default; + // The guard of the action. storm::dd::Dd guardDd; @@ -79,12 +91,27 @@ namespace storm { // This structure holds all decision diagrams related to a module. struct ModuleDecisionDiagram { - ModuleDecisionDiagram(storm::dd::DdManager const& manager) : independantAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()) { + ModuleDecisionDiagram() : independentAction(), synchronizingActionToDecisionDiagramMap(), identity() { + // Intentionally left empty. + } + + ModuleDecisionDiagram(storm::dd::DdManager const& manager) : independentAction(manager), synchronizingActionToDecisionDiagramMap(), identity(manager.getZero()) { + // Intentionally left empty. + } + + ModuleDecisionDiagram(ActionDecisionDiagram const& independentAction, std::map const& synchronizingActionToDecisionDiagramMap, storm::dd::Dd const& identity) : independentAction(independentAction), synchronizingActionToDecisionDiagramMap(synchronizingActionToDecisionDiagramMap), identity(identity) { // Intentionally left empty. } - // The decision diagram for the independant action. - ActionDecisionDiagram independantAction; + ModuleDecisionDiagram(ModuleDecisionDiagram const& other) = default; + ModuleDecisionDiagram& operator=(ModuleDecisionDiagram const& other) = default; + + bool hasSynchronizingAction(uint_fast64_t actionIndex) { + return synchronizingActionToDecisionDiagramMap.find(actionIndex) != synchronizingActionToDecisionDiagramMap.end(); + } + + // The decision diagram for the independent action. + ActionDecisionDiagram independentAction; // A mapping from synchronizing action indices to the decision diagram. std::map synchronizingActionToDecisionDiagramMap; @@ -97,23 +124,15 @@ namespace storm { * Structure to store all information required to generate the model from the program. */ class GenerationInformation { - GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), columnMetaVariables(), metaVariablePairs(), numberOfNondetVariables(0), variableToIdentityMap(), moduleToIdentityMap(), allSynchronizingActionIndices(), labelToStateDdMap() { + public: + GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), nondeterminismMetaVariables(), variableToIdentityMap(), moduleToIdentityMap() { // Initializes variables and identity DDs. - createMetaVariables(); - createIdentities(); + createMetaVariablesAndIdentities(); + + rowExpressionAdapter = std::unique_ptr>(new storm::adapters::DdExpressionAdapter(*manager, variableToRowMetaVariableMap)); + columnExpressionAdapter = std::unique_ptr>(new storm::adapters::DdExpressionAdapter(*manager, variableToColumnMetaVariableMap)); } - private: - /*! - * Creates the required meta variables. - */ - void createMetaVariables(); - - /*! - * Creates identity DDs for all variables and all modules. - */ - void createIdentities(); - // The program that is currently translated. storm::prism::Program const& program; @@ -121,135 +140,142 @@ namespace storm { std::shared_ptr> manager; // The meta variables for the row encoding. - std::vector rowMetaVariables; + std::set rowMetaVariables; + std::map variableToRowMetaVariableMap; + std::unique_ptr> rowExpressionAdapter; // The meta variables for the column encoding. - std::vector columnMetaVariables; - - // Pairs of meta variables (row, column). - std::vector> metaVariablePairs; - - // Number of variables used to encode the nondeterminism. - uint_fast64_t numberOfNondetVariables; + std::set columnMetaVariables; + std::map variableToColumnMetaVariableMap; + std::unique_ptr> columnExpressionAdapter; + + // The meta variables used to encode the nondeterminism. + std::vector nondeterminismMetaVariables; + + // The meta variables used to encode the synchronization. + std::vector synchronizationMetaVariables; // DDs representing the identity for each variable. std::map> variableToIdentityMap; // DDs representing the identity for each module (index). - std::map> moduleToIdentityMap; + std::map> moduleToIdentityMap; - // All synchronizing actions - std::set allSynchronizingActionIndices; - - // DDs representing the identity matrix for each module - std::unordered_map> labelToStateDdMap; + private: + /*! + * Creates the required meta variables and variable/module identities. + */ + void createMetaVariablesAndIdentities() { + // Add synchronization variables. + for (uint_fast64_t i = 0; i < program.getActionIndices().size(); ++i) { + std::pair variablePair = manager->addMetaVariable("sync" + std::to_string(i)); + synchronizationMetaVariables.push_back(variablePair.first); + } + + // Add nondeterminism variables (number of modules + number of commands). + uint_fast64_t numberOfNondeterminismVariables = program.getModules().size(); + for (auto const& module : program.getModules()) { + numberOfNondeterminismVariables += module.getNumberOfCommands(); + } + for (uint_fast64_t i = 0; i < numberOfNondeterminismVariables; ++i) { + std::pair variablePair = manager->addMetaVariable("nondet" + std::to_string(i)); + nondeterminismMetaVariables.push_back(variablePair.first); + } + + // Create meta variables for global program variables. + for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) { + std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)); + variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); + } + for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) { + int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); + int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); + std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first); + variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); + } + + // Create meta variables for each of the modules' variables. + for (storm::prism::Module const& module : program.getModules()) { + storm::dd::Dd moduleIdentity = manager->getOne(); + for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) { + std::pair variablePair = manager->addMetaVariable(booleanVariable.getName()); + STORM_LOG_TRACE("Created meta variables for boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second); + variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity); + moduleIdentity *= variableIdentity; + } + for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) { + int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt(); + int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt(); + std::pair variablePair = manager->addMetaVariable(integerVariable.getName(), low, high); + STORM_LOG_TRACE("Created meta variables for integer variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]"); + + rowMetaVariables.insert(variablePair.first); + variableToRowMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.first); + + columnMetaVariables.insert(variablePair.second); + variableToColumnMetaVariableMap.emplace(integerVariable.getExpressionVariable(), variablePair.second); + + storm::dd::Dd variableIdentity = manager->getIdentity(variablePair.first).equals(manager->getIdentity(variablePair.second)) * manager->getRange(variablePair.first) * manager->getRange(variablePair.second); + variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity); + moduleIdentity *= variableIdentity; + } + moduleToIdentityMap[module.getName()] = moduleIdentity; + } + } }; private: -// /*! -// * Creates system DD (full parallel) -// * -// * @return A DD representing the whole system -// */ -// static storm::dd::Dd createSystemDecisionDiagramm(GenerationInformation & generationInfo); -// -// /*! -// * Combines all DDs to one DD (including independent/synchronized actions) -// * -// * @param systemDds DDs representing the whole system -// * @return System DDs with combined independent/synchronized actions -// */ -// static SystemComponentDecisionDiagram combineSystem(GenerationInformation const & generationInfo, SystemComponentDecisionDiagram systemDds); -// -// /*! -// * Combines 2 modules with/without synchronizing actions -// * -// * @param synchronizing Synchronizing actions or not -// * @param module1 First module -// * @param module1 Second module -// * @param identity1 Identity matrix of first module -// * @param identity2 Identity matrix of second module -// * @return A module DD representing the combination of both modules -// */ -// static ModuleDecisionDiagram combineModules(GenerationInformation const & generationInfo, bool synchronizing, ModuleDecisionDiagram moduleDd1, ModuleDecisionDiagram moduleDd2, storm::dd::Dd const& identityDd1, storm::dd::Dd const& identityDd2); -// -// /*! -// * Combines 2 modules and solves non-determinism (MDP) -// * -// * @param module1 First module -// * @param module1 Second module -// * @return A module DD representing the combination of both modules -// */ -// static ModuleDecisionDiagram combineModulesMDP(GenerationInformation const & generationInfo, ModuleDecisionDiagram moduleDd1, ModuleDecisionDiagram moduleDd2); -// -// /*! -// * Creates a system component DD (module) -// * -// * @param module Module -// * @param usedNondetVariablesVector Number of used nondet. variables -// * @return A system component DD storing all required module information -// */ -// static SystemComponentDecisionDiagram createSystemComponentDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const & module, std::vector usedNondetVariablesVector); -// -// /*! -// * Combines commands (with guards) to a module DD (DTMC) -// * -// * @param numberOfCommands Number of commands in the current module -// * @param commandDds DDs containing all updates for each command -// * @param guardDds Guard DDs for each command -// * @return A DD representing the module. -// */ -// static ModuleDecisionDiagram combineCommandsDTMC(std::shared_ptr> const & manager, uint_fast64_t numberOfCommands, std::vector> const& commandDds, std::vector> const& guardDds); -// -// /*! -// * Combines commands (with guards) to a module DD (MDP) -// * -// * @param numberOfCommands Number of commands in the current module -// * @param commandDds DDs containing all updates for each command -// * @param guardDds Guard DDs for each command -// * @param usedNondetVariables Number of used nondet. variables -// * @return A DD representing the module. -// */ -// static ModuleDecisionDiagram combineCommandsMDP(std::shared_ptr> const & manager, uint_fast64_t numberOfCommands, std::vector> const& commandDds, std::vector> const& guardDds, uint_fast64_t usedNondetVariables); -// -// /*! -// * Creates a module DD -// * -// * @param module Module -// * @param synchronizingAction Name of the synchronizing action ("" = no synchronization) -// * @param usedNondetVariables Number of used nondet. variables -// * @return A DD representing the module (with/without synchronized actions). -// */ -// static ModuleDecisionDiagram createModuleDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, std::string const& synchronizingAction, uint_fast64_t usedNondetVariables); -// -// /*! -// * Creates a command DD -// * -// * @param module Current module -// * @param guard Command guard -// * @param update Command expression -// * @return A DD representing the command. -// */ -// static storm::dd::Dd createCommandDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Command const& command); -// -// /*! -// * Creates an update DD -// * -// * @param module Current module -// * @param guard Command guard -// * @param update Update expression -// * @return A DD representing the update. -// */ -// static storm::dd::Dd createUpdateDecisionDiagramm(GenerationInformation const & generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Update const& update); -// -// /*! -// * Creates initial state DD -// * -// * @return A DD representing the initial state. -// */ -// static storm::dd::Dd getInitialStateDecisionDiagram(GenerationInformation const & generationInfo); -// + static storm::dd::Dd encodeChoice(GenerationInformation& generationInfo, uint_fast64_t nondeterminismVariableOffset, uint_fast64_t numberOfBinaryVariables, int_fast64_t value); + + static storm::dd::Dd createUpdateDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::dd::Dd const& guard, storm::prism::Update const& update); + + static ActionDecisionDiagram createCommandDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, storm::prism::Command const& command); + + static ActionDecisionDiagram createActionDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, boost::optional synchronizationActionIndex, uint_fast64_t nondeterminismVariableOffset); + + static ActionDecisionDiagram combineCommandsToActionDTMC(GenerationInformation& generationInfo, std::vector const& commandDds); + + static ActionDecisionDiagram combineCommandsToActionMDP(GenerationInformation& generationInfo, std::vector const& commandDds, uint_fast64_t nondeterminismVariableOffset); + + static ActionDecisionDiagram combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2); + + static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2, storm::dd::Dd const& identityDd1, storm::dd::Dd const& identityDd2); + + static ModuleDecisionDiagram createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map const& synchronizingActionToOffsetMap); + + static storm::dd::Dd createSystemFromModule(GenerationInformation& generationInfo, ModuleDecisionDiagram const& module); + + static storm::dd::Dd createSystemDecisionDiagram(GenerationInformation& generationInfo); + + static storm::dd::Dd createInitialStatesDecisionDiagram(GenerationInformation& generationInfo); + + static storm::dd::Dd performReachability(GenerationInformation& generationInfo, storm::dd::Dd const& initialStates, storm::dd::Dd const& transitions); + // /*! // * Calculates the reachable states of the given transition matrix // * @@ -258,7 +284,7 @@ namespace storm { // * @return A DD representing all reachable states // */ // static storm::dd::Dd performReachability(GenerationInformation & generationInfo, storm::dd::Dd const& systemDd, storm::dd::Dd const& initialStateDd); -// +// // /*! // * Adds a self-loop to deadlock states // * diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h index a9a3075d2..e69e865f2 100644 --- a/src/builder/ExplicitPrismModelBuilder.h +++ b/src/builder/ExplicitPrismModelBuilder.h @@ -21,7 +21,7 @@ #include "src/settings/SettingsManager.h" #include "src/utility/constants.h" -#include "src/utility/PrismUtility.h" +#include "src/utility/prism.h" namespace storm { namespace builder { diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index bde97a841..db1ea2cee 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -13,7 +13,7 @@ #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h" #include "src/utility/counterexamples.h" -#include "src/utility/PrismUtility.h" +#include "src/utility/prism.h" namespace storm { namespace counterexamples { diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp index 25c99ced1..fc1a40aa9 100644 --- a/src/storage/dd/CuddDd.cpp +++ b/src/storage/dd/CuddDd.cpp @@ -175,7 +175,7 @@ namespace storm { std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); @@ -191,7 +191,7 @@ namespace storm { std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); @@ -207,7 +207,7 @@ namespace storm { std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); @@ -223,7 +223,7 @@ namespace storm { std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); @@ -239,7 +239,7 @@ namespace storm { std::set newMetaVariables = this->getContainedMetaVariables(); for (auto const& metaVariable : metaVariables) { // First check whether the DD contains the meta variable and erase it, if this is the case. - STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable that is not present in the DD."); + STORM_LOG_THROW(this->containsMetaVariable(metaVariable), storm::exceptions::InvalidArgumentException, "Cannot abstract from meta variable '" << metaVariable.getName() << "' that is not present in the DD."); newMetaVariables.erase(metaVariable); DdMetaVariable const& ddMetaVariable = this->getDdManager()->getMetaVariable(metaVariable); diff --git a/src/storage/dd/CuddDdManager.cpp b/src/storage/dd/CuddDdManager.cpp index 933b95af6..5a7d21f05 100644 --- a/src/storage/dd/CuddDdManager.cpp +++ b/src/storage/dd/CuddDdManager.cpp @@ -85,6 +85,7 @@ namespace storm { for (int_fast64_t value = metaVariable.getLow(); value <= metaVariable.getHigh(); ++value) { result.setValue(variable, value, static_cast(1)); } + return result; } diff --git a/src/utility/cli.h b/src/utility/cli.h index 6427f7dd9..2d6c48536 100644 --- a/src/utility/cli.h +++ b/src/utility/cli.h @@ -51,6 +51,7 @@ log4cplus::Logger printer; // Headers of builders. #include "src/builder/ExplicitPrismModelBuilder.h" +#include "src/builder/DdPrismModelBuilder.h" // Headers for model processing. #include "src/storage/NaiveDeterministicModelBisimulationDecomposition.h" @@ -272,14 +273,22 @@ namespace storm { } // Customize model-building. - typename storm::builder::ExplicitPrismModelBuilder::Options options; +// typename storm::builder::ExplicitPrismModelBuilder::Options options; +// if (formula) { +// options = typename storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); +// } +// options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); +// +// // Then, build the model from the symbolic description. +// result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); + + typename storm::builder::DdPrismModelBuilder::Options options; if (formula) { - options = typename storm::builder::ExplicitPrismModelBuilder::Options(*formula.get()); + options = typename storm::builder::DdPrismModelBuilder::Options(*formula.get()); } options.addConstantDefinitionsFromString(program, settings.getConstantDefinitionString()); - // Then, build the model from the symbolic description. - result = storm::builder::ExplicitPrismModelBuilder::translateProgram(program, options); + storm::builder::DdPrismModelBuilder::translateProgram(program, options); return result; } diff --git a/src/utility/math.h b/src/utility/math.h index 9ee653c4e..ba21bcfa1 100644 --- a/src/utility/math.h +++ b/src/utility/math.h @@ -6,15 +6,17 @@ #include "src/utility/OsDetection.h" namespace storm { - namespace math { - // We provide this method explicitly, because MSVC does not offer it (non-C99 compliant). - template - static inline double log2(ValueType number) { + namespace utility { + namespace math { + // We provide this method explicitly, because MSVC does not offer it (non-C99 compliant). + template + static inline double log2(ValueType number) { # ifndef WINDOWS - return std::log2(number); + return std::log2(number); # else - return std::log(number) / std::log(2); + return std::log(number) / std::log(2); # endif + } } } }