From 0842cb1bd701303de41798071cfebd3fe3b81447 Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 15 Oct 2019 20:51:01 +0200 Subject: [PATCH] DdJaniModelBuilder: adding source locations to guards to correctly track action fragments writing global variables --- src/storm/builder/DdJaniModelBuilder.cpp | 17 +++++++++-------- 1 file changed, 9 insertions(+), 8 deletions(-) diff --git a/src/storm/builder/DdJaniModelBuilder.cpp b/src/storm/builder/DdJaniModelBuilder.cpp index f05199ccc..3e0250ac8 100644 --- a/src/storm/builder/DdJaniModelBuilder.cpp +++ b/src/storm/builder/DdJaniModelBuilder.cpp @@ -1325,9 +1325,10 @@ namespace storm { STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect."); } - + // Now that we have built the destinations, we always take the full guard. - guard = rangedGuard; + storm::dd::Bdd sourceLocationBdd = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()); + guard = sourceLocationBdd && rangedGuard; // Start by gathering all variables that were written in at least one destination. std::set globalVariablesInSomeDestination; @@ -1361,8 +1362,8 @@ namespace storm { } // Add the source location and the guard. - storm::dd::Add sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd() * guard.template toAdd(); - transitions *= sourceLocationAndGuard; + storm::dd::Add guardAdd = guard.template toAdd(); + transitions *= guardAdd; // If we multiply the ranges of global variables, make sure everything stays within its bounds. if (!globalVariablesInSomeDestination.empty()) { @@ -1381,8 +1382,8 @@ namespace storm { // Finally treat the transient assignments. std::map> transientEdgeAssignments; if (!this->transientVariables.empty()) { - performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &sourceLocationAndGuard, &exitRates] (storm::jani::Assignment const& assignment) { - auto newTransientEdgeAssignments = sourceLocationAndGuard * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); + performTransientAssignments(edge.getAssignments().getTransientAssignments(), [this, &transientEdgeAssignments, &guardAdd, &exitRates] (storm::jani::Assignment const& assignment) { + auto newTransientEdgeAssignments = guardAdd * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression()); if (exitRates) { newTransientEdgeAssignments *= exitRates.get(); } @@ -1390,7 +1391,7 @@ namespace storm { } ); } - return EdgeDd(isMarkovian, guard, guard.template toAdd() * transitions, transientEdgeAssignments, globalVariablesInSomeDestination); + return EdgeDd(isMarkovian, guard, transitions, transientEdgeAssignments, globalVariablesInSomeDestination); } else { return EdgeDd(false, rangedGuard, rangedGuard.template toAdd(), std::map>(), std::set()); } @@ -1516,7 +1517,7 @@ namespace storm { // Check for overlapping guards. overlappingGuards = !(edgeDd.guard && allGuards).isZero(); - + // Issue a warning if there are overlapping guards in a DTMC. STORM_LOG_WARN_COND(!overlappingGuards || this->model.getModelType() == storm::jani::ModelType::CTMC || this->model.getModelType() == storm::jani::ModelType::MA, "Guard of an edge in a DTMC overlaps with previous guards.");