From 9aa5bff988cb7e618359b97569469373e542cc87 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Sat, 11 Feb 2017 20:17:40 +0100 Subject: [PATCH] pgcl prob operator fix --- src/storm-pgcl/builder/ProgramGraphBuilder.cpp | 13 +++++++------ src/storm-pgcl/storage/ppg/ProgramGraph.cpp | 2 +- 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/src/storm-pgcl/builder/ProgramGraphBuilder.cpp b/src/storm-pgcl/builder/ProgramGraphBuilder.cpp index 8a15d5de2..89856c3ee 100644 --- a/src/storm-pgcl/builder/ProgramGraphBuilder.cpp +++ b/src/storm-pgcl/builder/ProgramGraphBuilder.cpp @@ -55,22 +55,23 @@ namespace storm { builder.storeNextLocation(builder.nextLoc()); storm::ppg::ProgramLocation* bodyStart = builder.newLocation(); builder.buildBlock(*s.getLeftBranch()); - beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), builder.nextLocId()); + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), bodyStart->id()); builder.storeNextLocation(builder.nextLoc()); bodyStart = builder.newLocation(); - beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), builder.nextLocId()); + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), bodyStart->id()); builder.buildBlock(*s.getRightBranch()); } void ProgramGraphBuilderVisitor::visit(storm::pgcl::ProbabilisticBranch const& s) { 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(); - beforeStatementLocation->addProgramEdgeGroup(s.getProbability())->addEdge(builder.nextLocId(), builder.noAction()); + beforeStatementLocation->addProgramEdgeGroup(s.getProbability())->addEdge(builder.noAction(), bodyStart->id()); builder.buildBlock(*s.getLeftBranch()); - builder.storeNextLocation(builder.nextLoc()); + builder.storeNextLocation(afterStatementLocation); 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()); } } diff --git a/src/storm-pgcl/storage/ppg/ProgramGraph.cpp b/src/storm-pgcl/storage/ppg/ProgramGraph.cpp index c513ddfe1..547fe0b14 100644 --- a/src/storm-pgcl/storage/ppg/ProgramGraph.cpp +++ b/src/storm-pgcl/storage/ppg/ProgramGraph.cpp @@ -190,7 +190,7 @@ namespace storm { for (auto const& loc : locations) { if (loc.second.nrOutgoingEdgeGroups() > 1) { for (auto const& edgegroup : loc.second) { - os << "\teg" << edgegroup->getId() << "[shape=circle];"<< std::endl; + os << "\teg" << edgegroup->getId() << "[shape=rectangle];"<< std::endl; } } }