From 0f8e00a80ed74522dd57fb622acebea081890c87 Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 8 Feb 2017 22:18:12 +0100 Subject: [PATCH] action reusal in syncvectors is not invalid jani, but not properly supported. Changed error message accordingly, allows for changes in model generators --- src/storm/builder/DdJaniModelBuilder.cpp | 3 ++- .../jit/ExplicitJitJaniModelBuilder.cpp | 3 ++- .../generator/JaniNextStateGenerator.cpp | 4 +++- src/storm/storage/jani/Model.cpp | 9 +++++++- src/storm/storage/jani/Model.h | 6 +++++ .../storage/jani/ParallelComposition.cpp | 22 +++++++++++++++---- src/storm/storage/jani/ParallelComposition.h | 3 ++- 7 files changed, 41 insertions(+), 9 deletions(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index 33ee40758..2c308559c 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -1814,7 +1814,8 @@ namespace storm { } STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support assignment levels."); - + STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidSettingsException, "The symbolic JANI model builder currently does not support reusing actions in parallel composition"); + storm::jani::Model preparedModel = model; // Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway). diff --git a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp index ce2bd80c1..15805419b 100644 --- a/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp +++ b/src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp @@ -131,7 +131,8 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed."); } #endif - + STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition"); + // Comment this in to print the JANI model for debugging purposes. // this->model.makeStandardJaniCompliant(); // storm::jani::JsonExporter::toStream(this->model, std::vector>(), std::cout, false); diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp index b5a3d420b..d53974178 100644 --- a/src/storm/generator/JaniNextStateGenerator.cpp +++ b/src/storm/generator/JaniNextStateGenerator.cpp @@ -28,7 +28,9 @@ namespace storm { 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.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support assignment levels."); STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels."); - + STORM_LOG_THROW(!model.reusesActionsInComposition(), storm::exceptions::InvalidArgumentException, "The jit JANI model builder currently does not support reusing actions in parallel composition"); + + // Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway). if (this->model.hasTransientEdgeDestinationAssignments()) { this->model.liftTransientEdgeDestinationAssignments(); diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 193e7388d..083b8f7fb 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1132,7 +1132,14 @@ namespace storm { return result; } - + + bool Model::reusesActionsInComposition() const { + if(composition->isParallelComposition()) { + return composition->asParallelComposition().areActionsReused(); + } + return false; + } + Model Model::createModelFromAutomaton(Automaton const& automaton) const { // Copy the full model Model newModel(*this); diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index dffefef76..e942743bd 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -429,6 +429,12 @@ namespace storm { bool isLinear() const; void makeStandardJaniCompliant(); + + /*! + * Checks whether in the composition, actions are reused: That is, if the model is put in parallel composition and the same action potentially leads to multiple edges from the same state. + * @return + */ + bool reusesActionsInComposition() const; /// The name of the silent action. static const std::string SILENT_ACTION_NAME; diff --git a/src/storm/storage/jani/ParallelComposition.cpp b/src/storm/storage/jani/ParallelComposition.cpp index d08ddaab4..1eaa0ff08 100644 --- a/src/storm/storage/jani/ParallelComposition.cpp +++ b/src/storm/storage/jani/ParallelComposition.cpp @@ -188,18 +188,32 @@ namespace storm { std::size_t ParallelComposition::getNumberOfSynchronizationVectors() const { return synchronizationVectors.size(); } - - void ParallelComposition::checkSynchronizationVectors() const { + + bool ParallelComposition::areActionsReused() const { for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) { std::set actions; for (auto const& vector : synchronizationVectors) { - STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size."); std::string const& action = vector.getInput(inputIndex); if (action != SynchronizationVector::NO_ACTION_INPUT) { - STORM_LOG_THROW(actions.find(action) == actions.end(), storm::exceptions::WrongFormatException, "Cannot use the same action ('" << action << "') multiple times as input for index " << inputIndex << " in synchronization vectors."); + return true; actions.insert(action); } } + // And check recursively, in case we have nested parallel composition + if (subcompositions.at(inputIndex)->isParallelComposition()) { + if(subcompositions.at(inputIndex)->asParallelComposition().areActionsReused()) { + return true; + } + } + } + return false; + } + + void ParallelComposition::checkSynchronizationVectors() const { + for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) { + for (auto const& vector : synchronizationVectors) { + STORM_LOG_THROW(vector.size() == this->subcompositions.size(), storm::exceptions::WrongFormatException, "Synchronization vectors must match parallel composition size."); + } } for (auto const& vector : synchronizationVectors) { diff --git a/src/storm/storage/jani/ParallelComposition.h b/src/storm/storage/jani/ParallelComposition.h index 3dbad1aa6..c3d41717c 100644 --- a/src/storm/storage/jani/ParallelComposition.h +++ b/src/storm/storage/jani/ParallelComposition.h @@ -124,7 +124,8 @@ namespace storm { virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override; virtual void write(std::ostream& stream) const override; - + + bool areActionsReused() const; private: /*! * Checks the synchronization vectors for validity.