diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp index 6b4c93fdf..2c5104123 100644 --- a/src/cli/cli.cpp +++ b/src/cli/cli.cpp @@ -223,7 +223,13 @@ namespace storm { } if(model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { - storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule().getJaniFilename()); + if (storm::settings::getModule().isExportAsStandardJaniSet()) { + storm::jani::Model normalisedModel = storm::jani::Model(model.asJaniModel()); + normalisedModel.makeStandardJaniCompliant(); + storm::jani::JsonExporter::toFile(normalisedModel, storm::settings::getModule().getJaniFilename()); + } else { + storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule().getJaniFilename()); + } } // Get the string that assigns values to the unknown currently undefined constants in the model. diff --git a/src/settings/modules/JaniExportSettings.cpp b/src/settings/modules/JaniExportSettings.cpp index faa68b0b0..a702f6117 100644 --- a/src/settings/modules/JaniExportSettings.cpp +++ b/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() { } diff --git a/src/settings/modules/JaniExportSettings.h b/src/settings/modules/JaniExportSettings.h index dc356189a..83b77d15a 100644 --- a/src/settings/modules/JaniExportSettings.h +++ b/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; + }; } } diff --git a/src/storage/jani/Automaton.cpp b/src/storage/jani/Automaton.cpp index 1655933bb..8341cbc6e 100644 --- a/src/storage/jani/Automaton.cpp +++ b/src/storage/jani/Automaton.cpp @@ -429,5 +429,11 @@ namespace storm { return true; } + + void Automaton::pushEdgeAssignmentsToDestinations() { + for (auto& edge : edges) { + edge.pushAssignmentsToDestinations(); + } + } } } diff --git a/src/storage/jani/Automaton.h b/src/storage/jani/Automaton.h index 81adf3820..19659a091 100644 --- a/src/storage/jani/Automaton.h +++ b/src/storage/jani/Automaton.h @@ -315,6 +315,8 @@ namespace storm { */ bool containsVariablesOnlyInProbabilitiesOrTransientAssignments(std::set const& variables) const; + void pushEdgeAssignmentsToDestinations(); + private: /// The name of the automaton. std::string name; diff --git a/src/storage/jani/Edge.cpp b/src/storage/jani/Edge.cpp index 62c3d0143..f8d7e031d 100644 --- a/src/storage/jani/Edge.cpp +++ b/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 const& Edge::getWrittenGlobalVariables() const { return writtenGlobalVariables; } diff --git a/src/storage/jani/Edge.h b/src/storage/jani/Edge.h index fd040e40d..7f6172bc8 100644 --- a/src/storage/jani/Edge.h +++ b/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. */ diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp index 56e07c226..51f80e01b 100644 --- a/src/storage/jani/Model.cpp +++ b/src/storage/jani/Model.cpp @@ -510,6 +510,11 @@ namespace storm { } return true; } - + + void Model::makeStandardJaniCompliant() { + for (auto& automaton : automata) { + automaton.pushEdgeAssignmentsToDestinations(); + } + } } } diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h index 80b2d78ed..60b6b6546 100644 --- a/src/storage/jani/Model.h +++ b/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;