sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Merge branch 'jani_support' of https://sselab.de/lab9/private/git/storm into jani_support 

Former-commit-id: f2c3f1665b
tempestpy_adaptions
sjunges 9 years ago
parent
16e20ced0b 4c4e830a4c
commit
9a841a2bde
14 changed files with 511 additions and 224 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 607
      src/builder/DdPrismModelBuilder.cpp
  2. 14
      src/builder/DdPrismModelBuilder.h
  3. 4
      src/storage/prism/HidingComposition.cpp
  4. 2
      src/storage/prism/HidingComposition.h
  5. 2
      src/storage/prism/InterleavingParallelComposition.cpp
  6. 4
      src/storage/prism/InterleavingParallelComposition.h
  7. 51
      src/storage/prism/Program.cpp
  8. 29
      src/storage/prism/Program.h
  9. 4
      src/storage/prism/RenamingComposition.cpp
  10. 2
      src/storage/prism/RenamingComposition.h
  11. 6
      src/storage/prism/RestrictedParallelComposition.cpp
  12. 4
      src/storage/prism/RestrictedParallelComposition.h
  13. 2
      src/storage/prism/SynchronizingParallelComposition.cpp
  14. 4
      src/storage/prism/SynchronizingParallelComposition.h

607
src/builder/DdPrismModelBuilder.cpp
View File

@ -1,5 +1,7 @@
#include "src/builder/DdPrismModelBuilder.h"
#include <boost/algorithm/string/join.hpp>
#include "src/models/symbolic/Dtmc.h"
#include "src/models/symbolic/Ctmc.h"
#include "src/models/symbolic/Mdp.h"
@ -9,12 +11,13 @@
#include "src/settings/SettingsManager.h"
#include "src/exceptions/InvalidStateException.h"
#include "src/exceptions/NotSupportedException.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/utility/prism.h"
#include "src/utility/math.h"
#include "src/storage/prism/Program.h"
#include "src/storage/prism/Compositions.h"
#include "src/storage/dd/Add.h"
#include "src/storage/dd/cudd/CuddAddIterator.h"
@ -27,107 +30,148 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
class DdPrismModelBuilder<Type, ValueType>::GenerationInformation {
public:
GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() {
// Initializes variables and identity DDs.
createMetaVariablesAndIdentities();
rowExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToRowMetaVariableMap));
columnExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToColumnMetaVariableMap));
}
// The program that is currently translated.
storm::prism::Program const& program;
// The manager used to build the decision diagrams.
std::shared_ptr<storm::dd::DdManager<Type>> manager;
// The meta variables for the row encoding.
std::set<storm::expressions::Variable> rowMetaVariables;
std::map<storm::expressions::Variable, storm::expressions::Variable> variableToRowMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
// The meta variables for the column encoding.
std::set<storm::expressions::Variable> columnMetaVariables;
std::map<storm::expressions::Variable, storm::expressions::Variable> variableToColumnMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
// All pairs of row/column meta variables.
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
public:
GenerationInformation(storm::prism::Program const& program) : program(program), manager(std::make_shared<storm::dd::DdManager<Type>>()), rowMetaVariables(), variableToRowMetaVariableMap(), rowExpressionAdapter(nullptr), columnMetaVariables(), variableToColumnMetaVariableMap(), columnExpressionAdapter(nullptr), rowColumnMetaVariablePairs(), nondeterminismMetaVariables(), variableToIdentityMap(), allGlobalVariables(), moduleToIdentityMap() {
// Initializes variables and identity DDs.
createMetaVariablesAndIdentities();
// The meta variables used to encode the nondeterminism.
std::vector<storm::expressions::Variable> nondeterminismMetaVariables;
// The meta variables used to encode the synchronization.
std::vector<storm::expressions::Variable> synchronizationMetaVariables;
// A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization
// variables). This is handy to abstract from this variable set.
std::set<storm::expressions::Variable> allNondeterminismVariables;
rowExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToRowMetaVariableMap));
columnExpressionAdapter = std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>>(new storm::adapters::AddExpressionAdapter<Type>(manager, variableToColumnMetaVariableMap));
}
// As set of all variables used for encoding the synchronization.
std::set<storm::expressions::Variable> allSynchronizationMetaVariables;
// The program that is currently translated.
storm::prism::Program const& program;
// DDs representing the identity for each variable.
std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> variableToIdentityMap;
// The manager used to build the decision diagrams.
std::shared_ptr<storm::dd::DdManager<Type>> manager;
// A set of all meta variables that correspond to global variables.
std::set<storm::expressions::Variable> allGlobalVariables;
// The meta variables for the row encoding.
std::set<storm::expressions::Variable> rowMetaVariables;
std::map<storm::expressions::Variable, storm::expressions::Variable> variableToRowMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter;
// DDs representing the identity for each module.
std::map<std::string, storm::dd::Add<Type, ValueType>> moduleToIdentityMap;
// The meta variables for the column encoding.
std::set<storm::expressions::Variable> columnMetaVariables;
std::map<storm::expressions::Variable, storm::expressions::Variable> variableToColumnMetaVariableMap;
std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter;
// All pairs of row/column meta variables.
std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
// The meta variables used to encode the nondeterminism.
std::vector<storm::expressions::Variable> nondeterminismMetaVariables;
// The meta variables used to encode the synchronization.
std::vector<storm::expressions::Variable> synchronizationMetaVariables;
// A set of all variables used for encoding the nondeterminism (i.e. nondetermism + synchronization
// variables). This is handy to abstract from this variable set.
std::set<storm::expressions::Variable> allNondeterminismVariables;
// As set of all variables used for encoding the synchronization.
std::set<storm::expressions::Variable> allSynchronizationMetaVariables;
// DDs representing the identity for each variable.
std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> variableToIdentityMap;
// A set of all meta variables that correspond to global variables.
std::set<storm::expressions::Variable> allGlobalVariables;
// DDs representing the identity for each module.
std::map<std::string, storm::dd::Add<Type, ValueType>> moduleToIdentityMap;
// DDs representing the valid ranges of the variables of each module.
std::map<std::string, storm::dd::Add<Type, ValueType>> moduleToRangeMap;
private:
/*!
* Creates the required meta variables and variable/module identities.
*/
void createMetaVariablesAndIdentities() {
// Add synchronization variables.
for (auto const& actionIndex : program.getSynchronizingActionIndices()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(program.getActionName(actionIndex));
synchronizationMetaVariables.push_back(variablePair.first);
allSynchronizationMetaVariables.insert(variablePair.first);
allNondeterminismVariables.insert(variablePair.first);
}
// DDs representing the valid ranges of the variables of each module.
std::map<std::string, storm::dd::Add<Type, ValueType>> moduleToRangeMap;
// 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<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable("nondet" + std::to_string(i));
nondeterminismMetaVariables.push_back(variablePair.first);
allNondeterminismVariables.insert(variablePair.first);
}
private:
/*!
* Creates the required meta variables and variable/module identities.
*/
void createMetaVariablesAndIdentities() {
// Add synchronization variables.
for (auto const& actionIndex : program.getSynchronizingActionIndices()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(program.getActionName(actionIndex));
synchronizationMetaVariables.push_back(variablePair.first);
allSynchronizationMetaVariables.insert(variablePair.first);
allNondeterminismVariables.insert(variablePair.first);
}
// Create meta variables for global program variables.
for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) {
int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt();
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(integerVariable.getName(), low, high);
// 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<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable("nondet" + std::to_string(i));
nondeterminismMetaVariables.push_back(variablePair.first);
allNondeterminismVariables.insert(variablePair.first);
}
STORM_LOG_TRACE("Created meta variables for global 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::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * manager->getRange(variablePair.first).template toAdd<ValueType>() * manager->getRange(variablePair.second).template toAdd<ValueType>();
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
rowColumnMetaVariablePairs.push_back(variablePair);
allGlobalVariables.insert(integerVariable.getExpressionVariable());
}
for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(booleanVariable.getName());
STORM_LOG_TRACE("Created meta variables for global 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);
// Create meta variables for global program variables.
for (storm::prism::IntegerVariable const& integerVariable : program.getGlobalIntegerVariables()) {
storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>();
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
rowColumnMetaVariablePairs.push_back(variablePair);
allGlobalVariables.insert(booleanVariable.getExpressionVariable());
}
// Create meta variables for each of the modules' variables.
for (storm::prism::Module const& module : program.getModules()) {
storm::dd::Bdd<Type> moduleIdentity = manager->getBddOne();
storm::dd::Bdd<Type> moduleRange = manager->getBddOne();
for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) {
int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt();
std::pair<storm::expressions::Variable, storm::expressions::Variable> 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() << "]");
STORM_LOG_TRACE("Created meta variables for global 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::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>() * manager->getRange(variablePair.first).template toAdd<ValueType>() * manager->getRange(variablePair.second).template toAdd<ValueType>();
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity);
rowColumnMetaVariablePairs.push_back(variablePair);
storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
moduleIdentity &= variableIdentity;
moduleRange &= manager->getRange(variablePair.first);
allGlobalVariables.insert(integerVariable.getExpressionVariable());
rowColumnMetaVariablePairs.push_back(variablePair);
}
for (storm::prism::BooleanVariable const& booleanVariable : program.getGlobalBooleanVariables()) {
for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = manager->addMetaVariable(booleanVariable.getName());
STORM_LOG_TRACE("Created meta variables for global boolean variable: " << variablePair.first.getName() << "[" << variablePair.first.getIndex() << "] and " << variablePair.second.getName() << "[" << variablePair.second.getIndex() << "]");
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);
@ -135,60 +179,251 @@ namespace storm {
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Add<Type, ValueType> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)).template toAdd<ValueType>();
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity);
storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
moduleIdentity &= variableIdentity;
moduleRange &= manager->getRange(variablePair.first);
rowColumnMetaVariablePairs.push_back(variablePair);
allGlobalVariables.insert(booleanVariable.getExpressionVariable());
}
moduleToIdentityMap[module.getName()] = moduleIdentity.template toAdd<ValueType>();
moduleToRangeMap[module.getName()] = moduleRange.template toAdd<ValueType>();
}
}
};
template <storm::dd::DdType Type, typename ValueType>
class ModuleComposer : public storm::prism::CompositionVisitor {
public:
ModuleComposer(typename DdPrismModelBuilder<Type, ValueType>::GenerationInformation& generationInfo) : generationInfo(generationInfo) {
for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) {
synchronizingActionToOffsetMap[actionIndex] = 0;
}
}
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram compose(storm::prism::Composition const& composition) {
std::cout << "composing the system " << composition << std::endl;
return boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.accept(*this));
}
virtual boost::any visit(storm::prism::ModuleComposition const& composition) override {
STORM_LOG_TRACE("Translating module '" << composition.getModuleName() << "'.");
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram result = DdPrismModelBuilder<Type, ValueType>::createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(composition.getModuleName()), synchronizingActionToOffsetMap);
// Update the offset indices.
for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) {
if (result.hasSynchronizingAction(actionIndex)) {
synchronizingActionToOffsetMap[actionIndex] = result.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables;
}
}
return result;
}
virtual boost::any visit(storm::prism::RenamingComposition const& composition) override {
// First, we translate the subcomposition.
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram sub = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this));
// Create the mapping from action indices to action indices.
std::map<uint_fast64_t, uint_fast64_t> renaming;
for (auto const& namePair : composition.getActionRenaming()) {
STORM_LOG_THROW(generationInfo.program.hasAction(namePair.first), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << namePair.first << "'.");
STORM_LOG_THROW(generationInfo.program.hasAction(namePair.second), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << namePair.second << "'.");
renaming.emplace(generationInfo.program.getActionIndex(namePair.first), generationInfo.program.getActionIndex(namePair.second));
}
// Perform the renaming and return result.
return rename(sub, renaming);
}
virtual boost::any visit(storm::prism::HidingComposition const& composition) override {
// First, we translate the subcomposition.
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram sub = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getSubcomposition().accept(*this));
// Create the mapping from action indices to action indices.
std::set<uint_fast64_t> actionIndicesToHide;
for (auto const& action : composition.getActionsToHide()) {
STORM_LOG_THROW(generationInfo.program.hasAction(action), storm::exceptions::InvalidArgumentException, "Composition refers to unknown action '" << action << "'.");
actionIndicesToHide.insert(generationInfo.program.getActionIndex(action));
}
// Perform the hiding and return result.
return hide(sub, actionIndicesToHide);
}
virtual boost::any visit(storm::prism::SynchronizingParallelComposition const& composition) override {
// First, we translate the subcompositions.
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this));
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this));
// Then, determine the action indices on which we need to synchronize.
std::set<uint_fast64_t> leftSynchronizationActionIndices = left.getSynchronizingActionIndices();
std::set<uint_fast64_t> rightSynchronizationActionIndices = right.getSynchronizingActionIndices();
std::set<uint_fast64_t> synchronizationActionIndices;
std::set_intersection(leftSynchronizationActionIndices.begin(), leftSynchronizationActionIndices.end(), rightSynchronizationActionIndices.begin(), rightSynchronizationActionIndices.end(), std::inserter(synchronizationActionIndices, synchronizationActionIndices.begin()));
// Finally, we compose the subcompositions to create the result.
composeInParallel(left, right, synchronizationActionIndices);
return left;
}
virtual boost::any visit(storm::prism::InterleavingParallelComposition const& composition) override {
// First, we translate the subcompositions.
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this));
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this));
// Finally, we compose the subcompositions to create the result.
composeInParallel(left, right, std::set<uint_fast64_t>());
return left;
}
virtual boost::any visit(storm::prism::RestrictedParallelComposition const& composition) override {
// First, we translate the subcompositions.
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram left = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getLeftSubcomposition().accept(*this));
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram right = boost::any_cast<typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram>(composition.getRightSubcomposition().accept(*this));
// Construct the synchronizing action indices from the synchronizing action names.
std::set<uint_fast64_t> synchronizingActionIndices;
for (auto const& action : composition.getSynchronizingActions()) {
synchronizingActionIndices.insert(generationInfo.program.getActionIndex(action));
}
std::set<uint_fast64_t> leftSynchronizationActionIndices = left.getSynchronizingActionIndices();
bool isContainedInLeft = std::includes(leftSynchronizationActionIndices.begin(), leftSynchronizationActionIndices.end(), synchronizingActionIndices.begin(), synchronizingActionIndices.end());
STORM_LOG_WARN_COND(isContainedInLeft, "Left subcomposition of composition '" << composition << "' does not include all actions over which to synchronize.");
std::set<uint_fast64_t> rightSynchronizationActionIndices = right.getSynchronizingActionIndices();
bool isContainedInRight = std::includes(rightSynchronizationActionIndices.begin(), rightSynchronizationActionIndices.end(), synchronizingActionIndices.begin(), synchronizingActionIndices.end());
STORM_LOG_WARN_COND(isContainedInRight, "Right subcomposition of composition '" << composition << "' does not include all actions over which to synchronize.");
// Finally, we compose the subcompositions to create the result.
composeInParallel(left, right, synchronizingActionIndices);
return left;
}
private:
/*!
* Hides the actions of the given module according to the given set. As a result, the module is modified in
* place.
*/
void hide(typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram& sub, std::set<uint_fast64_t> const& actionIndicesToHide) const {
STORM_LOG_TRACE("Hiding the actions " << boost::join(actionIndicesToHide, ", ") << ".");
// Create meta variables for each of the modules' variables.
for (storm::prism::Module const& module : program.getModules()) {
storm::dd::Bdd<Type> moduleIdentity = manager->getBddOne();
storm::dd::Bdd<Type> moduleRange = manager->getBddOne();
for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) {
if (actionIndicesToHide.find(action) != actionIndicesToHide.end()) {
for (storm::prism::IntegerVariable const& integerVariable : module.getIntegerVariables()) {
int_fast64_t low = integerVariable.getLowerBoundExpression().evaluateAsInt();
int_fast64_t high = integerVariable.getUpperBoundExpression().evaluateAsInt();
std::pair<storm::expressions::Variable, storm::expressions::Variable> 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::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
variableToIdentityMap.emplace(integerVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
moduleIdentity &= variableIdentity;
moduleRange &= manager->getRange(variablePair.first);
rowColumnMetaVariablePairs.push_back(variablePair);
}
}
}
/*!
* Renames the actions of the given module according to the given renaming.
*/
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram rename(typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram& sub, std::map<uint_fast64_t, uint_fast64_t> const& renaming) const {
STORM_LOG_TRACE("Renaming actions.");
uint_fast64_t numberOfUsedNondeterminismVariables = sub.numberOfUsedNondeterminismVariables;
std::map<uint_fast64_t, typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram> actionIndexToDdMap;
// Go through all action DDs with a synchronizing label and rename them if they appear in the renaming.
for (auto const& action : sub.synchronizingActionToDecisionDiagramMap) {
auto renamingIt = renaming.find(action.first);
if (renamingIt != renaming.end()) {
// If the action is to be renamed and an action with the target index already exists, we need
// to combine the action DDs.
auto itNewActions = actionIndexToDdMap.find(renamingIt.second);
if (itNewActions != actionIndexToDdMap.end()) {
actionIndexToDdMap[renamingIt.second] = DdPrismModelBuilder<Type, ValueType>::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second);
} else {
// In this case, we can simply copy the action over.
actionIndexToDdMap[renamingIt.second] = action.second;
}
for (storm::prism::BooleanVariable const& booleanVariable : module.getBooleanVariables()) {
std::pair<storm::expressions::Variable, storm::expressions::Variable> 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() << "]");
} else {
// If the action is not to be renamed, we need to copy it over. However, if some other action
// was renamed to the very same action name before, we need to combine the transitions.
auto itNewActions = actionIndexToDdMap.find(action.first);
if (itNewActions != actionIndexToDdMap.end()) {
actionIndexToDdMap[action.first] = DdPrismModelBuilder<Type, ValueType>::combineUnsynchronizedActions(generationInfo, action.second, itNewActions->second);
} else {
// In this case, we can simply copy the action over.
actionIndexToDdMap[action.first] = action.second;
}
}
}
return ModuleDecisionDiagram(sub.independentAction, actionIndexToDdMap, sub.identity, numberOfUsedNondeterminismVariables);
}
/*!
* Composes the given modules while synchronizing over the provided action indices. As a result, the first
* module is modified in place and will contain the composition after a call to this method.
*/
void composeInParallel(typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram& left, typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram& right, std::set<uint_fast64_t> const& synchronizationActionIndices) const {
STORM_LOG_TRACE("Composing two modules over the actions " << boost::join(synchronizationActionIndices, ", ") << ".");
// Combine the tau action.
uint_fast64_t numberOfUsedNondeterminismVariables = right.independentAction.numberOfUsedNondeterminismVariables;
left.independentAction = DdPrismModelBuilder<Type, ValueType>::combineUnsynchronizedActions(generationInfo, left.independentAction, right.independentAction, left.identity, right.identity);
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, left.independentAction.numberOfUsedNondeterminismVariables);
rowMetaVariables.insert(variablePair.first);
variableToRowMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.first);
columnMetaVariables.insert(variablePair.second);
variableToColumnMetaVariableMap.emplace(booleanVariable.getExpressionVariable(), variablePair.second);
storm::dd::Bdd<Type> variableIdentity = manager->template getIdentity<ValueType>(variablePair.first).equals(manager->template getIdentity<ValueType>(variablePair.second)) && manager->getRange(variablePair.first) && manager->getRange(variablePair.second);
variableToIdentityMap.emplace(booleanVariable.getExpressionVariable(), variableIdentity.template toAdd<ValueType>());
moduleIdentity &= variableIdentity;
moduleRange &= manager->getRange(variablePair.first);
// Create an empty action for the case where one of the modules does not have a certain action.
typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram emptyAction(*generationInfo.manager);
rowColumnMetaVariablePairs.push_back(variablePair);
// Treat all non-tau actions of the left module.
for (auto& action : left.synchronizingActionToDecisionDiagramMap) {
// If we need to synchronize over this action index, we try to do so now.
if (synchronizationActionIndices.find(action.first) != synchronizationActionIndices.end()) {
// If we are to synchronize over an action that does not exist in the second module, the result
// is that the synchronization is the empty action.
if (!right.hasSynchronizingAction(action.first)) {
action.second = emptyAction;
} else {
// Otherwise, the actions of the modules are synchronized.
action.second = DdPrismModelBuilder<Type, ValueType>::combineSynchronizingActions(generationInfo, action.second, right.synchronizingActionToDecisionDiagramMap[action.first]);
}
} else {
// If we don't synchronize over this action, we need to construct the interleaving.
// If both modules contain the action, we need to mutually multiply the other identity.
if (right.hasSynchronizingAction(action.first)) {
action.second = DdPrismModelBuilder<Type, ValueType>::combineUnsynchronizedActions(generationInfo, action.second, right.synchronizingActionToDecisionDiagramMap[action.first], left.identity, right.identity);
} else {
// If only the first module has this action, we need to use a dummy action decision diagram
// for the second module.
action.second = DdPrismModelBuilder<Type, ValueType>::combineUnsynchronizedActions(generationInfo, action.second, emptyAction, left.identity, right.identity);
}
}
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, action.second.numberOfUsedNondeterminismVariables);
}
// Treat all non-tau actions of the right module.
for (auto const& actionIndex : right.getSynchronizingActionIndices()) {
// Here, we only need to treat actions that the first module does not have, because we have handled
// this case earlier.
if (!left.hasSynchronizingAction(actionIndex)) {
if (synchronizationActionIndices.find(actionIndex) != synchronizationActionIndices.end()) {
// If we are to synchronize over this action that does not exist in the first module, the
// result is that the synchronization is the empty action.
left.synchronizingActionToDecisionDiagramMap[actionIndex] = emptyAction;
} else {
// If only the second module has this action, we need to use a dummy action decision diagram
// for the first module.
left.synchronizingActionToDecisionDiagramMap[actionIndex] = DdPrismModelBuilder<Type, ValueType>::combineUnsynchronizedActions(generationInfo, emptyAction, right.synchronizingActionToDecisionDiagramMap[actionIndex], left.identity, right.identity);
}
moduleToIdentityMap[module.getName()] = moduleIdentity.template toAdd<ValueType>();
moduleToRangeMap[module.getName()] = moduleRange.template toAdd<ValueType>();
}
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, left.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables);
}
};
// Combine identity matrices.
left.identity = left.identity * right.identity;
// Keep track of the number of nondeterminism variables used.
left.numberOfUsedNondeterminismVariables = std::max(left.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables);
}
typename DdPrismModelBuilder<Type, ValueType>::GenerationInformation& generationInfo;
std::map<uint_fast64_t, uint_fast64_t> synchronizingActionToOffsetMap;
};
template <storm::dd::DdType Type, typename ValueType>
DdPrismModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), terminalStates(), negatedTerminalStates() {
// Intentionally left empty.
@ -224,7 +459,7 @@ namespace storm {
if (negatedTerminalStates) {
negatedTerminalStates.reset();
}
// If we are not required to build all reward models, we determine the reward models we need to build.
if (!buildAllRewardModels) {
std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels();
@ -369,7 +604,7 @@ namespace storm {
STORM_LOG_WARN_COND(!updateResults.back().updateDd.isZero(), "Update '" << update << "' does not have any effect.");
}
// Start by gathering all variables that were written in at least one update.
std::set<storm::expressions::Variable> globalVariablesInSomeUpdate;
@ -386,7 +621,7 @@ namespace storm {
for (auto& updateResult : updateResults) {
std::set<storm::expressions::Variable> missingIdentities;
std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), updateResult.assignedGlobalVariables.begin(), updateResult.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
for (auto const& variable : missingIdentities) {
STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << "[" << variable.getIndex() << "] to update.");
updateResult.updateDd *= generationInfo.variableToIdentityMap.at(variable);
@ -448,7 +683,7 @@ namespace storm {
// Start by gathering all variables that were written in at least one action DD.
std::set<storm::expressions::Variable> globalVariablesInActionDd;
std::set_union(action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), action2.assignedGlobalVariables.begin(), action2.assignedGlobalVariables.end(), std::inserter(globalVariablesInActionDd, globalVariablesInActionDd.begin()));
std::set<storm::expressions::Variable> missingIdentitiesInAction1;
std::set_difference(globalVariablesInActionDd.begin(), globalVariablesInActionDd.end(), action1.assignedGlobalVariables.begin(), action1.assignedGlobalVariables.end(), std::inserter(missingIdentitiesInAction1, missingIdentitiesInAction1.begin()));
for (auto const& variable : missingIdentitiesInAction1) {
@ -460,7 +695,7 @@ namespace storm {
for (auto const& variable : missingIdentitiesInAction2) {
action2.transitionsDd *= generationInfo.variableToIdentityMap.at(variable);
}
return globalVariablesInActionDd;
}
@ -473,7 +708,7 @@ namespace storm {
}
STORM_LOG_TRACE("Equalizing assigned global variables.");
// Then multiply the transitions of each action with the missing identities.
for (auto& actionDd : actionDds) {
STORM_LOG_TRACE("Equalizing next action.");
@ -545,7 +780,7 @@ namespace storm {
allGuards |= commandDd.guardDd.toBdd();
}
uint_fast64_t maxChoices = static_cast<uint_fast64_t>(sumOfGuards.getMax());
STORM_LOG_TRACE("Found " << maxChoices << " local choices.");
// Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism.
@ -626,7 +861,7 @@ namespace storm {
return ActionDecisionDiagram(allGuards.template toAdd<ValueType>(), allCommands, assignedGlobalVariables, nondeterminismVariableOffset + numberOfBinaryVariables);
}
}
template <storm::dd::DdType Type, typename ValueType>
typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram DdPrismModelBuilder<Type, ValueType>::combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2) {
std::set<storm::expressions::Variable> assignedGlobalVariables;
@ -636,21 +871,30 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram DdPrismModelBuilder<Type, ValueType>::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2, storm::dd::Add<Type, ValueType> const& identityDd1, storm::dd::Add<Type, ValueType> const& identityDd2) {
storm::dd::Add<Type, ValueType> action1Extended = action1.transitionsDd * identityDd2;
storm::dd::Add<Type, ValueType> action2Extended = action2.transitionsDd * identityDd1;
// First extend the action DDs by the other identities.
STORM_LOG_TRACE("Multiplying identities to combine unsynchronized actions.");
action1.transitionsDd = action1.transitionsDd * identityDd2;
action2.transitionsDd = action2.transitionsDd * identityDd1;
// Then combine the extended action DDs.
return combineUnsynchronizedActions(generationInfo, action1, action2);
}
template <storm::dd::DdType Type, typename ValueType>
typename DdPrismModelBuilder<Type, ValueType>::ActionDecisionDiagram DdPrismModelBuilder<Type, ValueType>::combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2) {
STORM_LOG_TRACE("Combining unsynchronized actions.");
// Make both action DDs write to the same global variables.
std::set<storm::expressions::Variable> assignedGlobalVariables = equalizeAssignedGlobalVariables(generationInfo, action1, action2);
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1Extended + action2Extended, assignedGlobalVariables, 0);
return ActionDecisionDiagram(action1.guardDd + action2.guardDd, action1.transitionsDd + action2.transitionsDd, assignedGlobalVariables, 0);
} else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::MDP) {
if (action1.transitionsDd.isZero()) {
return ActionDecisionDiagram(action2.guardDd, action2Extended, assignedGlobalVariables, action2.numberOfUsedNondeterminismVariables);
return ActionDecisionDiagram(action2.guardDd, action2.transitionsDd, assignedGlobalVariables, action2.numberOfUsedNondeterminismVariables);
} else if (action2.transitionsDd.isZero()) {
return ActionDecisionDiagram(action1.guardDd, action1Extended, assignedGlobalVariables, action1.numberOfUsedNondeterminismVariables);
return ActionDecisionDiagram(action1.guardDd, action1.transitionsDd, assignedGlobalVariables, action1.numberOfUsedNondeterminismVariables);
}
// Bring both choices to the same number of variables that encode the nondeterminism.
@ -661,25 +905,25 @@ namespace storm {
for (uint_fast64_t i = action2.numberOfUsedNondeterminismVariables; i < action1.numberOfUsedNondeterminismVariables; ++i) {
nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd<ValueType>();
}
action2Extended *= nondeterminismEncoding;
action2.transitionsDd *= nondeterminismEncoding;
} else if (action2.numberOfUsedNondeterminismVariables > action1.numberOfUsedNondeterminismVariables) {
storm::dd::Add<Type, ValueType> nondeterminismEncoding = generationInfo.manager->template getAddOne<ValueType>();
for (uint_fast64_t i = action1.numberOfUsedNondeterminismVariables; i < action2.numberOfUsedNondeterminismVariables; ++i) {
nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd<ValueType>();
}
action1Extended *= nondeterminismEncoding;
action1.transitionsDd *= nondeterminismEncoding;
}
// Add a new variable that resolves the nondeterminism between the two choices.
storm::dd::Add<Type, ValueType> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2Extended, action1Extended);
storm::dd::Add<Type, ValueType> combinedTransitions = generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[numberOfUsedNondeterminismVariables], 1).ite(action2.transitionsDd, action1.transitionsDd);
return ActionDecisionDiagram((action1.guardDd.toBdd() || action2.guardDd.toBdd()).template toAdd<ValueType>(), combinedTransitions, assignedGlobalVariables, numberOfUsedNondeterminismVariables + 1);
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "Illegal model type.");
}
}
template <storm::dd::DdType Type, typename ValueType>
typename DdPrismModelBuilder<Type, ValueType>::ModuleDecisionDiagram DdPrismModelBuilder<Type, ValueType>::createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap) {
// Start by creating the action DD for the independent action.
@ -726,7 +970,7 @@ namespace storm {
// First, determine the highest number of nondeterminism variables that is used in any action and make
// all actions use the same amout of nondeterminism variables.
uint_fast64_t numberOfUsedNondeterminismVariables = module.numberOfUsedNondeterminismVariables;
// Compute missing global variable identities in independent action.
std::set<storm::expressions::Variable> missingIdentities;
std::set_difference(generationInfo.allGlobalVariables.begin(), generationInfo.allGlobalVariables.end(), module.independentAction.assignedGlobalVariables.begin(), module.independentAction.assignedGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
@ -742,7 +986,7 @@ namespace storm {
nondeterminismEncoding *= generationInfo.manager->getEncoding(generationInfo.nondeterminismMetaVariables[i], 0).template toAdd<ValueType>();
}
result = identityEncoding * module.independentAction.transitionsDd * nondeterminismEncoding;
// Add variables to synchronized action DDs.
std::map<uint_fast64_t, storm::dd::Add<Type, ValueType>> synchronizingActionToDdMap;
for (auto const& synchronizingAction : module.synchronizingActionToDecisionDiagramMap) {
@ -773,7 +1017,7 @@ namespace storm {
for (auto const& synchronizingAction : synchronizingActionToDdMap) {
result += synchronizingAction.second;
}
return result;
} else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
// Simply add all actions.
@ -789,67 +1033,14 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
typename DdPrismModelBuilder<Type, ValueType>::SystemResult DdPrismModelBuilder<Type, ValueType>::createSystemDecisionDiagram(GenerationInformation& generationInfo) {
// Create the initial offset mapping.
std::map<uint_fast64_t, uint_fast64_t> synchronizingActionToOffsetMap;
for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) {
synchronizingActionToOffsetMap[actionIndex] = 0;
}
// Start by creating DDs for the first module.
STORM_LOG_TRACE("Translating (first) module '" << generationInfo.program.getModule(0).getName() << "'.");
ModuleDecisionDiagram system = createModuleDecisionDiagram(generationInfo, generationInfo.program.getModule(0), synchronizingActionToOffsetMap);
// Now 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);
STORM_LOG_TRACE("Translating module '" << currentModule.getName() << "'.");
// Update the offset index.
for (auto const& actionIndex : generationInfo.program.getSynchronizingActionIndices()) {
if (system.hasSynchronizingAction(actionIndex)) {
synchronizingActionToOffsetMap[actionIndex] = system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables;
}
}
ModuleDecisionDiagram currentModuleDd = createModuleDecisionDiagram(generationInfo, currentModule, synchronizingActionToOffsetMap);
// Combine the non-synchronizing action.
uint_fast64_t numberOfUsedNondeterminismVariables = currentModuleDd.numberOfUsedNondeterminismVariables;
system.independentAction = combineUnsynchronizedActions(generationInfo, system.independentAction, currentModuleDd.independentAction, system.identity, currentModuleDd.identity);
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.independentAction.numberOfUsedNondeterminismVariables);
ActionDecisionDiagram emptyAction(*generationInfo.manager);
// For all synchronizing actions that the next module does not have, we need to multiply the identity of the next module.
for (auto& action : system.synchronizingActionToDecisionDiagramMap) {
if (!currentModuleDd.hasSynchronizingAction(action.first)) {
action.second = combineUnsynchronizedActions(generationInfo, action.second, emptyAction, system.identity, currentModuleDd.identity);
}
}
// Combine synchronizing actions.
for (auto const& actionIndex : currentModule.getSynchronizingActionIndices()) {
if (system.hasSynchronizingAction(actionIndex)) {
system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineSynchronizingActions(generationInfo, system.synchronizingActionToDecisionDiagramMap[actionIndex], currentModuleDd.synchronizingActionToDecisionDiagramMap[actionIndex]);
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables);
} else {
system.synchronizingActionToDecisionDiagramMap[actionIndex] = combineUnsynchronizedActions(generationInfo, emptyAction, currentModuleDd.synchronizingActionToDecisionDiagramMap[actionIndex], system.identity, currentModuleDd.identity);
numberOfUsedNondeterminismVariables = std::max(numberOfUsedNondeterminismVariables, system.synchronizingActionToDecisionDiagramMap[actionIndex].numberOfUsedNondeterminismVariables);
}
}
// Combine identity matrices.
system.identity = system.identity * currentModuleDd.identity;
// Keep track of the number of nondeterminism variables used.
system.numberOfUsedNondeterminismVariables = std::max(system.numberOfUsedNondeterminismVariables, numberOfUsedNondeterminismVariables);
}
ModuleComposer<Type, ValueType> composer(generationInfo);
ModuleDecisionDiagram system = composer.compose(generationInfo.program.specifiesSystemComposition() ? generationInfo.program.getSystemCompositionConstruct().getSystemComposition() : *generationInfo.program.getDefaultSystemComposition());
storm::dd::Add<Type, ValueType> result = createSystemFromModule(generationInfo, system);
// Create an auxiliary DD that is used later during the construction of reward models.
storm::dd::Add<Type, ValueType> stateActionDd = result.sumAbstract(generationInfo.columnMetaVariables);
// For DTMCs, we normalize each row to 1 (to account for non-determinism).
if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC) {
result = result / stateActionDd;
@ -892,7 +1083,7 @@ namespace storm {
// Next, build the state-action reward vector.
boost::optional<storm::dd::Add<Type, ValueType>> stateActionRewards;
if (rewardModel.hasStateActionRewards()) {
stateActionRewards = generationInfo.manager->template getAddZero<ValueType>();
stateActionRewards = generationInfo.manager->template getAddZero<ValueType>();
for (auto const& stateActionReward : rewardModel.getStateActionRewards()) {
storm::dd::Add<Type, ValueType> states = generationInfo.rowExpressionAdapter->translateExpression(stateActionReward.getStatePredicateExpression());
@ -980,7 +1171,7 @@ namespace storm {
return storm::models::symbolic::StandardRewardModel<Type, double>(stateRewards, stateActionRewards, transitionRewards);
}
template <storm::dd::DdType Type, typename ValueType>
storm::prism::Program const& DdPrismModelBuilder<Type, ValueType>::getTranslatedProgram() const {
return preparedProgram.get();
@ -1017,7 +1208,7 @@ 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);
SystemResult system = createSystemDecisionDiagram(generationInfo);
storm::dd::Add<Type, ValueType> transitionMatrix = system.allTransitionsDd;
@ -1037,7 +1228,7 @@ namespace storm {
std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
terminalExpression = preparedProgram->getLabelExpression(labelName);
}
// If the expression refers to constants of the model, we need to substitute them.
terminalExpression = terminalExpression.substitute(constantsSubstitution);
@ -1078,7 +1269,7 @@ namespace storm {
// Detect deadlocks and 1) fix them if requested 2) throw an error otherwise.
storm::dd::Bdd<Type> statesWithTransition = transitionMatrixBdd.existsAbstract(generationInfo.columnMetaVariables);
storm::dd::Add<Type, ValueType> deadlockStates = (reachableStates && !statesWithTransition).template toAdd<ValueType>();
if (!deadlockStates.isZero()) {
// If we need to fix deadlocks, we do so now.
if (!storm::settings::getModule<storm::settings::modules::MarkovChainSettings>().isDontFixDeadlocksSet()) {
@ -1088,7 +1279,7 @@ namespace storm {
for (auto it = deadlockStates.begin(), ite = deadlockStates.end(); it != ite && count < 3; ++it, ++count) {
STORM_LOG_INFO((*it).first.toPrettyString(generationInfo.rowMetaVariables) << std::endl);
}
if (program.getModelType() == storm::prism::Program::ModelType::DTMC) {
// For DTMCs, we can simply add the identity of the global module for all deadlock states.
transitionMatrix += deadlockStates * globalModule.identity;
@ -1175,7 +1366,7 @@ namespace storm {
changed = false;
storm::dd::Bdd<Type> tmp = reachableStates.relationalProduct(transitionBdd, generationInfo.rowMetaVariables, generationInfo.columnMetaVariables);
storm::dd::Bdd<Type> newReachableStates = tmp && (!reachableStates);
// Check whether new states were indeed discovered.
if (!newReachableStates.isZero()) {
changed = true;
@ -1192,7 +1383,7 @@ namespace storm {
// Explicitly instantiate the symbolic model builder.
template class DdPrismModelBuilder<storm::dd::DdType::CUDD>;
template class DdPrismModelBuilder<storm::dd::DdType::Sylvan>;
} // namespace adapters
} // namespace storm

14
src/builder/DdPrismModelBuilder.h
View File

@ -188,6 +188,14 @@ namespace storm {
return synchronizingActionToDecisionDiagramMap.find(actionIndex) != synchronizingActionToDecisionDiagramMap.end();
}
std::set<uint_fast64_t> getSynchronizingActionIndices() const {
std::set<uint_fast64_t> result;
for (auto const& entry : synchronizingActionToDecisionDiagramMap) {
result.insert(entry.first);
}
return result;
}
// The decision diagram for the independent action.
ActionDecisionDiagram independentAction;
@ -210,7 +218,11 @@ namespace storm {
* Structure to store the result of the system creation phase.
*/
struct SystemResult;
private:
template <storm::dd::DdType TypePrime, typename ValueTypePrime>
friend class ModuleComposer;
static std::set<storm::expressions::Variable> equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2);
static std::set<storm::expressions::Variable> equalizeAssignedGlobalVariables(GenerationInformation const& generationInfo, std::vector<ActionDecisionDiagram>& actionDds);
@ -230,6 +242,8 @@ namespace storm {
static ActionDecisionDiagram combineSynchronizingActions(GenerationInformation const& generationInfo, ActionDecisionDiagram const& action1, ActionDecisionDiagram const& action2);
static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2, storm::dd::Add<Type, ValueType> const& identityDd1, storm::dd::Add<Type, ValueType> const& identityDd2);
static ActionDecisionDiagram combineUnsynchronizedActions(GenerationInformation const& generationInfo, ActionDecisionDiagram& action1, ActionDecisionDiagram& action2);
static ModuleDecisionDiagram createModuleDecisionDiagram(GenerationInformation& generationInfo, storm::prism::Module const& module, std::map<uint_fast64_t, uint_fast64_t> const& synchronizingActionToOffsetMap);

4
src/storage/prism/HidingComposition.cpp
View File

@ -17,6 +17,10 @@ namespace storm {
return *sub;
}
std::set<std::string> const& HidingComposition::getActionsToHide() const {
return actionsToHide;
}
void HidingComposition::writeToStream(std::ostream& stream) const {
stream << "(" << *sub << ")" << " " << "{" << boost::join(actionsToHide, ", ") << "}";
}

2
src/storage/prism/HidingComposition.h
View File

@ -16,6 +16,8 @@ namespace storm {
Composition const& getSubcomposition() const;
std::set<std::string> const& getActionsToHide() const;
protected:
virtual void writeToStream(std::ostream& stream) const override;

2
src/storage/prism/InterleavingParallelComposition.cpp
View File

@ -12,7 +12,7 @@ namespace storm {
}
void InterleavingParallelComposition::writeToStream(std::ostream& stream) const {
stream << "(" << *left << " ||| " << *right << ")";
stream << "(" << this->getLeftSubcomposition() << " ||| " << this->getRightSubcomposition() << ")";
}
}

4
src/storage/prism/InterleavingParallelComposition.h
View File

@ -13,10 +13,6 @@ namespace storm {
protected:
virtual void writeToStream(std::ostream& stream) const override;
private:
std::shared_ptr<Composition> left;
std::shared_ptr<Composition> right;
};
}
}

51
src/storage/prism/Program.cpp
View File

@ -27,11 +27,21 @@ namespace storm {
}
bool isValid(Composition const& composition) {
return boost::any_cast<bool>(composition.accept(*this));
bool isValid = boost::any_cast<bool>(composition.accept(*this));
if (appearingModules.size() != program.getNumberOfModules()) {
isValid = false;
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Not every module is used in the system composition.");
}
return isValid;
}
virtual boost::any visit(ModuleComposition const& composition) override {
return program.hasModule(composition.getModuleName());
bool isValid = program.hasModule(composition.getModuleName());
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "The module \"" << composition.getModuleName() << "\" referred to in the system composition does not exist.");
isValid = appearingModules.find(composition.getModuleName()) == appearingModules.end();
STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "The module \"" << composition.getModuleName() << "\" is referred to more than once in the system composition.");
appearingModules.insert(composition.getModuleName());
return isValid;
}
virtual boost::any visit(RenamingComposition const& composition) override {
@ -51,11 +61,20 @@ namespace storm {
}
virtual boost::any visit(RestrictedParallelComposition const& composition) override {
return boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this));
bool isValid = boost::any_cast<bool>(composition.getLeftSubcomposition().accept(*this)) && boost::any_cast<bool>(composition.getRightSubcomposition().accept(*this));
for (auto const& action : composition.getSynchronizingActions()) {
if (!program.hasAction(action)) {
STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "System composition refers to unknown action '" << action << "'.");
}
}
return isValid;
}
private:
storm::prism::Program const& program;
std::set<std::string> appearingModules;
};
Program::Program(std::shared_ptr<storm::expressions::ExpressionManager> manager, ModelType modelType, std::vector<Constant> const& constants, std::vector<BooleanVariable> const& globalBooleanVariables, std::vector<IntegerVariable> const& globalIntegerVariables, std::vector<Formula> const& formulas, std::vector<Module> const& modules, std::map<std::string, uint_fast64_t> const& actionToIndexMap, std::vector<RewardModel> const& rewardModels, std::vector<Label> const& labels, boost::optional<InitialConstruct> const& initialConstruct, boost::optional<SystemCompositionConstruct> const& compositionConstruct, std::string const& filename, uint_fast64_t lineNumber, bool finalModel)
@ -352,6 +371,18 @@ namespace storm {
return systemCompositionConstruct;
}
std::shared_ptr<Composition> Program::getDefaultSystemComposition() const {
std::shared_ptr<Composition> current = std::make_shared<ModuleComposition>(this->modules.front().getName());
for (uint_fast64_t index = 1; index < this->modules.size(); ++index) {
std::shared_ptr<Composition> newComposition = std::make_shared<SynchronizingParallelComposition>(current, std::make_shared<ModuleComposition>(this->modules[index].getName()));
current = newComposition;
}
return current;
}
std::set<std::string> const& Program::getActions() const {
return this->actions;
}
@ -366,6 +397,20 @@ namespace storm {
return indexNamePair->second;
}
uint_fast64_t Program::getActionIndex(std::string const& actionName) const {
auto const& nameIndexPair = this->actionToIndexMap.find(actionName);
STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::InvalidArgumentException, "Unknown action name '" << actionName << "'.");
return nameIndexPair->second;
}
bool Program::hasAction(std::string const& actionName) const {
return this->actionToIndexMap.find(actionName) != this->actionToIndexMap.end();
}
bool Program::hasAction(uint_fast64_t const& actionIndex) const {
return this->indexToActionMap.find(actionIndex) != this->indexToActionMap.end();
}
std::set<uint_fast64_t> const& Program::getModuleIndicesByAction(std::string const& action) const {
auto const& nameIndexPair = this->actionToIndexMap.find(action);
STORM_LOG_THROW(nameIndexPair != this->actionToIndexMap.end(), storm::exceptions::OutOfRangeException, "Action name '" << action << "' does not exist.");

29
src/storage/prism/Program.h
View File

@ -296,6 +296,13 @@ namespace storm {
*/
boost::optional<SystemCompositionConstruct> getOptionalSystemCompositionConstruct() const;
/*!
* Retrieves the default system composition for this program.
*
* @return The default system composition.
*/
std::shared_ptr<Composition> getDefaultSystemComposition() const;
/*!
* Retrieves the set of actions present in the program.
*
@ -318,6 +325,28 @@ namespace storm {
*/
std::string const& getActionName(uint_fast64_t actionIndex) const;
/*!
* Retrieves the index of the action with the given name.
*
* @param actionName The name of the action.
* @return The index of the action.
*/
uint_fast64_t getActionIndex(std::string const& actionName) const;
/*!
* Retrieves whether the program has an action with the given name.
*
* @return True iff the program has an action with the given name.
*/
bool hasAction(std::string const& actionName) const;
/*!
* Retrieves whether the program has an action with the given index.
*
* @return True iff the program has an action with the given index.
*/
bool hasAction(uint_fast64_t const& actionIndex) const;
/*!
* Retrieves the indices of all modules within this program that contain commands that are labelled with the
* given action.

4
src/storage/prism/RenamingComposition.cpp
View File

@ -19,6 +19,10 @@ namespace storm {
return *sub;
}
std::map<std::string, std::string> const& RenamingComposition::getActionRenaming() const {
return actionRenaming;
}
void RenamingComposition::writeToStream(std::ostream& stream) const {
std::vector<std::string> renamings;
for (auto const& renaming : actionRenaming) {

2
src/storage/prism/RenamingComposition.h
View File

@ -17,6 +17,8 @@ namespace storm {
Composition const& getSubcomposition() const;
std::map<std::string, std::string> const& getActionRenaming() const;
protected:
virtual void writeToStream(std::ostream& stream) const override;

6
src/storage/prism/RestrictedParallelComposition.cpp
View File

@ -12,9 +12,13 @@ namespace storm {
boost::any RestrictedParallelComposition::accept(CompositionVisitor& visitor) const {
return visitor.visit(*this);
}
std::set<std::string> const& RestrictedParallelComposition::getSynchronizingActions() const {
return synchronizingActions;
}
void RestrictedParallelComposition::writeToStream(std::ostream& stream) const {
stream << "(" << *left << " |[" << boost::algorithm::join(synchronizingActions, ", ") << "]| " << *right << ")";
stream << "(" << this->getLeftSubcomposition() << " |[" << boost::algorithm::join(synchronizingActions, ", ") << "]| " << this->getRightSubcomposition() << ")";
}
}

4
src/storage/prism/RestrictedParallelComposition.h
View File

@ -14,13 +14,13 @@ namespace storm {
virtual boost::any accept(CompositionVisitor& visitor) const override;
std::set<std::string> const& getSynchronizingActions() const;
protected:
virtual void writeToStream(std::ostream& stream) const override;
private:
std::shared_ptr<Composition> left;
std::set<std::string> synchronizingActions;
std::shared_ptr<Composition> right;
};
}
}

2
src/storage/prism/SynchronizingParallelComposition.cpp
View File

@ -12,7 +12,7 @@ namespace storm {
}
void SynchronizingParallelComposition::writeToStream(std::ostream& stream) const {
stream << "(" << *left << " || " << *right << ")";
stream << "(" << this->getLeftSubcomposition() << " || " << this->getRightSubcomposition() << ")";
}
}

4
src/storage/prism/SynchronizingParallelComposition.h
View File

@ -13,10 +13,6 @@ namespace storm {
protected:
virtual void writeToStream(std::ostream& stream) const override;
private:
std::shared_ptr<Composition> left;
std::shared_ptr<Composition> right;
};
}
}

Write Preview
Loading…
Cancel
Save