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

@@ -1814,6 +1814,7 @@ 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;
             

src/storm/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -131,6 +131,7 @@ 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();

src/storm/generator/JaniNextStateGenerator.cpp

@@ -28,6 +28,8 @@ 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()) {

src/storm/storage/jani/Model.cpp

@@ -1133,6 +1133,13 @@ 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);

src/storm/storage/jani/Model.h

@@ -430,6 +430,12 @@ namespace storm {
             
             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;
             

src/storm/storage/jani/ParallelComposition.cpp

@@ -189,17 +189,31 @@ namespace storm {
             return synchronizationVectors.size();
         }
 
-        void ParallelComposition::checkSynchronizationVectors() const {
+        bool ParallelComposition::areActionsReused() const {
             for (uint_fast64_t inputIndex = 0; inputIndex < subcompositions.size(); ++ inputIndex) {
                 std::set<std::string> 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) {

src/storm/storage/jani/ParallelComposition.h

@@ -125,6 +125,7 @@ namespace storm {
             
             virtual void write(std::ostream& stream) const override;
 
+            bool areActionsReused() const;
         private:
             /*!
              * Checks the synchronization vectors for validity.