Browse Source

Merge branch 'master' into storm-pars-analysis-monotonicity

tempestpy_adaptions
Jip Spel 5 years ago
parent
commit
0e04cfc883
  1. 17
      src/storm/builder/DdJaniModelBuilder.cpp

17
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."); 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. // Now that we have built the destinations, we always take the full guard.
guard = rangedGuard;
storm::dd::Bdd<Type> 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. // Start by gathering all variables that were written in at least one destination.
std::set<storm::expressions::Variable> globalVariablesInSomeDestination; std::set<storm::expressions::Variable> globalVariablesInSomeDestination;
@ -1361,8 +1362,8 @@ namespace storm {
} }
// Add the source location and the guard. // Add the source location and the guard.
storm::dd::Add<Type, ValueType> sourceLocationAndGuard = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard.template toAdd<ValueType>();
transitions *= sourceLocationAndGuard;
storm::dd::Add<Type, ValueType> guardAdd = guard.template toAdd<ValueType>();
transitions *= guardAdd;
// If we multiply the ranges of global variables, make sure everything stays within its bounds. // If we multiply the ranges of global variables, make sure everything stays within its bounds.
if (!globalVariablesInSomeDestination.empty()) { if (!globalVariablesInSomeDestination.empty()) {
@ -1381,8 +1382,8 @@ namespace storm {
// Finally treat the transient assignments. // Finally treat the transient assignments.
std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments; std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>> transientEdgeAssignments;
if (!this->transientVariables.empty()) { 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) { if (exitRates) {
newTransientEdgeAssignments *= exitRates.get(); newTransientEdgeAssignments *= exitRates.get();
} }
@ -1390,7 +1391,7 @@ namespace storm {
} ); } );
} }
return EdgeDd(isMarkovian, guard, guard.template toAdd<ValueType>() * transitions, transientEdgeAssignments, globalVariablesInSomeDestination);
return EdgeDd(isMarkovian, guard, transitions, transientEdgeAssignments, globalVariablesInSomeDestination);
} else { } else {
return EdgeDd(false, rangedGuard, rangedGuard.template toAdd<ValueType>(), std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>>(), std::set<storm::expressions::Variable>()); return EdgeDd(false, rangedGuard, rangedGuard.template toAdd<ValueType>(), std::map<storm::expressions::Variable, storm::dd::Add<Type, ValueType>>(), std::set<storm::expressions::Variable>());
} }
@ -1516,7 +1517,7 @@ namespace storm {
// Check for overlapping guards. // Check for overlapping guards.
overlappingGuards = !(edgeDd.guard && allGuards).isZero(); overlappingGuards = !(edgeDd.guard && allGuards).isZero();
// Issue a warning if there are overlapping guards in a DTMC. // 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."); 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.");

Loading…
Cancel
Save