From 33ac2e07933873bed14cef64dc8112c54e5b511b Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 2 May 2018 23:41:08 +0200 Subject: [PATCH] make jani models copyable --- src/storm/storage/jani/Automaton.cpp | 132 +++--------- src/storm/storage/jani/Automaton.h | 74 +------ src/storm/storage/jani/Edge.cpp | 16 ++ src/storm/storage/jani/Edge.h | 4 + src/storm/storage/jani/EdgeContainer.cpp | 200 ++++++++++++++++++ src/storm/storage/jani/EdgeContainer.h | 125 +++++++++++ src/storm/storage/jani/EdgeDestination.cpp | 4 + src/storm/storage/jani/EdgeDestination.h | 2 + src/storm/storage/jani/Model.cpp | 5 +- .../storage/jani/TemplateEdgeContainer.cpp | 12 ++ .../storage/jani/TemplateEdgeContainer.h | 16 ++ 11 files changed, 417 insertions(+), 173 deletions(-) create mode 100644 src/storm/storage/jani/EdgeContainer.cpp create mode 100644 src/storm/storage/jani/EdgeContainer.h create mode 100644 src/storm/storage/jani/TemplateEdgeContainer.cpp create mode 100644 src/storm/storage/jani/TemplateEdgeContainer.h diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index 8715a27a8..f4c65c759 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -12,47 +12,7 @@ namespace storm { namespace jani { - namespace detail { - Edges::Edges(iterator it, iterator ite) : it(it), ite(ite) { - // Intentionally left empty. - } - - Edges::iterator Edges::begin() const { - return it; - } - - Edges::iterator Edges::end() const { - return ite; - } - - bool Edges::empty() const { - return it == ite; - } - - std::size_t Edges::size() const { - return std::distance(it, ite); - } - - ConstEdges::ConstEdges(const_iterator it, const_iterator ite) : it(it), ite(ite) { - // Intentionally left empty. - } - - ConstEdges::const_iterator ConstEdges::begin() const { - return it; - } - - ConstEdges::const_iterator ConstEdges::end() const { - return ite; - } - - bool ConstEdges::empty() const { - return it == ite; - } - std::size_t ConstEdges::size() const { - return std::distance(it, ite); - } - } Automaton::Automaton(std::string const& name, storm::expressions::Variable const& locationExpressionVariable) : name(name), locationExpressionVariable(locationExpressionVariable) { // Add a sentinel element to the mapping from locations to starting indices. @@ -176,7 +136,7 @@ namespace storm { } Edge const& Automaton::getEdge(uint64_t index) const { - return edges[index]; + return edges.getConcreteEdges()[index]; } Automaton::Edges Automaton::getEdgesFromLocation(std::string const& name) { @@ -307,42 +267,30 @@ namespace storm { void Automaton::addEdge(Edge const& edge) { STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'."); - - // Find the right position for the edge and insert it properly. - auto posIt = edges.begin(); - std::advance(posIt, locationToStartingIndex[edge.getSourceLocationIndex() + 1]); - edges.insert(posIt, edge); - + assert(validate()); + + edges.insertEdge(edge, locationToStartingIndex[edge.getSourceLocationIndex()], locationToStartingIndex[edge.getSourceLocationIndex() + 1]); + // Update the set of action indices of this automaton. + actionIndices.insert(edge.getActionIndex()); + // Now update the starting indices of all subsequent locations. for (uint64_t locationIndex = edge.getSourceLocationIndex() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) { ++locationToStartingIndex[locationIndex]; } - // Sort all edges form the source location of the newly introduced edge by their action indices. - auto it = edges.begin(); - std::advance(it, locationToStartingIndex[edge.getSourceLocationIndex()]); - auto ite = edges.begin(); - std::advance(ite, locationToStartingIndex[edge.getSourceLocationIndex() + 1]); - std::sort(it, ite, [] (Edge const& a, Edge const& b) { return a.getActionIndex() < b.getActionIndex(); } ); - - // Update the set of action indices of this automaton. - actionIndices.insert(edge.getActionIndex()); + } std::vector& Automaton::getEdges() { - return edges; + return edges.getConcreteEdges(); } std::vector const& Automaton::getEdges() const { - return edges; + return edges.getConcreteEdges(); } std::set Automaton::getActionIndices() const { - std::set result; - for (auto const& edge : edges) { - result.insert(edge.getActionIndex()); - } - return result; + return edges.getActionIndices(); } uint64_t Automaton::getNumberOfLocations() const { @@ -426,35 +374,22 @@ namespace storm { this->setInitialStatesRestriction(this->getInitialStatesRestriction().substitute(substitution)); - for (auto& templateEdge : templateEdges) { - templateEdge->substitute(substitution); - } - for (auto& edge : this->getEdges()) { - edge.substitute(substitution); - } + edges.substitute(substitution); } void Automaton::registerTemplateEdge(std::shared_ptr const& te) { - templateEdges.insert(te); + edges.insertTemplateEdge(te); } void Automaton::changeAssignmentVariables(std::map> const& remapping) { for (auto& location : locations) { location.changeAssignmentVariables(remapping); } - for (auto& templateEdge : templateEdges) { - templateEdge->changeAssignmentVariables(remapping); - } + edges.changeAssignmentVariables(remapping); } void Automaton::finalize(Model const& containingModel) { //simplifyIndexedAssignments(); - templateEdges.clear(); - for (auto& edge : edges) { - templateEdges.insert(edge.getTemplateEdge()); - } - for (auto& templateEdge : templateEdges) { - templateEdge->finalize(containingModel); - } + edges.finalize(containingModel); } bool Automaton::containsVariablesOnlyInProbabilitiesOrTransientAssignments(std::set const& variables) const { @@ -481,9 +416,7 @@ namespace storm { } void Automaton::pushEdgeAssignmentsToDestinations() { - for (auto& templateEdge : templateEdges) { - templateEdge->pushAssignmentsToDestinations(); - } + edges.pushAssignmentsToDestinations(); } bool Automaton::hasTransientEdgeDestinationAssignments() const { @@ -496,25 +429,20 @@ namespace storm { } void Automaton::liftTransientEdgeDestinationAssignments() { - for (auto& templateEdge : templateEdges) { - templateEdge->liftTransientDestinationAssignments(); - } + edges.liftTransientDestinationAssignments(); } - void Automaton::simplifyIndexedAssignments() { - // TODO has to be fixed. - for (auto& edge : edges) { - edge.simplifyIndexedAssignments(variables); + bool Automaton::validate() const { + assert(locationToStartingIndex.size() == locations.size() + 1); + for(uint64_t i = 0; i < locations.size(); i++) { + assert(locationToStartingIndex[i] <= locationToStartingIndex[i+1]); } + return true; } + bool Automaton::usesAssignmentLevels() const { - for (auto const& edge : this->getEdges()) { - if (edge.usesAssignmentLevels()) { - return true; - } - } - return false; + return edges.usesAssignmentLevels(); } bool Automaton::isLinear() const { @@ -523,18 +451,16 @@ namespace storm { for (auto const& location : this->getLocations()) { result &= location.isLinear(); } - - for (auto const& templateEdge : templateEdges) { - result &= templateEdge->isLinear(); + if (result) { + return edges.isLinear(); } - - return result; + return false; } void Automaton::restrictToEdges(boost::container::flat_set const& edgeIndices) { - std::vector oldEdges = this->edges; + std::vector oldEdges = this->edges.getConcreteEdges(); - this->edges.clear(); + this->edges.clearConcreteEdges(); actionIndices.clear(); for (auto& e : locationToStartingIndex) { e = 0; diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h index 3ca635f7b..c549ecca8 100644 --- a/src/storm/storage/jani/Automaton.h +++ b/src/storm/storage/jani/Automaton.h @@ -7,6 +7,8 @@ #include #include "storm/storage/jani/VariableSet.h" +#include "storm/storage/jani/TemplateEdgeContainer.h" +#include "storm/storage/jani/EdgeContainer.h" namespace storm { @@ -16,73 +18,8 @@ namespace storm { class Edge; class TemplateEdge; class Location; - - namespace detail { - class Edges { - public: - typedef std::vector::iterator iterator; - typedef std::vector::const_iterator const_iterator; - - Edges(iterator it, iterator ite); - - /*! - * Retrieves an iterator to the edges. - */ - iterator begin() const; - - /*! - * Retrieves an end iterator to the edges. - */ - iterator end() const; - - /*! - * Determines whether this set of edges is empty. - */ - bool empty() const; - - /*! - * Retrieves the number of edges. - */ - std::size_t size() const; - - private: - iterator it; - iterator ite; - }; - - class ConstEdges { - public: - typedef std::vector::iterator iterator; - typedef std::vector::const_iterator const_iterator; - - ConstEdges(const_iterator it, const_iterator ite); - - /*! - * Retrieves an iterator to the edges. - */ - const_iterator begin() const; - - /*! - * Retrieves an end iterator to the edges. - */ - const_iterator end() const; - /*! - * Determines whether this set of edges is empty. - */ - bool empty() const; - /*! - * Retrieves the number of edges. - */ - std::size_t size() const; - - private: - const_iterator it; - const_iterator ite; - }; - } - class Model; class Automaton { @@ -262,6 +199,8 @@ namespace storm { * Adds an edge to the automaton. */ void addEdge(Edge const& edge); + + bool validate() const; /*! * Retrieves the edges of the automaton. @@ -401,10 +340,7 @@ namespace storm { std::unordered_map locationToIndex; /// All edges of the automaton - std::vector edges; - - /// The templates for the contained edges. - std::unordered_set> templateEdges; + EdgeContainer edges; /// A mapping from location indices to the starting indices. If l is mapped to i, it means that the edges /// leaving location l start at index i of the edges vector. diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp index 18fb35f4f..4460b2a65 100644 --- a/src/storm/storage/jani/Edge.cpp +++ b/src/storm/storage/jani/Edge.cpp @@ -116,8 +116,24 @@ namespace storm { } } + void Edge::setTemplateEdge(std::shared_ptr const& newTe) { + templateEdge = newTe; + uint64_t i = 0; + std::vector newdestinations; + + assert(destinations.size() == newTe->getNumberOfDestinations()); + for (auto& destination : destinations) { + newdestinations.emplace_back(destination.getLocationIndex(), destination.getProbability(), newTe->getDestination(i)); + //destination.updateTemplateEdgeDestination(newTe->getDestination(i)); + ++i; + } + destinations = newdestinations; + } + std::shared_ptr const& Edge::getTemplateEdge() { return templateEdge; } + + } } diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h index 5585296e6..002b97d40 100644 --- a/src/storm/storage/jani/Edge.h +++ b/src/storm/storage/jani/Edge.h @@ -112,6 +112,10 @@ namespace storm { void simplifyIndexedAssignments(VariableSet const& localVars); std::shared_ptr const& getTemplateEdge(); + + void setTemplateEdge(std::shared_ptr const& newTe); + + void assertValid() const; private: /// The index of the source location. diff --git a/src/storm/storage/jani/EdgeContainer.cpp b/src/storm/storage/jani/EdgeContainer.cpp new file mode 100644 index 000000000..b7a9ca1ec --- /dev/null +++ b/src/storm/storage/jani/EdgeContainer.cpp @@ -0,0 +1,200 @@ +#include "storm/storage/jani/EdgeContainer.h" +#include "storm/storage/jani/Edge.h" +#include "storm/storage/jani/TemplateEdge.h" +#include "storm/storage/jani/Variable.h" +#include "storm/storage/jani/Model.h" + + + +namespace storm { + namespace jani { + namespace detail { + Edges::Edges(iterator it, iterator ite) : it(it), ite(ite) { + // Intentionally left empty. + } + + Edges::iterator Edges::begin() const { + return it; + } + + Edges::iterator Edges::end() const { + return ite; + } + + bool Edges::empty() const { + return it == ite; + } + + std::size_t Edges::size() const { + return std::distance(it, ite); + } + + ConstEdges::ConstEdges(const_iterator it, const_iterator ite) : it(it), ite(ite) { + // Intentionally left empty. + } + + ConstEdges::const_iterator ConstEdges::begin() const { + return it; + } + + ConstEdges::const_iterator ConstEdges::end() const { + return ite; + } + + bool ConstEdges::empty() const { + return it == ite; + } + + std::size_t ConstEdges::size() const { + return std::distance(it, ite); + } + } + + EdgeContainer::EdgeContainer(EdgeContainer const& other) { + edges = other.getConcreteEdges(); + //templates = other.templates; + std::map, std::shared_ptr> map; + for (auto const& te : other.templates) { + auto newTe = std::make_shared(*te); + this->templates.insert(newTe); + map[te] = newTe; + } + + for (auto& e : edges) { + if(map.count(e.getTemplateEdge()) == 0) { + e.setTemplateEdge(std::make_shared(*(e.getTemplateEdge()))); + } else { + e.setTemplateEdge(map[e.getTemplateEdge()]); + } + } + + + + } + + void EdgeContainer::finalize(Model const& containingModel) { + templates.clear(); + for (auto& edge : edges) { + templates.insert(edge.getTemplateEdge()); + } + for (auto& templateEdge : templates) { + templateEdge->finalize(containingModel); + } + } + + void EdgeContainer::clearConcreteEdges() { + edges.clear(); + } + + void EdgeContainer::liftTransientDestinationAssignments() { + for (auto& templateEdge : templates) { + templateEdge->liftTransientDestinationAssignments(); + } + } + + void EdgeContainer::substitute(std::map const& substitution) { + for (auto& templateEdge : templates) { + templateEdge->substitute(substitution); + } + for (auto& edge : edges) { + edge.substitute(substitution); + } + } + + bool EdgeContainer::isLinear() const { + for (auto const& templateEdge : templates) { + if (!templateEdge->isLinear()) { + return false; + } + } + return true; + } + + + bool EdgeContainer::usesAssignmentLevels() const { + for (auto const& edge : edges) { + if (edge.usesAssignmentLevels()) { + return true; + } + } + return false; + + } + + + + std::vector & EdgeContainer::getConcreteEdges() { + return edges; + } + + std::vector const& EdgeContainer::getConcreteEdges() const { + return edges; + } + + std::set EdgeContainer::getActionIndices() const { + std::set result; + for (auto const& edge : edges) { + result.insert(edge.getActionIndex()); + } + return result; + } + + /** + * Insert an edge, then sort the range between locstart and locend according to the action index. + * @param e + * @param locStart index where to start + * @param locEnd index where to end + */ + void EdgeContainer::insertEdge(Edge const &e, uint64_t locStart, uint64_t locEnd) { + assert(locStart <= locEnd); + // Find the right position for the edge and insert it properly. + auto posIt = edges.begin(); + std::advance(posIt, locEnd); + edges.insert(posIt, e); + + // Sort all edges form the source location of the newly introduced edge by their action indices. + auto it = edges.begin(); + std::advance(it, locStart); + auto ite = edges.begin(); + std::advance(ite, locEnd + 1); + std::sort(it, ite, [] (Edge const& a, Edge const& b) { return a.getActionIndex() < b.getActionIndex(); } ); + + } + + void EdgeContainer::insertTemplateEdge(std::shared_ptr const &te) { + templates.insert(te); + } + + void EdgeContainer::pushAssignmentsToDestinations() { + for (auto& templateEdge : templates) { + templateEdge->pushAssignmentsToDestinations(); + } + } + + void EdgeContainer::changeAssignmentVariables(std::map> const& remapping) { + for (auto& templateEdge : templates) { + templateEdge->changeAssignmentVariables(remapping); + } + } + + size_t EdgeContainer::size() const { + return edges.size(); + } + + EdgeContainer::iterator EdgeContainer::begin() { + return edges.begin(); + } + EdgeContainer::iterator EdgeContainer::end() { + return edges.end(); + } + EdgeContainer::const_iterator EdgeContainer::begin() const { + return edges.begin(); + } + EdgeContainer::const_iterator EdgeContainer::end() const { + return edges.end(); + } + + + + } +} \ No newline at end of file diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h new file mode 100644 index 000000000..f4738e1e0 --- /dev/null +++ b/src/storm/storage/jani/EdgeContainer.h @@ -0,0 +1,125 @@ +#pragma once + +#include +#include +#include +#include "storm/storage/expressions/Expression.h" +#include "storm/storage/jani/TemplateEdgeContainer.h" + +namespace storm { + namespace jani { + + class Edge; + class TemplateEdge; + class Variable; + class Model; + + namespace detail { + class Edges { + public: + typedef std::vector::iterator iterator; + typedef std::vector::const_iterator const_iterator; + + Edges(iterator it, iterator ite); + + /*! + * Retrieves an iterator to the edges. + */ + iterator begin() const; + + /*! + * Retrieves an end iterator to the edges. + */ + iterator end() const; + + /*! + * Determines whether this set of edges is empty. + */ + bool empty() const; + + /*! + * Retrieves the number of edges. + */ + std::size_t size() const; + + private: + iterator it; + iterator ite; + }; + + + class ConstEdges { + public: + typedef std::vector::iterator iterator; + typedef std::vector::const_iterator const_iterator; + + ConstEdges(const_iterator it, const_iterator ite); + + /*! + * Retrieves an iterator to the edges. + */ + const_iterator begin() const; + + /*! + * Retrieves an end iterator to the edges. + */ + const_iterator end() const; + + /*! + * Determines whether this set of edges is empty. + */ + bool empty() const; + + /*! + * Retrieves the number of edges. + */ + std::size_t size() const; + + private: + const_iterator it; + const_iterator ite; + }; + } + + + class EdgeContainer { + public: + + typedef std::vector::iterator iterator; + typedef std::vector::const_iterator const_iterator; + + + EdgeContainer() = default; + EdgeContainer(EdgeContainer const& other); + + void clearConcreteEdges(); + std::vector const& getConcreteEdges() const; + std::vector & getConcreteEdges(); + size_t size() const; + + iterator begin(); + const_iterator begin() const; + iterator end(); + const_iterator end() const; + + std::set getActionIndices() const; + + void substitute(std::map const& substitution); + void liftTransientDestinationAssignments(); + void pushAssignmentsToDestinations(); + void insertEdge(Edge const& e, uint64_t locStart, uint64_t locEnd); + void insertTemplateEdge(std::shared_ptr const& te); + bool isLinear() const; + bool usesAssignmentLevels() const; + void finalize(Model const& containingModel); + + void changeAssignmentVariables(std::map> const& remapping); + + + private: + std::vector edges; + TemplateEdgeContainer templates; + }; + } +} + diff --git a/src/storm/storage/jani/EdgeDestination.cpp b/src/storm/storage/jani/EdgeDestination.cpp index 81efbfff5..62b92c1f0 100644 --- a/src/storm/storage/jani/EdgeDestination.cpp +++ b/src/storm/storage/jani/EdgeDestination.cpp @@ -58,5 +58,9 @@ namespace storm { TemplateEdgeDestination const& EdgeDestination::getTemplateEdgeDestination() const { return templateEdgeDestination.get(); } + + void EdgeDestination::updateTemplateEdgeDestination(TemplateEdgeDestination const& newTed) { + templateEdgeDestination = newTed; + } } } diff --git a/src/storm/storage/jani/EdgeDestination.h b/src/storm/storage/jani/EdgeDestination.h index 7cefe9c7a..62dd6114e 100644 --- a/src/storm/storage/jani/EdgeDestination.h +++ b/src/storm/storage/jani/EdgeDestination.h @@ -66,6 +66,8 @@ namespace storm { * Retrieves the template destination for this destination. */ TemplateEdgeDestination const& getTemplateEdgeDestination() const; + + void updateTemplateEdgeDestination(TemplateEdgeDestination const& newTed); private: // The index of the destination location. diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index da95f426f..47533126c 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -212,11 +212,14 @@ namespace storm { if (!SynchronizationVector::isNoActionInput(actionName)) { components.push_back(i); uint64_t actionIndex = oldModel.getActionIndex(actionName); + // store that automaton occurs in the sync vector. participatingAutomataAndActions.push_back(std::make_pair(composedAutomata[i], actionIndex)); + // Store for later that this action is one of the possible actions that synchronise synchronizingActionIndices[i].insert(actionIndex); } } - + + // What is the action label that should be attached to the composed actions uint64_t resultingActionIndex = Model::SILENT_ACTION_INDEX; if (vector.getOutput() != Model::SILENT_ACTION_NAME) { if (newModel.hasAction(vector.getOutput())) { diff --git a/src/storm/storage/jani/TemplateEdgeContainer.cpp b/src/storm/storage/jani/TemplateEdgeContainer.cpp new file mode 100644 index 000000000..81ce8f874 --- /dev/null +++ b/src/storm/storage/jani/TemplateEdgeContainer.cpp @@ -0,0 +1,12 @@ +#include "storm/storage/jani/TemplateEdgeContainer.h" +#include "storm/storage/jani/TemplateEdge.h" + +namespace storm { + namespace jani { + TemplateEdgeContainer::TemplateEdgeContainer(TemplateEdgeContainer const &other) { + for (auto const& te : other) { + this->insert(std::make_shared(*te)); + } + } + } +} \ No newline at end of file diff --git a/src/storm/storage/jani/TemplateEdgeContainer.h b/src/storm/storage/jani/TemplateEdgeContainer.h new file mode 100644 index 000000000..293302594 --- /dev/null +++ b/src/storm/storage/jani/TemplateEdgeContainer.h @@ -0,0 +1,16 @@ +#pragma once + +#include +#include + +namespace storm { + namespace jani { + + class TemplateEdge; + + struct TemplateEdgeContainer : public std::unordered_set> { + TemplateEdgeContainer() = default; + TemplateEdgeContainer(TemplateEdgeContainer const& other); + }; + } +} \ No newline at end of file