export standard compliant jani by moving destinations outwards

Former-commit-id: 12f9f7ba89 [formerly ef23fb88bf]
Former-commit-id: 8b749c0b60

src/cli/cli.cpp

@@ -223,7 +223,13 @@ namespace storm {
                 }
                 
                 if(model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
-                    storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+                    if (storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isExportAsStandardJaniSet()) {
+                        storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel());
+                        normalisedModel.makeStandardJaniCompliant();
+                        storm::jani::JsonExporter::toFile(normalisedModel, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+                    } else {
+                        storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+                    }
                 }
                 
                 // Get the string that assigns values to the unknown currently undefined constants in the model.

src/settings/modules/JaniExportSettings.cpp

@@ -16,10 +16,13 @@ namespace storm {
             
             const std::string JaniExportSettings::janiFileOptionName = "jani-output";
             const std::string JaniExportSettings::janiFileOptionShortName = "output";
+            const std::string JaniExportSettings::standardCompliantOptionName = "standard-compliant";
+            const std::string JaniExportSettings::standardCompliantOptionShortName = "standard";
 
             
             JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, janiFileOptionName, false, "Destination for the jani model.").setShortName(janiFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, standardCompliantOptionName, false, "Export in standard compliant variant.").setShortName(standardCompliantOptionShortName).build());
             }
             
             bool JaniExportSettings::isJaniFileSet() const {
@@ -30,6 +33,10 @@ namespace storm {
                 return this->getOption(janiFileOptionName).getArgumentByName("filename").getValueAsString();
             }
             
+            bool JaniExportSettings::isExportAsStandardJaniSet() const {
+                return this->getOption(standardCompliantOptionName).getHasOptionBeenSet();
+            }
+            
             void JaniExportSettings::finalize() {
                 
             }

src/settings/modules/JaniExportSettings.h

@@ -24,6 +24,8 @@ namespace storm {
                  */
                 std::string getJaniFilename() const;
                 
+                bool isExportAsStandardJaniSet() const;
+                
                 bool check() const override;
                 void finalize() override;
                 
@@ -32,6 +34,9 @@ namespace storm {
             private:
                 static const std::string janiFileOptionName;
                 static const std::string janiFileOptionShortName;
+                static const std::string standardCompliantOptionName;
+                static const std::string standardCompliantOptionShortName;
+                
             };
         }
     }

src/storage/jani/Automaton.cpp

@@ -429,5 +429,11 @@ namespace storm {
             
             return true;
         }
+        
+        void Automaton::pushEdgeAssignmentsToDestinations() {
+            for (auto& edge : edges) {
+                edge.pushAssignmentsToDestinations();
+            }
+        }
     }
 }

src/storage/jani/Automaton.h

@@ -315,6 +315,8 @@ namespace storm {
              */
             bool containsVariablesOnlyInProbabilitiesOrTransientAssignments(std::set<storm::expressions::Variable> const& variables) const;
             
+            void pushEdgeAssignmentsToDestinations();
+            
         private:
             /// The name of the automaton.
             std::string name;

src/storage/jani/Edge.cpp

@@ -113,6 +113,16 @@ namespace storm {
             }
         }
         
+        void Edge::pushAssignmentsToDestinations() {
+            assert(!destinations.empty());
+            for (auto const& assignment : this->getAssignments()) {
+                for (auto& destination : destinations) {
+                    destination.addAssignment(assignment);
+                }
+            }
+            assignments = OrderedAssignments();
+        }
+        
         boost::container::flat_set<storm::expressions::Variable> const& Edge::getWrittenGlobalVariables() const {
             return writtenGlobalVariables;
         }

src/storage/jani/Edge.h

@@ -106,6 +106,11 @@ namespace storm {
              */
             void liftTransientDestinationAssignments();
             
+            /**
+             * Shifts the assingments from the edges to the destinations.
+             */
+            void pushAssignmentsToDestinations();
+            
             /*!
              * Checks whether the provided variables appear on the right-hand side of non-transient assignments.
              */

src/storage/jani/Model.cpp

@@ -510,6 +510,11 @@ namespace storm {
             }
             return true;
         }
-        
+     
+        void Model::makeStandardJaniCompliant() {
+            for (auto& automaton : automata) {
+                automaton.pushEdgeAssignmentsToDestinations();
+            }
+        }
     }
 }

src/storage/jani/Model.h

@@ -335,6 +335,8 @@ namespace storm {
              */
             bool undefinedConstantsAreGraphPreserving() const;
             
+            void makeStandardJaniCompliant();
+            
             /// The name of the silent action.
             static const std::string SILENT_ACTION_NAME;