diff --git a/src/builder/ProgramGraphBuilder.cpp b/src/builder/ProgramGraphBuilder.cpp new file mode 100644 index 000000000..02aa89c12 --- /dev/null +++ b/src/builder/ProgramGraphBuilder.cpp @@ -0,0 +1,69 @@ +#include "ProgramGraphBuilder.h" +#include "src/storage/pgcl/ObserveStatement.h" +#include "src/storage/pgcl/LoopStatement.h" +#include "src/storage/pgcl/IfStatement.h" +#include "src/storage/pgcl/NondeterministicBranch.h" +#include "src/storage/pgcl/ProbabilisticBranch.h" + + +namespace storm { + namespace builder { + void ProgramGraphBuilderVisitor::visit(storm::pgcl::AssignmentStatement const& s) { + builder.currentLoc()->addProgramEdgeToAllGroups(builder.getAction(), builder.nextLocId()); + + } + void ProgramGraphBuilderVisitor::visit(storm::pgcl::ObserveStatement const& s) { + builder.currentLoc()->addProgramEdgeToAllGroups(builder.noAction(), s.getCondition().getBooleanExpression(), builder.nextLocId()); + } + void ProgramGraphBuilderVisitor::visit(storm::pgcl::IfStatement const& s) { + storm::expressions::Expression elseCondition; + storm::ppg::ProgramLocation* beforeStatementLocation = builder.currentLoc(); + builder.storeNextLocation(builder.nextLoc()); + storm::ppg::ProgramLocation* bodyStart = builder.newLocation(); + builder.buildBlock(*s.getIfBody()); + if(s.hasElse()) { + builder.storeNextLocation(builder.nextLoc()); + bodyStart = builder.newLocation(); + builder.buildBlock(*s.getElseBody()); + } + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), s.getCondition().getBooleanExpression(), bodyStart->id()); + if(s.hasElse()) { + elseCondition = !s.getCondition().getBooleanExpression(); + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), elseCondition, builder.nextLocId()); + } + + } + void ProgramGraphBuilderVisitor::visit(storm::pgcl::LoopStatement const& s) { + storm::ppg::ProgramLocation* beforeStatementLocation = builder.currentLoc(); + builder.storeNextLocation(beforeStatementLocation); + storm::ppg::ProgramLocation* bodyStart = builder.newLocation(); + builder.buildBlock(*s.getBody()); + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), s.getCondition().getBooleanExpression(), bodyStart->id()); + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), !s.getCondition().getBooleanExpression(), builder.nextLocId()); + } + + void ProgramGraphBuilderVisitor::visit(storm::pgcl::NondeterministicBranch const& s) { + storm::ppg::ProgramLocation* beforeStatementLocation = builder.currentLoc(); + builder.storeNextLocation(builder.nextLoc()); + storm::ppg::ProgramLocation* bodyStart = builder.newLocation(); + builder.buildBlock(*s.getLeftBranch()); + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), builder.nextLocId()); + builder.storeNextLocation(builder.nextLoc()); + bodyStart = builder.newLocation(); + beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), builder.nextLocId()); + 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* bodyStart = builder.newLocation(); + beforeStatementLocation->addProgramEdgeGroup(s.getProbability()); + builder.buildBlock(*s.getLeftBranch()); + builder.storeNextLocation(builder.nextLoc()); + bodyStart = builder.newLocation(); + beforeStatementLocation->addProgramEdgeGroup(1 - s.getProbability()); + builder.buildBlock(*s.getRightBranch()); + } + } +} \ No newline at end of file diff --git a/src/builder/ProgramGraphBuilder.h b/src/builder/ProgramGraphBuilder.h new file mode 100644 index 000000000..5cc61ada9 --- /dev/null +++ b/src/builder/ProgramGraphBuilder.h @@ -0,0 +1,141 @@ +#pragma once + +#include "src/storage/pgcl/PgclProgram.h" +#include "src/storage/ppg/ProgramGraph.h" +#include "src/storage/pgcl/AbstractStatementVisitor.h" + +namespace storm { + namespace builder { + class ProgramGraphBuilder; + + + class ProgramGraphBuilderVisitor: public storm::pgcl::AbstractStatementVisitor{ + public: + ProgramGraphBuilderVisitor(ProgramGraphBuilder& builder) : builder(builder) { + + } + + virtual void visit(storm::pgcl::AssignmentStatement const&); + virtual void visit(storm::pgcl::ObserveStatement const&); + virtual void visit(storm::pgcl::IfStatement const&); + virtual void visit(storm::pgcl::LoopStatement const&); + virtual void visit(storm::pgcl::NondeterministicBranch const&); + virtual void visit(storm::pgcl::ProbabilisticBranch const&); + + private: + ProgramGraphBuilder& builder; + }; + + + class ProgramGraphBuilder { + + + public: + static storm::ppg::ProgramGraph* build(storm::pgcl::PgclProgram const& program) { + ProgramGraphBuilder builder(program); + builder.run(); + return builder.finalize(); + } + + ~ProgramGraphBuilder() { + if(graph != nullptr) { + // delete graph; + } + } + + storm::ppg::ProgramLocation* currentLoc() const { + return currentStack.back(); + } + + storm::ppg::ProgramLocation* newLocation() { + currentStack.push_back(graph->addLocation()); + return currentLoc(); + } + + storm::ppg::ProgramLocation* storeNextLocation(storm::ppg::ProgramLocation* loc) { + nextStack.push_back(loc); + } + + storm::ppg::ProgramLocation* nextLoc() const { + return nextStack.back(); + } + + storm::ppg::ProgramLocationIdentifier nextLocId() const { + return nextLoc()->id(); + } + + storm::ppg::ProgramActionIdentifier getAction() const { + return graph->addAction(); + } + + storm::ppg::ProgramActionIdentifier noAction() const { + return noActionId; + } + + + + void buildBlock(storm::pgcl::PgclBlock const& block) { + + ProgramGraphBuilderVisitor visitor(*this); + for(auto const& statement : block) { + std::cout << "Statement " << statement->getLocationNumber() << std::endl; + if(!statement->isLast()) { + nextStack.push_back(graph->addLocation(false)); + } + assert(!currentStack.empty()); + assert(!nextStack.empty()); + statement->accept(visitor); + assert(!currentStack.empty()); + assert(!nextStack.empty()); + currentStack.back() = nextStack.back(); + nextStack.pop_back(); + } + } + + + private: + ProgramGraphBuilder(storm::pgcl::PgclProgram const& program) + : program(program) + { + graph = new storm::ppg::ProgramGraph(program.getExpressionManager(), program.getVariables()); + noActionId = getAction(); + + } + + void run() { + currentStack.push_back(graph->addLocation(true)); + // Terminal state. + nextStack.push_back(graph->addLocation(false)); + // Observe Violated State. + if(program.hasObserve()) { + observeFailedState = graph->addLocation(); + } + buildBlock(program); + } + + + storm::ppg::ProgramGraph* finalize() { + storm::ppg::ProgramGraph* tmp = graph; + graph = nullptr; + return tmp; + } + + + + + std::vector currentStack; + std::vector nextStack; + + storm::ppg::ProgramActionIdentifier noActionId; + + storm::ppg::ProgramLocation* observeFailedState = nullptr; + + storm::pgcl::PgclProgram const& program; + storm::ppg::ProgramGraph* graph; + + + + }; + + } +} \ No newline at end of file