From a7a3a82d892ba65fd24beaa45dcec447bccdb061 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Wed, 10 Apr 2019 13:37:43 +0200
Subject: [PATCH] Prism: ToJaniConverters now enforces variables occurring in
properties to become global. This fixes GitHub issue #40
---
src/storm/storage/prism/Program.cpp | 11 +++++++++--
src/storm/storage/prism/ToJaniConverter.cpp | 5 ++++-
src/storm/storage/prism/ToJaniConverter.h | 2 +-
3 files changed, 14 insertions(+), 4 deletions(-)
diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp
index a0b32175a..1a22f87dc 100644
--- a/src/storm/storage/prism/Program.cpp
+++ b/src/storm/storage/prism/Program.cpp
@@ -1843,7 +1843,7 @@ namespace storm {
storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const {
ToJaniConverter converter;
- auto janiModel = converter.convert(*this, allVariablesGlobal, suffix);
+ auto janiModel = 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.");
STORM_LOG_WARN_COND(!converter.rewardModelsWereRenamed(), "Rewardmodels were renamed in PRISM-to-JANI conversion, but the mapping is not stored.");
return janiModel;
@@ -1851,7 +1851,14 @@ namespace storm {
std::pair<storm::jani::Model, std::vector<storm::jani::Property>> Program::toJani(std::vector<storm::jani::Property> const& properties, bool allVariablesGlobal, std::string suffix) const {
ToJaniConverter converter;
- auto janiModel = converter.convert(*this, allVariablesGlobal, suffix);
+ std::set<storm::expressions::Variable> variablesToMakeGlobal;
+ if (!allVariablesGlobal) {
+ for (auto const& prop : properties) {
+ auto vars = prop.getUsedVariablesAndConstants();
+ variablesToMakeGlobal.insert(vars.begin(), vars.end());
+ }
+ }
+ auto janiModel = converter.convert(*this, allVariablesGlobal, variablesToMakeGlobal, suffix);
std::vector<storm::jani::Property> newProperties;
if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) {
newProperties = converter.applyRenaming(properties);
diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp
index bc6476e5b..8c9f624ed 100644
--- a/src/storm/storage/prism/ToJaniConverter.cpp
+++ b/src/storm/storage/prism/ToJaniConverter.cpp
@@ -18,7 +18,7 @@
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::set<storm::expressions::Variable> const& givenVariablesToMakeGlobal, std::string suffix) {
labelRenaming.clear();
rewardModelRenaming.clear();
formulaToFunctionCallMap.clear();
@@ -53,6 +53,9 @@ namespace storm {
// Maintain a mapping of each variable to a flag that is true if the variable will be made global.
std::map<storm::expressions::Variable, bool> variablesToMakeGlobal;
+ for (auto const& var : givenVariablesToMakeGlobal) {
+ variablesToMakeGlobal.emplace(var, true);
+ }
// Get the set of variables that appeare in a renaimng of a renamed module
if (program.getNumberOfFormulas() > 0) {
diff --git a/src/storm/storage/prism/ToJaniConverter.h b/src/storm/storage/prism/ToJaniConverter.h
index 38d5f331e..a86f6dea0 100644
--- a/src/storm/storage/prism/ToJaniConverter.h
+++ b/src/storm/storage/prism/ToJaniConverter.h
@@ -18,7 +18,7 @@ namespace storm {
class ToJaniConverter {
public:
- storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::string suffix = "");
+ storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::set<storm::expressions::Variable> const& variablesToMakeGlobal = {}, std::string suffix = "");
bool labelsWereRenamed() const;
bool rewardModelsWereRenamed() const;