diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 5573e32d4..45d221738 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -136,7 +136,7 @@ namespace storm { if (transformToJani) { storm::prism::Program const& model = output.model.get().asPrismProgram(); - auto modelAndProperties = model.toJani(output.properties, true, "", false); + auto modelAndProperties = model.toJani(output.properties); output.model = modelAndProperties.first; if (!modelAndProperties.second.empty()) { diff --git a/src/storm-conv/api/storm-conv.cpp b/src/storm-conv/api/storm-conv.cpp index f8e956a94..0ed03a071 100644 --- a/src/storm-conv/api/storm-conv.cpp +++ b/src/storm-conv/api/storm-conv.cpp @@ -35,8 +35,8 @@ namespace storm { janiModel = janiModel.flattenComposition(smtSolverFactory); } - if (options.standardCompliant) { - janiModel.makeStandardJaniCompliant(); + if (!options.edgeAssignments) { + janiModel.pushEdgeAssignmentsToDestinations(); } auto uneliminatedFeatures = janiModel.restrictToFeatures(options.allowedModelFeatures); @@ -50,7 +50,7 @@ namespace storm { std::pair> convertPrismToJani(storm::prism::Program const& program, std::vector const& properties, storm::converter::PrismToJaniConverterOptions options) { // Perform conversion - auto res = program.toJani(properties, true, "", false); + auto res = program.toJani(properties, options.allVariablesGlobal); if (res.second.empty()) { std::vector clondedProperties; for (auto const& p : properties) { diff --git a/src/storm-conv/converter/options/JaniConversionOptions.cpp b/src/storm-conv/converter/options/JaniConversionOptions.cpp index 123d281b3..9c1bc1b04 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() : standardCompliant(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { + JaniConversionOptions::JaniConversionOptions() : edgeAssignments(false), flatten(false), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { // Intentionally left empty }; - JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), standardCompliant(settings.isExportAsStandardJaniSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { + JaniConversionOptions::JaniConversionOptions(storm::settings::modules::JaniExportSettings const& settings) : locationVariables(settings.getLocationVariables()), edgeAssignments(settings.isAllowEdgeAssignmentsSet()), flatten(settings.isExportFlattenedSet()), substituteConstants(true), allowedModelFeatures(storm::jani::getAllKnownModelFeatures()) { 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 68dfd7d5a..e5af6e3d0 100644 --- a/src/storm-conv/converter/options/JaniConversionOptions.h +++ b/src/storm-conv/converter/options/JaniConversionOptions.h @@ -18,8 +18,8 @@ namespace storm { /// (Automaton,Variable)-pairs that will be transformed to location variables of the respective automaton. std::vector> locationVariables; - /// If set, the model will be made standard compliant (e.g. no state rewards for discrete time models) - bool standardCompliant; + /// If set, the model might have transient assignments to the edges + bool edgeAssignments; /// If set, the model is transformed into a single automaton bool flatten; diff --git a/src/storm-conv/settings/modules/JaniExportSettings.cpp b/src/storm-conv/settings/modules/JaniExportSettings.cpp index 37fb525ab..207de8edb 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.cpp +++ b/src/storm-conv/settings/modules/JaniExportSettings.cpp @@ -14,19 +14,17 @@ namespace storm { namespace modules { const std::string JaniExportSettings::moduleName = "exportJani"; - const std::string JaniExportSettings::standardCompliantOptionName = "standard-compliant"; - const std::string JaniExportSettings::standardCompliantOptionShortName = "standard"; + const std::string JaniExportSettings::edgeAssignmentsOptionName = "edge-assignments"; const std::string JaniExportSettings::exportFlattenOptionName = "flatten"; const std::string JaniExportSettings::locationVariablesOptionName = "location-variables"; const std::string JaniExportSettings::globalVariablesOptionName = "globalvars"; const std::string JaniExportSettings::compactJsonOptionName = "compactjson"; - const std::string JaniExportSettings::eliminateArraysOptionName = "eliminate-arrays"; - const std::string JaniExportSettings::eliminateFunctionsOptionName = "eliminate-functions"; - + const std::string JaniExportSettings::eliminateArraysOptionName = "remove-arrays"; + const std::string JaniExportSettings::eliminateFunctionsOptionName = "remove-functions"; 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()); - this->addOption(storm::settings::OptionBuilder(moduleName, standardCompliantOptionName, false, "Export in standard compliant variant.").setShortName(standardCompliantOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, edgeAssignmentsOptionName, false, "If set, the output model can have transient edge assignments. This can simplify the jani model but is not compliant to the jani standard.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, exportFlattenOptionName, false, "Flattens the composition of Automata to obtain an equivalent model that contains exactly one automaton").build()); this->addOption(storm::settings::OptionBuilder(moduleName, globalVariablesOptionName, false, "If set, variables will preferably be made global, e.g., to guarantee the same variable order as in the input file.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, compactJsonOptionName, false, "If set, the size of the resulting jani file will be reduced at the cost of (human-)readability.").build()); @@ -34,8 +32,8 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, eliminateFunctionsOptionName, false, "If set, transforms the model such that functions are eliminated.").build()); } - bool JaniExportSettings::isExportAsStandardJaniSet() const { - return this->getOption(standardCompliantOptionName).getHasOptionBeenSet(); + bool JaniExportSettings::isAllowEdgeAssignmentsSet() const { + return this->getOption(edgeAssignmentsOptionName).getHasOptionBeenSet(); } bool JaniExportSettings::isExportFlattenedSet() const { diff --git a/src/storm-conv/settings/modules/JaniExportSettings.h b/src/storm-conv/settings/modules/JaniExportSettings.h index 985eabe4a..04952e9fd 100644 --- a/src/storm-conv/settings/modules/JaniExportSettings.h +++ b/src/storm-conv/settings/modules/JaniExportSettings.h @@ -14,7 +14,7 @@ namespace storm { */ JaniExportSettings(); - bool isExportAsStandardJaniSet() const; + bool isAllowEdgeAssignmentsSet() const; bool isExportFlattenedSet() const; @@ -36,8 +36,7 @@ namespace storm { static const std::string moduleName; private: - static const std::string standardCompliantOptionName; - static const std::string standardCompliantOptionShortName; + static const std::string edgeAssignmentsOptionName; static const std::string exportFlattenOptionName; static const std::string locationVariablesOptionName; static const std::string globalVariablesOptionName; diff --git a/src/storm/storage/SymbolicModelDescription.cpp b/src/storm/storage/SymbolicModelDescription.cpp index a16e7df54..fe85673ad 100644 --- a/src/storm/storage/SymbolicModelDescription.cpp +++ b/src/storm/storage/SymbolicModelDescription.cpp @@ -120,23 +120,23 @@ namespace storm { return result; } - SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal, bool standardCompliant) const { + SymbolicModelDescription SymbolicModelDescription::toJani(bool makeVariablesGlobal) const { if (this->isJaniModel()) { return *this; } if (this->isPrismProgram()) { - return SymbolicModelDescription(this->asPrismProgram().toJani(makeVariablesGlobal, "", standardCompliant)); + return SymbolicModelDescription(this->asPrismProgram().toJani(makeVariablesGlobal, "")); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot transform model description to the JANI format."); } } - std::pair> SymbolicModelDescription::toJani(std::vector const& properties, bool makeVariablesGlobal, bool standardCompliant) const { + std::pair> SymbolicModelDescription::toJani(std::vector const& properties, bool makeVariablesGlobal) const { if (this->isJaniModel()) { return std::make_pair(*this, std::vector()); } if (this->isPrismProgram()) { - auto modelProperties = this->asPrismProgram().toJani(properties, makeVariablesGlobal, "", standardCompliant); + auto modelProperties = this->asPrismProgram().toJani(properties, makeVariablesGlobal, ""); 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 2f50c6986..eb64d2bef 100644 --- a/src/storm/storage/SymbolicModelDescription.h +++ b/src/storm/storage/SymbolicModelDescription.h @@ -38,7 +38,7 @@ namespace storm { std::vector getParameterNames() const; - SymbolicModelDescription toJani(bool makeVariablesGlobal = true, bool standardCompliant = false) const; + SymbolicModelDescription toJani(bool makeVariablesGlobal = true) const; /*! * Ensures that this model is a JANI model by, e.g., converting prism to jani. @@ -48,7 +48,7 @@ namespace storm { * * @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; + std::pair> toJani(std::vector const& properties, bool makeVariablesGlobal) const; SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const; SymbolicModelDescription preprocess(std::map const& constantDefinitions) const; diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 7aa546c85..11255bf12 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -1276,6 +1276,12 @@ namespace storm { automaton.pushEdgeAssignmentsToDestinations(); } } + + void Model::pushEdgeAssignmentsToDestinations() { + for (auto& automaton : automata) { + automaton.pushEdgeAssignmentsToDestinations(); + } + } void Model::liftTransientEdgeDestinationAssignments(int64_t maxLevel) { for (auto& automaton : this->getAutomata()) { diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h index 14ba38540..3824398e5 100644 --- a/src/storm/storage/jani/Model.h +++ b/src/storm/storage/jani/Model.h @@ -546,6 +546,9 @@ namespace storm { void makeStandardJaniCompliant(); + // Pushes all edge assignments to their destination + void pushEdgeAssignmentsToDestinations(); + /*! * Checks whether in the composition, actions are reused: That is, if the model is put in parallel composition and the same action potentially leads to multiple edges from the same state. * @return @@ -612,6 +615,7 @@ namespace storm { VariableSet globalVariables; /// A mapping from names to function definitions + /// Since we use an unordered_map, references to function definitions will not get invalidated when more function definitions are added std::unordered_map globalFunctions; /// The list of automata. diff --git a/src/storm/storage/prism/Program.cpp b/src/storm/storage/prism/Program.cpp index 3c6936d52..18299f4bd 100644 --- a/src/storm/storage/prism/Program.cpp +++ b/src/storm/storage/prism/Program.cpp @@ -1795,17 +1795,17 @@ namespace storm { return Command(newCommandIndex, false, actionIndex, actionName, newGuard, newUpdates, this->getFilename(), 0); } - storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix, bool standardCompliant) const { + storm::jani::Model Program::toJani(bool allVariablesGlobal, std::string suffix) const { ToJaniConverter converter; - auto janiModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant); + 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; } - std::pair> Program::toJani(std::vector const& properties, bool allVariablesGlobal, std::string suffix, bool standardCompliant) const { + std::pair> Program::toJani(std::vector const& properties, bool allVariablesGlobal, std::string suffix) const { ToJaniConverter converter; - auto janiModel = converter.convert(*this, allVariablesGlobal, suffix, standardCompliant); + auto janiModel = converter.convert(*this, allVariablesGlobal, suffix); std::vector newProperties; if (converter.labelsWereRenamed() || converter.rewardModelsWereRenamed()) { newProperties = converter.applyRenaming(properties); diff --git a/src/storm/storage/prism/Program.h b/src/storm/storage/prism/Program.h index 5046b5541..cb0fc696c 100644 --- a/src/storm/storage/prism/Program.h +++ b/src/storm/storage/prism/Program.h @@ -649,14 +649,14 @@ namespace storm { /*! * Converts the PRISM model into an equivalent JANI model. */ - storm::jani::Model toJani(bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const; + storm::jani::Model toJani(bool allVariablesGlobal = true, std::string suffix = "") const; /*! * 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> toJani(std::vector const& properties, bool allVariablesGlobal = true, std::string suffix = "", bool standardCompliant = false) const; + std::pair> toJani(std::vector const& properties, bool allVariablesGlobal = true, std::string suffix = "") const; private: /*! diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 7b62f2324..c1f9b14d3 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -18,15 +18,13 @@ namespace storm { namespace prism { - storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix, bool standardCompliant) { + storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix) { labelRenaming.clear(); rewardModelRenaming.clear(); formulaToFunctionCallMap.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; - // Start by creating an empty JANI model. storm::jani::ModelType modelType; switch (program.getModelType()) { @@ -254,20 +252,6 @@ namespace storm { } STORM_LOG_THROW(transientEdgeAssignments.empty() || transientLocationAssignments.empty() || !program.specifiesSystemComposition(), storm::exceptions::NotImplementedException, "Cannot translate reward models from PRISM to JANI that specify a custom system composition."); - // If we are not allowed to produce state rewards, we need to create a mapping from action indices to transient - // location assignments. This is done so that all assignments are added only *once* for synchronizing actions. - std::map> transientRewardLocationAssignmentsPerAction; - if (!produceStateRewards) { - for (auto const& action : program.getActions()) { - auto& list = transientRewardLocationAssignmentsPerAction[janiModel.getActionIndex(action)]; - for (auto const& assignment : transientLocationAssignments) { - if (assignment.isTransient() && assignment.getVariable().isRealVariable()) { - list.emplace_back(assignment); - } - } - } - } - // Now create the separate JANI automata from the modules of the PRISM program. While doing so, we use the // previously built mapping to make variables global that are read by more than one module. std::set firstModules; @@ -310,9 +294,7 @@ namespace storm { if (firstModule) { storm::jani::Location& onlyLocation = automaton.getLocation(onlyLocationIndex); for (auto const& assignment : transientLocationAssignments) { - if (assignment.getVariable().isBooleanVariable() || produceStateRewards) { - onlyLocation.addTransientAssignment(assignment); - } + onlyLocation.addTransientAssignment(assignment); } } @@ -357,12 +339,6 @@ namespace storm { templateEdge->addTransientAssignment(assignment); } } - if (!produceStateRewards) { - transientEdgeAssignmentsToAdd = transientRewardLocationAssignmentsPerAction.find(janiModel.getActionIndex(command.getActionName())); - for (auto const& assignment : transientEdgeAssignmentsToAdd->second) { - templateEdge->addTransientAssignment(assignment, true); - } - } // Create the edge object. storm::jani::Edge newEdge; diff --git a/src/storm/storage/prism/ToJaniConverter.h b/src/storm/storage/prism/ToJaniConverter.h index 3af62b61d..38d5f331e 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 = "", bool standardCompliant = false); + storm::jani::Model convert(storm::prism::Program const& program, bool allVariablesGlobal = true, std::string suffix = ""); bool labelsWereRenamed() const; bool rewardModelsWereRenamed() const;