fixed if statement to program graph, added dot output for program graphs, added variable bounds, added settings to work with that, and usability of program graphs improved

Former-commit-id: 710f40b60c [formerly 6bffd842ab]
Former-commit-id: dfd9187bef

src/builder/JaniProgramGraphBuilder.cpp

@@ -1,4 +1,5 @@
 #include "JaniProgramGraphBuilder.h"
+#include "src/storage/jani/EdgeDestination.h"
 
 namespace storm {
     namespace builder {
@@ -16,12 +17,13 @@ namespace storm {
             return storm::jani::OrderedAssignments(vec);
         }
         
-        std::vector<storm::jani::EdgeDestination> buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) {
+        std::vector<storm::jani::EdgeDestination> JaniProgramGraphBuilder::buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) {
             storm::ppg::ProbabilisticProgramAction const& act = static_cast<storm::ppg::ProbabilisticProgramAction const&>(edge.getAction());
             std::vector<storm::jani::EdgeDestination> vec;
-            //for(auto const& value : act ) {
-            //    vec.emplace_back(
-            //}
+            for(auto const& assign : act ) {
+                storm::jani::Assignment  assignment(automaton.getVariables().getVariable(act.getVariableName()), expManager->integer(assign.value) ,0);
+                vec.emplace_back(janiLocId.at(edge.getTargetId()), assign.probability, assignment);
+            }
             return vec;
         }
     
@@ -30,22 +32,67 @@ namespace storm {
                 return buildProbabilisticDestinations(automaton, edge);
             } else {
                 storm::jani::OrderedAssignments oa = buildOrderedAssignments(automaton, static_cast<storm::ppg::DeterministicProgramAction const&>(edge.getAction()));
-                storm::jani::EdgeDestination dest(edge.getTargetId(), expManager->rational(1.0), oa);
+                storm::jani::EdgeDestination dest(janiLocId.at(edge.getTargetId()), expManager->rational(1.0), oa);
                 return {dest};
             }
         }
         
+        storm::expressions::Expression simplifyExpression(storm::expressions::Expression const& in) {
+            // TODO use bound restrictions etc.
+            return in.simplify();
+        }
         
+        std::pair<std::vector<storm::jani::Edge>, storm::expressions::Expression> JaniProgramGraphBuilder::addVariableChecks(storm::ppg::ProgramEdge const& edge) {
+            std::vector<storm::jani::Edge> edges;
+            storm::expressions::Expression newGuard;
+            newGuard = expManager->boolean(true);
+            if (edge.getAction().isProbabilistic()) {
+            
+            } else {
+                storm::ppg::DeterministicProgramAction const& act = static_cast<storm::ppg::DeterministicProgramAction const&>(edge.getAction());
+                STORM_LOG_THROW(act.nrLevels() <= 1, storm::exceptions::NotSupportedException, "Multi-level assignments with user variable bounds not supported");
+                for(auto const& group : act) {
+                    for(auto const& assignment : group) {
+                        if (isUserRestricted(assignment.first)) {
+                            assert(variableRestrictions.count(assignment.first) == 1);
+                            storm::storage::IntegerInterval const& bound = variableRestrictions.at(assignment.first);
+                            if (!assignment.second.containsVariables()) {
+                                // Constant assignments can be checked statically.
+                                // TODO we might still want to allow assignments which go out of bounds.
+                                STORM_LOG_THROW(bound.contains(assignment.second.evaluateAsInt()), storm::exceptions::NotSupportedException, "User provided bounds must contain all constant expressions");
+                            } else {
+                                // TODO currently only fully bounded restrictions are supported;
+                                assert(variableRestrictions.at(assignment.first).hasLeftBound() && variableRestrictions.at(assignment.first).hasRightBound());
+                                storm::expressions::Expression newCondition = simplifyExpression(edge.getCondition() && (assignment.second > bound.getRightBound().get() || assignment.second < bound.getLeftBound().get()));
+                                storm::jani::EdgeDestination dest(varOutOfBoundsLocations.at(assignment.first), expManager->rational(1.0), storm::jani::OrderedAssignments());
+                                storm::jani::Edge e(janiLocId.at(edge.getSourceId()), storm::jani::Model::silentActionIndex, boost::none, newCondition, {dest});
+                                edges.push_back(e);
+                                newGuard = newGuard && assignment.second <= bound.getRightBound().get() && assignment.second >= bound.getLeftBound().get();
+                            }
+                        }
+                    }
+                }
+            }
+            return {edges, newGuard};
+        }
         
-        void JaniProgramGraphBuilder::addEdges(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg, std::map<storm::ppg::ProgramLocationIdentifier, uint64_t>  const& janiLocId) {
-            for(auto it = pg.locationBegin(); it != pg.locationEnd(); ++it) {
+        
+        void JaniProgramGraphBuilder::addEdges(storm::jani::Automaton& automaton) {
+            for(auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) {
                 ppg::ProgramLocation const& loc = it->second;
-                if(loc.nrOutgoingEdgeGroups() == 1) {
+                if (loc.nrOutgoingEdgeGroups() == 0) {
+                    // TODO deadlock!
+                } else if (loc.nrOutgoingEdgeGroups() == 1) {
                     for(auto const& edge :  **(loc.begin())) {
-                        storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::silentActionIndex, boost::none, edge->getCondition(), buildDestinations(automaton, *edge));
+                        std::pair<std::vector<storm::jani::Edge>, storm::expressions::Expression> checks = addVariableChecks(*edge);
+                        for(auto const& check : checks.first) {
+                            automaton.addEdge(check);
+                        }
+                        storm::jani::Edge e(janiLocId.at(loc.id()), storm::jani::Model::silentActionIndex, boost::none, simplifyExpression(edge->getCondition() && checks.second), buildDestinations(automaton, *edge));
                         automaton.addEdge(e);
                     }
                 } else {
+                    // We have probabilistic branching
                     if(loc.hasNonDeterminism())
                     {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Combi of nondeterminism and probabilistic choices within a loc not supported yet");

src/builder/JaniProgramGraphBuilder.h

@@ -24,7 +24,7 @@ namespace storm {
         public:
             static unsigned janiVersion;
             
-            JaniProgramGraphBuilder() {
+            JaniProgramGraphBuilder(storm::ppg::ProgramGraph const& pg) : programGraph(pg) {
                 
             }
             
@@ -33,14 +33,20 @@ namespace storm {
             //}
             
         
+            void restrictAllVariables(int64_t from, int64_t to) {
+                for (auto const& v : programGraph.getVariables()) {
+                    variableRestrictions.emplace(v.first, storm::storage::IntegerInterval(from, to));
+                }
+            }
             
-            storm::jani::Model* build(storm::ppg::ProgramGraph const& pg, std::string const& name = "program_graph") {
-                expManager = pg.getExpressionManager();
+            storm::jani::Model* build(std::string const& name = "program_graph") {
+                expManager = programGraph.getExpressionManager();
                 storm::jani::Model* model = new storm::jani::Model(name, storm::jani::ModelType::MDP, janiVersion, expManager);
                 storm::jani::Automaton mainAutomaton("main");
-                addProcedureVariables(mainAutomaton, pg);
-                auto janiLocs = addProcedureLocations(mainAutomaton, pg);
-                addEdges(mainAutomaton, pg, janiLocs);
+                addProcedureVariables(mainAutomaton);
+                janiLocId = addProcedureLocations(mainAutomaton);
+                addVariableOoBLocations(mainAutomaton);
+                addEdges(mainAutomaton);
                 model->addAutomaton(mainAutomaton);
                 model->setStandardSystemComposition();
                 return model;
@@ -51,40 +57,77 @@ namespace storm {
                 return "l" + std::to_string(i);
             }
             
+            std::string janiVariableOutOfBoundsLocationName(storm::ppg::ProgramVariableIdentifier i) {
+                return "oob-" + programGraph.getVariableName(i);
+            }
             
             
-            void addEdges(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg, std::map<storm::ppg::ProgramLocationIdentifier, uint64_t>  const& janiLocId);
+            void addEdges(storm::jani::Automaton& automaton);
             std::vector<storm::jani::EdgeDestination> buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge );
-                
+            /**
+             * Helper for probabilistic assignments
+             */
+            std::vector<storm::jani::EdgeDestination> buildProbabilisticDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge );
+            
+            std::pair<std::vector<storm::jani::Edge>, storm::expressions::Expression> addVariableChecks(storm::ppg::ProgramEdge const& edge);
             
-            void addProcedureVariables(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) {
-                for (auto const& v : pg.getVariables()) {
-                    if(variableRestrictions.count(v.getIndex())) {
-                        assert(false);
+            bool isUserRestricted(storm::ppg::ProgramVariableIdentifier i) {
+                return variableRestrictions.count(i) == 1;
+            }
+            
+            void addProcedureVariables(storm::jani::Automaton& automaton) {
+                for (auto const& v : programGraph.getVariables()) {
+                    if(variableRestrictions.count(v.first) == 1) {
+                        storm::storage::IntegerInterval const& bounds = variableRestrictions.at(v.first);
+                        if (bounds.hasLeftBound()) {
+                            if (bounds.hasRightBound()) {
+                                storm::jani::BoundedIntegerVariable janiVar(v.second.getName(), v.second, expManager->integer(0), false, expManager->integer(bounds.getLeftBound().get()), expManager->integer(bounds.getRightBound().get()));
+                                automaton.addVariable(janiVar);
+                            } else {
+                                // Not yet supported.
+                                assert(false);
+                            }
+                        } else {
+                            // Not yet supported.
+                            assert(false);
+                        }
                     } else {
-                        storm::jani::UnboundedIntegerVariable janiVar(v.getName(), v, expManager->integer(0), false);
+                        storm::jani::UnboundedIntegerVariable janiVar(v.second.getName(), v.second, expManager->integer(0), false);
                         automaton.addVariable(janiVar);
                     }
                 }
             }
             
-            std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> addProcedureLocations(storm::jani::Automaton& automaton, storm::ppg::ProgramGraph const& pg) {
+            std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> addProcedureLocations(storm::jani::Automaton& automaton) {
                 std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> result;
-                for(auto it = pg.locationBegin(); it != pg.locationEnd(); ++it) {
+                for (auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) {
                     storm::jani::Location janiLoc(janiLocationName(it->second.id()));
                     result[it->second.id()] = automaton.addLocation(janiLoc);
-                    if(it->second.isInitial()) {
+                    if (it->second.isInitial()) {
                         automaton.addInitialLocation(result[it->second.id()]);
                     }
                 }
                 return result;
             }
             
+            void addVariableOoBLocations(storm::jani::Automaton& automaton) {
+                for(auto const& restr : variableRestrictions) {
+                    storm::jani::Location janiLoc(janiVariableOutOfBoundsLocationName(restr.first));
+                    uint64_t locId = automaton.addLocation(janiLoc);
+                    varOutOfBoundsLocations[restr.first] = locId;
+                    
+                }
+            }
+            
             /// Restrictions on variables
             std::map<uint64_t, storm::storage::IntegerInterval> variableRestrictions;
+            /// Locations for variables that would have gone ot o
+            std::map<uint64_t, uint64_t> varOutOfBoundsLocations;
+            std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> janiLocId;
             /// The expression manager
             std::shared_ptr<storm::expressions::ExpressionManager> expManager;
-            
+            /// The program graph to be translated
+            storm::ppg::ProgramGraph const& programGraph;
             
             
         };

src/builder/ProgramGraphBuilder.cpp

@@ -13,7 +13,7 @@ namespace storm {
             if(s.isDeterministic()) {
                 builder.currentLoc()->addProgramEdgeToAllGroups(builder.addAction(s.getVariable(), boost::get<storm::expressions::Expression>(s.getExpression())),  builder.nextLocId());
             } else {
-                builder.currentLoc()->addProgramEdgeToAllGroups(builder.addAction(s.getVariable(), builder.getExpressionManager()->integer(2)),  builder.nextLocId());
+                builder.currentLoc()->addProgramEdgeToAllGroups(builder.addAction(s.getVariable(), boost::get<storm::pgcl::UniformExpression>(s.getExpression())),  builder.nextLocId());
 
             }
         }
@@ -24,16 +24,19 @@ namespace storm {
             storm::expressions::Expression elseCondition;
             storm::ppg::ProgramLocation* beforeStatementLocation = builder.currentLoc();
             builder.storeNextLocation(builder.nextLoc());
-            storm::ppg::ProgramLocation* bodyStart = builder.newLocation();
+            storm::ppg::ProgramLocation* ifbodyStart = builder.newLocation();
             builder.buildBlock(*s.getIfBody());
+            storm::ppg::ProgramLocation* elsebodyStart;
             if(s.hasElse()) {
                 builder.storeNextLocation(builder.nextLoc());
-                bodyStart = builder.newLocation();
+                elsebodyStart = builder.newLocation();
                 builder.buildBlock(*s.getElseBody());
             }
-            beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), s.getCondition().getBooleanExpression(), bodyStart->id());
+            beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), s.getCondition().getBooleanExpression(), ifbodyStart->id());
+            elseCondition = !s.getCondition().getBooleanExpression();
             if(s.hasElse()) {
-                elseCondition = !s.getCondition().getBooleanExpression();
+                beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), elseCondition, elsebodyStart->id());
+            } else {
                 beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), elseCondition, builder.nextLocId());
             }
             

src/builder/ProgramGraphBuilder.h

@@ -3,6 +3,7 @@
 #include "src/storage/pgcl/PgclProgram.h"
 #include "src/storage/ppg/ProgramGraph.h"
 #include "src/storage/pgcl/AbstractStatementVisitor.h"
+#include "src/storage/pgcl/UniformExpression.h"
 
 namespace storm {
     namespace builder {
@@ -38,7 +39,7 @@ namespace storm {
             }
             
             ~ProgramGraphBuilder() {
-                if(graph != nullptr) {
+                if (graph != nullptr) {
                     delete graph;
                 }
             }
@@ -70,6 +71,12 @@ namespace storm {
                 return action->id();
             }
             
+            storm::ppg::ProgramActionIdentifier addAction(storm::expressions::Variable const& var, storm::pgcl::UniformExpression const& expr) const {
+                storm::ppg::ProbabilisticProgramAction* action = graph->addUniformProbabilisticAction(graph->getVariableId(var.getName()), expr.getBegin(), expr.getEnd());
+                return action->id();
+                
+            }
+            
             storm::ppg::ProgramActionIdentifier noAction() const {
                 return noActionId;
             }
@@ -82,9 +89,8 @@ namespace storm {
             
             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()) {
+                for (auto const& statement : block) {
+                    if (!statement->isLast()) {
                         nextStack.push_back(graph->addLocation(false));
                     }
                     assert(!currentStack.empty());
@@ -103,7 +109,7 @@ namespace storm {
             : program(program)
             {
                 graph = new storm::ppg::ProgramGraph(program.getExpressionManager(), program.getVariables());
-                noActionId = graph->addDeterministicAction()->id();
+                noActionId = graph->getNoActionId();
                 
             }
              
@@ -112,7 +118,7 @@ namespace storm {
                 // Terminal state.
                 nextStack.push_back(graph->addLocation(false));
                 // Observe Violated State.
-                if(program.hasObserve()) {
+                if (program.hasObserve()) {
                     observeFailedState = graph->addLocation();
                 }
                 buildBlock(program);

src/settings/modules/PGCLSettings.cpp

@@ -18,10 +18,17 @@ namespace storm {
             const std::string PGCLSettings::pgclFileOptionShortName = "pgcl";
             const std::string PGCLSettings::pgclToJaniOptionName = "to-jani";
             const std::string PGCLSettings::pgclToJaniOptionShortName = "tj";
+            const std::string PGCLSettings::programGraphToDotOptionName = "draw-program-graph";
+            const std::string PGCLSettings::programGraphToDotShortOptionName = "pg";
+            const std::string PGCLSettings::programVariableRestrictionsOptionName = "variable-restrictions";
+            const std::string PGCLSettings::programVariableRestrictionShortOptionName = "rvar";
+            
             
             PGCLSettings::PGCLSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, pgclFileOptionName, false, "Parses the pgcl program.").setShortName(pgclFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, pgclToJaniOptionName, false, "Transform to JANI.").setShortName(pgclToJaniOptionShortName).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, programGraphToDotOptionName, false, "Destination for the program graph dot output.").setShortName(programGraphToDotShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, programVariableRestrictionsOptionName, false, "Restrictions of program variables").setShortName(programVariableRestrictionShortOptionName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("descriptio", "description of the variable restrictions").build()).build());
             }
             
             bool PGCLSettings::isPgclFileSet() const {
@@ -36,6 +43,22 @@ namespace storm {
                 return this->getOption(pgclToJaniOptionName).getHasOptionBeenSet();
             }
             
+            bool PGCLSettings::isProgramGraphToDotSet() const {
+                return this->getOption(programGraphToDotOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string PGCLSettings::getProgramGraphDotOutputFilename() const {
+                return this->getOption(programGraphToDotOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            bool PGCLSettings::isProgramVariableRestrictionSet() const {
+                return this->getOption(programVariableRestrictionsOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string PGCLSettings::getProgramVariableRestrictions() const {
+                return this->getOption(programVariableRestrictionsOptionName).getArgumentByName("description").getValueAsString();
+            }
+            
             void PGCLSettings::finalize() {
                 
             }

src/settings/modules/PGCLSettings.h

@@ -25,10 +25,31 @@ namespace storm {
                 std::string getPgclFilename() const;
                 
                 /**
-                 *
+                 * Whether the pgcl should be transformed to Jani
                  */
                 bool isToJaniSet() const;
                 
+                /**
+                 * Whether the program graph should be drawn (dot output)
+                 */
+                bool isProgramGraphToDotSet() const;
+                
+                /**
+                 * Destination where to write dot output of the program graph.
+                 */
+                std::string getProgramGraphDotOutputFilename() const ;
+                
+                /**
+                 * Is program variable restriction string given
+                 */
+                bool isProgramVariableRestrictionSet() const;
+                
+                /**
+                 * String for program variable restrictions
+                 */
+                std::string getProgramVariableRestrictions() const;
+                
+                
                 bool check() const override;
                 void finalize() override;
                 
@@ -39,6 +60,10 @@ namespace storm {
                 static const std::string pgclFileOptionShortName;
                 static const std::string pgclToJaniOptionName;
                 static const std::string pgclToJaniOptionShortName;
+                static const std::string programGraphToDotOptionName;
+                static const std::string programGraphToDotShortOptionName;
+                static const std::string programVariableRestrictionsOptionName;
+                static const std::string programVariableRestrictionShortOptionName;
                 
             };
         }

src/storage/IntegerInterval.h

@@ -7,33 +7,47 @@ namespace storm {
         class IntegerInterval {
             
         public:
-            explicit IntegerInterval(uint64_t v) : leftBound(v), rightBound(v) {
+            explicit IntegerInterval(int64_t v) : leftBound(v), rightBound(v) {
                 
             }
             
-            IntegerInterval(uint64_t lb, uint64_t rb) : leftBound(lb), rightBound(rb) {
+            IntegerInterval(int64_t lb, int64_t rb) : leftBound(lb), rightBound(rb) {
                 
             }
             
-            bool hasLeftBound() {
+            bool hasLeftBound() const {
                 return leftBound != boost::none;
             }
             
-            bool hasRightBound() {
+            bool hasRightBound() const {
                 return rightBound != boost::none;
             }
             
-            boost::optional<uint64_t> getLeftBound() {
+            bool contains(int64_t val) const {
+                if (hasLeftBound()) {
+                    if (val < leftBound.get()) {
+                        return false;
+                    }
+                }
+                if (hasRightBound()) {
+                    if (val > rightBound.get()) {
+                        return false;
+                    }
+                }
+                return true;
+            }
+            
+            boost::optional<int64_t> getLeftBound() const {
                 return leftBound;
             }
             
-            boost::optional<uint64_t> getRightBound() {
+            boost::optional<int64_t> getRightBound() const {
                 return rightBound;
             }
             
         private:
-            boost::optional<uint64_t> leftBound;
-            boost::optional<uint64_t> rightBound;
+            boost::optional<int64_t> leftBound;
+            boost::optional<int64_t> rightBound;
             
         };
         

src/storage/pgcl/CompoundStatement.h

@@ -1,12 +1,4 @@
-/* 
- * File:   CompoundStatement.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:41
- */
-
-#ifndef COMPOUNDSTATEMENT_H
-#define	COMPOUNDSTATEMENT_H
+#pragma once
 
 #include "src/storage/pgcl/Statement.h"
 
@@ -27,6 +19,3 @@ namespace storm {
         };
     }
 }
-
-#endif	/* COMPOUNDSTATEMENT_H */
-

src/storage/ppg/ProgramAction.cpp

@@ -4,12 +4,16 @@
 namespace storm {
     namespace ppg {
         
-        ProbabilisticProgramAction::ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, int64_t from, int64_t to) : ProgramAction(graph, actId) {
+        ProbabilisticProgramAction::ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, ProgramVariableIdentifier var, int64_t from, int64_t to) : ProgramAction(graph, actId), var(var) {
             assert(from <= to);
             storm::expressions::Expression prob = graph->getExpressionManager()->integer(1) / graph->getExpressionManager()->integer(to - from + 1);
             for(int64_t i = from; i <= to; ++i) {
                 values.emplace_back(i, prob);
             }
         }
+        
+        std::string const& ProbabilisticProgramAction::getVariableName() const {
+            return getProgramGraph().getVariableName(var);
+        }
     }
 }

src/storage/ppg/ProgramAction.h

@@ -49,12 +49,14 @@ namespace storm {
              * Constructs a uniform assignment operation to a variable;
              * Action assigns a variable according to a uniform distribution [from, to]
              */
-            ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, int64_t from, int64_t to);
+            ProbabilisticProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId, ProgramVariableIdentifier var, int64_t from, int64_t to);
             
             bool isProbabilistic() const override{
                 return true;
             }
             
+            std::string const& getVariableName() const;
+            
             iterator begin() {
                 return values.begin();
             }
@@ -74,6 +76,7 @@ namespace storm {
         private:
             // TODO not the smartest representation (but at least it is internal!)
             std::vector<ValueProbabilityPair> values;
+            ProgramVariableIdentifier var;
             
         };
         
@@ -107,7 +110,7 @@ namespace storm {
             }
             
         private:
-            std::unordered_map<uint64_t, storm::expressions::Expression> map;
+            std::unordered_map<ProgramVariableIdentifier, storm::expressions::Expression> map;
         };
         
         class DeterministicProgramAction : public ProgramAction {
@@ -120,9 +123,7 @@ namespace storm {
                 
             }
             
-            
-            
-            void addAssignment(uint64_t varIndex, storm::expressions::Expression const& expr, uint64_t level=0) {
+            void addAssignment(ProgramVariableIdentifier varIndex, storm::expressions::Expression const& expr, uint64_t level=0) {
                 if(assignments.size() <= level) {
                     assignments.resize(level+1);
                 }
@@ -130,6 +131,10 @@ namespace storm {
                 assignments[level][varIndex] = expr;
             }
             
+            size_t nrLevels() const {
+                return assignments.size();
+            }
+            
             iterator begin() {
                 return assignments.begin();
             }

src/storage/ppg/ProgramEdge.cpp

@@ -4,8 +4,16 @@
 namespace storm {
     namespace ppg {
         
+        ProgramLocationIdentifier ProgramEdge::getSourceId() const {
+            return group->getSourceId();
+        }
+        
         ProgramAction const& ProgramEdge::getAction() const {
             return group->getGraph().getAction(action);
         }
+        
+        bool ProgramEdge::hasNoAction() const {
+            return action == group->getGraph().getNoActionId();
+        }
     }
 }

src/storage/ppg/ProgramEdge.h

@@ -15,7 +15,7 @@ namespace storm {
                 // Intentionally left empty.
             }
             
-            
+            ProgramLocationIdentifier getSourceId() const;
             ProgramLocationIdentifier getTargetId() const {
                 return target;
             }
@@ -24,7 +24,11 @@ namespace storm {
                 return condition;
             }
             
+            bool hasNoAction() const; 
             ProgramAction const& getAction() const;
+            ProgramActionIdentifier getActionId() const {
+                return action;
+            }
             
             virtual ~ProgramEdge() {
                 // Intentionally left empty.

src/storage/ppg/ProgramEdgeGroup.h

@@ -53,6 +53,14 @@ namespace storm {
                 return *graph;
             }
             
+            ProgramLocationIdentifier getSourceId() const {
+                return sourceId;
+            }
+            
+            ProgramEdgeGroupIdentifier getId() const {
+                return groupId;
+            }
+            
         private:
             /// Pointer to the graph; not owned.
             ProgramGraph* graph;

src/storage/ppg/ProgramGraph.cpp

@@ -1,2 +1,48 @@
 
 #include "ProgramGraph.h"
+
+
+namespace storm {
+    namespace ppg {
+        void ProgramGraph::printDot(std::ostream& os) const {
+            os << "digraph ppg {" << std::endl;
+            
+            for (auto const& loc : locations) {
+                os << "\tl" << loc.first << "[label=" << loc.first << "];"<< std::endl;
+            }
+            os << std::endl;
+            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 << std::endl;
+            for (auto const& loc : locations) {
+                for (auto const& edgegroup : loc.second) {
+                    
+                    if (loc.second.nrOutgoingEdgeGroups() > 1) {
+                        os << "\tl" << loc.first << " -> eg" << edgegroup->getId() << ";" << std::endl;
+                        for (auto const& edge : *edgegroup) {
+                            os << "\teg" << edgegroup->getId() << " -> l" << edge->getTargetId();
+                            if (!edge->hasNoAction()) {
+                                os << " [label=\"" << edge->getActionId()  << "\"]";
+                            }
+                            os << ";" << std::endl;
+                        }
+                    } else {
+                        for (auto const& edge : *edgegroup) {
+                            os << "\tl" << loc.first << " -> l" << edge->getTargetId();
+                            if (!edge->hasNoAction()) {
+                                os << " [label=\"" << edge->getActionId()  << "\"]";
+                            }
+                            os << ";" << std::endl;
+                        }
+                    }
+                }
+            }
+            os << "}" << std::endl;
+        }
+    }
+}

src/storage/ppg/ProgramGraph.h

@@ -21,8 +21,12 @@ namespace storm {
             using EdgeGroupIterator = ProgramLocation::EdgeGroupIterator;
             using ConstLocationIterator = std::unordered_map<ProgramLocationIdentifier, ProgramLocation>::const_iterator;
             
-            ProgramGraph(std::shared_ptr<storm::expressions::ExpressionManager> const& expManager, std::vector<storm::expressions::Variable> const& variables) : expManager(expManager), variables(variables) {
-                
+            ProgramGraph(std::shared_ptr<storm::expressions::ExpressionManager> const& expManager, std::vector<storm::expressions::Variable> const& variables) : expManager(expManager), variables() {
+                for(auto const& v : variables) {
+                    this->variables.emplace(v.getIndex(), v);
+                }
+                // No Action:
+                deterministicActions.emplace(noActionId, DeterministicProgramAction(this, noActionId));
             }
             
             ProgramGraph(ProgramGraph const&) = delete;
@@ -36,6 +40,12 @@ namespace storm {
                 return &(deterministicActions.emplace(newId, DeterministicProgramAction(this, newId)).first->second);
             }
             
+            ProbabilisticProgramAction* addUniformProbabilisticAction(ProgramVariableIdentifier var, int64_t from, int64_t to) {
+                ProgramActionIdentifier newId = freeActionIndex();
+                assert(!hasAction(newId));
+                return &(probabilisticActions.emplace(newId, ProbabilisticProgramAction(this, newId, var, from, to)).first->second);
+            }
+            
             ProgramLocation* addLocation(bool isInitial = false) {
                 ProgramLocationIdentifier newId = freeLocationIndex();
                 assert(!hasLocation(newId));
@@ -86,6 +96,10 @@ namespace storm {
             }
             
             
+            ProgramActionIdentifier getNoActionId() const {
+                return noActionId;
+            }
+            
             std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramLocationIdentifier sourceId, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId) {
                 assert(hasLocation(sourceId));
                 return addProgramEdgeToAllGroups(getLocation(sourceId), action, condition, targetId);
@@ -94,12 +108,10 @@ namespace storm {
             
             ProgramVariableIdentifier getVariableId(std::string const& varName) const {
                 // TODO consider holding a map for this.
-                uint64_t res = 0;
                 for(auto const& v : variables) {
-                    if(v.getName() == varName) {
-                        return res;
+                    if(v.second.getName() == varName) {
+                        return v.first;
                     }
-                    ++res;
                 }
                 assert(false);
             }
@@ -110,7 +122,7 @@ namespace storm {
             
             bool hasVariable(std::string const& varName) const {
                 for(auto const& v : variables) {
-                    if(v.getName() == varName) {
+                    if(v.second.getName() == varName) {
                         return true;
                     }
                 }
@@ -160,7 +172,7 @@ namespace storm {
                 return locations.end();
             }
             
-            std::vector<storm::expressions::Variable> const& getVariables() const {
+            std::unordered_map<ProgramVariableIdentifier, storm::expressions::Variable> const& getVariables() const {
                 return variables;
             }
             
@@ -178,6 +190,7 @@ namespace storm {
                 os << "Number of actions: " << nrActions() << std::endl;
             }
             
+            void printDot(std::ostream& os) const;
         protected:
             
             ProgramLocation& getLocation(ProgramLocationIdentifier id) {
@@ -207,7 +220,7 @@ namespace storm {
             std::unordered_map<ProgramActionIdentifier, ProbabilisticProgramAction> probabilisticActions;
             std::unordered_map<ProgramLocationIdentifier, ProgramLocation> locations;
             storm::expressions::Expression initialValueRestriction;
-            std::vector<storm::expressions::Variable> variables;
+            std::unordered_map<ProgramVariableIdentifier, storm::expressions::Variable> variables;
             
             std::shared_ptr<storm::expressions::ExpressionManager> expManager;
         private:
@@ -215,7 +228,8 @@ namespace storm {
             ProgramEdgeGroupIdentifier newEdgeGroupId = 0;
             ProgramLocationIdentifier newLocationId = 0;
             ProgramEdgeIdentifier newEdgeId = 0;
-            ProgramActionIdentifier newActionId = 0;
+            ProgramActionIdentifier newActionId = 1;
+            ProgramActionIdentifier noActionId = 0;
             
         };
     }

src/storm-pgcl.cpp

@@ -11,22 +11,14 @@
 #include "src/builder/JaniProgramGraphBuilder.h"
 #include "src/storage/jani/JSONExporter.h"
 
+#include "src/exceptions/FileIoException.h"
+
 #include "src/settings/modules/GeneralSettings.h"
 #include "src/settings/modules/PGCLSettings.h"
 #include "src/settings/modules/CoreSettings.h"
 #include "src/settings/modules/DebugSettings.h"
 #include "src/settings/modules/JaniExportSettings.h"
-//#include "src/settings/modules/CounterexampleGeneratorSettings.h"
-//#include "src/settings/modules/CuddSettings.h"
-//#include "src/settings/modules/SylvanSettings.h"
-#include "src/settings/modules/GmmxxEquationSolverSettings.h"
-#include "src/settings/modules/NativeEquationSolverSettings.h"
-//#include "src/settings/modules/BisimulationSettings.h"
-//#include "src/settings/modules/GlpkSettings.h"
-//#include "src/settings/modules/GurobiSettings.h"
-//#include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
-//#include "src/settings/modules/ParametricSettings.h"
-#include "src/settings/modules/EliminationSettings.h"
+
 
 /*!
  * Initialize the settings manager.
@@ -39,23 +31,12 @@ void initializeSettings() {
     storm::settings::addModule<storm::settings::modules::PGCLSettings>();
     storm::settings::addModule<storm::settings::modules::CoreSettings>();
     storm::settings::addModule<storm::settings::modules::DebugSettings>();
-    //storm::settings::addModule<storm::settings::modules::CounterexampleGeneratorSettings>();
-    //storm::settings::addModule<storm::settings::modules::CuddSettings>();
-    //storm::settings::addModule<storm::settings::modules::SylvanSettings>();
-    storm::settings::addModule<storm::settings::modules::GmmxxEquationSolverSettings>();
-    storm::settings::addModule<storm::settings::modules::NativeEquationSolverSettings>();
-    //storm::settings::addModule<storm::settings::modules::BisimulationSettings>();
-    //storm::settings::addModule<storm::settings::modules::GlpkSettings>();
-    //storm::settings::addModule<storm::settings::modules::GurobiSettings>();
-    //storm::settings::addModule<storm::settings::modules::TopologicalValueIterationEquationSolverSettings>();
-    //storm::settings::addModule<storm::settings::modules::ParametricSettings>();
-    storm::settings::addModule<storm::settings::modules::EliminationSettings>();
     storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
 }
 
 int handleJani(storm::jani::Model& model) {
     
-    if(!storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
+    if (!storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
         // For now, we have to have a jani file
         storm::jani::JsonExporter::toStream(model, std::cout);
     } else {
@@ -63,6 +44,17 @@ int handleJani(storm::jani::Model& model) {
     }
 }
 
+void programGraphToDotFile(storm::ppg::ProgramGraph const& prog) {
+    std::string filepath = storm::settings::getModule<storm::settings::modules::PGCLSettings>().getProgramGraphDotOutputFilename();
+    std::ofstream ofs;
+    ofs.open(filepath, std::ofstream::out );
+    if (ofs.is_open()) {
+        prog.printDot(ofs);
+    } else {
+        STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath);
+    }
+}
+
 int main(const int argc, const char** argv) {
     try {
         storm::utility::setUp();
@@ -74,17 +66,20 @@ int main(const int argc, const char** argv) {
             return -1;
         }
         
-        if(!storm::settings::getModule<storm::settings::modules::PGCLSettings>().isPgclFileSet()) {
+        if (!storm::settings::getModule<storm::settings::modules::PGCLSettings>().isPgclFileSet()) {
             return -1;
         }
         storm::pgcl::PgclProgram prog = storm::parser::PgclParser::parse(storm::settings::getModule<storm::settings::modules::PGCLSettings>().getPgclFilename());
-        std::cout << prog << std::endl;
         storm::ppg::ProgramGraph* progGraph = storm::builder::ProgramGraphBuilder::build(prog);
     
         progGraph->printInfo(std::cout);
-        if(storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
-            storm::builder::JaniProgramGraphBuilder builder;
-            storm::jani::Model* model = builder.build(*progGraph);
+        if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isProgramGraphToDotSet()) {
+            programGraphToDotFile(*progGraph);
+        }
+        if (storm::settings::getModule<storm::settings::modules::PGCLSettings>().isToJaniSet()) {
+            storm::builder::JaniProgramGraphBuilder builder(*progGraph);
+            builder.restrictAllVariables(0, 120);
+            storm::jani::Model* model = builder.build();
             delete progGraph;
             handleJani(*model);
             delete model;