diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 4f41c4d4f..54381f7d4 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -17,6 +17,7 @@ #include "storm/storage/SymbolicModelDescription.h" +#include "storm/storage/jani/Property.h" #include "storm/models/ModelBase.h" @@ -129,7 +130,7 @@ namespace storm { if (transformToJani) { storm::prism::Program const& model = output.model.get().asPrismProgram(); - auto modelAndRenaming = model.toJaniWithLabelRenaming(true); + auto modelAndRenaming = model.toJaniWithLabelRenaming(true, "", false); output.model = modelAndRenaming.first; if (!modelAndRenaming.second.empty()) { @@ -153,10 +154,6 @@ namespace storm { if (ioSettings.isExportJaniDotSet()) { storm::api::exportJaniModelAsDot(model.asJaniModel(), ioSettings.getExportJaniDotFilename()); } - - if (model.isJaniModel() && storm::settings::getModule().isJaniFileSet()) { - storm::api::exportJaniModel(model.asJaniModel(), input.properties, storm::settings::getModule().getJaniFilename()); - } } } diff --git a/src/storm/api/export.cpp b/src/storm/api/export.cpp index 1a69a34da..80d45ed2c 100644 --- a/src/storm/api/export.cpp +++ b/src/storm/api/export.cpp @@ -4,31 +4,6 @@ namespace storm { namespace api { - void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filename) { - auto janiSettings = storm::settings::getModule(); - - storm::jani::Model exportModel = model; - if (janiSettings.isLocationVariablesSet()) { - for(auto const& pair : janiSettings.getLocationVariables()) { - storm::jani::JaniLocationExpander expander(exportModel); - expander.transform(pair.first, pair.second); - exportModel = expander.getResult(); - } - } - - if (janiSettings.isExportFlattenedSet()) { - exportModel = exportModel.flattenComposition(); - } - - if (janiSettings.isExportAsStandardJaniSet()) { - storm::jani::Model normalisedModel = exportModel; - normalisedModel.makeStandardJaniCompliant(); - storm::jani::JsonExporter::toFile(normalisedModel, properties, filename); - } else { - storm::jani::JsonExporter::toFile(exportModel, properties, filename); - } - } - void exportJaniModelAsDot(storm::jani::Model const& model, std::string const& filename) { std::ofstream out; storm::utility::openFile(filename, out); diff --git a/src/storm/api/export.h b/src/storm/api/export.h index 3ba81525d..825a9de48 100644 --- a/src/storm/api/export.h +++ b/src/storm/api/export.h @@ -1,8 +1,5 @@ #pragma once -#include "storm/storage/jani/JSONExporter.h" - - #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/JaniExportSettings.h" @@ -11,10 +8,13 @@ #include "storm/utility/macros.h" namespace storm { + + namespace jani { + class Model; + } + namespace api { - void exportJaniModel(storm::jani::Model const& model, std::vector const& properties, std::string const& filename); - void exportJaniModelAsDot(storm::jani::Model const& model, std::string const& filename); template diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index b08166125..79a12f8b1 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -119,23 +119,23 @@ namespace storm { return result; } - SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const { + SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal, bool standardCompliant) const { if (this->isJaniModel()) { return *this; } if (this->isPrismProgram()) { - return SymbolicModelDescription(this->asPrismProgram().toJani(makeVariablesGlobal)); + return SymbolicModelDescription(this->asPrismProgram().toJani(makeVariablesGlobal, "", standardCompliant)); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format."); } } - std::pair> SymbolicModelDescription::toJaniWithLabelRenaming(bool makeVariablesGlobal) const { + std::pair> SymbolicModelDescription::toJaniWithLabelRenaming(bool makeVariablesGlobal, bool standardCompliant) const { if (this->isJaniModel()) { return std::make_pair(*this, std::map()); } if (this->isPrismProgram()) { - auto modelAndRenaming = this->asPrismProgram().toJaniWithLabelRenaming(makeVariablesGlobal); + auto modelAndRenaming = this->asPrismProgram().toJaniWithLabelRenaming(makeVariablesGlobal, "", standardCompliant); return std::make_pair(SymbolicModelDescription(modelAndRenaming.first), modelAndRenaming.second); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format."); diff --git a/src/storm/storage/SymbolicModelDescription.h b/src/storm/storage/SymbolicModelDescription.h index 137f1a7d4..3ab94ba5d 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -38,8 +38,8 @@ namespace storm { std::vector getParameterNames() const; - SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const; - std::pair> toJaniWithLabelRenaming(bool makeVariablesGlobal = true) const; + SymbolicModelDescription toJani(bool makeVariablesGlobal = true, bool standardCompliant = false) const; + std::pair> toJaniWithLabelRenaming(bool makeVariablesGlobal = true, bool standardCompliant = false) const; SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const; SymbolicModelDescription preprocess(std::map const& constantDefinitions) const; diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 228df8541..f12686315 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1711,16 +1711,16 @@ namespace storm { return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0); } - storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const { + storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix, bool standardCompliant) const { ToJaniConverter converter; - storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix); + storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant); STORM_LOG_WARN_COND(!converter.labelsWereRenamed(), "Labels were renamed in PRISM-to-JANI conversion, but the mapping is not stored."); return resultingModel; } - std::pair> Program::toJaniWithLabelRenaming(bool allVariablesGlobal, std::string suffix) const { + std::pair> Program::toJaniWithLabelRenaming(bool allVariablesGlobal, std::string suffix, bool standardCompliant) const { ToJaniConverter converter; - storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix); + storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant); return std::make_pair(resultingModel, converter.getLabelRenaming()); } diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 4d6d303fc..3adc3151f 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -603,13 +603,13 @@ namespace storm { /*! * Converts the PRISM model into an equivalent JANI model. */ - storm::jani::Model toJani(bool allVariablesGlobal = false, std::string suffix = "") const; + storm::jani::Model toJani(bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const; /*! * Converts the PRISM model into an equivalent JANI model and retrieves possible label renamings that had * to be performed in the process. */ - std::pair> toJaniWithLabelRenaming(bool allVariablesGlobal = false, std::string suffix = "") const; + std::pair> toJaniWithLabelRenaming(bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const; private: /*! diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 36a47d7f9..dca6584a1 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -8,7 +8,6 @@ #include "storm/storage/jani/TemplateEdge.h" #include "storm/settings/SettingsManager.h" -#include "storm/settings/modules/JaniExportSettings.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" @@ -16,10 +15,10 @@ namespace storm { namespace prism { - storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix) { + storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix, bool standardCompliant) { std::shared_ptr manager = program.getManager().getSharedPointer(); - bool produceStateRewards = !storm::settings::getModule().isExportAsStandardJaniSet() || program.getModelType() == storm::prism::Program::ModelType::CTMC; + bool produceStateRewards = !standardCompliant || program.getModelType() == storm::prism::Program::ModelType::CTMC || program.getModelType() == storm::prism::Program::ModelType::MA; // Start by creating an empty JANI model. storm::jani::ModelType modelType; diff --git a/src/storm/storage/prism/ToJaniConverter.h b/src/storm/storage/prism/ToJaniConverter.h index e68c9612e..2ba1c870f 100644 --- a/src/storm/storage/prism/ToJaniConverter.h +++ b/src/storm/storage/prism/ToJaniConverter.h @@ -14,7 +14,7 @@ namespace storm { class ToJaniConverter { public: - storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false, std::string suffix = ""); + storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false); bool labelsWereRenamed() const; std::map const& getLabelRenaming() const;