diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 480e24a84..5573e32d4 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -136,16 +136,11 @@ namespace storm { if (transformToJani) { storm::prism::Program const& model = output.model.get().asPrismProgram(); - auto modelAndRenaming = model.toJaniWithLabelRenaming(true, "", false); - output.model = modelAndRenaming.first; + auto modelAndProperties = model.toJani(output.properties, true, "", false); + output.model = modelAndProperties.first; - if (!modelAndRenaming.second.empty()) { - std::map const& labelRenaming = modelAndRenaming.second; - std::vector amendedProperties; - for (auto const& property : output.properties) { - amendedProperties.emplace_back(property.substituteLabels(labelRenaming)); - } - output.preprocessedProperties = std::move(amendedProperties); + if (!modelAndProperties.second.empty()) { + output.preprocessedProperties = std::move(modelAndProperties.second); } } } diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index ff4d89276..7431b38be 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -36,7 +36,7 @@ namespace storm { } auto uneliminatedFeatures = janiModel.restrictToFeatures(options.allowedModelFeatures); - STORM_LOG_WARN(uneliminatedFeatures.empty(), "The following model features could not be eliminated: " << uneliminatedFeatures.toString()); + STORM_LOG_WARN_COND(uneliminatedFeatures.empty(), "The following model features could not be eliminated: " << uneliminatedFeatures.toString()); if (options.modelName) { janiModel.setName(options.modelName.get()); @@ -44,15 +44,15 @@ namespace storm { } std::pair> convertPrismToJani(storm::prism::Program const& program, std::vector const& properties, storm::converter::PrismToJaniConverterOptions options) { - std::pair> res; // Perform conversion - auto modelAndRenaming = program.toJaniWithLabelRenaming(options.allVariablesGlobal, options.suffix, options.janiOptions.standardCompliant); - res.first = std::move(modelAndRenaming.first); - - // Amend properties to potentially changed labels - for (auto const& property : properties) { - res.second.emplace_back(property.substituteLabels(modelAndRenaming.second)); + auto res = program.toJani(properties, true, "", false); + if (res.second.empty()) { + std::vector clondedProperties; + for (auto const& p : properties) { + clondedProperties.push_back(p.clone()); + } + res.second = std::move(clondedProperties); } // Postprocess Jani model based on the options diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index 1e769acd0..a16e7df54 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -5,6 +5,7 @@ #include "storm/utility/jani.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" #include "storm/storage/jani/Automaton.h" @@ -130,13 +131,13 @@ namespace storm { } } - std::pair> SymbolicModelDescription::toJaniWithLabelRenaming(bool makeVariablesGlobal, bool standardCompliant) const { + std::pair> SymbolicModelDescription::toJani(std::vector const& properties, bool makeVariablesGlobal, bool standardCompliant) const { if (this->isJaniModel()) { - return std::make_pair(*this, std::map()); + return std::make_pair(*this, std::vector()); } if (this->isPrismProgram()) { - auto modelAndRenaming = this->asPrismProgram().toJaniWithLabelRenaming(makeVariablesGlobal, "", standardCompliant); - return std::make_pair(SymbolicModelDescription(modelAndRenaming.first), modelAndRenaming.second); + auto modelProperties = this->asPrismProgram().toJani(properties, makeVariablesGlobal, "", standardCompliant); + return std::make_pair(SymbolicModelDescription(modelProperties.first), modelProperties.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 3ab94ba5d..2f50c6986 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -39,7 +39,16 @@ namespace storm { std::vector getParameterNames() const; SymbolicModelDescription toJani(bool makeVariablesGlobal = true, bool standardCompliant = false) const; - std::pair> toJaniWithLabelRenaming(bool makeVariablesGlobal = true, bool standardCompliant = false) const; + + /*! + * Ensures that this model is a JANI model by, e.g., converting prism to jani. + * If labels or reward models had to be converted during conversion, the renamings are applied to the given properties + * + * @return The jani model of this and either the new set of properties or an empty vector if no renamings were necessary + * + * @note The returned property vector might be empty in case no renaming is necessary. + */ + std::pair> toJani(std::vector const& properties, bool makeVariablesGlobal, bool standardCompliant) 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 98198af58..67e822ab3 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1741,15 +1741,20 @@ namespace storm { storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix, bool standardCompliant) const { ToJaniConverter converter; - storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant); + auto janiModel = 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; + STORM_LOG_WARN_COND(!converter.rewardModelsWereRenamed(), "Rewardmodels were renamed in PRISM-to-JANI conversion, but the mapping is not stored."); + return janiModel; } - std::pair> Program::toJaniWithLabelRenaming(bool allVariablesGlobal, std::string suffix, bool standardCompliant) const { + std::pair> Program::toJani(std::vector const& properties, bool allVariablesGlobal, std::string suffix, bool standardCompliant) const { ToJaniConverter converter; - storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant); - return std::make_pair(resultingModel, converter.getLabelRenaming()); + auto janiModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant); + std::vector newProperties; + if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) { + newProperties = converter.applyRenaming(properties); + } + return std::make_pair(janiModel, newProperties); } storm::expressions::ExpressionManager& Program::getManager() const { diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 517790074..aaefada9e 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -626,10 +626,11 @@ namespace storm { 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. + * Converts the PRISM model into an equivalent JANI model and if labels or reward models had + * to be renamed in the process, the renamings are applied to the given properties + * @return The jani model of this and either the new set of properties or an empty vector if no renamings were necessary */ - std::pair> toJaniWithLabelRenaming(bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const; + std::pair> toJani(std::vector const& properties, 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 f998e59ad..322a3baa2 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -5,6 +5,7 @@ #include "storm/storage/prism/Program.h" #include "storm/storage/prism/CompositionToJaniVisitor.h" #include "storm/storage/jani/Model.h" +#include "storm/storage/jani/Property.h" #include "storm/storage/jani/TemplateEdge.h" #include "storm/storage/jani/expressions/FunctionCallExpression.h" @@ -17,6 +18,9 @@ namespace storm { namespace prism { storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix, bool standardCompliant) { + labelRenaming.clear(); + rewardModelRenaming.clear(); + std::shared_ptr manager = program.getManager().getSharedPointer(); bool produceStateRewards = !standardCompliant || program.getModelType() == storm::prism::Program::ModelType::CTMC || program.getModelType() == storm::prism::Program::ModelType::MA; @@ -125,7 +129,7 @@ namespace storm { bool renameLabel = manager->hasVariable(label.getName()) || program.hasRewardModel(label.getName()); std::string finalLabelName = renameLabel ? "label_" + label.getName() + suffix : label.getName(); if (renameLabel) { - STORM_LOG_WARN_COND(!renameLabel, "Label '" << label.getName() << "' was renamed to '" << finalLabelName << "' in PRISM-to-JANI conversion, as another variable with that name already exists."); + STORM_LOG_INFO("Label '" << label.getName() << "' was renamed to '" << finalLabelName << "' in PRISM-to-JANI conversion, as another variable with that name already exists."); labelRenaming[label.getName()] = finalLabelName; } auto newExpressionVariable = manager->declareBooleanVariable(finalLabelName); @@ -155,8 +159,22 @@ namespace storm { // edges and transient assignments that are added to the locations. std::map> transientEdgeAssignments; for (auto const& rewardModel : program.getRewardModels()) { - auto newExpressionVariable = manager->declareRationalVariable(rewardModel.getName().empty() ? "default_reward_model" : rewardModel.getName()); - storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(rewardModel.getName().empty() ? "default" : rewardModel.getName(), newExpressionVariable, manager->rational(0.0), true)); + std::string finalRewardModelName; + if (rewardModel.getName().empty()) { + finalRewardModelName = "default_reward_model"; + } else { + if (manager->hasVariable(rewardModel.getName())) { + // Rename + finalRewardModelName = "rewardmodel_" + rewardModel.getName() + suffix; + STORM_LOG_INFO("Rewardmodel '" << rewardModel.getName() << "' was renamed to '" << finalRewardModelName << "' in PRISM-to-JANI conversion, as another variable with that name already exists."); + rewardModelRenaming[rewardModel.getName()] = finalRewardModelName; + } else { + finalRewardModelName = rewardModel.getName(); + } + } + + auto newExpressionVariable = manager->declareRationalVariable(finalRewardModelName); + storm::jani::RealVariable const& newTransientVariable = janiModel.addVariable(storm::jani::RealVariable(finalRewardModelName, newExpressionVariable, manager->rational(0.0), true)); if (rewardModel.hasStateRewards()) { storm::expressions::Expression transientLocationExpression; @@ -375,9 +393,40 @@ namespace storm { return !labelRenaming.empty(); } + bool ToJaniConverter::rewardModelsWereRenamed() const { + return !rewardModelRenaming.empty(); + } + std::map const& ToJaniConverter::getLabelRenaming() const { return labelRenaming; } + std::map const& ToJaniConverter::getRewardModelRenaming() const { + return rewardModelRenaming; + } + + storm::jani::Property ToJaniConverter::applyRenaming(storm::jani::Property const& property) const { + if (rewardModelsWereRenamed()) { + auto res = property.substituteRewardModelNames(getRewardModelRenaming()); + if (labelsWereRenamed()) { + res = res.substituteLabels(getLabelRenaming()); + } + return res; + } else { + if (labelsWereRenamed()) { + return property.substituteLabels(getLabelRenaming()); + } else { + return property.clone(); + } + } + } + + std::vector ToJaniConverter::applyRenaming(std::vector const& properties) const { + std::vector result; + for (auto const& p : properties) { + result.push_back(applyRenaming(p)); + } + return result; + } } } diff --git a/src/storm/storage/prism/ToJaniConverter.h b/src/storm/storage/prism/ToJaniConverter.h index 2ba1c870f..236855b54 100644 --- a/src/storm/storage/prism/ToJaniConverter.h +++ b/src/storm/storage/prism/ToJaniConverter.h @@ -6,6 +6,7 @@ namespace storm { namespace jani { class Model; + class Property; } namespace prism { @@ -17,10 +18,16 @@ namespace storm { storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false); bool labelsWereRenamed() const; + bool rewardModelsWereRenamed() const; std::map const& getLabelRenaming() const; + std::map const& getRewardModelRenaming() const; + + storm::jani::Property applyRenaming(storm::jani::Property const& property) const; + std::vector applyRenaming(std::vector const& property) const; private: std::map labelRenaming; + std::map rewardModelRenaming; }; }