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

adapted JANI parallel composition class to synchronization vector usage 

Former-commit-id: 71322c70f0 [formerly ec71a5adc5]
Former-commit-id: ccdb40b1f3
tempestpy_adaptions
dehnert 8 years ago
parent
24e89ecce6
commit
f616bf606b
10 changed files with 736 additions and 492 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. 921
      src/builder/DdJaniModelBuilder.cpp
  2. 8
      src/storage/jani/Automaton.cpp
  3. 5
      src/storage/jani/Automaton.h
  4. 77
      src/storage/jani/CompositionInformationVisitor.cpp
  5. 10
      src/storage/jani/CompositionInformationVisitor.h
  6. 6
      src/storage/jani/Model.cpp
  7. 5
      src/storage/jani/Model.h
  8. 116
      src/storage/jani/ParallelComposition.cpp
  9. 78
      src/storage/jani/ParallelComposition.h
  10. 2
      src/storage/prism/ToJaniConverter.cpp

921
src/builder/DdJaniModelBuilder.cpp
View File

@ -172,14 +172,15 @@ namespace storm {
template <storm::dd::DdType Type, typename ValueType>
class CompositionVariableCreator : public storm::jani::CompositionVisitor {
public:
CompositionVariableCreator(storm::jani::Model const& model) : model(model) {
CompositionVariableCreator(storm::jani::Model const& model) : model(model), automata() {
// Intentionally left empty.
}
CompositionVariables<Type, ValueType> create() {
// First, check whether every automaton appears exactly once in the system composition.
// First, check whether every automaton appears exactly once in the system composition. Simultaneously,
// we determine the set of non-silent actions used by the composition.
automata.clear();
this->model.getSystemComposition().accept(*this, boost::none);
nonSilentActions = boost::any_cast<std::set<std::string>>(this->model.getSystemComposition().accept(*this, boost::none));
STORM_LOG_THROW(automata.size() == this->model.getNumberOfAutomata(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition refers to a subset of automata.");
// Then, check that the model does not contain unbounded integer or non-transient real variables.
@ -193,25 +194,64 @@ namespace storm {
}
// Based on this assumption, we create the variables.
return createVariables();
return createVariables(nonSilentActions);
}
boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
auto it = automata.find(composition.getAutomatonName());
STORM_LOG_THROW(it == automata.end(), storm::exceptions::InvalidArgumentException, "Cannot build symbolic model from JANI model whose system composition that refers to the automaton '" << composition.getAutomatonName() << "' multiple times.");
automata.insert(it, composition.getAutomatonName());
return boost::none;
// Compute the set of actions used by this automaton.
std::set<uint64_t> actionIndices = model.getAutomaton(composition.getAutomatonName()).getUsedActionIndices();
std::set<std::string> result;
for (auto const& index : actionIndices) {
result.insert(this->model.getAction(index).getName());
}
return result;
}
boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
composition.getSubcomposition().accept(*this, boost::none);
return boost::none;
std::set<std::string> usedActions = boost::any_cast<std::set<std::string>>(composition.getSubcomposition().accept(*this, boost::none));
std::set<std::string> newUsedActions;
for (auto const& action : usedActions) {
auto it = composition.getRenaming().find(action);
if (it != composition.getRenaming().end()) {
if (it->second) {
newUsedActions.insert(it->second.get());
}
} else {
newUsedActions.insert(action);
}
}
return newUsedActions;
}
boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
composition.getLeftSubcomposition().accept(*this, boost::none);
composition.getRightSubcomposition().accept(*this, boost::none);
return boost::none;
std::vector<std::set<std::string>> subresults;
for (auto const& subcomposition : composition.getSubcompositions()) {
subresults.push_back(boost::any_cast<std::set<std::string>>(subcomposition->accept(*this, boost::none)));
}
// Determine all actions that do not take part in synchronization vectors.
std::set<std::string> result;
for (uint64_t subresultIndex = 0; subresultIndex < subresults.size(); ++subresultIndex) {
std::set<std::string> actionsInSynch;
for (auto const& synchVector : composition.getSynchronizationVectors()) {
actionsInSynch.insert(synchVector.getInput()[subresultIndex]);
}
std::set_difference(subresults[subresultIndex].begin(), subresults[subresultIndex].end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(result, result.begin()));
}
// Now add all outputs of synchronization vectors.
for (auto const& synchVector : composition.getSynchronizationVectors()) {
result.insert(synchVector.getOutput());
}
return result;
}
private:
@ -350,6 +390,7 @@ namespace storm {
storm::jani::Model const& model;
std::set<std::string> automata;
std::set<std::string> nonSilentActions;
};
template <storm::dd::DdType Type, typename ValueType>
@ -488,434 +529,434 @@ namespace storm {
return result;
}
template <storm::dd::DdType Type, typename ValueType>
class SeparateEdgesSystemComposer : public SystemComposer<Type, ValueType> {
public:
// This structure represents an edge.
struct EdgeDd {
EdgeDd(storm::dd::Add<Type> const& guard = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}, std::set<storm::expressions::Variable> const& globalVariablesWrittenMultipleTimes = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) {
// Intentionally left empty.
}
EdgeDd(EdgeDd const& other) : guard(other.guard), transitions(other.transitions), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) {
// Intentionally left empty.
}
EdgeDd& operator=(EdgeDd const& other) {
if (this != &other) {
globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes;
writtenGlobalVariables = other.writtenGlobalVariables;
guard = other.guard;
transitions = other.transitions;
}
return *this;
}
storm::dd::Add<Type, ValueType> guard;
storm::dd::Add<Type, ValueType> transitions;
std::set<storm::expressions::Variable> writtenGlobalVariables;
std::set<storm::expressions::Variable> globalVariablesWrittenMultipleTimes;
};
// This structure represents a subcomponent of a composition.
struct AutomatonDd {
AutomatonDd(storm::dd::Add<Type, ValueType> const& identity) : identity(identity) {
// Intentionally left empty.
}
std::map<uint64_t, std::vector<EdgeDd>> actionIndexToEdges;
storm::dd::Add<Type, ValueType> identity;
};
SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) : SystemComposer<Type, ValueType>(model, variables) {
// Intentionally left empty.
}
ComposerResult<Type, ValueType> compose() override {
AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, boost::none));
return buildSystemFromAutomaton(globalAutomaton);
}
boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
return buildAutomatonDd(composition.getAutomatonName());
}
boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
AutomatonDd subautomaton = boost::any_cast<AutomatonDd>(composition.getSubcomposition().accept(*this, boost::none));
// Build a mapping from indices to indices for the renaming.
std::map<uint64_t, uint64_t> renamingIndexToIndex;
for (auto const& entry : composition.getRenaming()) {
if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) {
// Distinguish the cases where we hide the action or properly rename it.
if (entry.second) {
renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get()));
} else {
renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex());
}
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action.");
}
}
// Finally, apply the renaming.
AutomatonDd result(subautomaton.identity);
for (auto const& actionEdges : subautomaton.actionIndexToEdges) {
auto it = renamingIndexToIndex.find(actionEdges.first);
if (it != renamingIndexToIndex.end()) {
// If we are to rename the action, do so.
result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end());
} else {
// Otherwise copy over the edges.
result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end());
}
}
return result;
}
boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
AutomatonDd leftSubautomaton = boost::any_cast<AutomatonDd>(composition.getLeftSubcomposition().accept(*this, boost::none));
AutomatonDd rightSubautomaton = boost::any_cast<AutomatonDd>(composition.getRightSubcomposition().accept(*this, boost::none));
// Build the set of synchronizing action indices.
std::set<uint64_t> synchronizingActionIndices;
for (auto const& entry : composition.getSynchronizationAlphabet()) {
if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) {
synchronizingActionIndices.insert(this->model.getActionIndex(entry));
} else {
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action.");
}
}
// Perform the composition.
// First, consider all actions in the left subcomposition.
AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity);
uint64_t index = 0;
for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) {
// If we need to synchronize over this action, do so now.
if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) {
auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first);
if (rightIt != rightSubautomaton.actionIndexToEdges.end()) {
for (auto const& edge1 : actionEdges.second) {
for (auto const& edge2 : rightIt->second) {
EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2);
if (!edgeDd.guard.isZero()) {
result.actionIndexToEdges[actionEdges.first].push_back(edgeDd);
}
index++;
}
}
}
} else {
// Extend all edges by the missing identity (unsynchronizing) and copy them over.
for (auto const& edge : actionEdges.second) {
result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity));
}
}
}
// Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because
// we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none,
// such transitions can not be taken and we can drop them.
for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) {
if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) {
for (auto const& edge : actionEdges.second) {
result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity));
}
}
}
return result;
}
private:
storm::dd::Add<Type, ValueType> combineEdgesBySummation(std::vector<EdgeDd> const& edges, CompositionVariables<Type, ValueType> const& variables) {
storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
for (auto const& edge : edges) {
// Simply add all actions, but make sure to include the missing global variable identities.
result += edge.transitions * computeMissingGlobalVariableIdentities(edge, variables);
}
return result;
}
std::pair<uint64_t, storm::dd::Add<Type, ValueType>> combineEdgesByNondeterministicChoice(std::vector<EdgeDd>& edges) {
// Complete all edges by adding the missing global variable identities.
for (auto& edge : edges) {
edge.transitions *= computeMissingGlobalVariableIdentities(edge, this->variables);
}
// Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state.
storm::dd::Add<Type, ValueType> sumOfGuards = this->variables.manager->template getAddZero<ValueType>();
for (auto const& edge : edges) {
sumOfGuards += edge.guard;
}
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.
if (maxChoices == 0) {
return std::make_pair(0, this->variables.manager->template getAddZero<ValueType>());
} else if (maxChoices == 1) {
return std::make_pair(0, combineEdgesBySummation(edges, this->variables));
} else {
// Calculate number of required variables to encode the nondeterminism.
uint_fast64_t numberOfBinaryVariables = static_cast<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
storm::dd::Add<Type, ValueType> allEdges = this->variables.manager->template getAddZero<ValueType>();
storm::dd::Bdd<Type> equalsNumberOfChoicesDd;
std::vector<storm::dd::Add<Type, ValueType>> choiceDds(maxChoices, this->variables.manager->template getAddZero<ValueType>());
std::vector<storm::dd::Bdd<Type>> remainingDds(maxChoices, this->variables.manager->getBddZero());
for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
// Determine the set of states with exactly currentChoices choices.
equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast<double>(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] = this->variables.manager->template getAddZero<ValueType>();
remainingDds[j] = equalsNumberOfChoicesDd;
}
for (std::size_t j = 0; j < edges.size(); ++j) {
// Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices
// choices such that one outgoing choice is given by the j-th edge.
storm::dd::Bdd<Type> guardChoicesIntersection = edges[j].guard.toBdd() && 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::Bdd<Type> 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.template toAdd<ValueType>() * edges[j].transitions;
}
// 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) {
allEdges += encodeIndex(j, 0, numberOfBinaryVariables, this->variables) * choiceDds[j];
}
// Delete currentChoices out of overlapping DD
sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<ValueType>();
}
return std::make_pair(numberOfBinaryVariables, allEdges);
}
}
storm::dd::Bdd<Type> computeIllegalFragmentFromEdges(std::map<uint64_t, std::vector<EdgeDd>> const& actionIndexToEdges) {
// Create the illegal fragment. For this, we need to find the edges that write global variables multiple times.
storm::dd::Bdd<Type> illegalFragment = this->variables.manager->getBddZero();
for (auto const& action : actionIndexToEdges) {
for (auto const& edge : action.second) {
if (!edge.globalVariablesWrittenMultipleTimes.empty()) {
for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) {
STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised.");
illegalFragment |= edge.guard.toBdd();
}
}
}
}
return illegalFragment;
}
ComposerResult<Type, ValueType> buildSystemFromAutomaton(AutomatonDd& automatonDd) {
// If the model is an MDP, we need to encode the nondeterminism using additional variables.
if (this->model.getModelType() == storm::jani::ModelType::MDP) {
std::map<uint64_t, std::pair<uint64_t, storm::dd::Add<Type, ValueType>>> actionIndexToUsedVariablesAndDd;
// Combine the edges of each action individually and keep track of how many local nondeterminism variables
// were used.
uint64_t highestNumberOfUsedNondeterminismVariables = 0;
for (auto& action : automatonDd.actionIndexToEdges) {
std::pair<uint64_t, storm::dd::Add<Type, ValueType>> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second);
actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd);
highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first);
}
storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
for (auto const& element : actionIndexToUsedVariablesAndDd) {
result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional<uint64_t>(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables);
}
return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables);
} else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) {
storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
for (auto const& action : automatonDd.actionIndexToEdges) {
result += combineEdgesBySummation(action.second, this->variables);
}
return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0);
}
STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
}
storm::dd::Add<Type, ValueType> computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables<Type, ValueType> const& variables) {
std::set<storm::expressions::Variable> missingIdentities;
std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
storm::dd::Add<Type, ValueType> identityEncoding = variables.manager->template getAddOne<ValueType>();
for (auto const& variable : missingIdentities) {
identityEncoding *= variables.variableToIdentityMap.at(variable);
}
return identityEncoding;
}
EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add<Type, ValueType> const& identity) {
EdgeDd result(edge);
result.transitions *= identity;
return result;
}
EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) {
EdgeDd result;
// Compose the guards.
result.guard = edge1.guard * edge2.guard;
// If the composed guard is already zero, we can immediately return an empty result.
if (result.guard.isZero()) {
result.transitions = edge1.transitions.getDdManager().template getAddZero<ValueType>();
return result;
}
// Compute the set of variables written multiple times by the composition.
std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes;
std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin()));
std::set<storm::expressions::Variable> newVariablesWrittenMultipleTimes;
std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin()));
std::set<storm::expressions::Variable> variablesWrittenMultipleTimes;
std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin()));
result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes);
// Compute the set of variables written by the composition.
std::set<storm::expressions::Variable> variablesWritten;
std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin()));
result.writtenGlobalVariables = variablesWritten;
// Compose the guards.
result.guard = edge1.guard * edge2.guard;
// Compose the transitions.
result.transitions = edge1.transitions * edge2.transitions;
return result;
}
/*!
* Builds the DD for the given edge.
*/
EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) {
STORM_LOG_TRACE("Translating guard " << edge.getGuard());
storm::dd::Add<Type, ValueType> guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());// * this->variables.automatonToRangeMap.at(automaton.getName());
STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable.");
if (!guard.isZero()) {
// Create the DDs representing the individual updates.
std::vector<EdgeDestinationDd<Type, ValueType>> destinationDds;
for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) {
destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard, this->variables));
STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect.");
}
// Start by gathering all variables that were written in at least one update.
std::set<storm::expressions::Variable> globalVariablesInSomeUpdate;
// If the edge is not labeled with the silent action, we have to analyze which portion of the global
// variables was written by any of the updates and make all update results equal w.r.t. this set. If
// the edge is labeled with the silent action, we can already multiply the identities of all global variables.
if (edge.getActionIndex() != this->model.getSilentActionIndex()) {
for (auto const& edgeDestinationDd : destinationDds) {
globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end());
}
} else {
globalVariablesInSomeUpdate = this->variables.allGlobalVariables;
}
// Then, multiply the missing identities.
for (auto& destinationDd : destinationDds) {
std::set<storm::expressions::Variable> missingIdentities;
std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
for (auto const& variable : missingIdentities) {
STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD.");
destinationDd.transitions *= this->variables.variableToIdentityMap.at(variable);
}
}
// Now combine the destination DDs to the edge DD.
storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
for (auto const& destinationDd : destinationDds) {
transitions += destinationDd.transitions;
}
// Add the source location and the guard.
transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
// If we multiply the ranges of global variables, make sure everything stays within its bounds.
if (!globalVariablesInSomeUpdate.empty()) {
transitions *= this->variables.globalVariableRanges;
}
// If the edge has a rate, we multiply it to the DD.
if (edge.hasRate()) {
transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate());
}
return EdgeDd(guard, transitions, globalVariablesInSomeUpdate);
} else {
return EdgeDd(this->variables.manager->template getAddZero<ValueType>(), this->variables.manager->template getAddZero<ValueType>());
}
}
/*!
* Builds the DD for the automaton with the given name.
*/
AutomatonDd buildAutomatonDd(std::string const& automatonName) {
AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName));
storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName);
for (auto const& edge : automaton.getEdges()) {
// Build the edge and add it if it adds transitions.
EdgeDd edgeDd = buildEdgeDd(automaton, edge);
if (!edgeDd.guard.isZero()) {
result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd);
}
}
return result;
}
};
// template <storm::dd::DdType Type, typename ValueType>
// class SeparateEdgesSystemComposer : public SystemComposer<Type, ValueType> {
// public:
// // This structure represents an edge.
// struct EdgeDd {
// EdgeDd(storm::dd::Add<Type> const& guard = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}, std::set<storm::expressions::Variable> const& globalVariablesWrittenMultipleTimes = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) {
// // Intentionally left empty.
// }
//
// EdgeDd(EdgeDd const& other) : guard(other.guard), transitions(other.transitions), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) {
// // Intentionally left empty.
// }
//
// EdgeDd& operator=(EdgeDd const& other) {
// if (this != &other) {
// globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes;
// writtenGlobalVariables = other.writtenGlobalVariables;
// guard = other.guard;
// transitions = other.transitions;
// }
// return *this;
// }
//
// storm::dd::Add<Type, ValueType> guard;
// storm::dd::Add<Type, ValueType> transitions;
// std::set<storm::expressions::Variable> writtenGlobalVariables;
// std::set<storm::expressions::Variable> globalVariablesWrittenMultipleTimes;
// };
//
// // This structure represents a subcomponent of a composition.
// struct AutomatonDd {
// AutomatonDd(storm::dd::Add<Type, ValueType> const& identity) : identity(identity) {
// // Intentionally left empty.
// }
//
// std::map<uint64_t, std::vector<EdgeDd>> actionIndexToEdges;
// storm::dd::Add<Type, ValueType> identity;
// };
//
// SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) : SystemComposer<Type, ValueType>(model, variables) {
// // Intentionally left empty.
// }
//
// ComposerResult<Type, ValueType> compose() override {
// AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, boost::none));
// return buildSystemFromAutomaton(globalAutomaton);
// }
//
// boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
// return buildAutomatonDd(composition.getAutomatonName());
// }
//
// boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
// AutomatonDd subautomaton = boost::any_cast<AutomatonDd>(composition.getSubcomposition().accept(*this, boost::none));
//
// // Build a mapping from indices to indices for the renaming.
// std::map<uint64_t, uint64_t> renamingIndexToIndex;
// for (auto const& entry : composition.getRenaming()) {
// if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) {
// // Distinguish the cases where we hide the action or properly rename it.
// if (entry.second) {
// renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get()));
// } else {
// renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex());
// }
// } else {
// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action.");
// }
// }
//
// // Finally, apply the renaming.
// AutomatonDd result(subautomaton.identity);
// for (auto const& actionEdges : subautomaton.actionIndexToEdges) {
// auto it = renamingIndexToIndex.find(actionEdges.first);
// if (it != renamingIndexToIndex.end()) {
// // If we are to rename the action, do so.
// result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end());
// } else {
// // Otherwise copy over the edges.
// result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end());
// }
// }
// return result;
// }
//
// boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
// AutomatonDd leftSubautomaton = boost::any_cast<AutomatonDd>(composition.getLeftSubcomposition().accept(*this, boost::none));
// AutomatonDd rightSubautomaton = boost::any_cast<AutomatonDd>(composition.getRightSubcomposition().accept(*this, boost::none));
//
// // Build the set of synchronizing action indices.
// std::set<uint64_t> synchronizingActionIndices;
// for (auto const& entry : composition.getSynchronizationAlphabet()) {
// if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) {
// synchronizingActionIndices.insert(this->model.getActionIndex(entry));
// } else {
// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action.");
// }
// }
//
// // Perform the composition.
//
// // First, consider all actions in the left subcomposition.
// AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity);
// uint64_t index = 0;
// for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) {
// // If we need to synchronize over this action, do so now.
// if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) {
// auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first);
// if (rightIt != rightSubautomaton.actionIndexToEdges.end()) {
// for (auto const& edge1 : actionEdges.second) {
// for (auto const& edge2 : rightIt->second) {
// EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2);
// if (!edgeDd.guard.isZero()) {
// result.actionIndexToEdges[actionEdges.first].push_back(edgeDd);
// }
// index++;
// }
// }
// }
// } else {
// // Extend all edges by the missing identity (unsynchronizing) and copy them over.
// for (auto const& edge : actionEdges.second) {
// result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity));
// }
// }
// }
//
// // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because
// // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none,
// // such transitions can not be taken and we can drop them.
// for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) {
// if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) {
// for (auto const& edge : actionEdges.second) {
// result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity));
// }
// }
// }
//
// return result;
// }
//
// private:
// storm::dd::Add<Type, ValueType> combineEdgesBySummation(std::vector<EdgeDd> const& edges, CompositionVariables<Type, ValueType> const& variables) {
// storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
// for (auto const& edge : edges) {
// // Simply add all actions, but make sure to include the missing global variable identities.
// result += edge.transitions * computeMissingGlobalVariableIdentities(edge, variables);
// }
// return result;
// }
//
// std::pair<uint64_t, storm::dd::Add<Type, ValueType>> combineEdgesByNondeterministicChoice(std::vector<EdgeDd>& edges) {
// // Complete all edges by adding the missing global variable identities.
// for (auto& edge : edges) {
// edge.transitions *= computeMissingGlobalVariableIdentities(edge, this->variables);
// }
//
// // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state.
// storm::dd::Add<Type, ValueType> sumOfGuards = this->variables.manager->template getAddZero<ValueType>();
// for (auto const& edge : edges) {
// sumOfGuards += edge.guard;
// }
// 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.
// if (maxChoices == 0) {
// return std::make_pair(0, this->variables.manager->template getAddZero<ValueType>());
// } else if (maxChoices == 1) {
// return std::make_pair(0, combineEdgesBySummation(edges, this->variables));
// } else {
// // Calculate number of required variables to encode the nondeterminism.
// uint_fast64_t numberOfBinaryVariables = static_cast<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
//
// storm::dd::Add<Type, ValueType> allEdges = this->variables.manager->template getAddZero<ValueType>();
//
// storm::dd::Bdd<Type> equalsNumberOfChoicesDd;
// std::vector<storm::dd::Add<Type, ValueType>> choiceDds(maxChoices, this->variables.manager->template getAddZero<ValueType>());
// std::vector<storm::dd::Bdd<Type>> remainingDds(maxChoices, this->variables.manager->getBddZero());
//
// for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
// // Determine the set of states with exactly currentChoices choices.
// equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast<double>(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] = this->variables.manager->template getAddZero<ValueType>();
// remainingDds[j] = equalsNumberOfChoicesDd;
// }
//
// for (std::size_t j = 0; j < edges.size(); ++j) {
// // Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices
// // choices such that one outgoing choice is given by the j-th edge.
// storm::dd::Bdd<Type> guardChoicesIntersection = edges[j].guard.toBdd() && 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::Bdd<Type> 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.template toAdd<ValueType>() * edges[j].transitions;
// }
//
// // 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) {
// allEdges += encodeIndex(j, 0, numberOfBinaryVariables, this->variables) * choiceDds[j];
// }
//
// // Delete currentChoices out of overlapping DD
// sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<ValueType>();
// }
//
// return std::make_pair(numberOfBinaryVariables, allEdges);
// }
// }
//
// storm::dd::Bdd<Type> computeIllegalFragmentFromEdges(std::map<uint64_t, std::vector<EdgeDd>> const& actionIndexToEdges) {
// // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times.
// storm::dd::Bdd<Type> illegalFragment = this->variables.manager->getBddZero();
// for (auto const& action : actionIndexToEdges) {
// for (auto const& edge : action.second) {
// if (!edge.globalVariablesWrittenMultipleTimes.empty()) {
// for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) {
// STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised.");
// illegalFragment |= edge.guard.toBdd();
// }
// }
// }
// }
// return illegalFragment;
// }
//
// ComposerResult<Type, ValueType> buildSystemFromAutomaton(AutomatonDd& automatonDd) {
// // If the model is an MDP, we need to encode the nondeterminism using additional variables.
// if (this->model.getModelType() == storm::jani::ModelType::MDP) {
// std::map<uint64_t, std::pair<uint64_t, storm::dd::Add<Type, ValueType>>> actionIndexToUsedVariablesAndDd;
//
// // Combine the edges of each action individually and keep track of how many local nondeterminism variables
// // were used.
// uint64_t highestNumberOfUsedNondeterminismVariables = 0;
// for (auto& action : automatonDd.actionIndexToEdges) {
// std::pair<uint64_t, storm::dd::Add<Type, ValueType>> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second);
// actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd);
// highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first);
// }
//
// storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
// for (auto const& element : actionIndexToUsedVariablesAndDd) {
// result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional<uint64_t>(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables);
// }
//
// return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables);
// } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) {
// storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
// for (auto const& action : automatonDd.actionIndexToEdges) {
// result += combineEdgesBySummation(action.second, this->variables);
// }
// return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0);
// }
//
// STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
// }
//
// storm::dd::Add<Type, ValueType> computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables<Type, ValueType> const& variables) {
// std::set<storm::expressions::Variable> missingIdentities;
// std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
// storm::dd::Add<Type, ValueType> identityEncoding = variables.manager->template getAddOne<ValueType>();
// for (auto const& variable : missingIdentities) {
// identityEncoding *= variables.variableToIdentityMap.at(variable);
// }
// return identityEncoding;
// }
//
// EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add<Type, ValueType> const& identity) {
// EdgeDd result(edge);
// result.transitions *= identity;
// return result;
// }
//
// EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) {
// EdgeDd result;
//
// // Compose the guards.
// result.guard = edge1.guard * edge2.guard;
//
// // If the composed guard is already zero, we can immediately return an empty result.
// if (result.guard.isZero()) {
// result.transitions = edge1.transitions.getDdManager().template getAddZero<ValueType>();
// return result;
// }
//
// // Compute the set of variables written multiple times by the composition.
// std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes;
// std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin()));
//
// std::set<storm::expressions::Variable> newVariablesWrittenMultipleTimes;
// std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin()));
//
// std::set<storm::expressions::Variable> variablesWrittenMultipleTimes;
// std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin()));
//
// result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes);
//
// // Compute the set of variables written by the composition.
// std::set<storm::expressions::Variable> variablesWritten;
// std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin()));
//
// result.writtenGlobalVariables = variablesWritten;
//
// // Compose the guards.
// result.guard = edge1.guard * edge2.guard;
//
// // Compose the transitions.
// result.transitions = edge1.transitions * edge2.transitions;
//
// return result;
// }
//
// /*!
// * Builds the DD for the given edge.
// */
// EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) {
// STORM_LOG_TRACE("Translating guard " << edge.getGuard());
// storm::dd::Add<Type, ValueType> guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());// * this->variables.automatonToRangeMap.at(automaton.getName());
// STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable.");
//
// if (!guard.isZero()) {
// // Create the DDs representing the individual updates.
// std::vector<EdgeDestinationDd<Type, ValueType>> destinationDds;
// for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) {
// destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard, this->variables));
//
// STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect.");
// }
//
// // Start by gathering all variables that were written in at least one update.
// std::set<storm::expressions::Variable> globalVariablesInSomeUpdate;
//
// // If the edge is not labeled with the silent action, we have to analyze which portion of the global
// // variables was written by any of the updates and make all update results equal w.r.t. this set. If
// // the edge is labeled with the silent action, we can already multiply the identities of all global variables.
// if (edge.getActionIndex() != this->model.getSilentActionIndex()) {
// for (auto const& edgeDestinationDd : destinationDds) {
// globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end());
// }
// } else {
// globalVariablesInSomeUpdate = this->variables.allGlobalVariables;
// }
//
// // Then, multiply the missing identities.
// for (auto& destinationDd : destinationDds) {
// std::set<storm::expressions::Variable> missingIdentities;
// std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
//
// for (auto const& variable : missingIdentities) {
// STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD.");
// destinationDd.transitions *= this->variables.variableToIdentityMap.at(variable);
// }
// }
//
// // Now combine the destination DDs to the edge DD.
// storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
// for (auto const& destinationDd : destinationDds) {
// transitions += destinationDd.transitions;
// }
//
// // Add the source location and the guard.
// transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
//
// // If we multiply the ranges of global variables, make sure everything stays within its bounds.
// if (!globalVariablesInSomeUpdate.empty()) {
// transitions *= this->variables.globalVariableRanges;
// }
//
// // If the edge has a rate, we multiply it to the DD.
// if (edge.hasRate()) {
// transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate());
// }
// return EdgeDd(guard, transitions, globalVariablesInSomeUpdate);
// } else {
// return EdgeDd(this->variables.manager->template getAddZero<ValueType>(), this->variables.manager->template getAddZero<ValueType>());
// }
// }
//
// /*!
// * Builds the DD for the automaton with the given name.
// */
// AutomatonDd buildAutomatonDd(std::string const& automatonName) {
// AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName));
//
// storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName);
// for (auto const& edge : automaton.getEdges()) {
// // Build the edge and add it if it adds transitions.
// EdgeDd edgeDd = buildEdgeDd(automaton, edge);
// if (!edgeDd.guard.isZero()) {
// result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd);
// }
// }
//
// return result;
// }
// };
template <storm::dd::DdType Type, typename ValueType>
class CombinedEdgesSystemComposer : public SystemComposer<Type, ValueType> {
@ -1019,9 +1060,11 @@ namespace storm {
};
CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables) {
CombinedEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables, std::vector<storm::expressions::Variable> const& transientVariables) : SystemComposer<Type, ValueType>(model, variables, transientVariables), actionToIndex(model.getActionToIndexMap()) {
// Intentionally left empty.
}
std::unordered_map<std::string, uint64_t> actionToIndex;
ComposerResult<Type, ValueType> compose() override {
std::map<uint_fast64_t, uint_fast64_t> actionIndexToLocalNondeterminismVariableOffset;

8
src/storage/jani/Automaton.cpp
View File

@ -391,6 +391,14 @@ namespace storm {
edge.finalize(containingModel);
}
}
std::set<uint64_t> Automaton::getUsedActionIndices() const {
std::set<uint64_t> result;
for (auto const& edge : edges) {
result.insert(edge.getActionIndex());
}
return result;
}
}
}

5
src/storage/jani/Automaton.h
View File

@ -294,6 +294,11 @@ namespace storm {
*/
void finalize(Model const& containingModel);
/*!
* Retrieves the action indices appearing at some edge of the automaton.
*/
std::set<uint64_t> getUsedActionIndices() const;
private:
/// The name of the automaton.
std::string name;

77
src/storage/jani/CompositionInformationVisitor.cpp
View File

@ -6,11 +6,11 @@
namespace storm {
namespace jani {
CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), restrictedParallelComposition(false) {
CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), nonStandardParallelComposition(false) {
// Intentionally left empty.
}
CompositionInformation::CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenameComposition, bool containsRestrictedParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), restrictedParallelComposition(containsRestrictedParallelComposition) {
CompositionInformation::CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenameComposition, bool nonStandardParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), nonStandardParallelComposition(nonStandardParallelComposition) {
// Intentionally left empty.
}
@ -49,12 +49,12 @@ namespace storm {
return renameComposition;
}
void CompositionInformation::setContainsRestrictedParallelComposition() {
restrictedParallelComposition = true;
void CompositionInformation::setContainsNonStandardParallelComposition() {
nonStandardParallelComposition = true;
}
bool CompositionInformation::containsRestrictedParallelComposition() const {
return restrictedParallelComposition;
bool CompositionInformation::containsNonStandardParallelComposition() const {
return nonStandardParallelComposition;
}
std::map<std::string, uint64_t> CompositionInformation::joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second) {
@ -90,30 +90,61 @@ namespace storm {
boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {
CompositionInformation subresult = boost::any_cast<CompositionInformation>(composition.getSubcomposition().accept(*this, data));
std::set<std::string> nonsilentActions = CompositionInformation::renameNonsilentActions(subresult.getNonsilentActions(), composition.getRenaming());
return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsRestrictedParallelComposition());
return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsNonStandardParallelComposition());
}
boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) {
CompositionInformation left = boost::any_cast<CompositionInformation>(composition.getLeftSubcomposition().accept(*this, data));
CompositionInformation right = boost::any_cast<CompositionInformation>(composition.getRightSubcomposition().accept(*this, data));
// Join the information from both sides.
bool containsRenameComposition = left.containsRenameComposition() || right.containsRenameComposition();
bool containsRestrictedParallelComposition = left.containsRestrictedParallelComposition() || right.containsRestrictedParallelComposition();
std::map<std::string, uint64_t> joinedAutomatonToMultiplicity = CompositionInformation::joinMultiplicityMaps(left.getAutomatonToMultiplicityMap(), right.getAutomatonToMultiplicityMap());
std::vector<CompositionInformation> subinformation;
std::set<std::string> nonsilentActions;
std::set_union(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(nonsilentActions, nonsilentActions.begin()));
for (auto const& subcomposition : composition.getSubcompositions()) {
subinformation.push_back(boost::any_cast<CompositionInformation>(subcomposition->accept(*this, data)));
}
std::map<std::string, uint64_t> joinedAutomatonToMultiplicityMap;
bool containsRenameComposition = false;
bool containsNonStandardParallelComposition = false;
for (auto const& subinfo : subinformation) {
containsRenameComposition |= subinfo.containsRenameComposition();
containsNonStandardParallelComposition |= subinfo.containsNonStandardParallelComposition();
joinedAutomatonToMultiplicityMap = CompositionInformation::joinMultiplicityMaps(joinedAutomatonToMultiplicityMap, subinfo.getAutomatonToMultiplicityMap());
}
// If there was no restricted parallel composition yet, maybe the current composition is one, so check it.
if (!containsRestrictedParallelComposition) {
std::set<std::string> commonNonsilentActions;
std::set_intersection(left.getNonsilentActions().begin(), left.getNonsilentActions().end(), right.getNonsilentActions().begin(), right.getNonsilentActions().end(), std::inserter(commonNonsilentActions, commonNonsilentActions.begin()));
bool allCommonActionsIncluded = std::includes(commonNonsilentActions.begin(), commonNonsilentActions.end(), composition.getSynchronizationAlphabet().begin(), composition.getSynchronizationAlphabet().end());
containsRestrictedParallelComposition = !allCommonActionsIncluded;
// Keep track of the synchronization vectors that are effective, meaning that the subcompositions all have
// the non-silent actions that are referred to.
std::set<uint64_t> effectiveSynchVectors;
for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) {
effectiveSynchVectors.insert(synchVectorIndex);
}
return CompositionInformation(joinedAutomatonToMultiplicity, nonsilentActions, containsRenameComposition, containsRestrictedParallelComposition);
// Now compute non-silent actions.
std::set<std::string> nonsilentActions;
for (uint_fast64_t infoIndex = 0; infoIndex < subinformation.size(); ++infoIndex) {
auto const& subinfo = subinformation[infoIndex];
std::set<uint64_t> enabledSynchVectors;
for (auto const& nonsilentAction : subinfo.getNonsilentActions()) {
bool appearsInSomeSynchVector = false;
for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) {
auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex);
if (synchVector.getInput(infoIndex) == nonsilentAction) {
appearsInSomeSynchVector = true;
enabledSynchVectors.insert(synchVectorIndex);
}
}
if (!appearsInSomeSynchVector) {
nonsilentActions.insert(nonsilentAction);
}
}
std::set<uint64_t> newEffectiveSynchVectors;
std::set_intersection(effectiveSynchVectors.begin(), effectiveSynchVectors.end(), enabledSynchVectors.begin(), enabledSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin()));
effectiveSynchVectors = std::move(newEffectiveSynchVectors);
}
return CompositionInformation(joinedAutomatonToMultiplicityMap, nonsilentActions, containsRenameComposition, containsNonStandardParallelComposition);
}
}

10
src/storage/jani/CompositionInformationVisitor.h
View File

@ -16,7 +16,7 @@ namespace storm {
class CompositionInformation {
public:
CompositionInformation();
CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenaming, bool containsRestrictedParallelComposition);
CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenaming, bool nonStandardParallelComposition);
void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1);
@ -27,8 +27,8 @@ namespace storm {
void setContainsRenameComposition();
bool containsRenameComposition() const;
void setContainsRestrictedParallelComposition();
bool containsRestrictedParallelComposition() const;
void setContainsNonStandardParallelComposition();
bool containsNonStandardParallelComposition() const;
static std::map<std::string, uint64_t> joinMultiplicityMaps(std::map<std::string, uint64_t> const& first, std::map<std::string, uint64_t> const& second);
std::map<std::string, uint64_t> const& getAutomatonToMultiplicityMap() const;
@ -43,8 +43,8 @@ namespace storm {
/// A flag indicating whether the composition contains a renaming composition.
bool renameComposition;
/// A flag indicating whether the composition contains
bool restrictedParallelComposition;
/// A flag indicating whether the composition contains any non-standard parallel composition.
bool nonStandardParallelComposition;
};
class CompositionInformationVisitor : public CompositionVisitor {

6
src/storage/jani/Model.cpp
View File

@ -75,6 +75,10 @@ namespace storm {
return it->second;
}
std::unordered_map<std::string, uint64_t> const& Model::getActionToIndexMap() const {
return actionToIndex;
}
std::vector<Action> const& Model::getActions() const {
return actions;
}
@ -448,7 +452,7 @@ namespace storm {
bool Model::hasDefaultComposition() const {
CompositionInformationVisitor visitor;
CompositionInformation info = visitor.getInformation(this->getSystemComposition(), *this);
if (info.containsRestrictedParallelComposition() || info.containsRenameComposition()) {
if (info.containsNonStandardParallelComposition() || info.containsRenameComposition()) {
return false;
}
for (auto const& multiplicity : info.getAutomatonToMultiplicityMap()) {

5
src/storage/jani/Model.h
View File

@ -65,6 +65,11 @@ namespace storm {
*/
uint64_t getActionIndex(std::string const& name) const;
/*!
* Retrieves the mapping from action names to their indices.
*/
std::unordered_map<std::string, uint64_t> const& getActionToIndexMap() const;
/**
* Adds an action to the model.
*

116
src/storage/jani/ParallelComposition.cpp
View File

@ -1,32 +1,132 @@
#include "src/storage/jani/ParallelComposition.h"
#include <sstream>
#include <boost/algorithm/string/join.hpp>
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm {
namespace jani {
ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet) : leftSubcomposition(leftSubcomposition), rightSubcomposition(rightSubcomposition), alphabet(alphabet) {
SynchronizationVector::SynchronizationVector(std::vector<std::string> const& input, std::string const& output) : input(input), output(output) {
// Intentionally left empty.
}
Composition const& ParallelComposition::getLeftSubcomposition() const {
return *leftSubcomposition;
std::size_t SynchronizationVector::size() const {
return input.size();
}
std::vector<std::string> const& SynchronizationVector::getInput() const {
return input;
}
std::string const& SynchronizationVector::getInput(uint64_t index) const {
return input[index];
}
std::string const& SynchronizationVector::getOutput() const {
return output;
}
Composition const& ParallelComposition::getRightSubcomposition() const {
return *rightSubcomposition;
std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector) {
bool first = true;
stream << "(";
for (auto const& element : synchronizationVector.getInput()) {
if (!first) {
stream << ", ";
}
stream << element;
}
stream << ") -> " << synchronizationVector.getOutput();
return stream;
}
std::set<std::string> const& ParallelComposition::getSynchronizationAlphabet() const {
return alphabet;
ParallelComposition::ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::vector<SynchronizationVector> const& synchronizationVectors) : subcompositions(subcompositions), synchronizationVectors(synchronizationVectors) {
STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition.");
for (auto const& vector : this->synchronizationVectors) {
STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size.");
}
}
ParallelComposition::ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::set<std::string> const& synchronizationAlphabet) : subcompositions(subcompositions), synchronizationVectors() {
STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition.");
// Manually construct the synchronization vectors for all elements of the synchronization alphabet.
for (auto const& action : synchronizationAlphabet) {
synchronizationVectors.emplace_back(std::vector<std::string>(this->subcompositions.size(), action), action);
}
}
ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& synchronizationAlphabet) {
subcompositions.push_back(leftSubcomposition);
subcompositions.push_back(rightSubcomposition);
// Manually construct the synchronization vectors for all elements of the synchronization alphabet.
for (auto const& action : synchronizationAlphabet) {
synchronizationVectors.emplace_back(std::vector<std::string>(this->subcompositions.size(), action), action);
}
}
Composition const& ParallelComposition::getSubcomposition(uint64_t index) const {
return *subcompositions[index];
}
std::vector<std::shared_ptr<Composition>> const& ParallelComposition::getSubcompositions() const {
return subcompositions;
}
uint64_t ParallelComposition::getNumberOfSubcompositions() const {
return subcompositions.size();
}
SynchronizationVector const& ParallelComposition::getSynchronizationVector(uint64_t index) const {
return synchronizationVectors[index];
}
std::vector<SynchronizationVector> const& ParallelComposition::getSynchronizationVectors() const {
return synchronizationVectors;
}
std::size_t ParallelComposition::getNumberOfSynchronizationVectors() const {
return synchronizationVectors.size();
}
bool ParallelComposition::checkSynchronizationVectors() const {
for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) {
std::set<std::string> actions;
for (auto const& vector : synchronizationVectors) {
std::string const& action = vector.getInput(inputIndex);
STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action multiple times as input in synchronization vector.");
actions.insert(action);
}
}
}
boost::any ParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const {
return visitor.visit(*this, data);
}
void ParallelComposition::write(std::ostream& stream) const {
stream << this->getLeftSubcomposition() << " |[" << boost::algorithm::join(alphabet, ", ") << "]| " << this->getRightSubcomposition();
std::vector<std::string> synchronizationVectorsAsStrings;
for (auto const& synchronizationVector : synchronizationVectors) {
std::stringstream tmpStream;
tmpStream << synchronizationVector;
synchronizationVectorsAsStrings.push_back(tmpStream.str());
}
bool first = true;
stream << "(";
for (auto const& subcomposition : subcompositions) {
if (!first) {
stream << " || ";
first = false;
}
stream << *subcomposition;
}
stream << ")[" << boost::algorithm::join(synchronizationVectorsAsStrings, ", ") << "]";
}
}

78
src/storage/jani/ParallelComposition.h
View File

@ -2,47 +2,95 @@
#include <set>
#include <memory>
#include <vector>
#include <string>
#include "src/storage/jani/Composition.h"
namespace storm {
namespace jani {
class SynchronizationVector {
public:
SynchronizationVector(std::vector<std::string> const& input, std::string const& output);
std::size_t size() const;
std::vector<std::string> const& getInput() const;
std::string const& getInput(uint64_t index) const;
std::string const& getOutput() const;
private:
/// The input to the synchronization.
std::vector<std::string> input;
/// The output of the synchronization.
std::string output;
};
std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector);
class ParallelComposition : public Composition {
public:
/*!
* Creates a parallel composition of the two subcompositions.
* Creates a parallel composition of the subcompositions and the provided synchronization vectors.
*/
ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& alphabet = {});
ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::vector<SynchronizationVector> const& synchronizationVectors);
/*!
* Retrieves the left subcomposition.
* Creates a parallel composition of the subcompositions over the provided synchronization alphabet.
*/
Composition const& getLeftSubcomposition() const;
ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::set<std::string> const& synchronizationAlphabet);
/*!
* Retrieves the right subcomposition.
* Creates a parallel composition of the subcompositions over the provided synchronization alphabet.
*/
Composition const& getRightSubcomposition() const;
ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& synchronizationAlphabet);
/*!
* Retrieves the alphabet of actions over which to synchronize the automata.
* Retrieves the subcomposition with the given index.
*/
std::set<std::string> const& getSynchronizationAlphabet() const;
Composition const& getSubcomposition(uint64_t index) const;
/*!
* Retrieves the subcompositions of the parallel composition.
*/
std::vector<std::shared_ptr<Composition>> const& getSubcompositions() const;
/*!
* Retrieves the number of subcompositions of this parallel composition.
*/
uint64_t getNumberOfSubcompositions() const;
/*!
* Retrieves the synchronization vector with the given index.
*/
SynchronizationVector const& getSynchronizationVector(uint64_t index) const;
/*!
* Retrieves the synchronization vectors of the parallel composition.
*/
std::vector<SynchronizationVector> const& getSynchronizationVectors() const;
/*!
* Retrieves the number of synchronization vectors.
*/
std::size_t getNumberOfSynchronizationVectors() const;
virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override;
virtual void write(std::ostream& stream) const override;
private:
// The left subcomposition.
std::shared_ptr<Composition> leftSubcomposition;
/*!
* Checks the synchronization vectors for validity.
*/
bool checkSynchronizationVectors() const;
// The right subcomposition.
std::shared_ptr<Composition> rightSubcomposition;
/// The subcompositions.
std::vector<std::shared_ptr<Composition>> subcompositions;
// The alphabet of actions over which to synchronize.
std::set<std::string> alphabet;
/// The synchronization vectors of the parallel composition.
std::vector<SynchronizationVector> synchronizationVectors;
};
}

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

@ -137,7 +137,7 @@ namespace storm {
}
STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotImplementedException, "Transition reward translation currently not implemented.");
}
STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition.");
STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition.");
// Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the
// previously built mapping to make variables global that are read by more than one module.

Write Preview
Loading…
Cancel
Save