Browse Source

pgcl prob operator fix

tempestpy_adaptions
Sebastian Junges 8 years ago
parent
commit
9aa5bff988
  1. 13
      src/storm-pgcl/builder/ProgramGraphBuilder.cpp
  2. 2
      src/storm-pgcl/storage/ppg/ProgramGraph.cpp

13
src/storm-pgcl/builder/ProgramGraphBuilder.cpp

@ -55,22 +55,23 @@ namespace storm {
builder.storeNextLocation(builder.nextLoc()); builder.storeNextLocation(builder.nextLoc());
storm::ppg::ProgramLocation* bodyStart = builder.newLocation(); storm::ppg::ProgramLocation* bodyStart = builder.newLocation();
builder.buildBlock(*s.getLeftBranch()); builder.buildBlock(*s.getLeftBranch());
beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), builder.nextLocId());
beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), bodyStart->id());
builder.storeNextLocation(builder.nextLoc()); builder.storeNextLocation(builder.nextLoc());
bodyStart = builder.newLocation(); bodyStart = builder.newLocation();
beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), builder.nextLocId());
beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), bodyStart->id());
builder.buildBlock(*s.getRightBranch()); builder.buildBlock(*s.getRightBranch());
} }
void ProgramGraphBuilderVisitor::visit(storm::pgcl::ProbabilisticBranch const& s) { void ProgramGraphBuilderVisitor::visit(storm::pgcl::ProbabilisticBranch const& s) {
storm::ppg::ProgramLocation* beforeStatementLocation = builder.currentLoc(); storm::ppg::ProgramLocation* beforeStatementLocation = builder.currentLoc();
builder.storeNextLocation(builder.nextLoc());
storm::ppg::ProgramLocation* afterStatementLocation = builder.nextLoc();
builder.storeNextLocation(afterStatementLocation);
storm::ppg::ProgramLocation* bodyStart = builder.newLocation(); storm::ppg::ProgramLocation* bodyStart = builder.newLocation();
beforeStatementLocation->addProgramEdgeGroup(s.getProbability())->addEdge(builder.nextLocId(), builder.noAction());
beforeStatementLocation->addProgramEdgeGroup(s.getProbability())->addEdge(builder.noAction(), bodyStart->id());
builder.buildBlock(*s.getLeftBranch()); builder.buildBlock(*s.getLeftBranch());
builder.storeNextLocation(builder.nextLoc());
builder.storeNextLocation(afterStatementLocation);
bodyStart = builder.newLocation(); bodyStart = builder.newLocation();
beforeStatementLocation->addProgramEdgeGroup(1 - s.getProbability())->addEdge(builder.nextLocId(), builder.noAction());
beforeStatementLocation->addProgramEdgeGroup(1 - s.getProbability())->addEdge(builder.noAction(), bodyStart->id());
builder.buildBlock(*s.getRightBranch()); builder.buildBlock(*s.getRightBranch());
} }
} }

2
src/storm-pgcl/storage/ppg/ProgramGraph.cpp

@ -190,7 +190,7 @@ namespace storm {
for (auto const& loc : locations) { for (auto const& loc : locations) {
if (loc.second.nrOutgoingEdgeGroups() > 1) { if (loc.second.nrOutgoingEdgeGroups() > 1) {
for (auto const& edgegroup : loc.second) { for (auto const& edgegroup : loc.second) {
os << "\teg" << edgegroup->getId() << "[shape=circle];"<< std::endl;
os << "\teg" << edgegroup->getId() << "[shape=rectangle];"<< std::endl;
} }
} }
} }

Loading…
Cancel
Save