From 1c9f7b0f2f2cb4c0ac680a6dd9dfc9183b2c2923 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Wed, 2 May 2018 23:42:00 +0200 Subject: [PATCH] translate prism to jani with a suffix for location names etc when doing this for multiple models --- src/storm/storage/prism/Program.cpp | 8 ++++---- src/storm/storage/prism/Program.h | 4 ++-- src/storm/storage/prism/ToJaniConverter.cpp | 8 ++++---- src/storm/storage/prism/ToJaniConverter.h | 2 +- 4 files changed, 11 insertions(+), 11 deletions(-) diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 41a9693bc..228df8541 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) const { + storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const { ToJaniConverter converter; - storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal); + storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix); 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) const { + std::pair> Program::toJaniWithLabelRenaming(bool allVariablesGlobal, std::string suffix) const { ToJaniConverter converter; - storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal); + storm::jani::Model resultingModel = converter.convert(*this, allVariablesGlobal, suffix); return std::make_pair(resultingModel, converter.getLabelRenaming()); } diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 7dedc6667..4d6d303fc 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) const; + storm::jani::Model toJani(bool allVariablesGlobal = false, std::string suffix = "") 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) const; + std::pair> toJaniWithLabelRenaming(bool allVariablesGlobal = false, std::string suffix = "") const; private: /*! diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 7719b08e5..9712a52a7 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -13,7 +13,7 @@ namespace storm { namespace prism { - storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal) { + storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix) { std::shared_ptr manager = program.getManager().getSharedPointer(); // Start by creating an empty JANI model. @@ -95,11 +95,11 @@ namespace storm { } } - // Go through the labels and construct assignments to transient variables that are added to the loctions. + // Go through the labels and construct assignments to transient variables that are added to the locations. std::vector transientLocationAssignments; for (auto const& label : program.getLabels()) { bool renameLabel = manager->hasVariable(label.getName()) || program.hasRewardModel(label.getName()); - std::string finalLabelName = renameLabel ? "label_" + label.getName() : 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."); labelRenaming[label.getName()] = finalLabelName; @@ -161,7 +161,7 @@ namespace storm { // Keep track of the action indices contained in this module. std::set actionIndicesOfModule; - storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName())); + storm::jani::Automaton automaton(module.getName(), manager->declareIntegerVariable("_loc_prism2jani_" + module.getName() + "_" + suffix)); for (auto const& variable : module.getIntegerVariables()) { storm::jani::BoundedIntegerVariable newIntegerVariable = *storm::jani::makeBoundedIntegerVariable(variable.getName(), variable.getExpressionVariable(), variable.hasInitialValue() ? boost::make_optional(variable.getInitialValueExpression()) : boost::none, false, variable.getLowerBoundExpression(), variable.getUpperBoundExpression()); std::set const& accessingModuleIndices = variablesToAccessingModuleIndices[variable.getExpressionVariable()]; diff --git a/src/storm/storage/prism/ToJaniConverter.h b/src/storm/storage/prism/ToJaniConverter.h index 2ab5c0509..e68c9612e 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); + storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = false, std::string suffix = ""); bool labelsWereRenamed() const; std::map const& getLabelRenaming() const;