Builder for ProgramGraphs, for now, ignores actions.

Former-commit-id: 5f51f17e17 [formerly 1e48ddd098] Former-commit-id: 80434a7402
8 years ago · 8f8ef1564b
2 changed files with 210 additions and 0 deletions
--- a/src/builder/ProgramGraphBuilder.cpp
+++ 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());
+        }
+    }
+}
--- a/src/builder/ProgramGraphBuilder.h
+++ 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<storm::ppg::ProgramLocation*> currentStack;
+            std::vector<storm::ppg::ProgramLocation*> nextStack;
+            
+            storm::ppg::ProgramActionIdentifier noActionId;
+            
+            storm::ppg::ProgramLocation* observeFailedState = nullptr;
+            
+            storm::pgcl::PgclProgram const& program;
+            storm::ppg::ProgramGraph* graph;
+            
+            
+            
+        };
+        
+    }
+}