From 5aca2a432d8f6fc9dea2923177c8b74fd7b815b5 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 9 Dec 2016 22:04:20 +0100 Subject: [PATCH] towards template edges --- src/storm/storage/jani/EdgeDestination.cpp | 28 ++++--------- src/storm/storage/jani/EdgeDestination.h | 34 +++++++-------- src/storm/storage/jani/TemplateEdge.cpp | 3 ++ src/storm/storage/jani/TemplateEdge.h | 7 ++-- .../storage/jani/TemplateEdgeDestination.cpp | 31 ++++++++++++++ .../storage/jani/TemplateEdgeDestination.h | 42 +++++++++++++++++++ 6 files changed, 103 insertions(+), 42 deletions(-) create mode 100644 src/storm/storage/jani/TemplateEdgeDestination.cpp create mode 100644 src/storm/storage/jani/TemplateEdgeDestination.h diff --git a/src/storm/storage/jani/EdgeDestination.cpp b/src/storm/storage/jani/EdgeDestination.cpp index 77e2e7a78..ba35aabe5 100644 --- a/src/storm/storage/jani/EdgeDestination.cpp +++ b/src/storm/storage/jani/EdgeDestination.cpp @@ -6,22 +6,10 @@ namespace storm { namespace jani { - EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, OrderedAssignments const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) { - // Intentionally left empty. - } - - EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, Assignment const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) { - // Intentionally left empty. - } - - EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) { + EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::shared_ptr const& templateEdgeDestination) : locationIndex(locationIndex), probability(probability), templateEdgeDestination(templateEdgeDestination) { // Intentionally left empty. } - void EdgeDestination::addAssignment(Assignment const& assignment) { - assignments.add(assignment); - } - uint64_t EdgeDestination::getLocationIndex() const { return locationIndex; } @@ -45,24 +33,19 @@ namespace storm { } OrderedAssignments const& EdgeDestination::getOrderedAssignments() const { - return assignments; + return templateEdgeDestination->getOrderedAssignments(); } void EdgeDestination::substitute(std::map const& substitution) { this->setProbability(this->getProbability().substitute(substitution)); - assignments.substitute(substitution); } bool EdgeDestination::hasAssignment(Assignment const& assignment) const { - return assignments.contains(assignment); - } - - bool EdgeDestination::removeAssignment(Assignment const& assignment) { - return assignments.remove(assignment); + return this->getOrderedAssignments().contains(assignment); } bool EdgeDestination::hasTransientAssignment() const { - return !assignments.getTransientAssignments().empty(); + return !this->getOrderedAssignments().getTransientAssignments().empty(); } bool EdgeDestination::usesAssignmentLevels() const { @@ -72,5 +55,8 @@ namespace storm { return this->getOrderedAssignments().getLowestLevel() != 0 || this->getOrderedAssignments().getHighestLevel() != 0; } + std::shared_ptr EdgeDestination::getTemplateEdgeDestination() const { + return templateEdgeDestination; + } } } diff --git a/src/storm/storage/jani/EdgeDestination.h b/src/storm/storage/jani/EdgeDestination.h index 8fba514c2..a9dcb4bdd 100644 --- a/src/storm/storage/jani/EdgeDestination.h +++ b/src/storm/storage/jani/EdgeDestination.h @@ -4,7 +4,7 @@ #include "storm/storage/expressions/Expression.h" -#include "storm/storage/jani/OrderedAssignments.h" +#include "storm/storage/jani/TemplateEdgeDestination.h" namespace storm { namespace jani { @@ -14,16 +14,8 @@ namespace storm { /*! * Creates a new edge destination. */ - EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, OrderedAssignments const& assignments); - - EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, Assignment const& assignment); - EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector const& assignments = {}); - - /*! - * Additionally performs the given assignment when choosing this destination. - */ - void addAssignment(Assignment const& assignment); - + EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::shared_ptr const& templateEdgeDestination); + /*! * Retrieves the id of the destination location. */ @@ -39,6 +31,11 @@ namespace storm { */ void setProbability(storm::expressions::Expression const& probability); + /*! + * Substitutes all variables in all expressions according to the given substitution. + */ + void substitute(std::map const& substitution); + /*! * Retrieves the mapping from variables to their assigned expressions that corresponds to the assignments * of this destination. @@ -51,13 +48,9 @@ namespace storm { OrderedAssignments const& getOrderedAssignments() const; /*! - * Substitutes all variables in all expressions according to the given substitution. + * Checks whether this destination has the given assignment. */ - void substitute(std::map const& substitution); - - // Convenience methods to access the assignments. bool hasAssignment(Assignment const& assignment) const; - bool removeAssignment(Assignment const& assignment); /*! * Retrieves whether this destination has transient assignments. @@ -69,6 +62,11 @@ namespace storm { */ bool usesAssignmentLevels() const; + /*! + * Retrieves the template destination for this destination. + */ + std::shared_ptr getTemplateEdgeDestination() const; + private: // The index of the destination location. uint64_t locationIndex; @@ -76,8 +74,8 @@ namespace storm { // The probability to go to the destination. storm::expressions::Expression probability; - // The (ordered) assignments to make when choosing this destination. - OrderedAssignments assignments; + // The template edge destination + std::shared_ptr templateEdgeDestination; }; } diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp index fd88f83c3..89fa3c24b 100644 --- a/src/storm/storage/jani/TemplateEdge.cpp +++ b/src/storm/storage/jani/TemplateEdge.cpp @@ -3,6 +3,9 @@ namespace storm { namespace jani { + TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard, std::vector> destinations) : guard(guard), destinations(destinations) { + // Intentionally left empty. + } } diff --git a/src/storm/storage/jani/TemplateEdge.h b/src/storm/storage/jani/TemplateEdge.h index b03d9d043..bc18c16a6 100644 --- a/src/storm/storage/jani/TemplateEdge.h +++ b/src/storm/storage/jani/TemplateEdge.h @@ -1,10 +1,11 @@ #pragma once #include +#include #include "storm/storage/expressions/Expression.h" -#include "storm/storage/jani/EdgeDestination.h" +#include "storm/storage/jani/TemplateEdgeDestination.h" namespace storm { namespace jani { @@ -12,14 +13,14 @@ namespace storm { class TemplateEdge { public: TemplateEdge() = default; - TemplateEdge(storm::expressions::Expression const& guard, std::vector destinations = {}); + TemplateEdge(storm::expressions::Expression const& guard, std::vector> destinations = {}); private: // The guard of the template edge. storm::expressions::Expression guard; // The destinations of the template edge. - std::vector destinations; + std::vector> destinations; }; } diff --git a/src/storm/storage/jani/TemplateEdgeDestination.cpp b/src/storm/storage/jani/TemplateEdgeDestination.cpp new file mode 100644 index 000000000..10f9758b5 --- /dev/null +++ b/src/storm/storage/jani/TemplateEdgeDestination.cpp @@ -0,0 +1,31 @@ +#include "storm/storage/jani/TemplateEdgeDestination.h" + +namespace storm { + namespace jani { + + TemplateEdgeDestination::TemplateEdgeDestination(OrderedAssignments const& assignments) : assignments(assignments) { + // Intentionally left empty. + } + + TemplateEdgeDestination::TemplateEdgeDestination(Assignment const& assignment) : assignments(assignment) { + // Intentionally left empty. + } + + TemplateEdgeDestination::TemplateEdgeDestination(std::vector const& assignments) : assignments(assignments) { + // Intentionally left empty. + } + + void TemplateEdgeDestination::substitute(std::map const& substitution) { + assignments.substitute(substitution); + } + + OrderedAssignments const& TemplateEdgeDestination::getOrderedAssignments() const { + return assignments; + } + + bool TemplateEdgeDestination::removeAssignment(Assignment const& assignment) { + return assignments.remove(assignment); + } + + } +} diff --git a/src/storm/storage/jani/TemplateEdgeDestination.h b/src/storm/storage/jani/TemplateEdgeDestination.h new file mode 100644 index 000000000..c5b369a3d --- /dev/null +++ b/src/storm/storage/jani/TemplateEdgeDestination.h @@ -0,0 +1,42 @@ +#pragma once + +#include "storm/storage/jani/OrderedAssignments.h" + +namespace storm { + namespace jani { + + class TemplateEdgeDestination { + public: + TemplateEdgeDestination() = default; + TemplateEdgeDestination(OrderedAssignments const& assignments); + TemplateEdgeDestination(Assignment const& assignment); + TemplateEdgeDestination(std::vector const& assignments = {}); + + /*! + * Substitutes all variables in all expressions according to the given substitution. + */ + void substitute(std::map const& substitution); + + OrderedAssignments const& getOrderedAssignments() const; + + // Convenience methods to access the assignments. + bool hasAssignment(Assignment const& assignment) const; + bool removeAssignment(Assignment const& assignment); + + /*! + * Retrieves whether this destination has transient assignments. + */ + bool hasTransientAssignment() const; + + /*! + * Retrieves whether the edge uses an assignment level other than zero. + */ + bool usesAssignmentLevels() const; + + private: + // The (ordered) assignments to make when choosing this destination. + OrderedAssignments assignments; + }; + + } +}