From d6a32ca6344d97310b87e28b258246a580d864a2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 11 Dec 2016 21:06:24 +0100 Subject: [PATCH] more work on flattening JANI compositions --- .../generator/JaniNextStateGenerator.cpp | 40 ++--- .../storage/SymbolicModelDescription.cpp | 1 + src/storm/storage/jani/Edge.cpp | 10 ++ src/storm/storage/jani/Edge.h | 1 + src/storm/storage/jani/Model.cpp | 150 ++++++++++++++++-- src/storm/utility/combinatorics.h | 68 ++++++++ 6 files changed, 226 insertions(+), 44 deletions(-) create mode 100644 src/storm/utility/combinatorics.h diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index 42372b291..51b96b122 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -9,6 +9,7 @@ #include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/utility/solver.h" +#include "storm/utility/combinatorics.h" #include "storm/exceptions/InvalidSettingsException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -200,41 +201,18 @@ namespace storm { } // Gather iterators to the initial locations of all the automata. - std::vector::const_iterator> initialLocationsIterators; - uint64_t currentLocationVariable = 0; - for (auto const& automaton : this->model.getAutomata()) { - initialLocationsIterators.push_back(automaton.getInitialLocationIndices().cbegin()); - - // Initialize the locations to the first possible combination. - setLocation(initialState, this->variableInformation.locationVariables[currentLocationVariable], *initialLocationsIterators.back()); - ++currentLocationVariable; + std::vector::const_iterator> initialLocationsIts; + std::vector::const_iterator> initialLocationsItes; + for (auto const& automaton : allAutomata) { + initialLocationsIts.push_back(automaton.get().getInitialLocationIndices().cbegin()); + initialLocationsItes.push_back(automaton.get().getInitialLocationIndices().cend()); } - - // Now iterate through all combinations of initial locations. - while (true) { + storm::utility::combinatorics::forEach(initialLocationsIts, initialLocationsItes, [this,&initialState] (uint64_t index, uint64_t value) { setLocation(initialState, this->variableInformation.locationVariables[index], value); }, [&stateToIdCallback,&initialStateIndices,&initialState] () { // Register initial state. StateType id = stateToIdCallback(initialState); initialStateIndices.push_back(id); - - uint64_t index = 0; - for (; index < initialLocationsIterators.size(); ++index) { - ++initialLocationsIterators[index]; - if (initialLocationsIterators[index] == this->model.getAutomata()[index].getInitialLocationIndices().cend()) { - initialLocationsIterators[index] = this->model.getAutomata()[index].getInitialLocationIndices().cbegin(); - } else { - break; - } - } - - // If we are at the end, leave the loop. Otherwise, create the next initial state. - if (index == initialLocationsIterators.size()) { - break; - } else { - for (uint64_t j = 0; j <= index; ++j) { - setLocation(initialState, this->variableInformation.locationVariables[j], *initialLocationsIterators[j]); - } - } - } + return true; + }); // Block the current initial state to search for the next one. if (!blockingExpression.isInitialized()) { diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index a9e4488b3..4b6dc4a18 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -119,6 +119,7 @@ namespace storm { if (this->isJaniModel()) { std::map substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString); storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants(); + preparedModel = preparedModel.flattenComposition(); return SymbolicModelDescription(preparedModel); } else if (this->isPrismProgram()) { std::map substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString); diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp index 6868a88e4..36b51745e 100644 --- a/src/storm/storage/jani/Edge.cpp +++ b/src/storm/storage/jani/Edge.cpp @@ -18,6 +18,16 @@ namespace storm { } } + Edge::Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector const& destinationLocations, std::vector const& destinationProbabilities) : sourceLocationIndex(sourceLocationIndex), actionIndex(actionIndex), rate(rate), templateEdge(templateEdge) { + + // Create the concrete destinations from the template edge. + STORM_LOG_THROW(templateEdge->getNumberOfDestinations() == destinationLocations.size() && destinationLocations.size() == destinationProbabilities.size(), storm::exceptions::InvalidArgumentException, "Sizes of template edge destinations and target locations mismatch."); + for (uint64_t i = 0; i < templateEdge->getNumberOfDestinations(); ++i) { + auto const& templateDestination = templateEdge->getDestination(i); + destinations.emplace_back(destinationLocations[i], destinationProbabilities[i], templateDestination); + } + } + uint64_t Edge::getSourceLocationIndex() const { return sourceLocationIndex; } diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h index ecfe58edc..928f54a78 100644 --- a/src/storm/storage/jani/Edge.h +++ b/src/storm/storage/jani/Edge.h @@ -16,6 +16,7 @@ namespace storm { Edge() = default; Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector> const& destinationTargetLocationsAndProbabilities); + Edge(uint64_t sourceLocationIndex, uint64_t actionIndex, boost::optional const& rate, std::shared_ptr const& templateEdge, std::vector const& destinationLocations, std::vector const& destinationProbabilities); /*! * Retrieves the index of the source location. diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 7fa3ac552..a37679c14 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -5,6 +5,8 @@ #include "storm/storage/jani/Compositions.h" #include "storm/storage/jani/CompositionInformationVisitor.h" +#include "storm/utility/combinatorics.h" + #include "storm/utility/macros.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -61,15 +63,15 @@ namespace storm { } uint64_t actionIndex; - std::vector> condition; + std::vector components; + std::vector condition; boost::optional rate; std::vector probabilities; - std::vector>> effects; + std::vector> effects; std::shared_ptr templateEdge; }; - std::vector createSynchronizingMetaEdges(Model const& model, Automaton& newAutomaton, std::vector>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector> const& composedAutomata, storm::solver::SmtSolver& solver) { - + std::vector createSynchronizingMetaEdges(Model const& oldModel, Model& newModel, std::vector>& synchronizingActionIndices, SynchronizationVector const& vector, std::vector> const& composedAutomata, storm::solver::SmtSolver& solver) { std::vector result; // Gather all participating automata and the corresponding input symbols. @@ -77,22 +79,113 @@ namespace storm { for (uint64_t i = 0; i < composedAutomata.size(); ++i) { std::string const& actionName = vector.getInput(i); if (!SynchronizationVector::isNoActionInput(actionName)) { - uint64_t actionIndex = model.getActionIndex(actionName); + uint64_t actionIndex = oldModel.getActionIndex(actionName); participatingAutomataAndActions.push_back(std::make_pair(composedAutomata[i], actionIndex)); synchronizingActionIndices[i].insert(actionIndex); } } + uint64_t resultingActionIndex = Model::SILENT_ACTION_INDEX; + if (vector.getOutput() != Model::SILENT_ACTION_NAME) { + if (newModel.hasAction(vector.getOutput())) { + resultingActionIndex = newModel.getActionIndex(vector.getOutput()); + } else { + resultingActionIndex = newModel.addAction(vector.getOutput()); + } + } + + bool noCombinations = false; + + // Prepare the list that stores for each automaton the list of edges with the participating action. + std::vector>> possibleEdges; + + for (auto const& automatonActionPair : participatingAutomataAndActions) { + possibleEdges.emplace_back(); + for (auto const& edge : automatonActionPair.first.get().getEdges()) { + if (edge.getActionIndex() == automatonActionPair.second) { + possibleEdges.back().push_back(edge); + } + } + + // If there were no edges with the participating action index, then there is no synchronization possible. + if (possibleEdges.back().empty()) { + noCombinations = true; + break; + } + } + + return result; } - void addEdgesToReachableLocations(Model const& model, std::vector> const& composedAutomata, Automaton& newAutomaton, std::vector const& conditionalMetaEdges) { + std::unordered_map, uint64_t, storm::utility::vector::VectorHash> addEdgesToReachableLocations(Model const& model, std::vector> const& composedAutomata, Automaton& newAutomaton, std::vector const& conditionalMetaEdges) { - std::vector locations; + // Maintain a stack of locations that still need to be to explored. + std::vector> locationsToExplore; + + // Enumerate all initial location combinations. + std::vector::const_iterator> initialLocationsIts; + std::vector::const_iterator> initialLocationsItes; for (auto const& automaton : composedAutomata) { - // TODO: iterate over initial locations of all automata + initialLocationsIts.push_back(automaton.get().getInitialLocationIndices().cbegin()); + initialLocationsItes.push_back(automaton.get().getInitialLocationIndices().cend()); + } + std::vector initialLocation(composedAutomata.size()); + storm::utility::combinatorics::forEach(initialLocationsIts, initialLocationsItes, [&initialLocation] (uint64_t index, uint64_t value) { initialLocation[index] = value; }, [&locationsToExplore, &initialLocation] () { + locationsToExplore.push_back(initialLocation); + return true; + }); + + // We also maintain a mapping from location combinations to new locations. + std::unordered_map, uint64_t, storm::utility::vector::VectorHash> newLocationMapping; + + // Register all initial locations as new locations. + for (auto const& location : locationsToExplore) { + uint64_t id = newLocationMapping.size(); + newLocationMapping[location] = id; + } + + // As long as there are locations to explore, do so. + while (!locationsToExplore.empty()) { + std::vector currentLocations = std::move(locationsToExplore.back()); + locationsToExplore.pop_back(); + + for (auto const& metaEdge : conditionalMetaEdges) { + bool isApplicable = true; + for (uint64_t i = 0; i < metaEdge.components.size(); ++i) { + if (currentLocations[metaEdge.components[i]] != metaEdge.condition[i]) { + isApplicable = false; + break; + } + } + + if (isApplicable) { + std::vector newLocations; + + for (auto const& effect : metaEdge.effects) { + std::vector targetLocationCombination = currentLocations; + for (uint64_t i = 0; i < metaEdge.components.size(); ++i) { + targetLocationCombination[metaEdge.components[i]] = effect[i]; + } + + // Check whether the target combination is new. + auto it = newLocationMapping.find(targetLocationCombination); + if (it != newLocationMapping.end()) { + newLocations.emplace_back(it->second); + } else { + uint64_t id = newLocationMapping.size(); + newLocationMapping[targetLocationCombination] = id; + locationsToExplore.emplace_back(std::move(targetLocationCombination)); + newLocations.emplace_back(id); + } + } + + newAutomaton.addEdge(Edge(newLocationMapping.at(currentLocations), metaEdge.actionIndex, metaEdge.rate, metaEdge.templateEdge, newLocations, metaEdge.probabilities)); + } + } } + return newLocationMapping; } Model Model::flattenComposition(std::shared_ptr const& smtSolverFactory) const { @@ -107,7 +200,8 @@ namespace storm { STORM_LOG_THROW(this->getModelType() == ModelType::DTMC || this->getModelType() == ModelType::MDP, storm::exceptions::InvalidTypeException, "Unable to flatten modules for model of type '" << this->getModelType() << "'."); // Otherwise, we need to actually flatten composition. - + Model flattenedModel(this->getName() + "_flattened", this->getModelType(), this->getJaniVersion(), this->getManager().shared_from_this()); + // Get an SMT solver for computing possible guard combinations. std::unique_ptr solver = smtSolverFactory->create(*expressionManager); @@ -168,7 +262,7 @@ namespace storm { } // Create all conditional template edges corresponding to this synchronization vector. - std::vector newConditionalMetaEdges = createSynchronizingMetaEdges(*this, newAutomaton, synchronizingActionIndices, vector, composedAutomata, *solver); + std::vector newConditionalMetaEdges = createSynchronizingMetaEdges(*this, flattenedModel, synchronizingActionIndices, vector, composedAutomata, *solver); conditionalMetaEdges.insert(conditionalMetaEdges.end(), newConditionalMetaEdges.begin(), newConditionalMetaEdges.end()); } @@ -177,15 +271,28 @@ namespace storm { Automaton const& automaton = composedAutomata[i].get(); for (auto const& edge : automaton.getEdges()) { if (synchronizingActionIndices[i].find(edge.getActionIndex()) == synchronizingActionIndices[i].end()) { + uint64_t actionIndex = edge.getActionIndex(); + if (actionIndex != SILENT_ACTION_INDEX) { + std::string actionName = this->getActionIndexToNameMap().at(edge.getActionIndex()); + if (flattenedModel.hasAction(actionName)) { + actionIndex = flattenedModel.getActionIndex(actionName); + } else { + actionIndex = flattenedModel.addAction(actionName); + } + } + std::shared_ptr templateEdge = newAutomaton.createTemplateEdge(edge.getGuard()); conditionalMetaEdges.emplace_back(); ConditionalMetaEdge& conditionalMetaEdge = conditionalMetaEdges.back(); conditionalMetaEdge.actionIndex = edge.getActionIndex(); - conditionalMetaEdge.condition.emplace_back(static_cast(i), edge.getSourceLocationIndex()); + conditionalMetaEdge.components.emplace_back(static_cast(i)); + conditionalMetaEdge.condition.emplace_back(edge.getSourceLocationIndex()); conditionalMetaEdge.rate = edge.getOptionalRate(); for (auto const& destination : edge.getDestinations()) { - conditionalMetaEdge.effects.emplace_back(i, destination.getLocationIndex()); + conditionalMetaEdge.effects.emplace_back(); + + conditionalMetaEdge.effects.back().emplace_back(destination.getLocationIndex()); conditionalMetaEdge.probabilities.emplace_back(destination.getProbability()); } conditionalMetaEdge.templateEdge = templateEdge; @@ -193,9 +300,26 @@ namespace storm { } } - addEdgesToReachableLocations(*this, composedAutomata, newAutomaton, conditionalMetaEdges); + std::unordered_map, uint64_t, storm::utility::vector::VectorHash> newLocationMapping = addEdgesToReachableLocations(*this, composedAutomata, newAutomaton, conditionalMetaEdges); + + for (auto const& newLocation : newLocationMapping) { + std::stringstream locationNameBuilder; + for (uint64_t i = 0; i < newLocation.first.size(); ++i) { + locationNameBuilder << composedAutomata[i].get().getLocation(newLocation.first[i]).getName() << "_"; + } + + uint64_t locationIndex = newAutomaton.addLocation(Location(locationNameBuilder.str())); + Location& location = newAutomaton.getLocation(locationIndex); + for (uint64_t i = 0; i < newLocation.first.size(); ++i) { + for (auto const& assignment : composedAutomata[i].get().getLocation(newLocation.first[i]).getAssignments()) { + location.addTransientAssignment(assignment); + } + } + } + flattenedModel.addAutomaton(newAutomaton); + return flattenedModel; } uint64_t Model::addAction(Action const& action) { diff --git a/src/storm/utility/combinatorics.h b/src/storm/utility/combinatorics.h new file mode 100644 index 000000000..de27ec868 --- /dev/null +++ b/src/storm/utility/combinatorics.h @@ -0,0 +1,68 @@ +#pragma once + +#include +#include +#include + +namespace storm { + namespace utility { + namespace combinatorics { + + template + void forEach(std::vector const& its, std::vector const& ites, std::function()))> const& setValueCallback, std::function const& newCombinationCallback) { + typedef decltype((*std::declval())) value_type; + STORM_LOG_ASSERT(its.size() == ites.size(), "Iterator begin/end mismatch."); + + if (its.size() == 0) { + return; + } + + bool allNonEmpty = true; + for (uint64_t index = 0; index < its.size(); ++index) { + if (its[index] == ites[index]) { + allNonEmpty = false; + break; + } + } + if (!allNonEmpty) { + return; + } + + std::vector currentIterators(its); + + // Fill the initial combination. + for (uint64_t index = 0; index < currentIterators.size(); ++index) { + setValueCallback(index, *currentIterators[index]); + } + + // Enumerate all combinations until the callback yields false (or there are no more combinations). + while (true) { + bool cont = newCombinationCallback(); + if (!cont) { + break; + } + + uint64_t index = 0; + for (; index < currentIterators.size(); ++index) { + ++currentIterators[index]; + if (currentIterators[index] == ites[index]) { + currentIterators[index] = its[index]; + } else { + break; + } + } + + // If we are at the end, leave the loop. + if (index == currentIterators.size()) { + break; + } else { + for (uint64_t j = 0; j <= index; ++j) { + setValueCallback(j, *currentIterators[index]); + } + } + } + } + + } + } +}