From 95b2095151503e867f178d706ddfb4aefea05e3b Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 27 Feb 2020 13:12:47 +0100
Subject: [PATCH] Implemented simplification of system composition (this
enables compatibility for more benchmarks in the dd engine).
---
src/storm-conv/api/storm-conv.cpp | 4 ++
.../options/JaniConversionOptions.cpp | 4 +-
.../converter/options/JaniConversionOptions.h | 4 ++
.../settings/modules/JaniExportSettings.cpp | 6 ++
.../settings/modules/JaniExportSettings.h | 3 +
src/storm/builder/DdJaniModelBuilder.cpp | 15 +----
src/storm/storage/jani/Automaton.cpp | 1 +
src/storm/storage/jani/Model.cpp | 63 +++++++++++++++++++
src/storm/storage/jani/Model.h | 7 +++
9 files changed, 91 insertions(+), 16 deletions(-)
diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp
index 95ca5c4ee..14c140770 100644
--- a/src/storm-conv/api/storm-conv.cpp
+++ b/src/storm-conv/api/storm-conv.cpp
@@ -53,6 +53,10 @@ namespace storm {
}
}
+ if (options.simplifyComposition) {
+ janiModel.simplifyComposition();
+ }
+
if (options.flatten) {
std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
if (storm::settings::hasModule<storm::settings::modules::CoreSettings>()) {
diff --git a/src/storm-conv/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp
index c8a4ab8a3..4d0937c3a 100644
--- a/src/storm-conv/converter/options/JaniConversionOptions.cpp
+++ b/src/storm-conv/converter/options/JaniConversionOptions.cpp
@@ -3,11 +3,11 @@
namespace storm {
namespace converter {
- JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), localVars(false), globalVars(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(false) {
+ JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), localVars(false), globalVars(false), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(false), simplifyComposition(false) {
// Intentionally left empty
}
- JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), localVars(settings.isLocalVarsSet()), globalVars(settings.isGlobalVarsSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(settings.isReplaceUnassignedVariablesWithConstantsSet()) {
+ JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), localVars(settings.isLocalVarsSet()), globalVars(settings.isGlobalVarsSet()), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()), addPropertyConstants(true), replaceUnassignedVariablesWithConstants(settings.isReplaceUnassignedVariablesWithConstantsSet()), simplifyComposition(settings.isSimplifyCompositionSet()) {
if (settings.isEliminateFunctionsSet()) {
allowedModelFeatures.remove(storm::jani::ModelFeature::Functions);
}
diff --git a/src/storm-conv/converter/options/JaniConversionOptions.h b/src/storm-conv/converter/options/JaniConversionOptions.h
index 65f6f7ce5..301d94b08 100644
--- a/src/storm-conv/converter/options/JaniConversionOptions.h
+++ b/src/storm-conv/converter/options/JaniConversionOptions.h
@@ -44,6 +44,10 @@ namespace storm {
/// If set, local and global variables that are (a) not assigned to some value and (b) have a known initial value are replaced by constants.
bool replaceUnassignedVariablesWithConstants;
+
+ /// If set, attempts to simplify the system composition
+ bool simplifyComposition;
+
};
}
}
diff --git a/src/storm-conv/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp
index cc6aeef29..90d02e8aa 100644
--- a/src/storm-conv/settings/modules/JaniExportSettings.cpp
+++ b/src/storm-conv/settings/modules/JaniExportSettings.cpp
@@ -23,6 +23,7 @@ namespace storm {
const std::string JaniExportSettings::eliminateArraysOptionName = "remove-arrays";
const std::string JaniExportSettings::eliminateFunctionsOptionName = "remove-functions";
const std::string JaniExportSettings::replaceUnassignedVariablesWithConstantsOptionName = "replace-unassigned-vars";
+ const std::string JaniExportSettings::simplifyCompositionOptionName = "simplify-composition";
JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
this->addOption(storm::settings::OptionBuilder(moduleName, locationVariablesOptionName, true, "Variables to export in the location").addArgument(storm::settings::ArgumentBuilder::createStringArgument("variables", "A comma separated list of automaton and local variable names seperated by a dot, e.g. A.x,B.y.").setDefaultValueString("").build()).build());
@@ -34,6 +35,7 @@ namespace storm {
this->addOption(storm::settings::OptionBuilder(moduleName, eliminateArraysOptionName, false, "If set, transforms the model such that array variables/expressions are eliminated.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, eliminateFunctionsOptionName, false, "If set, transforms the model such that functions are eliminated.").build());
this->addOption(storm::settings::OptionBuilder(moduleName, replaceUnassignedVariablesWithConstantsOptionName, false, "If set, local and global variables that are (a) not assigned to some value and (b) have a known initial value are replaced by constants.").build());
+ this->addOption(storm::settings::OptionBuilder(moduleName, simplifyCompositionOptionName, false, "If set, attempts to simplify the system composition.").build());
}
bool JaniExportSettings::isAllowEdgeAssignmentsSet() const {
@@ -88,6 +90,10 @@ namespace storm {
return this->getOption(replaceUnassignedVariablesWithConstantsOptionName).getHasOptionBeenSet();
}
+ bool JaniExportSettings::isSimplifyCompositionSet() const {
+ return this->getOption(simplifyCompositionOptionName).getHasOptionBeenSet();
+ }
+
void JaniExportSettings::finalize() {
}
diff --git a/src/storm-conv/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h
index c91097b5f..cf492af78 100644
--- a/src/storm-conv/settings/modules/JaniExportSettings.h
+++ b/src/storm-conv/settings/modules/JaniExportSettings.h
@@ -31,6 +31,8 @@ namespace storm {
bool isEliminateFunctionsSet() const;
bool isReplaceUnassignedVariablesWithConstantsSet() const;
+
+ bool isSimplifyCompositionSet() const;
std::vector<std::pair<std::string, std::string>> getLocationVariables() const;
@@ -49,6 +51,7 @@ namespace storm {
static const std::string eliminateArraysOptionName;
static const std::string eliminateFunctionsOptionName;
static const std::string replaceUnassignedVariablesWithConstantsOptionName;
+ static const std::string simplifyCompositionOptionName;
};
}
diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp
index c4509c6ea..259ad60d9 100644
--- a/src/storm/builder/DdJaniModelBuilder.cpp
+++ b/src/storm/builder/DdJaniModelBuilder.cpp
@@ -91,20 +91,6 @@ namespace storm {
return false;
}
}
- // Check system composition
- auto compositionInfo = storm::jani::CompositionInformationVisitor(model, model.getSystemComposition()).getInformation();
-
- // Every automaton has to occur exactly once.
- if (compositionInfo.getAutomatonToMultiplicityMap().size() != model.getNumberOfAutomata()) {
- STORM_LOG_INFO("Symbolic engine can not build Jani model since the system composition does not list each automaton exactly once.");
- return false;
- }
- for (auto automatonMultiplicity : compositionInfo.getAutomatonToMultiplicityMap()) {
- if (automatonMultiplicity.second > 1) {
- STORM_LOG_INFO("Symbolic engine can not build Jani model since the system composition does not list each automaton exactly once.");
- return false;
- }
- }
// There probably are more cases where the model is unsupported. However, checking these is often more involved.
// As this method is supposed to be a quick check, we just return true at this point.
@@ -2155,6 +2141,7 @@ namespace storm {
features.remove(storm::jani::ModelFeature::StateExitRewards);
storm::jani::Model preparedModel = model;
+ preparedModel.simplifyComposition();
if (features.hasArrays()) {
STORM_LOG_ERROR("The jani model still considers arrays. These should have been eliminated before calling the dd builder. The arrays are eliminated now, but occurrences in properties will not be handled properly.");
preparedModel.eliminateArrays();
diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index dd2c3a386..919d7d967 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -38,6 +38,7 @@ namespace storm {
}
result.variables.substituteExpressionVariables(oldToNewVarMap);
result.substitute(oldToNewVarMap);
+ return result;
}
std::string const& Automaton::getName() const {
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 224857989..d5ba829b4 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -955,6 +955,69 @@ namespace storm {
return *composition;
}
+ class CompositionSimplificationVisitor : public CompositionVisitor {
+ public:
+ CompositionSimplificationVisitor(std::unordered_map<std::string, std::vector<std::string>> const& automatonToCopiesMap) : automatonToCopiesMap(automatonToCopiesMap) {}
+
+ std::shared_ptr<Composition> simplify(Composition const& oldComposition) {
+ return boost::any_cast<std::shared_ptr<Composition>>(oldComposition.accept(*this, boost::any()));
+ }
+
+ virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override {
+ std::string name = composition.getAutomatonName();
+ if (automatonToCopiesMap.count(name) != 0) {
+ auto& copies = automatonToCopiesMap[name];
+ STORM_LOG_ASSERT(!copies.empty(), "Not enough copies of automaton " << name << ".");
+ name = copies.back();
+ copies.pop_back();
+ }
+ return std::shared_ptr<Composition>(new AutomatonComposition(name, composition.getInputEnabledActions()));
+ }
+
+ virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override {
+ std::vector<std::shared_ptr<Composition>> subcomposition;
+ for (auto const& p : composition.getSubcompositions()) {
+ subcomposition.push_back(boost::any_cast<std::shared_ptr<Composition>>(p->accept(*this, data)));
+ }
+ return std::shared_ptr<Composition>(new ParallelComposition(subcomposition, composition.getSynchronizationVectors()));
+ }
+
+ private:
+ std::unordered_map<std::string, std::vector<std::string>> automatonToCopiesMap;
+ };
+
+ void Model::simplifyComposition() {
+ CompositionInformationVisitor visitor(*this, this->getSystemComposition());
+ CompositionInformation info = visitor.getInformation();
+ if (info.containsNestedParallelComposition()) {
+ STORM_LOG_WARN("Unable to simplify non-standard compliant system composition.");
+ }
+
+ // Check whether we need to copy certain automata
+ std::unordered_map<std::string, std::vector<std::string>> automatonToCopiesMap;
+ for (auto const& automatonMultiplicity : info.getAutomatonToMultiplicityMap()) {
+ if (automatonMultiplicity.second > 1) {
+ std::vector<std::string> copies = {automatonMultiplicity.first};
+ // We need to copy this automaton n-1 times.
+ for (uint64_t copyIndex = 1; copyIndex < automatonMultiplicity.second; ++copyIndex) {
+ std::string copyPrefix = "Copy__" + std::to_string(copyIndex) + "_Of";
+ std::string copyAutName = copyPrefix + automatonMultiplicity.first;
+ this->addAutomaton(this->getAutomaton(automatonMultiplicity.first).clone(getManager(), copyAutName, copyPrefix));
+ copies.push_back(copyAutName);
+ }
+ // For esthetic reasons we reverse the list of copies so that the ones with the lowest index will be pop_back'ed first
+ std::reverse(copies.begin(), copies.end());
+ // We insert the copies in reversed order as they will be popped in reversed order, as well.
+ automatonToCopiesMap[automatonMultiplicity.first] = std::move(copies);
+ }
+ }
+
+ // Traverse the system composition and exchange automata by their copy
+ auto newComposition = CompositionSimplificationVisitor(automatonToCopiesMap).simplify(getSystemComposition());
+ this->setSystemComposition(newComposition);
+
+ }
+
void Model::setSystemComposition(std::shared_ptr<Composition> const& composition) {
this->composition = composition;
}
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index 41e205274..afaa4bda6 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -412,6 +412,13 @@ namespace storm {
*/
Composition const& getSystemComposition() const;
+ /*!
+ * Attempts to simplify the composition.
+ * Right now, this only means that automata that occur multiple times in the composition will be
+ * duplicated su that each automata occurs at most once.
+ */
+ void simplifyComposition();
+
/*!
* Retrieves the set of action names.
*/