From 269041feda1cdcc469329985f16375df6d1ea458 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 23 Sep 2016 21:02:39 +0200 Subject: [PATCH] implemented lifting edge-destination assignments to edges as a JANI preprocessing step Former-commit-id: 2aea0d3eb77f9edf29053302acf8211e80ab35ce [formerly 6e16d3336d8c542d349fc9ce726bd3b3c73da553] Former-commit-id: 04843c974987128535d9c6b8815c61ceed2d166e --- src/adapters/DereferenceIteratorAdapter.h | 10 +++++++++- src/builder/DdJaniModelBuilder.cpp | 2 ++ src/generator/JaniNextStateGenerator.cpp | 1 + src/storage/SymbolicModelDescription.cpp | 9 +++++++-- src/storage/jani/Automaton.cpp | 15 +++++++++++++++ src/storage/jani/Automaton.h | 10 ++++++++++ src/storage/jani/Edge.cpp | 9 +++++++++ src/storage/jani/Edge.h | 5 +++++ src/storage/jani/EdgeDestination.cpp | 4 ++++ src/storage/jani/EdgeDestination.h | 5 +++++ src/storage/jani/Model.cpp | 15 +++++++++++++++ src/storage/jani/Model.h | 12 ++++++++++-- 12 files changed, 92 insertions(+), 5 deletions(-) diff --git a/src/adapters/DereferenceIteratorAdapter.h b/src/adapters/DereferenceIteratorAdapter.h index 16ac0834e..9a6e2b4fc 100644 --- a/src/adapters/DereferenceIteratorAdapter.h +++ b/src/adapters/DereferenceIteratorAdapter.h @@ -37,10 +37,18 @@ namespace storm { return boost::make_transform_iterator(it, Dereferencer()); } + bool empty() const { + return it == ite; + } + + std::size_t size() const { + return std::distance(it, ite); + } + private: input_iterator it; input_iterator ite; }; } -} \ No newline at end of file +} diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp index 98f075bac..ee1f0d669 100644 --- a/src/builder/DdJaniModelBuilder.cpp +++ b/src/builder/DdJaniModelBuilder.cpp @@ -1749,6 +1749,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " << boost::join(strings, ", ") << "."); } + STORM_LOG_THROW(!model.hasTransientEdgeDestinationAssignments(), storm::exceptions::WrongFormatException, "The symbolic JANI model builder currently does not support transient edge destination assignments."); + // Determine the actions that will appear in the parallel composition. storm::jani::CompositionInformationVisitor visitor(model, model.getSystemComposition()); storm::jani::CompositionInformation actionInformation = visitor.getInformation(); diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp index 49efb76d1..b84ffca3c 100644 --- a/src/generator/JaniNextStateGenerator.cpp +++ b/src/generator/JaniNextStateGenerator.cpp @@ -25,6 +25,7 @@ namespace storm { JaniNextStateGenerator::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) { STORM_LOG_THROW(model.hasStandardComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions."); STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables."); + STORM_LOG_THROW(!model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); // Only after checking validity of the program, we initialize the variable information. diff --git a/src/storage/SymbolicModelDescription.cpp b/src/storage/SymbolicModelDescription.cpp index 1058e464f..ccbb7c25b 100644 --- a/src/storage/SymbolicModelDescription.cpp +++ b/src/storage/SymbolicModelDescription.cpp @@ -71,7 +71,12 @@ namespace storm { SymbolicModelDescription SymbolicModelDescription::preprocess(std::string const& constantDefinitionString) const { if (this->isJaniModel()) { std::map substitution = storm::utility::jani::parseConstantDefinitionString(this->asJaniModel(), constantDefinitionString); - return SymbolicModelDescription(this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants()); + storm::jani::Model preparedModel = this->asJaniModel().defineUndefinedConstants(substitution).substituteConstants(); + if (preparedModel.hasTransientEdgeDestinationAssignments()) { + STORM_LOG_WARN("JANI model has transient edge-destinations assignments, which are currently not supported. Trying to lift these assignments to edges rather than destinations."); + preparedModel.liftTransientEdgeDestinationAssignments(); + } + return SymbolicModelDescription(preparedModel); } else if (this->isPrismProgram()) { std::map substitution = storm::utility::prism::parseConstantDefinitionString(this->asPrismProgram(), constantDefinitionString); return SymbolicModelDescription(this->asPrismProgram().defineUndefinedConstants(substitution).substituteConstants()); @@ -80,4 +85,4 @@ namespace storm { } } -} \ No newline at end of file +} diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index fcb843112..8e99f25c1 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -439,5 +439,20 @@ namespace storm { edge.pushAssignmentsToDestinations(); } } + + bool Automaton::hasTransientEdgeDestinationAssignments() const { + for (auto const& edge : this->getEdges()) { + if (edge.hasTransientEdgeDestinationAssignments()) { + return true; + } + } + return false; + } + + void Automaton::liftTransientEdgeDestinationAssignments() { + for (auto& edge : this->getEdges()) { + edge.liftTransientDestinationAssignments(); + } + } } } diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index 19659a091..5ae609853 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -317,6 +317,16 @@ namespace storm { void pushEdgeAssignmentsToDestinations(); + /*! + * Retrieves whether there is any transient edge destination assignment in the automaton. + */ + bool hasTransientEdgeDestinationAssignments() const; + + /*! + * Lifts the common edge destination assignments to edge assignments. + */ + void liftTransientEdgeDestinationAssignments(); + private: /// The name of the automaton. std::string name; diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp index f8d7e031d..69c85db59 100644 --- a/src/storage/jani/Edge.cpp +++ b/src/storage/jani/Edge.cpp @@ -137,5 +137,14 @@ namespace storm { } return false; } + + bool Edge::hasTransientEdgeDestinationAssignments() const { + for (auto const& destination : this->getDestinations()) { + if (destination.hasTransientAssignment()) { + return true; + } + } + return false; + } } } diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h index 7f6172bc8..de4becb3e 100644 --- a/src/storage/jani/Edge.h +++ b/src/storage/jani/Edge.h @@ -116,6 +116,11 @@ namespace storm { */ bool usesVariablesInNonTransientAssignments(std::set const& variables) const; + /*! + * Retrieves whether there is any transient edge destination assignment in the edge. + */ + bool hasTransientEdgeDestinationAssignments() const; + private: /// The index of the source location. uint64_t sourceLocationIndex; diff --git a/src/storage/jani/EdgeDestination.cpp b/src/storage/jani/EdgeDestination.cpp index 8bd3415bc..b5c785c05 100644 --- a/src/storage/jani/EdgeDestination.cpp +++ b/src/storage/jani/EdgeDestination.cpp @@ -51,5 +51,9 @@ namespace storm { return assignments.remove(assignment); } + bool EdgeDestination::hasTransientAssignment() const { + return !assignments.getTransientAssignments().empty(); + } + } } diff --git a/src/storage/jani/EdgeDestination.h b/src/storage/jani/EdgeDestination.h index 628be0efe..c9e5e5e64 100644 --- a/src/storage/jani/EdgeDestination.h +++ b/src/storage/jani/EdgeDestination.h @@ -53,6 +53,11 @@ namespace storm { bool hasAssignment(Assignment const& assignment) const; bool removeAssignment(Assignment const& assignment); + /*! + * Retrieves whether this destination has transient assignments. + */ + bool hasTransientAssignment() const; + private: // The index of the destination location. uint64_t locationIndex; diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 5c6dbf273..343d88d78 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -520,5 +520,20 @@ namespace storm { automaton.pushEdgeAssignmentsToDestinations(); } } + + void Model::liftTransientEdgeDestinationAssignments() { + for (auto& automaton : this->getAutomata()) { + automaton.liftTransientEdgeDestinationAssignments(); + } + } + + bool Model::hasTransientEdgeDestinationAssignments() const { + for (auto const& automaton : this->getAutomata()) { + if (automaton.hasTransientEdgeDestinationAssignments()) { + return true; + } + } + return false; + } } } diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 60b6b6546..9a941a48f 100644 --- a/src/storage/jani/Model.h +++ b/src/storage/jani/Model.h @@ -17,8 +17,6 @@ namespace storm { class Exporter; - - class Model { public: friend class Exporter; @@ -335,6 +333,16 @@ namespace storm { */ bool undefinedConstantsAreGraphPreserving() const; + /*! + * Lifts the common edge destination assignments to edge assignments. + */ + void liftTransientEdgeDestinationAssignments(); + + /*! + * Retrieves whether there is any transient edge destination assignment in the model. + */ + bool hasTransientEdgeDestinationAssignments() const; + void makeStandardJaniCompliant(); /// The name of the silent action.