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 smtSolverFactory; if (storm::settings::hasModule()) { 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> 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> const& automatonToCopiesMap) : automatonToCopiesMap(automatonToCopiesMap) {} + + std::shared_ptr simplify(Composition const& oldComposition) { + return boost::any_cast>(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(new AutomatonComposition(name, composition.getInputEnabledActions())); + } + + virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override { + std::vector> subcomposition; + for (auto const& p : composition.getSubcompositions()) { + subcomposition.push_back(boost::any_cast>(p->accept(*this, data))); + } + return std::shared_ptr(new ParallelComposition(subcomposition, composition.getSynchronizationVectors())); + } + + private: + std::unordered_map> 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> automatonToCopiesMap; + for (auto const& automatonMultiplicity : info.getAutomatonToMultiplicityMap()) { + if (automatonMultiplicity.second > 1) { + std::vector 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 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. */