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,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).

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::shared_ptr<storm::logic::Formula const>>(), std::cout, false);

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();

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);

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;

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<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

@@ -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.