Browse Source

A more accurate version of having multiple levels; seems to fix at least one open issue.

tempestpy_adaptions
sjunges 8 years ago
parent
commit
0c2d906b09
  1. 1
      src/storm/storage/jani/Edge.cpp
  2. 2
      src/storm/storage/jani/OrderedAssignments.cpp
  3. 3
      src/storm/storage/jani/TemplateEdge.cpp

1
src/storm/storage/jani/Edge.cpp

@ -107,6 +107,7 @@ namespace storm {
if(usesAssignmentLevels()) { if(usesAssignmentLevels()) {
templateEdge = std::make_shared<TemplateEdge>(templateEdge->simplifyIndexedAssignments(!hasSilentAction(), localVars)); templateEdge = std::make_shared<TemplateEdge>(templateEdge->simplifyIndexedAssignments(!hasSilentAction(), localVars));
std::vector<EdgeDestination> newdestinations; std::vector<EdgeDestination> newdestinations;
assert(templateEdge->getNumberOfDestinations() == destinations.size());
for (uint64_t i = 0; i < templateEdge->getNumberOfDestinations(); ++i) { for (uint64_t i = 0; i < templateEdge->getNumberOfDestinations(); ++i) {
auto const& templateDestination = templateEdge->getDestination(i); auto const& templateDestination = templateEdge->getDestination(i);
newdestinations.emplace_back(destinations[i].getLocationIndex(), destinations[i].getProbability(), templateDestination); newdestinations.emplace_back(destinations[i].getLocationIndex(), destinations[i].getProbability(), templateDestination);

2
src/storm/storage/jani/OrderedAssignments.cpp

@ -74,7 +74,7 @@ namespace storm {
if (allAssignments.empty()) { if (allAssignments.empty()) {
return false; return false;
} }
return getLowestLevel() != getHighestLevel();
return getLowestLevel() != 0 || getHighestLevel() != 0;
} }
bool OrderedAssignments::empty() const { bool OrderedAssignments::empty() const {

3
src/storm/storage/jani/TemplateEdge.cpp

@ -133,6 +133,9 @@ namespace storm {
} }
bool TemplateEdge::usesAssignmentLevels() const { bool TemplateEdge::usesAssignmentLevels() const {
if (assignments.hasMultipleLevels()) {
return true;
}
for (auto const& destination : this->getDestinations()) { for (auto const& destination : this->getDestinations()) {
if (destination.usesAssignmentLevels()) { if (destination.usesAssignmentLevels()) {
return true; return true;

Loading…
Cancel
Save