From a616e2743dfcfe51a2d04f1734cc1593bd06d9e3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 11 Jul 2018 15:51:12 +0200 Subject: [PATCH] fixes to standard-compliant prism-to-jani conversion --- src/storm/storage/jani/Automaton.cpp | 11 +++++-- src/storm/storage/jani/Model.cpp | 5 --- src/storm/storage/prism/ToJaniConverter.cpp | 35 ++++++++++++++++++++- 3 files changed, 42 insertions(+), 9 deletions(-) diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp index e962562d2..790a0489d 100644 --- a/src/storm/storage/jani/Automaton.cpp +++ b/src/storm/storage/jani/Automaton.cpp @@ -427,23 +427,28 @@ namespace storm { auto& location = locations[locationIndex]; auto edges = this->getEdgesFromLocation(locationIndex); + storm::jani::Location newLocation(location.getName()); + bool createNewLocation = true; for (auto& edge : edges) { STORM_LOG_THROW(encounteredTemplateEdges.find(edge.getTemplateEdge()) == encounteredTemplateEdges.end(), storm::exceptions::NotSupportedException, "Pushing location assignments to edges is only supported for automata with unique template edges."); auto& templateEdge = edge.getTemplateEdge(); encounteredTemplateEdges.insert(templateEdge); - storm::jani::Location newLocation(location.getName()); for (auto const& assignment : location.getAssignments().getTransientAssignments()) { if (assignment.getVariable().isTransient() && assignment.getVariable().isRealVariable()) { templateEdge->addTransientAssignment(assignment, true); - } else { + } else if (createNewLocation) { newLocation.addTransientAssignment(assignment); } } - location = std::move(newLocation); + if (createNewLocation) { + createNewLocation = false; + } } + + location = std::move(newLocation); } } diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp index 0cbbaae14..30072fa56 100644 --- a/src/storm/storage/jani/Model.cpp +++ b/src/storm/storage/jani/Model.cpp @@ -742,11 +742,6 @@ namespace storm { } std::shared_ptr Model::getStandardSystemComposition() const { - // If there's just one automaton, we must not use the parallel composition operator. - if (this->getNumberOfAutomata() == 1) { - return std::make_shared(this->getAutomata().front().getName()); - } - // Determine the action indices used by each of the automata and create the standard subcompositions. std::set allActionIndices; std::vector> automatonActionIndices; diff --git a/src/storm/storage/prism/ToJaniConverter.cpp b/src/storm/storage/prism/ToJaniConverter.cpp index 9712a52a7..36a47d7f9 100644 --- a/src/storm/storage/prism/ToJaniConverter.cpp +++ b/src/storm/storage/prism/ToJaniConverter.cpp @@ -7,6 +7,9 @@ #include "storm/storage/jani/Model.h" #include "storm/storage/jani/TemplateEdge.h" +#include "storm/settings/SettingsManager.h" +#include "storm/settings/modules/JaniExportSettings.h" + #include "storm/utility/macros.h" #include "storm/exceptions/NotImplementedException.h" @@ -15,6 +18,8 @@ namespace storm { storm::jani::Model ToJaniConverter::convert(storm::prism::Program const& program, bool allVariablesGlobal, std::string suffix) { std::shared_ptr manager = program.getManager().getSharedPointer(); + + bool produceStateRewards = !storm::settings::getModule().isExportAsStandardJaniSet() || program.getModelType() == storm::prism::Program::ModelType::CTMC; // Start by creating an empty JANI model. storm::jani::ModelType modelType; @@ -153,6 +158,20 @@ 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; @@ -195,10 +214,13 @@ namespace storm { automaton.addInitialLocation(onlyLocationIndex); // If we are translating the first module that has the action, we need to add the transient assignments to the location. + // However, in standard compliant JANI, there are no state rewards if (firstModule) { storm::jani::Location& onlyLocation = automaton.getLocation(onlyLocationIndex); for (auto const& assignment : transientLocationAssignments) { - onlyLocation.addTransientAssignment(assignment); + if (assignment.getVariable().isBooleanVariable() || produceStateRewards) { + onlyLocation.addTransientAssignment(assignment); + } } } @@ -243,6 +265,12 @@ 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; @@ -261,6 +289,11 @@ namespace storm { // NOTE: This only works for the standard composition and not for any custom compositions. This case // must be checked for earlier. for (auto actionIndex : actionIndicesOfModule) { + // Do not delete rewards dealt out on non-synchronizing edges. + if (actionIndex == janiModel.getActionIndex("")) { + continue; + } + auto it = transientEdgeAssignments.find(actionIndex); if (it != transientEdgeAssignments.end()) { transientEdgeAssignments.erase(it);