Merge branch 'jani_support' into rewards_in_jani

Former-commit-id: 671bbe40a5 [formerly e9070da8a6]
Former-commit-id: e7ec1284ea

src/builder/DdJaniModelBuilder.cpp

@@ -412,7 +412,7 @@ namespace storm {
             
             // Iterate over all assignments (boolean and integer) and build the DD for it.
             std::set<storm::expressions::Variable> assignedVariables;
-            for (auto const& assignment : destination.getAssignments().getNonTransientAssignments()) {
+            for (auto const& assignment : destination.getOrderedAssignments().getNonTransientAssignments()) {
                 // Record the variable as being written.
                 STORM_LOG_TRACE("Assigning to variable " << variables.variableToRowMetaVariableMap->at(assignment.getExpressionVariable()).getName());
                 assignedVariables.insert(assignment.getExpressionVariable());
@@ -623,7 +623,7 @@ namespace storm {
                 for (auto const& actionIndex : actionInformation.getNonSilentActionIndices()) {
                     actionIndexToLocalNondeterminismVariableOffset[actionIndex] = 0;
                 }
-                actionIndexToLocalNondeterminismVariableOffset[storm::jani::Model::getSilentActionIndex()] = 0;
+                actionIndexToLocalNondeterminismVariableOffset[storm::jani::Model::SILENT_ACTION_INDEX] = 0;
 
                 AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, actionIndexToLocalNondeterminismVariableOffset));
                 return buildSystemFromAutomaton(globalAutomaton);
@@ -955,7 +955,7 @@ namespace storm {
                     // If the edge is not labeled with the silent action, we have to analyze which portion of the global
                     // variables was written by any of the updates and make all update results equal w.r.t. this set. If
                     // the edge is labeled with the silent action, we can already multiply the identities of all global variables.
-                    if (edge.getActionIndex() != this->model.getSilentActionIndex()) {
+                    if (edge.getActionIndex() != storm::jani::Model::SILENT_ACTION_INDEX) {
                         for (auto const& edgeDestinationDd : destinationDds) {
                             globalVariablesInSomeDestination.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end());
                         }
@@ -1415,7 +1415,7 @@ namespace storm {
                     for (auto& action : automaton.actionIndexToAction) {
                         illegalFragment |= action.second.illegalFragment;
                         addMissingGlobalVariableIdentities(action.second);
-                        storm::dd::Add<Type, ValueType> actionEncoding = encodeAction(action.first != this->model.getSilentActionIndex() ? boost::optional<uint64_t>(action.first) : boost::none, this->variables);
+                        storm::dd::Add<Type, ValueType> actionEncoding = encodeAction(action.first != storm::jani::Model::SILENT_ACTION_INDEX ? boost::optional<uint64_t>(action.first) : boost::none, this->variables);
                         storm::dd::Add<Type, ValueType> missingNondeterminismEncoding = encodeIndex(0, action.second.getHighestLocalNondeterminismVariable(), numberOfUsedNondeterminismVariables - action.second.getHighestLocalNondeterminismVariable(), this->variables);
                         storm::dd::Add<Type, ValueType> extendedTransitions = actionEncoding * missingNondeterminismEncoding * action.second.transitions;
                         

src/builder/JaniProgramGraphBuilder.cpp

@@ -0,0 +1,116 @@
+#include "JaniProgramGraphBuilder.h"
+#include "src/storage/jani/EdgeDestination.h"
+
+namespace storm {
+    namespace builder {
+        unsigned JaniProgramGraphBuilder::janiVersion = 1;
+        
+        storm::jani::OrderedAssignments buildOrderedAssignments(storm::jani::Automaton& automaton, storm::ppg::DeterministicProgramAction const& act) {
+            std::vector<storm::jani::Assignment> vec;
+            uint64_t level = 0;
+            for(auto const& group : act) {
+                for(auto const& assignment : group) {
+                    vec.emplace_back(automaton.getVariables().getVariable(act.getProgramGraph().getVariableName(assignment.first)) , assignment.second, level);
+                }
+                ++level;
+            }
+            return storm::jani::OrderedAssignments(vec);
+        }
+        
+        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& 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;
+        }
+    
+        std::vector<storm::jani::EdgeDestination> JaniProgramGraphBuilder::buildDestinations(storm::jani::Automaton& automaton, storm::ppg::ProgramEdge const& edge ) {
+            if (edge.getAction().isProbabilistic()) {
+                return buildProbabilisticDestinations(automaton, edge);
+            } else {
+                storm::jani::OrderedAssignments oa = buildOrderedAssignments(automaton, static_cast<storm::ppg::DeterministicProgramAction const&>(edge.getAction()));
+                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::SILENT_ACTION_INDEX, 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) {
+            for(auto it = programGraph.locationBegin(); it != programGraph.locationEnd(); ++it) {
+                ppg::ProgramLocation const& loc = it->second;
+                if (loc.nrOutgoingEdgeGroups() == 0) {
+                    // TODO deadlock!
+                } else if (loc.nrOutgoingEdgeGroups() == 1) {
+                    for(auto const& edge :  **(loc.begin())) {
+                        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::SILENT_ACTION_INDEX, 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");
+                    } else {
+                        std::vector<storm::jani::EdgeDestination> destinations;
+                        for(auto const& eg : loc) {
+                            // TODO add assignments
+                            assert(eg->nrEdges() < 2); // Otherwise, non-determinism occurs.
+                            assert(eg->nrEdges() > 0); // Empty edge groups should not occur in input.
+                            uint64_t target = janiLocId.at((*eg->begin())->getTargetId());
+                            destinations.emplace_back(target, eg->getProbability());
+                        }
+                        storm::jani::Edge e(janiLocId.at(it->second.id()), storm::jani::Model::SILENT_ACTION_INDEX, boost::none,  expManager->boolean(true), destinations);
+                        automaton.addEdge(e);
+                    }
+                }
+            }
+        }
+
+    }
+}

src/builder/JaniProgramGraphBuilder.h

@@ -0,0 +1,135 @@
+#include <string>
+
+#include "src/storage/ppg/ProgramGraph.h"
+#include "src/storage/jani/Model.h"
+#include "src/storage/jani/Location.h"
+#include "src/storage/jani/EdgeDestination.h"
+#include "src/storage/IntegerInterval.h"
+#include "src/exceptions/NotSupportedException.h"
+
+#include "src/utility/macros.h"
+
+namespace storm {
+    namespace builder {
+        
+        enum class JaniProgramGraphVariableDomainMethod  {
+            Unrestricted, IntervalPropagation
+        };
+        
+        struct JaniProgramGraphBuilderSetting {
+            JaniProgramGraphVariableDomainMethod variableDomainMethod = JaniProgramGraphVariableDomainMethod::Unrestricted;
+        };
+        
+        class JaniProgramGraphBuilder {
+        public:
+            static unsigned janiVersion;
+            
+            JaniProgramGraphBuilder(storm::ppg::ProgramGraph const& pg) : programGraph(pg) {
+                
+            }
+            
+            //void addVariableRestriction(storm::expressions::Variable const& var, storm::IntegerInterval const& interval ) {
+                
+            //}
+            
+        
+            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(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);
+                janiLocId = addProcedureLocations(mainAutomaton);
+                addVariableOoBLocations(mainAutomaton);
+                addEdges(mainAutomaton);
+                model->addAutomaton(mainAutomaton);
+                model->setStandardSystemComposition();
+                return model;
+            }
+            
+        private:
+            std::string janiLocationName(storm::ppg::ProgramLocationIdentifier i) {
+                return "l" + std::to_string(i);
+            }
+            
+            std::string janiVariableOutOfBoundsLocationName(storm::ppg::ProgramVariableIdentifier i) {
+                return "oob-" + programGraph.getVariableName(i);
+            }
+            
+            
+            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);
+            
+            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.second.getName(), v.second, expManager->integer(0), false);
+                        automaton.addVariable(janiVar);
+                    }
+                }
+            }
+            
+            std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> addProcedureLocations(storm::jani::Automaton& automaton) {
+                std::map<storm::ppg::ProgramLocationIdentifier, uint64_t> result;
+                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()) {
+                        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

@@ -0,0 +1,77 @@
+#include "ProgramGraphBuilder.h"
+#include "src/storage/pgcl/AssignmentStatement.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) {
+            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(), boost::get<storm::pgcl::UniformExpression>(s.getExpression())),  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* ifbodyStart = builder.newLocation();
+            builder.buildBlock(*s.getIfBody());
+            storm::ppg::ProgramLocation* elsebodyStart;
+            if(s.hasElse()) {
+                builder.storeNextLocation(builder.nextLoc());
+                elsebodyStart = builder.newLocation();
+                builder.buildBlock(*s.getElseBody());
+            }
+            beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), s.getCondition().getBooleanExpression(), ifbodyStart->id());
+            elseCondition = !s.getCondition().getBooleanExpression();
+            if(s.hasElse()) {
+                beforeStatementLocation->addProgramEdgeToAllGroups(builder.noAction(), elseCondition, elsebodyStart->id());
+            } else {
+                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())->addEdge(builder.nextLocId(), builder.noAction());
+            builder.buildBlock(*s.getLeftBranch());
+            builder.storeNextLocation(builder.nextLoc());
+            bodyStart = builder.newLocation();
+            beforeStatementLocation->addProgramEdgeGroup(1 - s.getProbability())->addEdge(builder.nextLocId(), builder.noAction());
+            builder.buildBlock(*s.getRightBranch());
+        }
+    }
+}

src/builder/ProgramGraphBuilder.h

@@ -0,0 +1,152 @@
+#pragma once
+
+#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 {
+        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();
+            }
+            
+            void 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 addAction(storm::expressions::Variable const& var, storm::expressions::Expression const& expr) const {
+                storm::ppg::DeterministicProgramAction* action = graph->addDeterministicAction();
+                action->addAssignment(graph->getVariableId(var.getName()), expr);
+                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;
+            }
+            
+            std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const {
+                return program.getExpressionManager();
+            }
+            
+            
+            
+            void buildBlock(storm::pgcl::PgclBlock const& block) {
+                ProgramGraphBuilderVisitor visitor(*this);
+                for (auto const& statement : block) {
+                    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 = graph->getNoActionId();
+                
+            }
+             
+            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;
+            
+            
+            
+        };
+        
+    }
+}

src/cli/cli.cpp

@@ -9,8 +9,10 @@
 #include "src/settings/modules/IOSettings.h"
 #include "src/settings/modules/CoreSettings.h"
 #include "src/exceptions/OptionParserException.h"
+#include "src/settings/modules/JaniExportSettings.h"
 
 #include "src/utility/storm-version.h"
+#include "src/storage/jani/JSONExporter.h"
 
 
 // Includes for the linked libraries and versions header.
@@ -220,6 +222,10 @@ namespace storm {
                     model = storm::parseJaniModel(ioSettings.getJaniInputFilename()).first;
                 }
                 
+                if(model.isJaniModel() && storm::settings::getModule<storm::settings::modules::JaniExportSettings>().isJaniFileSet()) {
+                    storm::jani::JsonExporter::toFile(model.asJaniModel(), storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+                }
+                
                 // Get the string that assigns values to the unknown currently undefined constants in the model.
                 std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
                 model = model.preprocess(constantDefinitionString);

src/generator/JaniNextStateGenerator.cpp

@@ -207,8 +207,8 @@ namespace storm {
         CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) {
             CompressedState newState(state);
             
-            auto assignmentIt = destination.getAssignments().getNonTransientAssignments().begin();
-            auto assignmentIte = destination.getAssignments().getNonTransientAssignments().end();
+            auto assignmentIt = destination.getOrderedAssignments().getNonTransientAssignments().begin();
+            auto assignmentIte = destination.getOrderedAssignments().getNonTransientAssignments().end();
             
             // Iterate over all boolean assignments and carry them out.
             auto boolIt = this->variableInformation.booleanVariables.begin();
@@ -345,7 +345,7 @@ namespace storm {
                 // Iterate over all edges from the source location.
                 for (auto const& edge : automaton.getEdgesFromLocation(location)) {
                     // Skip the edge if it is labeled with a non-silent action.
-                    if (edge.getActionIndex() != model.getSilentActionIndex()) {
+                    if (edge.getActionIndex() != storm::jani::Model::SILENT_ACTION_INDEX) {
                         continue;
                     }
                     

src/parser/JaniParser.cpp

@@ -1,11 +1,14 @@
 #include "JaniParser.h"
 #include "src/storage/jani/Model.h"
 #include "src/storage/jani/Property.h"
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/ParallelComposition.h"
 #include "src/exceptions/FileIoException.h"
 #include "src/exceptions/InvalidJaniException.h"
 #include "src/exceptions/NotImplementedException.h"
 #include "src/storage/jani/ModelType.h"
 
+
 #include <iostream>
 #include <sstream>
 #include <fstream>
@@ -21,6 +24,7 @@ namespace storm {
         ////////////
         const bool JaniParser::defaultVariableTransient = false;
         const bool JaniParser::defaultBooleanInitialValue = false;
+        const double JaniParser::defaultRationalInitialValue = 0.0;
         const int64_t JaniParser::defaultIntegerInitialValue = 0;
         const std::set<std::string> JaniParser::unsupportedOpstrings({"sin", "cos", "tan", "cot", "sec", "csc", "asin", "acos", "atan", "acot", "asec", "acsc",
                                                          "sinh", "cosh", "tanh", "coth", "sech", "csch", "asinh", "acosh", "atanh", "asinh", "acosh"});
@@ -87,30 +91,31 @@ namespace storm {
             parseActions(parsedStructure.at("actions"), model);
             size_t constantsCount = parsedStructure.count("constants");
             STORM_LOG_THROW(constantsCount < 2, storm::exceptions::InvalidJaniException, "Constant-declarations can be given at most once.");
-            if(constantsCount == 1) {
+            if (constantsCount == 1) {
                 for (auto const &constStructure : parsedStructure.at("constants")) {
                     model.addConstant(*parseConstant(constStructure, "global"));
                 }
             }
             size_t variablesCount = parsedStructure.count("variables");
             STORM_LOG_THROW(variablesCount < 2, storm::exceptions::InvalidJaniException, "Variable-declarations can be given at most once for global variables.");
-            if(variablesCount == 1) {
-                for(auto const& varStructure : parsedStructure.at("variables")) {
+            if (variablesCount == 1) {
+                for (auto const& varStructure : parsedStructure.at("variables")) {
                     model.addVariable(*parseVariable(varStructure, "global"));
                 }
             }
             STORM_LOG_THROW(parsedStructure.count("automata") == 1, storm::exceptions::InvalidJaniException, "Exactly one list of automata must be given");
             STORM_LOG_THROW(parsedStructure.at("automata").is_array(), storm::exceptions::InvalidJaniException, "Automata must be an array");
             // Automatons can only be parsed after constants and variables.
-            for(auto const& automataEntry : parsedStructure.at("automata")) {
+            for (auto const& automataEntry : parsedStructure.at("automata")) {
                 model.addAutomaton(parseAutomaton(automataEntry, model));
             }
             STORM_LOG_THROW(parsedStructure.count("system") == 1, storm::exceptions::InvalidJaniException, "Exactly one system description must be given");
-            //std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
+            std::shared_ptr<storm::jani::Composition> composition = parseComposition(parsedStructure.at("system"));
+            model.setSystemComposition(composition);
             STORM_LOG_THROW(parsedStructure.count("properties") <= 1, storm::exceptions::InvalidJaniException, "At most one list of properties can be given");
-            STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array");
             PropertyVector properties;
-            if(parseProperties) {
+            if (parseProperties && parsedStructure.count("properties") == 1) {
+                STORM_LOG_THROW(parsedStructure.at("properties").is_array(), storm::exceptions::InvalidJaniException, "Properties should be an array");
                 for(auto const& propertyEntry : parsedStructure.at("properties")) {
                     properties.push_back(this->parseProperty(propertyEntry));
                 }
@@ -124,9 +129,10 @@ namespace storm {
             // TODO check unique name
             std::string name = getString(propertyStructure.at("name"), "property-name");
             std::string comment = "";
-            if(propertyStructure.count("comment") > 0) {
+            if (propertyStructure.count("comment") > 0) {
                 comment = getString(propertyStructure.at("comment"), "comment for property named '" + name + "'.");
             }
+            
 
         }
 
@@ -140,13 +146,13 @@ namespace storm {
             size_t valueCount = constantStructure.count("value");
             storm::expressions::Expression initExpr;
             STORM_LOG_THROW(valueCount < 2, storm::exceptions::InvalidJaniException, "Value for constant '" + name +  "'  (scope: " + scopeDescription + ") must be given at most once.");
-            if(valueCount == 1) {
+            if (valueCount == 1) {
                 // Read initial value before; that makes creation later on a bit easier, and has as an additional benefit that we do not need to check whether the variable occurs also on the assignment.
                 initExpr = parseExpression(constantStructure.at("value"), "Value of constant " + name + " (scope: " + scopeDescription + ")");
                 assert(initExpr.isInitialized());
             }
 
-            if(constantStructure.at("type").is_object()) {
+            if (constantStructure.at("type").is_object()) {
 //                STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ")  kind must be given");
 //                std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name  + "(scope: " + scopeDescription + ") ");
 //                if(kind == "bounded") {
@@ -172,8 +178,11 @@ namespace storm {
              }
              else if(constantStructure.at("type").is_string()) {
                 if(constantStructure.at("type") == "real") {
-                    // expressionManager->declareRationalVariable(name);
-                    // TODO something.
+                    if(initExpr.isInitialized()) {
+                        return std::make_shared<storm::jani::Constant>(name, expressionManager->declareRationalVariable(exprManagerName), initExpr);
+                    } else {
+                        return std::make_shared<storm::jani::Constant>(name, expressionManager->declareRationalVariable(exprManagerName));
+                    }
                 } else if(constantStructure.at("type") == "bool") {
                     if(initExpr.isInitialized()) {
                         return std::make_shared<storm::jani::Constant>(name, expressionManager->declareBooleanVariable(exprManagerName), initExpr);
@@ -189,7 +198,7 @@ namespace storm {
                     }
                 } else {
                     // TODO clocks.
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << constantStructure.at("type").dump()  << " for Variable '" << name << "' (scope: " << scopeDescription << ")");
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << constantStructure.at("type").dump()  << " for constant '" << name << "' (scope: " << scopeDescription << ")");
                 }
             }
 
@@ -217,52 +226,27 @@ namespace storm {
             }
             STORM_LOG_THROW(variableStructure.count("type") == 1, storm::exceptions::InvalidJaniException, "Variable '" + name + "' (scope: " + scopeDescription + ") must have a (single) type-declaration.");
             boost::optional<storm::expressions::Expression> initVal;
-            if(variableStructure.at("type").is_object()) {
-                STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ")  kind must be given");
-                std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name  + "(scope: " + scopeDescription + ") ");
-                if(kind == "bounded") {
-                    // First do the bounds, that makes the code a bit more streamlined
-                    STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given");
-                    storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")");
-                    assert(lowerboundExpr.isInitialized());
-                    STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given");
-                    storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")");
-                    assert(upperboundExpr.isInitialized());
-                    STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given");
+            if(variableStructure.at("type").is_string()) {
+                if(variableStructure.at("type") == "real") {
+                    expressionManager->declareRationalVariable(name);
                     if(initvalcount == 1) {
                         if(variableStructure.at("initial-value").is_null()) {
-                            initVal = storm::expressions::ite(lowerboundExpr < 0 && upperboundExpr > 0, expressionManager->integer(0), lowerboundExpr);
-                                                                                          // TODO as soon as we support half-open intervals, we have to change this.
+                            initVal = expressionManager->rational(defaultRationalInitialValue);
                         } else {
                             initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
+                            STORM_LOG_THROW(initVal.get().hasRationalType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a rational");
                         }
+                        return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar);
+                        
                     }
-                    std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name  + "(scope: " + scopeDescription + ") ");
-                    if(basictype == "int") {
-                        if(initVal) {
-                            STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer");
-                        }
-                        STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
-                        STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
-                        return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr);
-                    } else {
-                        STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") ");
-                    }
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") ");
-                }
-            }
-            else if(variableStructure.at("type").is_string()) {
-                if(variableStructure.at("type") == "real") {
-                    // expressionManager->declareRationalVariable(name);
-                    // TODO something.
+                    return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), transientVar);
                 } else if(variableStructure.at("type") == "bool") {
                     if(initvalcount == 1) {
                         if(variableStructure.at("initial-value").is_null()) {
                             initVal = expressionManager->boolean(defaultBooleanInitialValue);
                         } else {
                             initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
-                            STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean");
+                            STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean");
                         }
                         return std::make_shared<storm::jani::BooleanVariable>(name, expressionManager->declareBooleanVariable(exprManagerName), initVal.get(), transientVar);
                     }
@@ -285,6 +269,40 @@ namespace storm {
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description " << variableStructure.at("type").dump()  << " for variable '" << name << "' (scope: " << scopeDescription << ")");
                 }
+            } else if(variableStructure.at("type").is_object()) {
+                STORM_LOG_THROW(variableStructure.at("type").count("kind") == 1, storm::exceptions::InvalidJaniException, "For complex type as in variable " << name << "(scope: " << scopeDescription << ")  kind must be given");
+                std::string kind = getString(variableStructure.at("type").at("kind"), "kind for complex type as in variable " + name  + "(scope: " + scopeDescription + ") ");
+                if(kind == "bounded") {
+                    // First do the bounds, that makes the code a bit more streamlined
+                    STORM_LOG_THROW(variableStructure.at("type").count("lower-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") lower-bound must be given");
+                    storm::expressions::Expression lowerboundExpr = parseExpression(variableStructure.at("type").at("lower-bound"), "Lower bound for variable " + name + " (scope: " + scopeDescription + ")");
+                    assert(lowerboundExpr.isInitialized());
+                    STORM_LOG_THROW(variableStructure.at("type").count("upper-bound") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") upper-bound must be given");
+                    storm::expressions::Expression upperboundExpr = parseExpression(variableStructure.at("type").at("upper-bound"), "Upper bound for variable "+ name + " (scope: " + scopeDescription + ")");
+                    assert(upperboundExpr.isInitialized());
+                    STORM_LOG_THROW(variableStructure.at("type").count("base") == 1, storm::exceptions::InvalidJaniException, "For bounded type as in variable " << name << "(scope: " << scopeDescription << ") base must be given");
+                    if(initvalcount == 1) {
+                        if(variableStructure.at("initial-value").is_null()) {
+                            initVal = storm::expressions::ite(lowerboundExpr < 0 && upperboundExpr > 0, expressionManager->integer(0), lowerboundExpr);
+                            // TODO as soon as we support half-open intervals, we have to change this.
+                        } else {
+                            initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ");
+                        }
+                    }
+                    std::string basictype = getString(variableStructure.at("type").at("base"), "base for bounded type as in variable " + name  + "(scope: " + scopeDescription + ") ");
+                    if(basictype == "int") {
+                        if(initVal) {
+                            STORM_LOG_THROW(initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be an integer");
+                        }
+                        STORM_LOG_THROW(lowerboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Lower bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
+                        STORM_LOG_THROW(upperboundExpr.hasIntegerType(), storm::exceptions::InvalidJaniException, "Upper bound for bounded integer variable " << name << "(scope: " << scopeDescription << ") must be integer-typed");
+                        return storm::jani::makeBoundedIntegerVariable(name, expressionManager->declareIntegerVariable(exprManagerName), initVal, transientVar, lowerboundExpr, upperboundExpr);
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported base " << basictype << " for bounded variable " << name << "(scope: " << scopeDescription << ") ");
+                    }
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unsupported kind " << kind << " for complex type of variable " << name << "(scope: " << scopeDescription << ") ");
+                }
             }
 
             STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown type description, " << variableStructure.at("type").dump()  << " for variable '" << name << "' (scope: " << scopeDescription << ")");
@@ -323,7 +341,7 @@ namespace storm {
 
         storm::jani::Variable const& getLValue(std::string const& ident, storm::jani::VariableSet const& globalVars, storm::jani::VariableSet const& localVars, std::string const& scopeDescription) {
             if(localVars.hasVariable(ident)) {
-                return globalVars.getVariable(ident);
+                return localVars.getVariable(ident);
             } else if(globalVars.hasVariable(ident)) {
                 return globalVars.getVariable(ident);
             } else {
@@ -446,7 +464,7 @@ namespace storm {
                         ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
                         ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
                         return arguments[0] - arguments[1];
-                    } else if (opstring == "--") {
+                    } else if (opstring == "-") {
                         arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars);
                         assert(arguments.size() == 1);
                         ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
@@ -482,12 +500,12 @@ namespace storm {
                         ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
                         ensureNumericalType(arguments[1], opstring, 1, scopeDescription);
                         return storm::expressions::minimum(arguments[0],arguments[1]);
-                    } else if (opstring == "⌊⌋") {
+                    } else if (opstring == "floor") {
                         arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars);
                         assert(arguments.size() == 1);
                         ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
                         return storm::expressions::floor(arguments[0]);
-                    } else if (opstring == "⌈⌉") {
+                    } else if (opstring == "ceil") {
                         arguments = parseUnaryExpressionArguments(expressionStructure, opstring, scopeDescription, localVars);
                         assert(arguments.size() == 1);
                         ensureNumericalType(arguments[0], opstring, 0, scopeDescription);
@@ -535,7 +553,7 @@ namespace storm {
                         STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Unknown operator " << opstring << " in  " << scopeDescription << ".");
                     }
                 }
-                STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Only standard operators are supported for complex expressions as " << expressionStructure.dump() << " in  " << scopeDescription << ".");
+                STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "No supported operator declaration found for complex expressions as " << expressionStructure.dump() << " in  " << scopeDescription << ".");
             }
             assert(false);
 
@@ -564,7 +582,7 @@ namespace storm {
                 STORM_LOG_THROW(locEntry.count("name") == 1, storm::exceptions::InvalidJaniException, "Locations for automaton '" << name << "' must have exactly one name");
                 std::string locName = getString(locEntry.at("name"), "location of automaton " + name);
                 STORM_LOG_THROW(locIds.count(locName) == 0, storm::exceptions::InvalidJaniException, "Location with name '" + locName + "' already exists in automaton '" + name + "'");
-                STORM_LOG_THROW(locEntry.count("invariant") > 0, storm::exceptions::InvalidJaniException, "Invariants in locations as in '" + locName + "' are not supported");
+                STORM_LOG_THROW(locEntry.count("invariant") == 0, storm::exceptions::InvalidJaniException, "Invariants in locations as in '" + locName + "' in automaton '" + name + "' are not supported");
                 //STORM_LOG_THROW(locEntry.count("invariant") > 0 && !supportsInvariants(parentModel.getModelType()), storm::exceptions::InvalidJaniException, "Invariants are not supported in the model type " + to_string(parentModel.getModelType()));
                 std::vector<storm::jani::Assignment> transientAssignments;
                 for(auto const& transientValueEntry : locEntry.at("transient-values")) {
@@ -585,7 +603,8 @@ namespace storm {
             STORM_LOG_THROW(automatonStructure.count("restrict-initial") < 2, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' has multiple initial value restrictions");
             storm::expressions::Expression initialValueRestriction = expressionManager->boolean(true);
             if(automatonStructure.count("restrict-initial") > 0) {
-                initialValueRestriction  = parseExpression(automatonStructure.at("restrict-initial"), "Initial value restriction for automaton " + name);
+                STORM_LOG_THROW(automatonStructure.at("restrict-initial").count("exp") == 1, storm::exceptions::InvalidJaniException, "Automaton '" << name << "' needs an expression inside the initial restricion");
+                initialValueRestriction  = parseExpression(automatonStructure.at("restrict-initial").at("exp"), "Initial value restriction for automaton " + name);
             }
             automaton.setInitialStatesRestriction(initialValueRestriction);
             uint64_t varDeclCount = automatonStructure.count("variables");
@@ -645,7 +664,7 @@ namespace storm {
                     if(probDeclCount == 0) {
                         probExpr = expressionManager->rational(1.0);
                     } else {
-                        STORM_LOG_THROW(destEntry.at("probability").count("exp") == 1, storm::exceptions::InvalidJaniException, "Destination in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have one expression.");
+                        STORM_LOG_THROW(destEntry.at("probability").count("exp") == 1, storm::exceptions::InvalidJaniException, "Destination in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "' must have a probability expression.");
                         probExpr = parseExpression(destEntry.at("probability").at("exp"), "probability expression in edge from '" + sourceLoc + "' to  '"  + targetLoc + "' in automaton '" + name + "'", localVars);
                     }
                     assert(probExpr.isInitialized());
@@ -661,7 +680,7 @@ namespace storm {
                         storm::jani::Variable const& lhs = getLValue(refstring, parentModel.getGlobalVariables(), automaton.getVariables(), "Assignment variable in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
                         // value
                         STORM_LOG_THROW(assignmentEntry.count("value") == 1, storm::exceptions::InvalidJaniException, "Assignment in edge from '" << sourceLoc << "' to '" << targetLoc << "' in automaton '" << name << "'  must have one value field");
-                        storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'");
+                        storm::expressions::Expression assignmentExpr = parseExpression(assignmentEntry.at("value"), "assignment in edge from '" + sourceLoc + "' to '" + targetLoc + "' in automaton '" + name + "'", localVars);
                         // TODO check types
                         assignments.emplace_back(lhs, assignmentExpr);
                     }
@@ -676,7 +695,52 @@ namespace storm {
         }
 
         std::shared_ptr<storm::jani::Composition> JaniParser::parseComposition(json const &compositionStructure) {
-
+            
+            STORM_LOG_THROW(compositionStructure.count("elements") == 1, storm::exceptions::InvalidJaniException, "Elements of a composition must be given");
+            
+            if (compositionStructure.at("elements").size() == 1) {
+                if (compositionStructure.count("syncs") == 0) {
+                    // We might have an automaton.
+                    STORM_LOG_THROW(compositionStructure.at("elements").back().count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in composition");
+                    if (compositionStructure.at("elements").back().at("automaton").is_string()) {
+                        std::string name = compositionStructure.at("elements").back().at("automaton");
+                        // TODO check whether name exist?
+                        return std::shared_ptr<storm::jani::AutomatonComposition>(new storm::jani::AutomatonComposition(name));
+                    }
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Nesting parallel composition is not supported");
+                } else {
+                    // Might be rename or input-enable.
+                }
+            }
+            
+            std::vector<std::shared_ptr<storm::jani::Composition>>  compositions;
+            for (auto const& elemDecl : compositionStructure.at("elements")) {
+                if(!allowRecursion) {
+                    STORM_LOG_THROW(elemDecl.count("automaton") == 1, storm::exceptions::InvalidJaniException, "Automaton must be given in the element");
+                }
+                compositions.push_back(parseComposition(elemDecl));
+            }
+            
+            STORM_LOG_THROW(compositionStructure.count("syncs") < 2, storm::exceptions::InvalidJaniException, "Sync vectors can be given at most once");
+            std::vector<storm::jani::SynchronizationVector> syncVectors;
+            if (compositionStructure.count("syncs") > 0) {
+                // TODO add error checks
+                for (auto const& syncEntry : compositionStructure.at("syncs")) {
+                    std::vector<std::string> inputs;
+                    for (auto const& syncInput : syncEntry.at("synchronise")) {
+                        if(syncInput.is_null()) {
+                            // TODO handle null;
+                        } else {
+                            inputs.push_back(syncInput);
+                        }
+                    }
+                    std::string syncResult = syncEntry.at("result");
+                    syncVectors.emplace_back(inputs, syncResult);
+                }
+            }
+            
+            return std::shared_ptr<storm::jani::Composition>(new storm::jani::ParallelComposition(compositions, syncVectors));
+            
         }
     }
 }

src/parser/JaniParser.h

@@ -67,6 +67,7 @@ namespace storm {
              */
             std::shared_ptr<storm::expressions::ExpressionManager> expressionManager;
 
+            bool allowRecursion = true;
 
             //////////
             //   Default values -- assumptions from JANI.
@@ -74,6 +75,7 @@ namespace storm {
             static const bool defaultVariableTransient;
             
             static const bool defaultBooleanInitialValue;
+            static const double defaultRationalInitialValue;
             static const int64_t defaultIntegerInitialValue;
 
             static const std::set<std::string> unsupportedOpstrings;

src/parser/PgclParser.cpp

@@ -143,12 +143,12 @@ namespace storm {
             }
             // Creates the actual program.
             std::shared_ptr<storm::pgcl::PgclProgram> result(
-                    new storm::pgcl::PgclProgram(statements, this->locationToStatement, params, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, true)
+                    new storm::pgcl::PgclProgram(statements, this->locationToStatement, params, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated)
             );
             result->back()->setLast(true);
             // Sets the current program as a parent to all its direct children statements.
             for(storm::pgcl::iterator it = result->begin(); it != result->end(); ++it) {
-                (*it)->setParentProgram(result);
+                (*it)->setParentBlock(result.get());
             }
             return *result;
         }
@@ -204,29 +204,26 @@ namespace storm {
         }
 
         std::shared_ptr<storm::pgcl::IfStatement> PgclParser::createIfElseStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& ifBody, boost::optional<std::vector<std::shared_ptr<storm::pgcl::Statement> > > const& elseBody) {
-            std::shared_ptr<storm::pgcl::PgclProgram> ifBodyProgram(new storm::pgcl::PgclProgram(ifBody, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+            std::shared_ptr<storm::pgcl::PgclBlock> ifBodyProgram(new storm::pgcl::PgclBlock(ifBody, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated));
             std::shared_ptr<storm::pgcl::IfStatement> ifElse;
             if(elseBody) {
-                std::shared_ptr<storm::pgcl::PgclProgram> elseBodyProgram(new storm::pgcl::PgclProgram(*elseBody, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+                std::shared_ptr<storm::pgcl::PgclBlock> elseBodyProgram(new storm::pgcl::PgclBlock(*elseBody, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated));
                 ifElse = std::shared_ptr<storm::pgcl::IfStatement>(new storm::pgcl::IfStatement(condition, ifBodyProgram, elseBodyProgram));
                 (*(ifElse->getIfBody()->back())).setLast(true);
                 (*(ifElse->getElseBody()->back())).setLast(true);
                 // Sets the current program as a parent to all its children statements.
                 for(storm::pgcl::iterator it = ifElse->getElseBody()->begin(); it != ifElse->getElseBody()->end(); ++it) {
-                    (*it)->setParentProgram(ifElse->getElseBody());
-                    (*it)->setParentStatement(ifElse);
+                    (*it)->setParentBlock(ifElse->getElseBody().get());
                 }
                 for(storm::pgcl::iterator it = ifElse->getIfBody()->begin(); it != ifElse->getIfBody()->end(); ++it) {
-                    (*it)->setParentProgram(ifElse->getIfBody());
-                    (*it)->setParentStatement(ifElse);
+                    (*it)->setParentBlock(ifElse->getIfBody().get());
                 }
             } else {
                 ifElse = std::shared_ptr<storm::pgcl::IfStatement>(new storm::pgcl::IfStatement(condition, ifBodyProgram));
                 (*(ifElse->getIfBody()->back())).setLast(true);
                 // Sets the current program as a parent to all its children statements.
                 for(storm::pgcl::iterator it = ifElse->getIfBody()->begin(); it != ifElse->getIfBody()->end(); ++it) {
-                    (*it)->setParentProgram(ifElse->getIfBody());
-                    (*it)->setParentStatement(ifElse);
+                    (*it)->setParentBlock(ifElse->getIfBody().get());
                 }
             }
             ifElse->setLocationNumber(this->currentLocationNumber);
@@ -236,13 +233,12 @@ namespace storm {
         }
 
         std::shared_ptr<storm::pgcl::LoopStatement> PgclParser::createLoopStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& body) {
-            std::shared_ptr<storm::pgcl::PgclProgram> bodyProgram(new storm::pgcl::PgclProgram(body, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+            std::shared_ptr<storm::pgcl::PgclBlock> bodyProgram(new storm::pgcl::PgclBlock(body, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated));
             std::shared_ptr<storm::pgcl::LoopStatement> loop(new storm::pgcl::LoopStatement(condition, bodyProgram));
             this->loopCreated = true;
             // Sets the current program as a parent to all its children statements.
             for(storm::pgcl::iterator it = loop->getBody()->begin(); it != loop->getBody()->end(); ++it) {
-                (*it)->setParentProgram(loop->getBody());
-                (*it)->setParentStatement(loop);
+                (*it)->setParentBlock(loop->getBody().get());
             }
             (*(loop->getBody()->back())).setLast(true);
             loop->setLocationNumber(this->currentLocationNumber);
@@ -252,19 +248,17 @@ namespace storm {
         }
 
         std::shared_ptr<storm::pgcl::NondeterministicBranch> PgclParser::createNondeterministicBranch(std::vector<std::shared_ptr<storm::pgcl::Statement> > const& left, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& right) {
-            std::shared_ptr<storm::pgcl::PgclProgram> leftProgram(new storm::pgcl::PgclProgram(left, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
-            std::shared_ptr<storm::pgcl::PgclProgram> rightProgram(new storm::pgcl::PgclProgram(right, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+            std::shared_ptr<storm::pgcl::PgclBlock> leftProgram(new storm::pgcl::PgclBlock(left, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated));
+            std::shared_ptr<storm::pgcl::PgclBlock> rightProgram(new storm::pgcl::PgclBlock(right, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated));
             std::shared_ptr<storm::pgcl::NondeterministicBranch> branch(new storm::pgcl::NondeterministicBranch(leftProgram, rightProgram));
             this->nondetCreated = true;
             // Sets the left program as a parent to all its children statements.
             for(storm::pgcl::iterator it = branch->getLeftBranch()->begin(); it != branch->getLeftBranch()->end(); ++it) {
-                (*it)->setParentProgram(branch->getLeftBranch());
-                (*it)->setParentStatement(branch);
+                (*it)->setParentBlock(branch->getLeftBranch().get());
             }
             // Sets the right program as a parent to all its children statements.
             for(storm::pgcl::iterator it = branch->getRightBranch()->begin(); it != branch->getRightBranch()->end(); ++it) {
-                (*it)->setParentProgram(branch->getRightBranch());
-                (*it)->setParentStatement(branch);
+                (*it)->setParentBlock(branch->getRightBranch().get());
             }
             (*(branch->getLeftBranch()->back())).setLast(true);
             (*(branch->getRightBranch()->back())).setLast(true);
@@ -275,18 +269,16 @@ namespace storm {
         }
 
         std::shared_ptr<storm::pgcl::ProbabilisticBranch> PgclParser::createProbabilisticBranch(storm::expressions::Expression const& probability, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& left, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& right) {
-            std::shared_ptr<storm::pgcl::PgclProgram> leftProgram(new storm::pgcl::PgclProgram(left, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
-            std::shared_ptr<storm::pgcl::PgclProgram> rightProgram(new storm::pgcl::PgclProgram(right, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated, false));
+            std::shared_ptr<storm::pgcl::PgclBlock> leftProgram(new storm::pgcl::PgclBlock(left, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated));
+            std::shared_ptr<storm::pgcl::PgclBlock> rightProgram(new storm::pgcl::PgclBlock(right, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated));
             std::shared_ptr<storm::pgcl::ProbabilisticBranch> branch(new storm::pgcl::ProbabilisticBranch(probability, leftProgram, rightProgram));
             // Sets the left program as a parent to all its children statements.
             for(storm::pgcl::iterator it = branch->getLeftBranch()->begin(); it != branch->getLeftBranch()->end(); ++it) {
-                (*it)->setParentProgram(branch->getLeftBranch());
-                (*it)->setParentStatement(branch);
+                (*it)->setParentBlock(branch->getLeftBranch().get());
             }
             // Sets the right program as a parent to all its children statements.
             for(storm::pgcl::iterator it = branch->getRightBranch()->begin(); it != branch->getRightBranch()->end(); ++it) {
-                (*it)->setParentProgram(branch->getRightBranch());
-                (*it)->setParentStatement(branch);
+                (*it)->setParentBlock(branch->getRightBranch().get());
             }
             (*(branch->getLeftBranch()->back())).setLast(true);
             (*(branch->getRightBranch()->back())).setLast(true);

src/parser/PgclParser.h

@@ -58,8 +58,8 @@ namespace storm {
             qi::rule<Iterator, storm::pgcl::PgclProgram(), Skipper> program;
             qi::rule<Iterator, std::vector<std::shared_ptr<storm::pgcl::Statement> >(), Skipper> sequenceOfStatements;
             qi::rule<Iterator, std::shared_ptr<storm::pgcl::Statement>(), Skipper> statement;
-            qi::rule<Iterator, std::shared_ptr<storm::pgcl::SimpleStatement>(), Skipper> simpleStatement;
-            qi::rule<Iterator, std::shared_ptr<storm::pgcl::CompoundStatement>(), Skipper> compoundStatement;
+            qi::rule<Iterator, std::shared_ptr<storm::pgcl::Statement>(), Skipper> simpleStatement;
+            qi::rule<Iterator, std::shared_ptr<storm::pgcl::Statement>(), Skipper> compoundStatement;
             qi::rule<Iterator, std::shared_ptr<storm::pgcl::IfStatement>(), Skipper> ifElseStatement;
             qi::rule<Iterator, std::shared_ptr<storm::pgcl::BranchStatement>(), Skipper> branchStatement;
             qi::rule<Iterator, std::shared_ptr<storm::pgcl::LoopStatement>(), Skipper> loopStatement;

src/settings/SettingsManager.cpp

@@ -33,6 +33,7 @@
 #include "src/settings/modules/RegionSettings.h"
 #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
 #include "src/settings/modules/ExplorationSettings.h"
+#include "src/settings/modules/JaniExportSettings.h"
 #include "src/utility/macros.h"
 #include "src/settings/Option.h"
 
@@ -524,6 +525,7 @@ namespace storm {
             storm::settings::addModule<storm::settings::modules::RegionSettings>();
             storm::settings::addModule<storm::settings::modules::Smt2SmtSolverSettings>();
             storm::settings::addModule<storm::settings::modules::ExplorationSettings>();
+            storm::settings::addModule<storm::settings::modules::JaniExportSettings>();
         }
 
     }

src/settings/modules/JaniExportSettings.cpp

@@ -0,0 +1,42 @@
+#include "JaniExportSettings.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/SettingMemento.h"
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+
+#include "src/exceptions/InvalidSettingsException.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            const std::string JaniExportSettings::moduleName = "exportJani";
+            
+            const std::string JaniExportSettings::janiFileOptionName = "jani-output";
+            const std::string JaniExportSettings::janiFileOptionShortName = "output";
+
+            
+            JaniExportSettings::JaniExportSettings() : ModuleSettings(moduleName) {
+                this->addOption(storm::settings::OptionBuilder(moduleName, janiFileOptionName, false, "Destination for the jani model.").setShortName(janiFileOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "path to file").build()).build());
+            }
+            
+            bool JaniExportSettings::isJaniFileSet() const {
+                return this->getOption(janiFileOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string JaniExportSettings::getJaniFilename() const {
+                return this->getOption(janiFileOptionName).getArgumentByName("filename").getValueAsString();
+            }
+            
+            void JaniExportSettings::finalize() {
+                
+            }
+            
+            bool JaniExportSettings::check() const {
+                return true;
+            }
+        }
+    }
+}

src/settings/modules/JaniExportSettings.h

@@ -0,0 +1,38 @@
+#pragma once
+
+#include "storm-config.h"
+#include "src/settings/modules/ModuleSettings.h"
+
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            class JaniExportSettings : public ModuleSettings {
+            public:
+                /*!
+                 * Creates a new JaniExport setting
+                 */
+                JaniExportSettings();
+                
+                /**
+                 * Retrievew whether the pgcl file option was set
+                 */
+                bool isJaniFileSet() const;
+                
+                /**
+                 * Retrieves the pgcl file name
+                 */
+                std::string getJaniFilename() const;
+                
+                bool check() const override;
+                void finalize() override;
+                
+                static const std::string moduleName;
+                
+            private:
+                static const std::string janiFileOptionName;
+                static const std::string janiFileOptionShortName;
+            };
+        }
+    }
+}

src/settings/modules/PGCLSettings.cpp

@@ -16,9 +16,19 @@ namespace storm {
             
             const std::string PGCLSettings::pgclFileOptionName = "pgclfile";
             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 {
@@ -29,6 +39,26 @@ namespace storm {
                 return this->getOption(pgclFileOptionName).getArgumentByName("filename").getValueAsString();
             }
             
+            bool PGCLSettings::isToJaniSet() const {
+                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

@@ -24,6 +24,32 @@ 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;
                 
@@ -32,6 +58,12 @@ namespace storm {
             private:
                 static const std::string pgclFileOptionName;
                 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/solver/SmtlibSmtSolver.cpp

@@ -23,7 +23,7 @@
 namespace storm {
     namespace solver {
 
-        SmtlibSmtSolver::SmtlibModelReference::SmtlibModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter) : ModelReference(manager), expressionAdapter(expressionAdapter){
+        SmtlibSmtSolver::SmtlibModelReference::SmtlibModelReference(storm::expressions::ExpressionManager const& manager, storm::adapters::Smt2ExpressionAdapter& expressionAdapter) : ModelReference(manager) {
             // Intentionally left empty.
         }
 

src/solver/SmtlibSmtSolver.h

@@ -30,7 +30,7 @@ namespace storm {
             private:
 
                 // The expression adapter that is used to translate the variable names.
-                storm::adapters::Smt2ExpressionAdapter& expressionAdapter;
+                //storm::adapters::Smt2ExpressionAdapter& expressionAdapter;
             };
 
         public:

src/storage/IntegerInterval.cpp

@@ -0,0 +1,2 @@
+#include "IntegerInterval.h"
+

src/storage/IntegerInterval.h

@@ -0,0 +1,56 @@
+#pragma once 
+
+#include <boost/optional.hpp>
+
+namespace storm {
+    namespace storage {
+        class IntegerInterval {
+            
+        public:
+            explicit IntegerInterval(int64_t v) : leftBound(v), rightBound(v) {
+                
+            }
+            
+            IntegerInterval(int64_t lb, int64_t rb) : leftBound(lb), rightBound(rb) {
+                
+            }
+            
+            bool hasLeftBound() const {
+                return leftBound != boost::none;
+            }
+            
+            bool hasRightBound() const {
+                return rightBound != boost::none;
+            }
+            
+            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<int64_t> getRightBound() const {
+                return rightBound;
+            }
+            
+        private:
+            boost::optional<int64_t> leftBound;
+            boost::optional<int64_t> rightBound;
+            
+        };
+        
+        std::ostream& operator<<(std::ostream& os, IntegerInterval const& i);
+    }
+}

src/storage/expressions/Expression.cpp

@@ -194,11 +194,26 @@ namespace storm {
             return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getManager(), first.getType().plusMinusTimes(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Plus)));
         }
         
+        Expression operator+(Expression const& first, int64_t second) {
+            return first + Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second)));
+        }
+        
+        Expression operator+(int64_t first, Expression const& second) {
+            return second + first;
+        }
+        
         Expression operator-(Expression const& first, Expression const& second) {
             assertSameManager(first.getBaseExpression(), second.getBaseExpression());
             return Expression(std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().plusMinusTimes(second.getType()), first.getBaseExpressionPointer(), second.getBaseExpressionPointer(), BinaryNumericalFunctionExpression::OperatorType::Minus)));
         }
         
+        Expression operator-(Expression const& first, int64_t second) {
+            return first - Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(first.getBaseExpression().getManager(), second)));
+        }
+        
+        Expression operator-(int64_t first, Expression const& second) {
+            return Expression(std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(second.getBaseExpression().getManager(), first))) - second;        }
+        
         Expression operator-(Expression const& first) {
             return Expression(std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(first.getBaseExpression().getManager(), first.getType().minus(), first.getBaseExpressionPointer(), UnaryNumericalFunctionExpression::OperatorType::Minus)));
         }

src/storage/expressions/Expression.h

@@ -23,7 +23,11 @@ namespace storm {
             template<typename MapType> friend class SubstitutionVisitor;
             
             friend Expression operator+(Expression const& first, Expression const& second);
+            friend Expression operator+(Expression const& first, int64_t second);
+            friend Expression operator+(int64_t first, Expression const& second);
             friend Expression operator-(Expression const& first, Expression const& second);
+            friend Expression operator-(Expression const& first, int64_t second);
+            friend Expression operator-(int64_t first, Expression const& second);
             friend Expression operator-(Expression const& first);
             friend Expression operator*(Expression const& first, Expression const& second);
             friend Expression operator/(Expression const& first, Expression const& second);
@@ -333,7 +337,11 @@ namespace storm {
         
         // Provide operator overloads to conveniently construct new expressions from other expressions.
         Expression operator+(Expression const& first, Expression const& second);
+        Expression operator+(Expression const& first, int64_t second);
+        Expression operator+(int64_t first, Expression const& second);
         Expression operator-(Expression const& first, Expression const& second);
+        Expression operator-(Expression const& first, int64_t second);
+        Expression operator-(int64_t first, Expression const& second);
         Expression operator-(Expression const& first);
         Expression operator*(Expression const& first, Expression const& second);
         Expression operator/(Expression const& first, Expression const& second);

src/storage/expressions/ExpressionManager.cpp

@@ -52,7 +52,7 @@ namespace storm {
             }
         }
         
-        ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), numberOfVariables(0), numberOfBooleanVariables(0), numberOfIntegerVariables(0), numberOfBitVectorVariables(0), numberOfRationalVariables(0), numberOfAuxiliaryVariables(0), numberOfAuxiliaryBooleanVariables(0), numberOfAuxiliaryIntegerVariables(0), numberOfAuxiliaryBitVectorVariables(0), numberOfAuxiliaryRationalVariables(0), freshVariableCounter(0), types() {
+        ExpressionManager::ExpressionManager() : nameToIndexMapping(), indexToNameMapping(), indexToTypeMapping(), numberOfBooleanVariables(0), numberOfIntegerVariables(0), numberOfBitVectorVariables(0), numberOfRationalVariables(0), numberOfAuxiliaryVariables(0), numberOfAuxiliaryBooleanVariables(0), numberOfAuxiliaryIntegerVariables(0), numberOfAuxiliaryBitVectorVariables(0), numberOfAuxiliaryRationalVariables(0), freshVariableCounter(0), types() {
             // Intentionally left empty.
         }
         
@@ -236,7 +236,7 @@ namespace storm {
         }
         
         uint_fast64_t ExpressionManager::getNumberOfVariables() const {
-            return numberOfVariables;
+            return numberOfBooleanVariables + numberOfIntegerVariables + numberOfBitVectorVariables + numberOfRationalVariables;
         }
         
         uint_fast64_t ExpressionManager::getNumberOfBooleanVariables() const {

src/storage/expressions/ExpressionManager.h

@@ -414,9 +414,6 @@ namespace storm {
             // A mapping from all variable indices to their types.
             std::unordered_map<uint64_t, Type> indexToTypeMapping;
             
-            // The number of declared variables.
-            uint_fast64_t numberOfVariables;
-
             // Store counts for variables.
             uint_fast64_t numberOfBooleanVariables;
             uint_fast64_t numberOfIntegerVariables;

src/storage/jani/Action.cpp

@@ -9,6 +9,5 @@ namespace storm {
         std::string const& Action::getName() const {
             return this->name;
         }
-
     }
 }

src/storage/jani/Action.h

@@ -15,7 +15,6 @@ namespace storm {
              * Returns the name of the location.
              */
             std::string const& getName() const;
-
         private:
             /// The name of the action.
             std::string name;

src/storage/jani/Automaton.cpp

@@ -148,6 +148,16 @@ namespace storm {
         std::set<uint64_t> const& Automaton::getInitialLocationIndices() const {
             return initialLocationIndices;
         }
+        
+        std::map<uint64_t, std::string> Automaton::buildIdToLocationNameMap() const {
+            std::map<uint64_t, std::string> mapping;
+            uint64_t i = 0;
+            for(auto const& loc : locations) {
+                mapping[i] = loc.getName();
+                ++i;
+            }
+            return mapping;
+        }
 
         Automaton::Edges Automaton::getEdgesFromLocation(std::string const& name) {
             auto it = locationToIndex.find(name);
@@ -299,6 +309,7 @@ namespace storm {
             actionIndices.insert(edge.getActionIndex());
         }
         
+        
         std::vector<Edge>& Automaton::getEdges() {
             return edges;
         }
@@ -322,6 +333,10 @@ namespace storm {
         uint64_t Automaton::getNumberOfEdges() const {
             return edges.size();
         }
+        
+        bool Automaton::hasRestrictedInitialStates() const {
+            return hasInitialStatesRestriction() && !(getInitialStatesExpression().evaluateAsBool());
+        }
 
         bool Automaton::hasInitialStatesRestriction() const {
             return initialStatesRestriction.isInitialized();

src/storage/jani/Automaton.h

@@ -193,6 +193,11 @@ namespace storm {
              */
             std::set<uint64_t> const& getInitialLocationIndices() const;
 
+            /*!
+             * Builds a map from ID to Location Name.
+             */
+            std::map<uint64_t, std::string> buildIdToLocationNameMap() const;
+            
             /*!
              * Retrieves the edges of the location with the given name.
              */
@@ -253,6 +258,11 @@ namespace storm {
              */
             uint64_t getNumberOfEdges() const;
             
+            /*!
+             * Retrieves whether the initial restriction is set and unequal to true
+             */
+            bool hasRestrictedInitialStates() const;
+            
             /*!
              * Retrieves whether this automaton has an initial states restriction.
              */

src/storage/jani/AutomatonComposition.cpp

@@ -19,6 +19,10 @@ namespace storm {
             return inputEnabledActions;
         }
         
+        bool AutomatonComposition::isAutomaton() const {
+            return true;
+        }
+        
         void AutomatonComposition::write(std::ostream& stream) const {
             stream << name;
         }

src/storage/jani/AutomatonComposition.h

@@ -24,6 +24,8 @@ namespace storm {
             virtual void write(std::ostream& stream) const override;
             
             std::set<std::string> const& getInputEnabledActions() const;
+
+            bool isAutomaton() const override;
             
         private:
             /// The name of the automaton this composition element refers to.

src/storage/jani/Composition.h

@@ -9,6 +9,8 @@ namespace storm {
         
         class Composition {
         public:
+            virtual bool isAutomaton() const { return false; }
+            
             virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const = 0;
             
             virtual void write(std::ostream& stream) const = 0;

src/storage/jani/CompositionInformationVisitor.cpp

@@ -104,7 +104,7 @@ namespace storm {
             CompositionInformation result;
             result.increaseAutomatonMultiplicity(composition.getAutomatonName());
             for (auto const& actionIndex : automaton.getActionIndices()) {
-                if (actionIndex != model.getSilentActionIndex()) {
+                if (actionIndex != storm::jani::Model::SILENT_ACTION_INDEX) {
                     result.addNonSilentActionIndex(actionIndex);
                 }
             }
@@ -149,15 +149,15 @@ namespace storm {
                 auto const& subinfo = subinformation[infoIndex];
                 
                 std::set<uint64_t> enabledSynchVectors;
-                std::set<std::string> actionsInSynch;
+                std::set<uint64_t> actionsInSynch;
                 for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) {
                     auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex);
                     if (synchVector.getInput(infoIndex) != SynchronizationVector::getNoActionInput()) {
-                        for (auto const& nonsilentActionIndex : subinfo.getNonSilentActionIndices()) {
-                            std::string const& nonSilentAction = indexToNameMap.at(nonsilentActionIndex);
+                        for (auto const& nonSilentActionIndex : subinfo.getNonSilentActionIndices()) {
+                            std::string const& nonSilentAction = indexToNameMap.at(nonSilentActionIndex);
                             if (synchVector.getInput(infoIndex) == nonSilentAction) {
                                 enabledSynchVectors.insert(synchVectorIndex);
-                                actionsInSynch.insert(nonSilentAction);
+                                actionsInSynch.insert(nonSilentActionIndex);
                             }
                         }
                     } else {
@@ -172,6 +172,14 @@ namespace storm {
                 effectiveSynchVectors = std::move(newEffectiveSynchVectors);
             }
 
+            // Now add all outputs of effective synchronization vectors.
+            for (auto const& synchVectorIndex : effectiveSynchVectors) {
+                auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex);
+                if (synchVector.getOutput() != storm::jani::Model::SILENT_ACTION_NAME) {
+                    nonSilentActionIndices.insert(addOrGetActionIndex(synchVector.getOutput()));
+                }
+            }
+            
             // Finally check whether it's a non-standard parallel composition. We do that by first constructing a set of
             // all effective synchronization vectors and then checking whether this set is fully contained within the
             // set of expected synchronization vectors.

src/storage/jani/Edge.cpp

@@ -71,7 +71,7 @@ namespace storm {
         
         void Edge::finalize(Model const& containingModel) {
             for (auto const& destination : getDestinations()) {
-                for (auto const& assignment : destination.getAssignments()) {
+                for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
                     if (containingModel.getGlobalVariables().hasVariable(assignment.getExpressionVariable())) {
                         writtenGlobalVariables.insert(assignment.getExpressionVariable());
                     }
@@ -79,6 +79,10 @@ namespace storm {
             }
         }
         
+        bool Edge::hasSilentAction() const {
+            return actionIndex == Model::SILENT_ACTION_INDEX;
+        }
+        
         bool Edge::addTransientAssignment(Assignment const& assignment) {
             STORM_LOG_THROW(assignment.isTransient(), storm::exceptions::InvalidArgumentException, "Must not add non-transient assignment to location.");
             return assignments.add(assignment);
@@ -88,7 +92,7 @@ namespace storm {
             if (!destinations.empty()) {
                 auto const& destination = *destinations.begin();
                 
-                for (auto const& assignment : destination.getAssignments().getTransientAssignments()) {
+                for (auto const& assignment : destination.getOrderedAssignments().getTransientAssignments()) {
                     // Check if we can lift the assignment to the edge.
                     bool canBeLifted = true;
                     for (auto const& destination : destinations) {
@@ -115,7 +119,7 @@ namespace storm {
         
         bool Edge::usesVariablesInNonTransientAssignments(std::set<storm::expressions::Variable> const& variables) const {
             for (auto const& destination : destinations) {
-                for (auto const& assignment : destination.getAssignments().getNonTransientAssignments()) {
+                for (auto const& assignment : destination.getOrderedAssignments().getNonTransientAssignments()) {
                     if (assignment.getAssignedExpression().containsVariable(variables)) {
                         return true;
                     }

src/storage/jani/Edge.h

@@ -25,6 +25,11 @@ namespace storm {
              */
             uint64_t getActionIndex() const;
             
+            /*!
+             * Returns whether it contains the silent action.
+             */
+            bool hasSilentAction() const;
+            
             /*!
              * Retrieves whether this edge has an associated rate.
              */

src/storage/jani/EdgeDestination.cpp

@@ -6,6 +6,14 @@
 namespace storm {
     namespace jani {
         
+        EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, OrderedAssignments const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) {
+            // Intentionally left empty.
+        }
+
+        EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, Assignment const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) {
+            // Intentionally left empty.
+        }
+
         EdgeDestination::EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments) : locationIndex(locationIndex), probability(probability), assignments(assignments) {
             // Intentionally left empty.
         }
@@ -26,7 +34,7 @@ namespace storm {
             this->probability = probability;
         }
         
-        OrderedAssignments const& EdgeDestination::getAssignments() const {
+        OrderedAssignments const& EdgeDestination::getOrderedAssignments() const {
             return assignments;
         }
         

src/storage/jani/EdgeDestination.h

@@ -14,6 +14,9 @@ namespace storm {
             /*!
              * Creates a new edge destination.
              */
+            EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, OrderedAssignments const& assignments);
+            
+            EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, Assignment const& assignment);
             EdgeDestination(uint64_t locationIndex, storm::expressions::Expression const& probability, std::vector<Assignment> const& assignments = {});
             
             /*!
@@ -39,7 +42,7 @@ namespace storm {
             /*!
              * Retrieves the assignments to make when choosing this destination.
              */
-            OrderedAssignments const& getAssignments() const;
+            OrderedAssignments const& getOrderedAssignments() const;
             
             /*!
              * Substitutes all variables in all expressions according to the given substitution.

src/storage/jani/JSONExporter.cpp

@@ -0,0 +1,405 @@
+#include "JSONExporter.h"
+
+#include <iostream>
+#include <fstream>
+#include <vector>
+
+#include "src/utility/macros.h"
+#include "src/exceptions/FileIoException.h"
+
+#include "src/exceptions/InvalidJaniException.h"
+
+#include "src/storage/expressions/RationalLiteralExpression.h"
+#include "src/storage/expressions/IntegerLiteralExpression.h"
+#include "src/storage/expressions/BooleanLiteralExpression.h"
+#include "src/storage/expressions/UnaryBooleanFunctionExpression.h"
+#include "src/storage/expressions/UnaryNumericalFunctionExpression.h"
+#include "src/storage/expressions/BinaryBooleanFunctionExpression.h"
+#include "src/storage/expressions/BinaryNumericalFunctionExpression.h"
+#include "src/storage/expressions/IfThenElseExpression.h"
+#include "src/storage/expressions/BinaryRelationExpression.h"
+#include "src/storage/expressions/VariableExpression.h"
+
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/ParallelComposition.h"
+
+namespace storm {
+    namespace jani {
+        
+        
+        class CompositionJsonExporter : public CompositionVisitor {
+        public:
+            CompositionJsonExporter(bool allowRecursion) : allowRecursion(allowRecursion){
+                
+            }
+            
+            static modernjson::json translate(storm::jani::Composition const& comp, bool allowRecursion = true) {
+                CompositionJsonExporter visitor(allowRecursion);
+                return boost::any_cast<modernjson::json>(comp.accept(visitor, boost::none));
+            }
+            
+            virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) {
+                modernjson::json compDecl;
+                modernjson::json autDecl;
+                autDecl["automaton"] = composition.getAutomatonName();
+                std::vector<modernjson::json> elements;
+                elements.push_back(autDecl);
+                compDecl["elements"] = elements;
+                return compDecl;
+            }
+            
+            virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) {
+                modernjson::json compDecl;
+                
+                std::vector<modernjson::json> elems;
+                for (auto const& subcomp : composition.getSubcompositions()) {
+                    modernjson::json elemDecl;
+                    if (subcomp->isAutomaton()) {
+                        modernjson::json autDecl;
+                        autDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName();
+                        std::vector<modernjson::json> elements;
+                        elements.push_back(autDecl);
+                        elemDecl["elements"] = elements;
+                    } else {
+                        STORM_LOG_THROW(allowRecursion, storm::exceptions::InvalidJaniException, "Nesting composition " << *subcomp << " is not supported by JANI.");
+                        elemDecl = boost::any_cast<modernjson::json>(subcomp->accept(*this, boost::none));
+                    }
+                    elems.push_back(elemDecl);
+                }
+                compDecl["elements"] = elems;
+                std::vector<modernjson::json> synElems;
+                for (auto const& syncs : composition.getSynchronizationVectors()) {
+                    modernjson::json syncDecl;
+                    syncDecl["synchronise"] = syncs.getInput();
+                    syncDecl["result"] = syncs.getOutput();
+                    synElems.push_back(syncDecl);
+                }
+                if (!synElems.empty()) {
+                    compDecl["syncs"] = synElems;
+                }
+                
+                return compDecl;
+            }
+            
+        private:
+            bool allowRecursion;
+        };
+        
+        
+        std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) {
+            
+            using OpType = storm::expressions::OperatorType;
+            switch(optype) {
+                case OpType::And:
+                    return "∧";
+                case OpType::Or:
+                    return "∨";
+                case OpType::Xor:
+                    return "≠";
+                case OpType::Implies:
+                    return "⇒";
+                case OpType::Iff:
+                    return "=";
+                case OpType::Plus:
+                    return "+";
+                case OpType::Minus:
+                    return "-";
+                case OpType::Times:
+                    return "*";
+                case OpType::Divide:
+                    return "/";
+                case OpType::Min:
+                    return "min";
+                case OpType::Max:
+                    return "max";
+                case OpType::Power:
+                    return "pow";
+                case OpType::Equal:
+                    return "=";
+                case OpType::NotEqual:
+                    return "≠";
+                case OpType::Less:
+                    return "<";
+                case OpType::LessOrEqual:
+                    return "≤";
+                case OpType::Greater:
+                    return ">";
+                case OpType::GreaterOrEqual:
+                    return "≥";
+                case OpType::Not:
+                    return "¬";
+                case OpType::Floor:
+                    return "floor";
+                case OpType::Ceil:
+                    return "ceil";
+                case OpType::Ite:
+                    return "ite";
+                default:
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidJaniException, "Operator not supported by Jani");
+            }
+        }
+        
+        modernjson::json ExpressionToJson::translate(storm::expressions::Expression const& expr) {
+            ExpressionToJson visitor;
+            return boost::any_cast<modernjson::json>(expr.accept(visitor, boost::none));
+        }
+        
+        
+        boost::any ExpressionToJson::visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) {
+            modernjson::json opDecl;
+            opDecl["op"] = "ite";
+            opDecl["if"] = boost::any_cast<modernjson::json>(expression.getCondition()->accept(*this, boost::none));
+            opDecl["then"] = boost::any_cast<modernjson::json>(expression.getThenExpression()->accept(*this, boost::none));
+            opDecl["else"] = boost::any_cast<modernjson::json>(expression.getElseExpression()->accept(*this, boost::none));
+            return opDecl;
+        }
+        boost::any ExpressionToJson::visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            modernjson::json opDecl;
+            opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
+            opDecl["left"] = boost::any_cast<modernjson::json>(expression.getOperand(0)->accept(*this, boost::none));
+            opDecl["right"] = boost::any_cast<modernjson::json>(expression.getOperand(1)->accept(*this, boost::none));
+            return opDecl;
+        }
+        boost::any ExpressionToJson::visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            modernjson::json opDecl;
+            opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
+            opDecl["left"] = boost::any_cast<modernjson::json>(expression.getOperand(0)->accept(*this, boost::none));
+            opDecl["right"] = boost::any_cast<modernjson::json>(expression.getOperand(1)->accept(*this, boost::none));
+            return opDecl;
+        }
+        boost::any ExpressionToJson::visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) {
+            modernjson::json opDecl;
+            opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
+            opDecl["left"] = boost::any_cast<modernjson::json>(expression.getOperand(0)->accept(*this, boost::none));
+            opDecl["right"] = boost::any_cast<modernjson::json>(expression.getOperand(1)->accept(*this, boost::none));
+            return opDecl;
+        }
+        boost::any ExpressionToJson::visit(storm::expressions::VariableExpression const& expression, boost::any const& data) {
+            return modernjson::json(expression.getVariableName());
+        }
+        boost::any ExpressionToJson::visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            modernjson::json opDecl;
+            opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
+            opDecl["exp"] = boost::any_cast<modernjson::json>(expression.getOperand()->accept(*this, boost::none));
+            return opDecl;
+        }
+        boost::any ExpressionToJson::visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            modernjson::json opDecl;
+            opDecl["op"] = operatorTypeToJaniString(expression.getOperator());
+            opDecl["exp"] = boost::any_cast<modernjson::json>(expression.getOperand()->accept(*this, boost::none));
+            return opDecl;
+        }
+        boost::any ExpressionToJson::visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data) {
+            return modernjson::json(expression.getValue());
+        }
+        boost::any ExpressionToJson::visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data) {
+            return modernjson::json(expression.getValue());
+        }
+        boost::any ExpressionToJson::visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data) {
+            return modernjson::json(expression.getValueAsDouble());
+        }
+        
+        
+        
+        
+        
+        
+        
+        void JsonExporter::toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid) {
+            std::ofstream ofs;
+            ofs.open (filepath, std::ofstream::out );
+            if(ofs.is_open()) {
+                toStream(janiModel, ofs, checkValid);
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Cannot open " << filepath);
+            }
+        }
+        
+        void JsonExporter::toStream(storm::jani::Model const& janiModel, std::ostream& os, bool checkValid) {
+            if(checkValid) {
+                janiModel.checkValid();
+            }
+            JsonExporter exporter;
+            exporter.convertModel(janiModel);
+            os << exporter.finalize().dump(4) << std::endl;
+        }
+        
+        modernjson::json buildActionArray(std::vector<storm::jani::Action> const& actions) {
+            std::vector<modernjson::json> actionReprs;
+            uint64_t actIndex = 0;
+            for(auto const& act : actions) {
+                if(actIndex == storm::jani::Model::SILENT_ACTION_INDEX) {
+                    actIndex++;
+                    continue;
+                }
+                actIndex++;
+                modernjson::json actEntry;
+                actEntry["name"] = act.getName();
+                actionReprs.push_back(actEntry);
+            }
+            
+            return modernjson::json(actionReprs);
+            
+        }
+        
+        
+        modernjson::json buildExpression(storm::expressions::Expression const& exp) {
+            return ExpressionToJson::translate(exp);
+        }
+        
+        
+        modernjson::json buildConstantsArray(std::vector<storm::jani::Constant> const& constants) {
+            std::vector<modernjson::json> constantDeclarations;
+            for(auto const& constant : constants) {
+                modernjson::json constantEntry;
+                constantEntry["name"] = constant.getName();
+                modernjson::json typeDesc;
+                if(constant.isBooleanConstant()) {
+                    typeDesc = "bool";
+                } else if(constant.isRealConstant()) {
+                    typeDesc = "real";
+                } else {
+                    assert(constant.isIntegerConstant());
+                    typeDesc = "int";
+                }
+                constantEntry["type"] = typeDesc;
+                if(constant.isDefined()) {
+                    constantEntry["value"] = buildExpression(constant.getExpression());
+                }
+                constantDeclarations.push_back(constantEntry);
+            }
+            return modernjson::json(constantDeclarations);
+        }
+        
+        modernjson::json buildVariablesArray(storm::jani::VariableSet const& varSet) {
+            std::vector<modernjson::json> variableDeclarations;
+            for(auto const& variable : varSet) {
+                modernjson::json varEntry;
+                varEntry["name"] = variable.getName();
+                varEntry["transient"] = variable.isTransient();
+                modernjson::json typeDesc;
+                if(variable.isBooleanVariable()) {
+                    typeDesc = "bool";
+                } else if(variable.isRealVariable()) {
+                    typeDesc = "real";
+                } else if(variable.isUnboundedIntegerVariable()) {
+                    typeDesc = "int";
+                } else {
+                    assert(variable.isBoundedIntegerVariable());
+                    typeDesc["kind"] = "bounded";
+                    typeDesc["base"] = "int";
+                    typeDesc["lower-bound"] = buildExpression(variable.asBoundedIntegerVariable().getLowerBound());
+                    typeDesc["upper-bound"] = buildExpression(variable.asBoundedIntegerVariable().getUpperBound());
+                }
+                
+                varEntry["type"] = typeDesc;
+                if(variable.hasInitExpression()) {
+                    varEntry["initial-value"] = buildExpression(variable.getInitExpression());
+                }
+                variableDeclarations.push_back(varEntry);
+            }
+            return modernjson::json(variableDeclarations);
+            
+        }
+        
+        modernjson::json buildAssignmentArray(storm::jani::OrderedAssignments const& orderedAssignments) {
+            std::vector<modernjson::json> assignmentDeclarations;
+            bool addIndex = orderedAssignments.hasMultipleLevels();
+            for(auto const& assignment : orderedAssignments) {
+                modernjson::json assignmentEntry;
+                assignmentEntry["ref"] = assignment.getVariable().getName();
+                assignmentEntry["value"] = buildExpression(assignment.getAssignedExpression());
+                if(addIndex) {
+                    assignmentEntry["index"] = assignment.getLevel();
+                }
+                assignmentDeclarations.push_back(assignmentEntry);
+            }
+            return modernjson::json(assignmentDeclarations);
+        }
+        
+        modernjson::json buildLocationsArray(std::vector<storm::jani::Location> const& locations) {
+            std::vector<modernjson::json> locationDeclarations;
+            for(auto const& location : locations) {
+                modernjson::json locEntry;
+                locEntry["name"] = location.getName();
+                // TODO support invariants?
+                locEntry["transient-values"] = buildAssignmentArray(location.getAssignments());
+                locationDeclarations.push_back(locEntry);
+            }
+            return modernjson::json(locationDeclarations);
+        }
+        
+        modernjson::json buildInitialLocations(storm::jani::Automaton const& automaton) {
+            std::vector<std::string> names;
+            for(auto const& initLocIndex : automaton.getInitialLocationIndices()) {
+                names.push_back(automaton.getLocation(initLocIndex).getName());
+            }
+            return modernjson::json(names);
+        }
+        
+        modernjson::json buildDestinations(std::vector<EdgeDestination> const& destinations, std::map<uint64_t, std::string> const& locationNames) {
+            std::vector<modernjson::json> destDeclarations;
+            for(auto const& destination : destinations) {
+                modernjson::json destEntry;
+                destEntry["location"] = locationNames.at(destination.getLocationIndex());
+                destEntry["probability"]["exp"] = buildExpression(destination.getProbability());
+                destEntry["assignments"] = buildAssignmentArray(destination.getOrderedAssignments());
+                destDeclarations.push_back(destEntry);
+            }
+            return modernjson::json(destDeclarations);
+        }
+        
+        modernjson::json buildEdges(std::vector<Edge> const& edges , std::map<uint64_t, std::string> const& actionNames, std::map<uint64_t, std::string> const& locationNames) {
+            std::vector<modernjson::json> edgeDeclarations;
+            for(auto const& edge : edges) {
+                modernjson::json edgeEntry;
+                edgeEntry["location"] = locationNames.at(edge.getSourceLocationIndex());
+                if(!edge.hasSilentAction()) {
+                    edgeEntry["action"] = actionNames.at(edge.getActionIndex());
+                }
+                if(edge.hasRate()) {
+                    edgeEntry["rate"]["exp"] = buildExpression(edge.getRate());
+                }
+                edgeEntry["guard"]["exp"] = buildExpression(edge.getGuard());
+                edgeEntry["destinations"] = buildDestinations(edge.getDestinations(), locationNames);
+                
+                edgeDeclarations.push_back(edgeEntry);
+            }
+            return modernjson::json(edgeDeclarations);
+        }
+        
+        modernjson::json buildAutomataArray(std::vector<storm::jani::Automaton> const& automata, std::map<uint64_t, std::string> const& actionNames) {
+            std::vector<modernjson::json> automataDeclarations;
+            for(auto const& automaton : automata) {
+                modernjson::json autoEntry;
+                autoEntry["name"] = automaton.getName();
+                autoEntry["variables"] = buildVariablesArray(automaton.getVariables());
+                if(automaton.hasRestrictedInitialStates()) {
+                    autoEntry["restrict-initial"]["exp"] = buildExpression(automaton.getInitialStatesRestriction());
+                }
+                autoEntry["locations"] = buildLocationsArray(automaton.getLocations());
+                autoEntry["initial-locations"] = buildInitialLocations(automaton);
+                autoEntry["edges"] = buildEdges(automaton.getEdges(), actionNames, automaton.buildIdToLocationNameMap());
+                automataDeclarations.push_back(autoEntry);
+            }
+            return modernjson::json(automataDeclarations);
+        }
+        
+        
+        void JsonExporter::convertModel(storm::jani::Model const& janiModel) {
+            jsonStruct["jani-version"] = janiModel.getJaniVersion();
+            jsonStruct["name"] = janiModel.getName();
+            jsonStruct["type"] = to_string(janiModel.getModelType());
+            jsonStruct["actions"] = buildActionArray(janiModel.getActions());
+            jsonStruct["constants"] = buildConstantsArray(janiModel.getConstants());
+            jsonStruct["variables"] = buildVariablesArray(janiModel.getGlobalVariables());
+            jsonStruct["restrict-initial"]["exp"] = buildExpression(janiModel.getInitialStatesRestriction());
+            jsonStruct["automata"] = buildAutomataArray(janiModel.getAutomata(), janiModel.getActionIndexToNameMap());
+            jsonStruct["system"] = CompositionJsonExporter::translate(janiModel.getSystemComposition());
+            
+        }
+        
+        
+        
+    }
+}

src/storage/jani/JSONExporter.h

@@ -0,0 +1,51 @@
+#pragma once
+
+
+#include "src/storage/expressions/ExpressionVisitor.h"
+#include "Model.h"
+// JSON parser
+#include "json.hpp"
+namespace modernjson = nlohmann;
+
+namespace storm {
+    namespace jani {
+        
+        class ExpressionToJson : public storm::expressions::ExpressionVisitor {
+            
+        public:
+            static modernjson::json translate(storm::expressions::Expression const& expr);
+            
+            virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const& data);
+            virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const& data);
+            
+        };
+        
+        class JsonExporter {
+            JsonExporter() = default;
+            
+        public:
+            static void toFile(storm::jani::Model const& janiModel, std::string const& filepath, bool checkValid = true);
+            static void toStream(storm::jani::Model const& janiModel, std::ostream& ostream, bool checkValid = false);
+            
+        private:
+            void convertModel(storm::jani::Model const& model);
+            void appendVariableDeclaration(storm::jani::Variable const& variable);
+            
+            modernjson::json finalize() {
+                return jsonStruct;
+            }
+            
+            modernjson::json jsonStruct;
+            
+            
+        };
+    }
+}

src/storage/jani/Model.cpp

@@ -14,6 +14,7 @@ namespace storm {
     namespace jani {
         
         const std::string Model::SILENT_ACTION_NAME = "";
+        const uint64_t Model::SILENT_ACTION_INDEX = 0;
         
         Model::Model() {
             // Intentionally left empty.
@@ -31,7 +32,8 @@ namespace storm {
             initialStatesRestriction = this->expressionManager->boolean(true);
             
             // Add a prefined action that represents the silent action.
-            silentActionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME));
+            uint64_t actionIndex = addAction(storm::jani::Action(SILENT_ACTION_NAME));
+            STORM_LOG_ASSERT(actionIndex == SILENT_ACTION_INDEX, "Illegal silent action index.");
         }
         
         storm::expressions::ExpressionManager& Model::getManager() const {
@@ -226,7 +228,7 @@ namespace storm {
             std::vector<std::shared_ptr<Composition>> subcompositions;
             for (auto const& automaton : automata) {
                 automatonActionIndices.push_back(automaton.getActionIndices());
-                automatonActionIndices.back().erase(silentActionIndex);
+                automatonActionIndices.back().erase(SILENT_ACTION_INDEX);
                 allActionIndices.insert(automatonActionIndices.back().begin(), automatonActionIndices.back().end());
                 subcompositions.push_back(std::make_shared<AutomatonComposition>(automaton.getName()));
             }
@@ -266,18 +268,28 @@ namespace storm {
             this->composition = composition;
         }
         
+        void Model::setStandardSystemComposition() {
+            setSystemComposition(getStandardSystemComposition());
+        }
+        
         std::set<std::string> Model::getActionNames(bool includeSilent) const {
             std::set<std::string> result;
             for (auto const& entry : actionToIndex) {
-                if (includeSilent || entry.second != silentActionIndex) {
+                if (includeSilent || entry.second != SILENT_ACTION_INDEX) {
                     result.insert(entry.first);
                 }
             }
             return result;
         }
-                
-        uint64_t Model::getSilentActionIndex() const {
-            return SILENT_ACTION_INDEX;
+
+        std::map<uint64_t, std::string> Model::getActionIndexToNameMap() const {
+            std::map<uint64_t, std::string> mapping;
+            uint64_t i = 0;
+            for(auto const& act : actions) {
+                mapping[i] = act.getName();
+                ++i;
+            }
+            return mapping;
         }
         
         Model Model::defineUndefinedConstants(std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantDefinitions) const {
@@ -435,31 +447,17 @@ namespace storm {
             }
         }
         
-        bool Model::checkValidity(bool logdbg) const {
+        void Model::checkValid() const {
             // TODO switch to exception based return value.
-            
-            if (version == 0) {
-                if(logdbg) STORM_LOG_DEBUG("Jani version is unspecified");
-                return false;
-            }
-            
-            if(modelType == ModelType::UNDEFINED) {
-                if(logdbg) STORM_LOG_DEBUG("Model type is unspecified");
-                return false;
-            }
-            
-            if(automata.empty()) {
-                if(logdbg) STORM_LOG_DEBUG("No automata specified");
-                return false;
-            }
-            // All checks passed.
-            return true;
+            STORM_LOG_ASSERT(getModelType() != storm::jani::ModelType::UNDEFINED, "Model type not set");
+            STORM_LOG_ASSERT(!automata.empty(), "No automata set");
+            STORM_LOG_ASSERT(composition != nullptr, "Composition is not set");
             
         }
         
         bool Model::hasStandardComposition() const {
-            CompositionInformationVisitor visitor;
-            CompositionInformation info = visitor.getInformation(this->getSystemComposition(), *this);
+            CompositionInformationVisitor visitor(*this, this->getSystemComposition());
+            CompositionInformation info = visitor.getInformation();
             if (info.containsNonStandardParallelComposition()) {
                 return false;
             }
@@ -513,13 +511,5 @@ namespace storm {
             return true;
         }
         
-        std::string const& Model::getSilentActionName() {
-            return Model::SILENT_ACTION_NAME;
-        }
-        
-        bool Model::isSilentAction(std::string const& name) {
-            return name == Model::SILENT_ACTION_NAME;
-        }
-
     }
 }

src/storage/jani/Model.h

@@ -17,6 +17,8 @@ namespace storm {
         
         class Exporter;
         
+        
+        
         class Model {
         public:
             friend class Exporter;
@@ -86,6 +88,11 @@ namespace storm {
              * Retrieves the actions of the model.
              */
             std::vector<Action> const& getActions() const;
+    
+            /*!
+             *  Builds a map with action indices mapped to their names
+             */
+            std::map<uint64_t, std::string> getActionIndexToNameMap() const;
             
             /*!
              * Retrieves all non-silent action indices of the model.
@@ -217,6 +224,11 @@ namespace storm {
              */
             void setSystemComposition(std::shared_ptr<Composition> const& composition);
             
+            /*!
+             * Sets the system composition to be the fully-synchronizing parallel composition of all automat
+             * @see getStandardSystemComposition
+             */
+            void setStandardSystemComposition();
             /*!
              * Gets the system composition as the standard, fully-synchronizing parallel composition.
              */
@@ -314,7 +326,7 @@ namespace storm {
             /*!
              *  Checks if the model is valid JANI, which should be verified before any further operations are applied to a model.
              */
-            bool checkValidity(bool logdbg = true) const;
+            void checkValid() const;
             
             /*!
              * Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.
@@ -323,25 +335,13 @@ namespace storm {
              */
             bool undefinedConstantsAreGraphPreserving() const;
             
-            /*!
-             * Retrieves the name of the silent action.
-             */
-            static std::string const& getSilentActionName();
-            
-            /*!
-             * Checks whether the provided action name belongs to the silent action.
-             */
-            static bool isSilentAction(std::string const& name);
-            
-            /*!
-             * Retrieves the index of the silent action.
-             */
-            static uint64_t getSilentActionIndex();
-            
-        private:
             /// The name of the silent action.
             static const std::string SILENT_ACTION_NAME;
             
+            /// The index of the silent action.
+            static const uint64_t SILENT_ACTION_INDEX;
+            
+        private:
             /// The model name.
             std::string name;
             
@@ -363,9 +363,6 @@ namespace storm {
             /// The set of non-silent action indices.
             boost::container::flat_set<uint64_t> nonsilentActionIndices;
             
-            /// The index of the silent action.
-            uint64_t silentActionIndex;
-            
             /// The constants defined by the model.
             std::vector<Constant> constants;
             

src/storage/jani/ModelType.cpp

@@ -4,48 +4,38 @@ namespace storm {
     namespace jani {
         
         std::ostream& operator<<(std::ostream& stream, ModelType const& type) {
+            return stream << to_string(type);
+        }
+        
+        std::string to_string(ModelType const& type) {
             switch (type) {
                 case ModelType::UNDEFINED:
-                    stream << "undefined";
-                    break;
+                    return "undefined";
                 case ModelType::LTS:
-                    stream << "lts";
-                    break;
+                    return "lts";
                 case ModelType::DTMC:
-                    stream << "dtmc";
-                    break;
+                    return "dtmc";
                 case ModelType::CTMC:
-                    stream << "ctmc";
-                    break;
+                    return "ctmc";
                 case ModelType::MDP:
-                    stream << "mdp";
-                    break;
+                    return "mdp";
                 case ModelType::CTMDP:
-                    stream << "ctmdp";
-                    break;
+                    return "ctmdp";
                 case ModelType::MA:
-                    stream << "ma";
-                    break;
+                    return "ma";
                 case ModelType::TA:
-                    stream << "ta";
-                    break;
+                    return "ta";
                 case ModelType::PTA:
-                    stream << "pta";
-                    break;
+                    return "pta";
                 case ModelType::STA:
-                    stream << "sta";
-                    break;
+                    return "sta";
                 case ModelType::HA:
-                    stream << "ha";
-                    break;
+                    return "ha";
                 case ModelType::PHA:
-                    stream << "pha";
-                    break;
+                    return "pha";
                 case ModelType::SHA:
-                    stream << "sha";
-                    break;
+                    return "sha";
             }
-            return stream;
         }
 
         ModelType getModelType(std::string const& input) {

src/storage/jani/ModelType.h

@@ -10,6 +10,7 @@ namespace storm {
                             HA = 10, PHA = 11, SHA = 12};
 
         ModelType getModelType(std::string const& input);
+        std::string to_string(ModelType const& type);
         std::ostream& operator<<(std::ostream& stream, ModelType const& type);
         
     }

src/storage/jani/OrderedAssignments.cpp

@@ -12,6 +12,10 @@ namespace storm {
             }
         }
         
+        OrderedAssignments::OrderedAssignments(Assignment const& assignment) {
+            add(assignment);
+        }
+        
         bool OrderedAssignments::add(Assignment const& assignment) {
             // If the element is contained in this set of assignment, nothing needs to be added.
             if (this->contains(assignment)) {
@@ -65,6 +69,19 @@ namespace storm {
             return true;
         }
         
+        bool OrderedAssignments::hasMultipleLevels() const {
+            if(allAssignments.empty()) {
+                return false;
+            }
+            uint64_t firstLevel = allAssignments.front()->getLevel();
+            for(auto const& assignment : allAssignments) {
+                if(assignment->getLevel() != firstLevel) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
         bool OrderedAssignments::contains(Assignment const& assignment) const {
             auto it = lowerBound(assignment, allAssignments);
             if (it != allAssignments.end() && assignment == **it) {

src/storage/jani/OrderedAssignments.h

@@ -19,6 +19,8 @@ namespace storm {
              */
             OrderedAssignments(std::vector<Assignment> const& assignments = std::vector<Assignment>());
 
+            explicit OrderedAssignments(Assignment const& assignment);
+            
             /*!
              * Adds the given assignment to the set of assignments.
              *
@@ -32,7 +34,14 @@ namespace storm {
              * @return True if the assignment was found and removed.
              */
             bool remove(Assignment const& assignment);
-
+            
+            /*!
+             * Checks whether the assignments have several levels.
+             * 
+             * @return True if more than one level occurs in the assignment set.
+             */
+            bool hasMultipleLevels() const;
+            
             /*!
              * Retrieves whether the given assignment is contained in this set of assignments.
              */

src/storage/pgcl/AbstractStatementVisitor.h

@@ -1,9 +1,4 @@
-//
-// Created by Lukas Westhofen on 22.04.15.
-//
-
-#ifndef STORM_ABSTRACTSTATEVISITOR_H
-#define STORM_ABSTRACTSTATEVISITOR_H
+#pragma once 
 
 namespace storm {
     namespace pgcl {
@@ -20,14 +15,13 @@ namespace storm {
         public:
             // Those functions need to be implemented for every possible
             // statement instantiation.
-            virtual void visit(class AssignmentStatement&) = 0;
-            virtual void visit(class ObserveStatement&) = 0;
-            virtual void visit(class IfStatement&) = 0;
-            virtual void visit(class LoopStatement&) = 0;
-            virtual void visit(class NondeterministicBranch&) = 0;
-            virtual void visit(class ProbabilisticBranch&) = 0;
+            virtual void visit(class AssignmentStatement const&) = 0;
+            virtual void visit(class ObserveStatement const&) = 0;
+            virtual void visit(class IfStatement const&) = 0;
+            virtual void visit(class LoopStatement const&) = 0;
+            virtual void visit(class NondeterministicBranch const&) = 0;
+            virtual void visit(class ProbabilisticBranch const&) = 0;
         };
     }
 }
 
-#endif //STORM_ABSTRACTSTATEVISITOR_H

src/storage/pgcl/AssignmentStatement.cpp

@@ -1,10 +1,3 @@
-/* 
- * File:   AssignmentStatement.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:42
- */
-
 #include "src/storage/pgcl/AssignmentStatement.h"
 
 namespace storm {
@@ -13,25 +6,21 @@ namespace storm {
             variable(variable), expression(expression) {
         }
         
-        boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& AssignmentStatement::getExpression() {
+        bool AssignmentStatement::isDeterministic() const {
+            return expression.which() == 0;
+        }
+        
+        boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& AssignmentStatement::getExpression() const {
             return this->expression;
         }
 
-        storm::expressions::Variable const& AssignmentStatement::getVariable() {
+        storm::expressions::Variable const& AssignmentStatement::getVariable() const {
             return this->variable;
         }
 
         void AssignmentStatement::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
             visitor.visit(*this);
         }
-
-        std::size_t AssignmentStatement::getNumberOfOutgoingTransitions() {
-            if(this->expression.which() == 1) {
-                return boost::get<storm::pgcl::UniformExpression>(this->expression).getEnd() - boost::get<storm::pgcl::UniformExpression>(this->expression).getBegin() + 1;
-            } else {
-                return 1;
-            }
-        }
     }
 }
 

src/storage/pgcl/AssignmentStatement.h

@@ -1,12 +1,4 @@
-/* 
- * File:   AssignmentStatement.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:42
- */
-
-#ifndef ASSIGNMENTSTATEMENT_H
-#define	ASSIGNMENTSTATEMENT_H
+#pragma once
 
 #include "src/storage/pgcl/SimpleStatement.h"
 #include "src/storage/pgcl/UniformExpression.h"
@@ -22,7 +14,7 @@ namespace storm {
          * identifier := expression; where the expression is either handled by
          * the expression manager or is a uniform distribution expression.
          */
-        class AssignmentStatement : public SimpleStatement {
+        class AssignmentStatement : public Statement {
         public:
             AssignmentStatement() = default;
             /**
@@ -34,18 +26,19 @@ namespace storm {
             AssignmentStatement(storm::expressions::Variable const& variable, boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& expression);
             AssignmentStatement(const AssignmentStatement& orig) = default;
             virtual ~AssignmentStatement() = default;
-            std::size_t getNumberOfOutgoingTransitions();
-            void accept(class AbstractStatementVisitor&);
+            void accept(AbstractStatementVisitor&);
             /**
              * Returns the right hand expression of the assignemnt.
              * @return The expression of the assignment.
              */
-            boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& getExpression();
+            boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& getExpression() const;
+            
+            bool isDeterministic() const;
             /**
              * Returns the left hand variable of the assignemnt.
              * @return The variable to which the expression is assigned.
              */
-            storm::expressions::Variable const& getVariable();
+            storm::expressions::Variable const& getVariable() const;
         private:
             /// Represents the variable of our assignment statement.
             storm::expressions::Variable variable;
@@ -54,6 +47,3 @@ namespace storm {
         };
     }
 }
-
-#endif	/* ASSIGNMENTSTATEMENT_H */
-

src/storage/pgcl/Block.cpp

@@ -0,0 +1,92 @@
+#include "Block.h"
+#include "StatementPrinterVisitor.h"
+#include <typeinfo>
+
+namespace storm {
+    namespace pgcl {
+        
+        
+        PgclBlock::PgclBlock(vector const &statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve)
+        : sequenceOfStatements(statements),
+        expressions(expressions),
+        loop(hasLoop),
+        nondet(hasNondet),
+        observe(hasObserve)
+        {
+            
+        }
+        
+        iterator PgclBlock::begin() {
+            return this->sequenceOfStatements.begin();
+        }
+        
+        const_iterator PgclBlock::begin() const {
+            return this->sequenceOfStatements.begin();
+        }
+        
+        iterator PgclBlock::end() {
+            return this->sequenceOfStatements.end();
+        }
+        
+        const_iterator PgclBlock::end() const {
+            return this->sequenceOfStatements.end();
+        }
+        
+        bool PgclBlock::empty() {
+            return this->sequenceOfStatements.empty();
+        }
+        
+        element PgclBlock::front() {
+            return this->sequenceOfStatements.front();
+        }
+        
+        element PgclBlock::back() {
+            return this->sequenceOfStatements.back();
+        }
+        
+        unsigned long PgclBlock::size() {
+            return this->sequenceOfStatements.size();
+        }
+        
+        element PgclBlock::at(size_type n) {
+            return this->sequenceOfStatements.at(n);
+        }
+        
+        iterator PgclBlock::insert(iterator position, const element& statement) {
+            return this->sequenceOfStatements.insert(position, statement);
+        }
+        
+        void PgclBlock::clear() {
+            this->sequenceOfStatements.clear();
+        }
+        
+        std::shared_ptr<storm::expressions::ExpressionManager> const&  PgclBlock::getExpressionManager() const  {
+            return this->expressions;
+        }
+        
+        std::vector<storm::expressions::Variable> PgclBlock::getParameters() {
+            return this->parameters;
+        }
+        
+        bool PgclBlock::hasParameters() const {
+            return !(this->parameters.empty());
+        }
+        
+        bool PgclBlock::hasObserve() const {
+            return this->observe;
+        }
+        
+        bool PgclBlock::hasNondet() const {
+            return this->nondet;
+        }
+        
+        bool PgclBlock::hasLoop() const {
+            return this->loop;
+        }
+        
+        iterator PgclBlock::find(element &statement) {
+            return std::find(this->sequenceOfStatements.begin(), this->sequenceOfStatements.end(), statement);
+        }
+        
+    }
+}

src/storage/pgcl/Block.h

@@ -0,0 +1,121 @@
+#pragma once
+
+#include <vector>
+#include "src/storage/pgcl/Statement.h"
+#include "src/storage/pgcl/StatementPrinterVisitor.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+    namespace pgcl {
+        
+        typedef std::shared_ptr<storm::pgcl::Statement> element;
+        typedef std::vector<element> vector;
+        typedef std::vector<element>::iterator iterator;
+        typedef std::vector<element>::const_iterator const_iterator;
+        typedef std::vector<element>::size_type size_type;
+        
+        /**
+         * This class represents a complete and functional PGCL program. It
+         * contains an expression manager which keeps track of the current
+         * identifiers and variable valuations. Other than that, it basically
+         * wraps a std::vector of program statements and is intended to be used
+         * as such.
+         */
+        class PgclBlock {
+        public:
+            PgclBlock() = default;
+            /**
+             * Does the same as the beforementioned constructor, but sets the
+             * location to statement vector to the empty vector. This
+             * constructor should be used for sub-programs, for which the
+             * location to statement relation doesn't make much sense.
+             * @param statements The sequence of statements representing the
+             * program.
+             * @param expressions The manager responsible for the expressions
+             * and variables of the program.
+             * @param hasLoop Whether the program contains a loop
+             * @param hasNondet Whether the program contains a nondeterministic
+             * statement.
+             * @param hasParam Whether the program is parameterized.
+             */
+            PgclBlock(vector const& statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve);
+            PgclBlock(const PgclBlock & orig) = default;
+            PgclBlock & operator=(PgclBlock const& other) = default;
+            iterator begin();
+            const_iterator begin() const;
+            iterator end();
+            const_iterator end() const;
+            element front();
+            element back();
+            unsigned long size();
+            element at(size_type n);
+            iterator insert(iterator position, const element& statement);
+            iterator find(element& statement);
+            void clear();
+            bool empty();
+      
+            /**
+             * Returns the list of parameters of the PGCL program.
+             */
+            std::vector<storm::expressions::Variable> getParameters();
+            /**
+             * Returns the expression manager of the PGCL program, which is
+             * responsible for managing all expressions and variables of the
+             * the program and all its subprograms.
+             * @return The expression manager of the program.
+             */
+            std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const;
+            
+            /**
+             * Returns true if the program contains a loop statement.
+             * @return True if the program has a loop.
+             */
+            bool hasLoop() const;
+            /**
+             * Returns true if the program contains a nondeterministic
+             * statement.
+             * @return True if the program has a nondeterministic statement.
+             */
+            bool hasNondet() const;
+            /**
+             * Returns true if the program contains an observe statement.
+             * @return True if the program has an observe statement.
+             */
+            bool hasObserve() const;
+            /**
+             * Returns true if the program is parameterized.
+             * @return True if the program has at least one parameter.
+             */
+            bool hasParameters() const;
+            
+        protected:
+            /**
+             * We are basically wrapping a std::vector which represents the
+             * ordered single statements of the program.
+             */
+            vector sequenceOfStatements;
+            /**
+             * Stores the parameters a.k.a. free variables of the PGCL program.
+             */
+            std::vector<storm::expressions::Variable> parameters;
+            /**
+             * Handles the expressions and variables for the whole program.
+             * The expressions of every subprogram are also handled by this
+             * manager. We are using a shared pointer since all subprograms
+             * are referring to that expression manager, too.
+             */
+            std::shared_ptr<storm::expressions::ExpressionManager> expressions;
+            /**
+             * Boolean variables to save some properties of the PGCL program.
+             * They are later on used by the model builder to possibly
+             * construct simpler models (e.g. if no loops, params and nondets
+             * are used, a DTMC suffices).
+             * The values are set to true if the PGCL parser hits a loop resp.
+             * nondet resp. observe resp. parameter statement.
+             */
+            bool loop    = false;
+            bool nondet  = false;
+            bool observe = false;
+        };
+    }
+}

src/storage/pgcl/BooleanExpression.cpp

@@ -1,10 +1,3 @@
-/* 
- * File:   BooleanExpression.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:44
- */
-
 #include "src/storage/pgcl/BooleanExpression.h"
 #include "src/storage/expressions/ExpressionManager.h"
 
@@ -14,7 +7,7 @@ namespace storm {
             booleanExpression(booleanExpression) {
         }
         
-        storm::expressions::Expression& BooleanExpression::getBooleanExpression() {
+        storm::expressions::Expression const& BooleanExpression::getBooleanExpression() const {
             return this->booleanExpression;
         }
     }

src/storage/pgcl/BooleanExpression.h

@@ -1,12 +1,4 @@
-/* 
- * File:   BooleanExpression.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:44
- */
-
-#ifndef BOOLEANEXPRESSION_H
-#define	BOOLEANEXPRESSION_H
+#pragma once
 
 #include "src/storage/expressions/Expression.h"
 
@@ -31,12 +23,9 @@ namespace storm {
              * Returns the expression.
              * @return The expression of boolean type.
              */
-            storm::expressions::Expression& getBooleanExpression();
+            storm::expressions::Expression const& getBooleanExpression() const;
         private:
             storm::expressions::Expression booleanExpression;
         };
     }
-}
-
-#endif	/* BOOLEANEXPRESSION_H */
-
+}

src/storage/pgcl/BranchStatement.cpp

@@ -1,25 +1,15 @@
-/* 
- * File:   BranchStatement.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:42
- */
-
 #include "src/storage/pgcl/BranchStatement.h"
 #include "src/storage/pgcl/AbstractStatementVisitor.h"
 
 namespace storm {
     namespace pgcl {
-        std::shared_ptr<storm::pgcl::PgclProgram> BranchStatement::getLeftBranch() {
+        std::shared_ptr<storm::pgcl::PgclBlock> const& BranchStatement::getLeftBranch() const {
             return this->leftBranch;
         }
 
-        std::shared_ptr<storm::pgcl::PgclProgram> BranchStatement::getRightBranch() {
+        std::shared_ptr<storm::pgcl::PgclBlock> const& BranchStatement::getRightBranch() const {
             return this->rightBranch;
         }
 
-        std::size_t BranchStatement::getNumberOfOutgoingTransitions() {
-            return 2;
-        }
     }
 }

src/storage/pgcl/BranchStatement.h

@@ -1,12 +1,4 @@
-/* 
- * File:   BranchStatement.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:42
- */
-
-#ifndef BRANCHSTATEMENT_H
-#define	BRANCHSTATEMENT_H
+#pragma once 
 
 #include "src/storage/pgcl/PgclProgram.h"
 #include "src/storage/pgcl/CompoundStatement.h"
@@ -19,28 +11,25 @@ namespace storm {
          * compound statements, every branch is again a complete PGCL program
          * itself.
          */
-        class BranchStatement : public CompoundStatement {
+        class BranchStatement : public Statement {
         public:
             BranchStatement() = default;
             BranchStatement(const BranchStatement& orig) = default;
             virtual ~BranchStatement() = default;
             virtual void accept(class AbstractStatementVisitor&) = 0;
-            std::size_t getNumberOfOutgoingTransitions();
             /**
              * Returns the left branch of the statement.
              * @return The left branch PGCL program.
              */
-            std::shared_ptr<storm::pgcl::PgclProgram> getLeftBranch();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getLeftBranch() const;
             /**
              * Returns the right branch of the statement.
              * @return The right branch PGCL program.
              */
-            std::shared_ptr<storm::pgcl::PgclProgram> getRightBranch();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getRightBranch() const;
         protected:
-            std::shared_ptr<storm::pgcl::PgclProgram> leftBranch;
-            std::shared_ptr<storm::pgcl::PgclProgram> rightBranch;
+            std::shared_ptr<storm::pgcl::PgclBlock> leftBranch;
+            std::shared_ptr<storm::pgcl::PgclBlock> rightBranch;
         };
     }
 }
-
-#endif	/* BRANCHSTATEMENT_H */

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/pgcl/IfStatement.cpp

@@ -1,41 +1,31 @@
-/* 
- * File:   IfStatement.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:42
- */
-
 #include "IfStatement.h"
 #include "src/storage/pgcl/AbstractStatementVisitor.h"
 
 namespace storm {
     namespace pgcl {
-        IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body) :
+        IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& body) :
             ifBody(body), condition(condition) {
         }
 
-        IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& ifBody, std::shared_ptr<storm::pgcl::PgclProgram> const& elseBody) :
+        IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& ifBody, std::shared_ptr<storm::pgcl::PgclBlock> const& elseBody) :
             ifBody(ifBody), elseBody(elseBody), condition(condition) {
             this->hasElseBody = true;
         }
 
-        std::shared_ptr<storm::pgcl::PgclProgram> IfStatement::getIfBody() {
+        std::shared_ptr<storm::pgcl::PgclBlock> const& IfStatement::getIfBody() const {
             return this->ifBody;
         }
 
-        std::shared_ptr<storm::pgcl::PgclProgram> IfStatement::getElseBody() {
-            if(this->elseBody) {
-                return this->elseBody;
-            } else {
-                throw "Tried to access non-present else body of if statement.";
-            }
+        std::shared_ptr<storm::pgcl::PgclBlock> const& IfStatement::getElseBody() const {
+            assert(hasElse());
+            return this->elseBody;
         }
         
-        bool IfStatement::hasElse() {
+        bool IfStatement::hasElse() const{
             return this->hasElseBody;
         }
         
-        storm::pgcl::BooleanExpression& IfStatement::getCondition() {
+        storm::pgcl::BooleanExpression const& IfStatement::getCondition() const {
             return this->condition;
         }
 
@@ -43,8 +33,5 @@ namespace storm {
             visitor.visit(*this);
         }
 
-        std::size_t IfStatement::getNumberOfOutgoingTransitions() {
-            return 1;
-        }
     }
 }

src/storage/pgcl/IfStatement.h

@@ -1,12 +1,4 @@
-/* 
- * File:   IfStatement.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:42
- */
-
-#ifndef IFSTATEMENT_H
-#define	IFSTATEMENT_H
+#pragma once
 
 #include "src/storage/pgcl/CompoundStatement.h"
 #include "src/storage/pgcl/BooleanExpression.h"
@@ -21,7 +13,7 @@ namespace storm {
          * It is possibly for if statements to have one else body, but not
          * mandatory.
          */
-        class IfStatement : public CompoundStatement {
+        class IfStatement : public Statement {
         public:
             IfStatement() = default;
             /**
@@ -29,43 +21,42 @@ namespace storm {
              * @param condition The guard of the statement body.
              * @param body The if body.
              */
-            IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body);
+            IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& body);
             /**
              * Creates an if statement with an if and an else body.
              * @param condition The guard of the if body.
              * @param ifBody The if body.
              * @param elseBody The else body.
              */
-            IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& ifBody, std::shared_ptr<storm::pgcl::PgclProgram> const& elseBody);
+            IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& ifBody, std::shared_ptr<storm::pgcl::PgclBlock> const& elseBody);
             IfStatement(const IfStatement& orig) = default;
             virtual ~IfStatement() = default;
-            std::size_t getNumberOfOutgoingTransitions();
             void accept(class AbstractStatementVisitor&);
             /**
              * Returns the if body of the if statement.
              * @return The if body.
              */
-            std::shared_ptr<storm::pgcl::PgclProgram> getIfBody();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getIfBody() const;
             /**
              * Returns the else body of the if statement, if present. Otherwise
              * it throws an excpetion.
              * @return The else body.
              */
-            std::shared_ptr<storm::pgcl::PgclProgram> getElseBody();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getElseBody() const;
             /**
              * Returns true iff the if statement has an else body.
              */
-            bool hasElse();
+            bool hasElse() const;
             /**
              * Returns the guard of the if statement.
              * @return The condition.
              */
-            storm::pgcl::BooleanExpression& getCondition();
+            storm::pgcl::BooleanExpression const& getCondition() const;
         private:
             /// The if body is again a PGCL program.
-            std::shared_ptr<storm::pgcl::PgclProgram> ifBody;
+            std::shared_ptr<storm::pgcl::PgclBlock> ifBody;
             /// The else body is again a PGCL program.
-            std::shared_ptr<storm::pgcl::PgclProgram> elseBody;
+            std::shared_ptr<storm::pgcl::PgclBlock> elseBody;
             /// Memorizes if an else body was set. Set to false by default.
             bool hasElseBody = false;
             /// Saves the guard of the if statement.
@@ -74,5 +65,3 @@ namespace storm {
     }
 }
 
-#endif	/* IFSTATEMENT_H */
-

src/storage/pgcl/LoopStatement.cpp

@@ -1,34 +1,24 @@
-/* 
- * File:   LoopStatement.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:42
- */
 
 #include "src/storage/pgcl/LoopStatement.h"
 #include "src/storage/pgcl/AbstractStatementVisitor.h"
 
 namespace storm {
     namespace pgcl {
-        LoopStatement::LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body) :
+        LoopStatement::LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& body) :
             body(body), condition(condition) {
         }
 
-        std::shared_ptr<storm::pgcl::PgclProgram> LoopStatement::getBody() {
+        std::shared_ptr<storm::pgcl::PgclBlock> const& LoopStatement::getBody() const {
             return this->body;
         }
         
-        storm::pgcl::BooleanExpression& LoopStatement::getCondition() {
+        storm::pgcl::BooleanExpression const& LoopStatement::getCondition() const{
             return this->condition;
         }
 
         void LoopStatement::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
             visitor.visit(*this);
         }
-
-        std::size_t LoopStatement::getNumberOfOutgoingTransitions() {
-            return 1;
-        }
     }
 }
 

src/storage/pgcl/LoopStatement.h

@@ -18,7 +18,7 @@ namespace storm {
          * This class represents a guarded loop statement. The guard is saved as
          * a boolean expression. The body of the loop is again a PGCL program.
          */
-        class LoopStatement : public CompoundStatement {
+        class LoopStatement : public Statement {
         public:
             LoopStatement() = default;
             /**
@@ -27,24 +27,23 @@ namespace storm {
              * @param condition The guard of the loop.
              * @param body The body of the loop.
              */
-            LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body);
+            LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& body);
             LoopStatement(const LoopStatement& orig) = default;
             virtual ~LoopStatement() = default;
-            std::size_t getNumberOfOutgoingTransitions();
             void accept(class AbstractStatementVisitor&);
             /**
              * Returns the loop body program.
              * @return The loop body program.
              */
-            std::shared_ptr<storm::pgcl::PgclProgram> getBody();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getBody() const;
             /**
              * Returns the guard of the loop.
              * @return The boolean condition of the loop.
              */
-            storm::pgcl::BooleanExpression& getCondition();
+            storm::pgcl::BooleanExpression const& getCondition() const;
         private:
             /// Represents the loop body.
-            std::shared_ptr<storm::pgcl::PgclProgram> body;
+            std::shared_ptr<storm::pgcl::PgclBlock> body;
             /// Represents the loop guard.
             storm::pgcl::BooleanExpression condition;
         };

src/storage/pgcl/NondeterministicBranch.cpp

@@ -1,16 +1,9 @@
-/* 
- * File:   NondeterministicBranch.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:44
- */
-
 #include "src/storage/pgcl/NondeterministicBranch.h"
 #include "src/storage/pgcl/AbstractStatementVisitor.h"
 
 namespace storm {
     namespace pgcl {
-        NondeterministicBranch::NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right) {
+        NondeterministicBranch::NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclBlock> const& left, std::shared_ptr<storm::pgcl::PgclBlock> const& right) {
             leftBranch = left;
             rightBranch = right;
         }
@@ -19,7 +12,7 @@ namespace storm {
             visitor.visit(*this);
         }
 
-        bool NondeterministicBranch::isNondet() {
+        bool NondeterministicBranch::isNondet() const {
             return true;
         }
     }

src/storage/pgcl/NondeterministicBranch.h

@@ -25,11 +25,11 @@ namespace storm {
              * @param left The left (first) subprogram of the branch.
              * @param right The right (second) subprogram of the branch.
              */
-            NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right);
+            NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclBlock> const& left, std::shared_ptr<storm::pgcl::PgclBlock> const& right);
             NondeterministicBranch(const NondeterministicBranch& orig) = default;
             virtual ~NondeterministicBranch() = default;
             void accept(class AbstractStatementVisitor&);
-            bool isNondet();
+            bool isNondet() const;
         private:
         };
     }

src/storage/pgcl/ObserveStatement.cpp

@@ -1,10 +1,3 @@
-/* 
- * File:   ObserveStatement.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:42
- */
-
 #include "src/storage/pgcl/ObserveStatement.h"
 #include "src/storage/pgcl/AbstractStatementVisitor.h"
 
@@ -17,13 +10,10 @@ namespace storm {
             visitor.visit(*this);
         }
 
-        storm::pgcl::BooleanExpression& ObserveStatement::getCondition() {
+        storm::pgcl::BooleanExpression const& ObserveStatement::getCondition() const {
             return this->condition;
         }
 
-        std::size_t ObserveStatement::getNumberOfOutgoingTransitions() {
-            return 1;
-        }
     }
 }
 

src/storage/pgcl/ObserveStatement.h

@@ -1,12 +1,4 @@
-/* 
- * File:   ObserveStatement.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:42
- */
-
-#ifndef OBSERVESTATEMENT_H
-#define	OBSERVESTATEMENT_H
+#pragma once
 
 #include "src/storage/pgcl/SimpleStatement.h"
 #include "src/storage/pgcl/BooleanExpression.h"
@@ -18,7 +10,7 @@ namespace storm {
          * include a condition. If this condition doesn't hold, the program
          * stops at that point in its execution.
          */
-        class ObserveStatement : public SimpleStatement {
+        class ObserveStatement : public Statement {
         public:
             ObserveStatement() = default;
             /**
@@ -28,13 +20,12 @@ namespace storm {
              */
             ObserveStatement(storm::pgcl::BooleanExpression const& condition);
             ObserveStatement(const ObserveStatement& orig) = default;
-            std::size_t getNumberOfOutgoingTransitions();
             virtual ~ObserveStatement() = default;
             /**
              * Returns the condition of the observe statement.
              * @return The boolean expression of the observe statement.
              */
-            storm::pgcl::BooleanExpression& getCondition();
+            storm::pgcl::BooleanExpression const& getCondition() const;
             void accept(class AbstractStatementVisitor&);
         private:
             /// Represents the assigned condition.
@@ -42,6 +33,3 @@ namespace storm {
         };
     }
 }
-
-#endif	/* OBSERVESTATEMENT_H */
-

src/storage/pgcl/PgclProgram.cpp

@@ -1,106 +1,28 @@
-/* 
- * File:   PgclProgram.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:39
- */
-
 #include "PgclProgram.h"
 #include "StatementPrinterVisitor.h"
 #include <typeinfo>
 
 namespace storm {
     namespace pgcl {
-        PgclProgram::PgclProgram(vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop) :
-            sequenceOfStatements(statements),
-            locationToStatement(locationToStatement),
-            parameters(parameters),
-            expressions(expressions),
-            loop(hasLoop),
-            nondet(hasNondet),
-            observe(hasObserve),
-            top(isTop) {
-        }
-
-        PgclProgram::PgclProgram(vector const &statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop) :
-            sequenceOfStatements(statements),
-            expressions(expressions),
-            loop(hasLoop),
-            nondet(hasNondet),
-            observe(hasObserve),
-            top(isTop) {
-        }
-
-        iterator PgclProgram::begin() {
-            return this->sequenceOfStatements.begin();
+        PgclProgram::PgclProgram(vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve) :
+            PgclBlock(statements,
+                      expressions, hasLoop, hasNondet, hasObserve),
+            locationToStatement(locationToStatement)
+        {
         }
 
-        iterator PgclProgram::end() {
-            return this->sequenceOfStatements.end();
-        }
-
-        bool PgclProgram::empty() {
-            return this->sequenceOfStatements.empty();
-        }
-        
-        element PgclProgram::front() {
-            return this->sequenceOfStatements.front();
-        }
         
-        element PgclProgram::back() {
-            return this->sequenceOfStatements.back();
-        }
-
-        unsigned long PgclProgram::size() {
-            return this->sequenceOfStatements.size();
-        }
-        
-        element PgclProgram::at(size_type n) {
-            return this->sequenceOfStatements.at(n);
-        }
-        
-        iterator PgclProgram::insert(iterator position, const element& statement) {
-            return this->sequenceOfStatements.insert(position, statement);
-        }
-        
-        void PgclProgram::clear() {
-            this->sequenceOfStatements.clear();
-        }
-
-        std::shared_ptr<storm::expressions::ExpressionManager> PgclProgram::getExpressionManager() {
-            return this->expressions;
-        }
-
-        std::vector<storm::expressions::Variable> PgclProgram::getParameters() {
-            return this->parameters;
-        }
-
-        bool PgclProgram::hasParameters() const {
-            return !(this->parameters.empty());
-        }
-
-        bool PgclProgram::hasObserve() const {
-            return this->observe;
-        }
-
-        bool PgclProgram::hasNondet() const {
-            return this->nondet;
-        }
-
-        bool PgclProgram::hasLoop() const {
-            return this->loop;
-        }
-
         vector PgclProgram::getLocationToStatementVector() {
             return this->locationToStatement;
         }
-
-        iterator PgclProgram::find(element &statement) {
-            return std::find(this->sequenceOfStatements.begin(), this->sequenceOfStatements.end(), statement);
-        }
-
-        bool PgclProgram::isTop() const {
-            return this->top;
+        
+        std::vector<storm::expressions::Variable> PgclProgram::getVariables() const {
+            std::vector<storm::expressions::Variable> vars;
+            for(auto const& v : *(this->getExpressionManager())) {
+                vars.push_back(v.first);
+            }
+            
+            return vars;
         }
 
         std::ostream& operator<<(std::ostream& stream, PgclProgram& program) {

src/storage/pgcl/PgclProgram.h

@@ -1,14 +1,7 @@
-/* 
- * File:   PgclProgram.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:39
- */
-
-#ifndef PGCLPROGRAM_H
-#define	PGCLPROGRAM_H
+#pragma once
 
 #include <vector>
+#include "Block.h"
 #include "src/storage/pgcl/Statement.h"
 #include "src/storage/pgcl/StatementPrinterVisitor.h"
 #include "src/storage/expressions/ExpressionManager.h"
@@ -16,11 +9,6 @@
 namespace storm {
     namespace pgcl {
         
-        typedef std::shared_ptr<storm::pgcl::Statement> element;
-        typedef std::vector<element> vector;
-        typedef std::vector<element>::iterator iterator;
-        typedef std::vector<element>::const_iterator const_iterator;
-        typedef std::vector<element>::size_type size_type;
 
         /**
          * This class represents a complete and functional PGCL program. It
@@ -29,7 +17,7 @@ namespace storm {
          * wraps a std::vector of program statements and is intended to be used
          * as such.
          */
-        class PgclProgram {
+        class PgclProgram : public PgclBlock {
         public:
             PgclProgram() = default;
             /**
@@ -48,114 +36,27 @@ namespace storm {
              * statement.
              * @param hasParam Whether the program is parameterized.
              */
-            PgclProgram(vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop);
-            /**
-             * Does the same as the beforementioned constructor, but sets the
-             * location to statement vector to the empty vector. This
-             * constructor should be used for sub-programs, for which the
-             * location to statement relation doesn't make much sense.
-             * @param statements The sequence of statements representing the
-             * program.
-             * @param expressions The manager responsible for the expressions
-             * and variables of the program.
-             * @param hasLoop Whether the program contains a loop
-             * @param hasNondet Whether the program contains a nondeterministic
-             * statement.
-             * @param hasParam Whether the program is parameterized.
-             */
-            PgclProgram(vector const& statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop);
+            PgclProgram(vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve);
+            
             PgclProgram(const PgclProgram & orig) = default;
-            PgclProgram & operator=(PgclProgram const& other) = default;
-            iterator begin();
-            iterator end();
-            element front();
-            element back();
-            unsigned long size();
-            element at(size_type n);
-            iterator insert(iterator position, const element& statement);
-            iterator find(element& statement);
-            void clear();
-            bool empty();
+            
             /**
              * Returns a vector that has the statement with location number i at
              * its i-th position. This allows for O(1)-access of statements if
              * only the location number is given.
              */
             vector getLocationToStatementVector();
-            /**
-             * Returns the list of parameters of the PGCL program.
-             */
-            std::vector<storm::expressions::Variable> getParameters();
-            /**
-             * Returns the expression manager of the PGCL program, which is
-             * responsible for managing all expressions and variables of the
-             * the program and all its subprograms.
-             * @return The expression manager of the program.
-             */
-            std::shared_ptr<storm::expressions::ExpressionManager> getExpressionManager();
-            /**
-             * Returns true if the program contains a loop statement.
-             * @return True if the program has a loop.
-             */
-            bool hasLoop() const;
-            /**
-             * Returns true if the program contains a nondeterministic
-             * statement.
-             * @return True if the program has a nondeterministic statement.
-             */
-            bool hasNondet() const;
-            /**
-             * Returns true if the program contains an observe statement.
-             * @return True if the program has an observe statement.
-             */
-            bool hasObserve() const;
-            /**
-             * Returns true if the program is parameterized.
-             * @return True if the program has at least one parameter.
-             */
-            bool hasParameters() const;
-            /**
-             * Returns whether the program is no subprogram.
-             * @return True if the program is no subprogram of another
-             * program.
-             */
-            bool isTop() const;
+            
+            std::vector<storm::expressions::Variable> getVariables() const;
+            
         private:
-            /**
-             * We are basically wrapping a std::vector which represents the
-             * ordered single statements of the program.
-             */
-            vector sequenceOfStatements;
             /**
              * Contains the statement with location i at its i-th position.
              * Imagine this as the "unrolled" sequence of statements, so the
              * recursion is resolved here.
              */
             vector locationToStatement;
-            /**
-             * Stores the parameters a.k.a. free variables of the PGCL program.
-             */
-            std::vector<storm::expressions::Variable> parameters;
-            /**
-             * Handles the expressions and variables for the whole program.
-             * The expressions of every subprogram are also handled by this
-             * manager. We are using a shared pointer since all subprograms
-             * are referring to that expression manager, too.
-             */
-            std::shared_ptr<storm::expressions::ExpressionManager> expressions;
-            /**
-             * Boolean variables to save some properties of the PGCL program.
-             * They are later on used by the model builder to possibly
-             * construct simpler models (e.g. if no loops, params and nondets
-             * are used, a DTMC suffices).
-             * The values are set to true if the PGCL parser hits a loop resp.
-             * nondet resp. observe resp. parameter statement.
-             */
-            bool loop    = false;
-            bool nondet  = false;
-            bool observe = false;
-            bool top     = false;
-        };
+                    };
         /**
          * Prints every statement of the program along with their location
          * numbers.
@@ -166,5 +67,4 @@ namespace storm {
     }
 }
 
-#endif	/* PGCLPROGRAM_H */
 

src/storage/pgcl/ProbabilisticBranch.cpp

@@ -1,22 +1,15 @@
-/* 
- * File:   ProbabilisticBranch.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:43
- */
-
 #include "src/storage/pgcl/ProbabilisticBranch.h"
 #include "src/storage/pgcl/AbstractStatementVisitor.h"
 
 namespace storm {
     namespace pgcl {
-        ProbabilisticBranch::ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right) :
+        ProbabilisticBranch::ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclBlock> const& left, std::shared_ptr<storm::pgcl::PgclBlock> const& right) :
         probability(probability) {
             rightBranch = right;
             leftBranch = left;
         }
         
-        storm::expressions::Expression& ProbabilisticBranch::getProbability() {
+        storm::expressions::Expression const& ProbabilisticBranch::getProbability() const {
             return this->probability;
         }
 

src/storage/pgcl/ProbabilisticBranch.h

@@ -1,12 +1,4 @@
-/* 
- * File:   ProbabilisticBranch.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:43
- */
-
-#ifndef PROBABILISTICBRANCH_H
-#define	PROBABILISTICBRANCH_H
+#pragma once
 
 #include "src/storage/pgcl/BranchStatement.h"
 
@@ -31,14 +23,14 @@ namespace storm {
              * @param left The left (first) subprogram of the branch.
              * @param right The right (second) subprogram of the branch.
              */
-            ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right);
+            ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclBlock> const& left, std::shared_ptr<storm::pgcl::PgclBlock> const& right);
             ProbabilisticBranch(const ProbabilisticBranch& orig) = default;
             virtual ~ProbabilisticBranch() = default;
             /**
              * Returns the expression representing the probability.
              * @return The expression representing the probability.
              */
-            storm::expressions::Expression& getProbability();
+            storm::expressions::Expression const& getProbability() const;
             void accept(class AbstractStatementVisitor&);
         private:
             /// The expression represents the probability of the branch.
@@ -46,6 +38,3 @@ namespace storm {
         };
     }
 }
-
-#endif	/* PROBABILISTICBRANCH_H */
-

src/storage/pgcl/Statement.cpp

@@ -1,11 +1,5 @@
-/* 
- * File:   Statement.cpp
- * Author: Lukas Westhofen
- * 
- * Created on 11. April 2015, 17:41
- */
-
 #include "src/storage/pgcl/Statement.h"
+#include "Block.h"
 
 namespace storm {
     namespace pgcl {
@@ -17,11 +11,11 @@ namespace storm {
             this->lineNumber = lineNumber;
         }
 
-        std::size_t Statement::getLineNumber() {
+        std::size_t Statement::getLineNumber() const {
             return this->lineNumber;
         }
 
-        std::size_t Statement::getLocationNumber() {
+        std::size_t Statement::getLocationNumber() const {
             return this->locationNumber;
         }
 
@@ -29,7 +23,7 @@ namespace storm {
             this->locationNumber = locationNumber;
         }
 
-        bool Statement::isLast() {
+        bool Statement::isLast() const {
             return this->last;
         }
 
@@ -37,27 +31,20 @@ namespace storm {
             this->last = isLast;
         }
 
-        bool Statement::isNondet() {
+        bool Statement::isNondet() const {
             return false;
         }
 
-        void Statement::setParentProgram(std::shared_ptr<storm::pgcl::PgclProgram> parentProgram) {
-                this->parentProgram = parentProgram;
-        }
-
-        boost::optional<std::shared_ptr<storm::pgcl::PgclProgram> > Statement::getParentProgram() {
-            return this->parentProgram;
+        void Statement::setParentBlock(PgclBlock* b) {
+                this->parentBlock = b;
         }
 
-        void Statement::setParentStatement(std::shared_ptr<storm::pgcl::Statement> parentStatement) {
-            this->parentStatement = parentStatement;
+        PgclBlock* Statement::getParentBlock() {
+            return this->parentBlock;
         }
 
-        boost::optional<std::shared_ptr<storm::pgcl::Statement> > Statement::getParentStatement() {
-            return this->parentStatement;
-        }
 
-        std::size_t Statement::getNumberOfOutgoingTransitions() {
+        std::size_t Statement::getNumberOfOutgoingTransitions() const {
             return 1;
         }
     }

src/storage/pgcl/Statement.h

@@ -1,12 +1,4 @@
-/* 
- * File:   Statement.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:41
- */
-
-#ifndef STATEMENT_H
-#define	STATEMENT_H
+#pragma once
 
 #include <cstdint>
 #include <memory>
@@ -14,7 +6,7 @@
 
 namespace storm {
     namespace pgcl {
-        class PgclProgram;
+        class PgclBlock;
         /**
          * A PGCL program consists of various statements. Statements can again
          * save lists of statements as their children. To make life easier, the
@@ -39,7 +31,7 @@ namespace storm {
              * was parsed from.
              * @return The line number of the statement.
              */
-            std::size_t getLineNumber();
+            std::size_t getLineNumber() const;
             /**
              * Sets the line number during the parsing process.
              * @param lineNumber The location number of the statement.
@@ -49,7 +41,7 @@ namespace storm {
              * Returns the unique location number of the statement.
              * @return The line number of the statement.
              */
-            std::size_t getLocationNumber();
+            std::size_t getLocationNumber() const;
             /**
              * Sets the unique location number of the statement.
              * @param lineNumber The location number of the statement.
@@ -60,7 +52,7 @@ namespace storm {
              * program.
              * @return true Whether the statement is the last statement.
              */
-            bool isLast();
+            bool isLast() const;
             /**
              * Sets the information whether the statement is the last of its
              * direct parent program.
@@ -70,37 +62,26 @@ namespace storm {
             /**
              * Returns wether the statements represents nondeterminism.
              */
-            virtual bool isNondet();
+            virtual bool isNondet() const;
             /**
              * Returns the number of transitions this statement will produce.
              */
-            virtual std::size_t getNumberOfOutgoingTransitions();
+            virtual std::size_t getNumberOfOutgoingTransitions() const;
             virtual void accept(class AbstractStatementVisitor&) = 0;
             /**
              * Sets the parent program of the statement.
              * @param parentProgram The parent program of the statement.
              */
-            void setParentProgram(std::shared_ptr<storm::pgcl::PgclProgram> parentProgram);
+            void setParentBlock(PgclBlock* block);
             /**
              * Returns the parent program of the statement.
              * @return The parent program of the statement.
              */
-            boost::optional<std::shared_ptr<storm::pgcl::PgclProgram> > getParentProgram();
-            /**
-             * Sets the parent statement of the statement.
-             * @param parentProgram The parent statement of the statement.
-             */
-            void setParentStatement(std::shared_ptr<storm::pgcl::Statement> parentStatement);
-            /**
-             * Returns the parent statement of the statement.
-             * @return The parent statement of the statement.
-             */
-            boost::optional<std::shared_ptr<storm::pgcl::Statement> > getParentStatement();
+            PgclBlock* getParentBlock();
+            
         protected:
             /// The parent program of the statement.
-            boost::optional<std::shared_ptr<storm::pgcl::PgclProgram> > parentProgram;
-            /// The parent program of the statement.
-            boost::optional<std::shared_ptr<storm::pgcl::Statement> > parentStatement;
+            PgclBlock* parentBlock;
             /// Represents the line number of the statement.
             std::size_t lineNumber = 0;
             /// Represents the unique statement location.
@@ -110,5 +91,4 @@ namespace storm {
         };
     }
 }
-#endif	/* STATEMENT_H */
 

src/storage/pgcl/StatementPrinterVisitor.cpp

@@ -1,7 +1,3 @@
-//
-// Created by Lukas Westhofen on 21.04.15.
-//
-
 #include "src/storage/pgcl/StatementPrinterVisitor.h"
 
 #include "src/storage/pgcl/AssignmentStatement.h"
@@ -16,7 +12,7 @@ namespace storm {
         StatementPrinterVisitor::StatementPrinterVisitor(std::ostream &stream) : stream(stream) {
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::AssignmentStatement& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::AssignmentStatement const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             if(statement.getExpression().which() == 0) {
                 storm::expressions::Expression const& expression = boost::get<storm::expressions::Expression>(statement.getExpression());
@@ -27,14 +23,14 @@ namespace storm {
             }
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::ObserveStatement& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::ObserveStatement const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             this->stream << "observe(" << statement.getCondition().getBooleanExpression() << ");" << std::endl;
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::IfStatement& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::IfStatement const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
-            this->stream << "if(" << statement.getCondition().getBooleanExpression() << ") {" << std::endl;
+            this->stream << "if (" << statement.getCondition().getBooleanExpression() << ") {" << std::endl;
             int i = 1;
             for(iterator it = (*(statement.getIfBody())).begin(); it != (*(statement.getIfBody())).end(); ++it) {
                 (*(*it)).accept(*this);
@@ -51,9 +47,9 @@ namespace storm {
             }
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::LoopStatement& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::LoopStatement const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
-            this->stream << "while(" << statement.getCondition().getBooleanExpression() << ") {" << std::endl;
+            this->stream << "while (" << statement.getCondition().getBooleanExpression() << ") {" << std::endl;
             int i = 1;
             for(iterator it = (*(statement.getBody())).begin(); it != (*(statement.getBody())).end(); ++it) {
                 (*(*it)).accept(*this);
@@ -62,7 +58,7 @@ namespace storm {
             this->stream << "}" << std::endl;
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::NondeterministicBranch& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::NondeterministicBranch const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             this->stream << "{" << std::endl;
             int i = 1;
@@ -78,7 +74,7 @@ namespace storm {
             this->stream << "}" << std::endl;
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::ProbabilisticBranch& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::ProbabilisticBranch const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             this->stream << "{" << std::endl;
             int i = 1;

src/storage/pgcl/StatementPrinterVisitor.h

@@ -1,9 +1,4 @@
-//
-// Created by Lukas Westhofen on 21.04.15.
-//
-
-#ifndef STORM_STATEMENTVISITOR_H
-#define STORM_STATEMENTVISITOR_H
+#pragma once
 
 #include <iostream>
 #include <boost/variant/get.hpp>
@@ -24,16 +19,14 @@ namespace storm {
              * @param stream The stream to print to.
              */
             StatementPrinterVisitor(std::ostream& stream);
-            void visit(class AssignmentStatement&);
-            void visit(class ObserveStatement&);
-            void visit(class IfStatement&);
-            void visit(class LoopStatement&);
-            void visit(class NondeterministicBranch&);
-            void visit(class ProbabilisticBranch&);
+            void visit(AssignmentStatement const&);
+            void visit(ObserveStatement const&);
+            void visit(IfStatement const&);
+            void visit(LoopStatement const&);
+            void visit(NondeterministicBranch const&);
+            void visit(ProbabilisticBranch const&);
         private:
             std::ostream& stream;
         };
     }
 }
-
-#endif //STORM_STATEMENTVISITOR_H

src/storage/pgcl/UniformExpression.cpp

@@ -1,7 +1,3 @@
-//
-// Created by foxnbk on 16.03.16.
-//
-
 #include "UniformExpression.h"
 
 namespace storm {
@@ -19,5 +15,3 @@ namespace storm {
         }
     }
 }
-
-#include "UniformExpression.h"

src/storage/pgcl/UniformExpression.h

@@ -1,9 +1,4 @@
-//
-// Created by Lukas Westhofen on 16.03.16.
-//
-
-#ifndef STORM_UNIFORMEXPRESSION_H
-#define STORM_UNIFORMEXPRESSION_H
+#pragma once
 
 #include <stdint.h>
 
@@ -38,6 +33,4 @@ namespace storm {
             int_fast64_t end = 0;
         };
     }
-}
-
-#endif //STORM_UNIFORMEXPRESSION_H
+}

src/storage/ppg/ProgramAction.cpp

@@ -0,0 +1,19 @@
+#include "ProgramAction.h"
+#include "ProgramGraph.h"
+
+namespace storm {
+    namespace ppg {
+        
+        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

@@ -0,0 +1,163 @@
+#pragma once
+#include "defines.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+    namespace ppg {
+        
+        class ProgramAction {
+        public:
+            ProgramAction(ProgramGraph* graph, ProgramActionIdentifier id) : graph(graph), actId(id) {
+                
+            }
+            
+            ProgramActionIdentifier id() const {
+                return actId;
+            }
+            
+            ProgramGraph const& getProgramGraph() const {
+                return *graph;
+            }
+            
+            virtual bool isProbabilistic() const = 0;
+        private:
+            ProgramGraph* graph;
+            ProgramActionIdentifier actId;
+        };
+        
+        
+        struct ValueProbabilityPair {
+            ValueProbabilityPair(int64_t value, storm::expressions::Expression const& probability) : value(value), probability(probability) {
+                // Intentionally left empty.
+            }
+            
+            int64_t value;
+            storm::expressions::Expression probability;
+        };
+        
+        class ProbabilisticProgramAction : public ProgramAction {
+        public:
+            // TODO in the long run, we probably need own iterators for this.
+            using iterator = std::vector<ValueProbabilityPair>::iterator;
+            using const_iterator = std::vector<ValueProbabilityPair>::const_iterator;
+            
+            
+            
+            /**
+             * Constructs a uniform assignment operation to a variable;
+             * Action assigns a variable according to a uniform distribution [from, 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();
+            }
+            
+            iterator end() {
+                return values.end();
+            }
+            
+            const_iterator begin() const {
+                return values.begin();
+            }
+            
+            const_iterator end() const {
+                return values.end();
+            }
+            
+        private:
+            // TODO not the smartest representation (but at least it is internal!)
+            std::vector<ValueProbabilityPair> values;
+            ProgramVariableIdentifier var;
+            
+        };
+        
+        
+        struct AssignmentGroup {
+            using iterator = std::unordered_map<uint64_t, storm::expressions::Expression>::iterator;
+            using const_iterator = std::unordered_map<uint64_t, storm::expressions::Expression>::const_iterator;
+            
+            storm::expressions::Expression& operator[](uint64_t varIndex) {
+                return map[varIndex];
+            }
+            
+            bool hasVariable(uint64_t varIndex) const {
+                return map.count(varIndex) > 0;
+            }
+            
+            iterator begin() {
+                return map.begin();
+            }
+            
+            iterator end() {
+                return map.end();
+            }
+            
+            const_iterator begin() const {
+                return map.begin();
+            }
+            
+            const_iterator end() const {
+                return map.end();
+            }
+            
+        private:
+            std::unordered_map<ProgramVariableIdentifier, storm::expressions::Expression> map;
+        };
+        
+        class DeterministicProgramAction : public ProgramAction {
+            
+        public:
+            using iterator = std::vector<AssignmentGroup>::iterator;
+            using const_iterator = std::vector<AssignmentGroup>::const_iterator;
+            
+            DeterministicProgramAction(ProgramGraph* graph, ProgramActionIdentifier actId) : ProgramAction(graph, actId) {
+                
+            }
+            
+            void addAssignment(ProgramVariableIdentifier varIndex, storm::expressions::Expression const& expr, uint64_t level=0) {
+                if(assignments.size() <= level) {
+                    assignments.resize(level+1);
+                }
+                assert(!assignments[level].hasVariable(varIndex));
+                assignments[level][varIndex] = expr;
+            }
+            
+            size_t nrLevels() const {
+                return assignments.size();
+            }
+            
+            iterator begin() {
+                return assignments.begin();
+            }
+            
+            iterator end() {
+                return assignments.end();
+            }
+            
+            const_iterator begin() const {
+                return assignments.begin();
+            }
+            
+            const_iterator end() const {
+                return assignments.end();
+            }
+            
+            bool isProbabilistic() const override{
+                return false;
+            }
+            
+        protected:
+            std::vector<AssignmentGroup> assignments;
+        };
+        
+    }
+}

src/storage/ppg/ProgramEdge.cpp

@@ -0,0 +1,19 @@
+#include "ProgramEdge.h"
+#include "ProgramGraph.h"
+
+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

@@ -0,0 +1,51 @@
+#pragma once
+#include "defines.h"
+
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace ppg {
+        class ProgramAction;
+        
+        class ProgramEdge {
+        public:
+            ProgramEdge(ProgramEdgeGroup* group, ProgramEdgeIdentifier id, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId)
+            : group(group), edgeId(id), target(targetId), action(action), condition(condition)
+            {
+                // Intentionally left empty.
+            }
+            
+            ProgramLocationIdentifier getSourceId() const;
+            ProgramLocationIdentifier getTargetId() const {
+                return target;
+            }
+            
+            storm::expressions::Expression const& getCondition() const {
+                return condition;
+            }
+            
+            bool hasNoAction() const; 
+            ProgramAction const& getAction() const;
+            ProgramActionIdentifier getActionId() const {
+                return action;
+            }
+            
+            virtual ~ProgramEdge() {
+                // Intentionally left empty.
+            }
+            
+        private:
+            /// Pointer to the group; not owned
+            ProgramEdgeGroup* group;
+            /// Edge identifier
+            ProgramEdgeIdentifier edgeId;
+            /// Target location identifier
+            ProgramLocationIdentifier target;
+            /// Action identifier
+            ProgramActionIdentifier action;
+            /// Condition
+            storm::expressions::Expression condition;
+            
+        };
+    }
+}

src/storage/ppg/ProgramEdgeGroup.cpp

@@ -0,0 +1,14 @@
+#include "ProgramEdgeGroup.h"
+#include "ProgramGraph.h"
+
+namespace storm {
+    namespace ppg {
+        ProgramEdge* ProgramEdgeGroup::addEdge(ProgramActionIdentifier action, ProgramLocationIdentifier target) {
+            return graph->addProgramEdge(*this, action, target);
+        }
+        ProgramEdge* ProgramEdgeGroup::addEdge(ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier target) {
+            return graph->addProgramEdge(*this, action, condition, target);
+        }
+
+    }
+}

src/storage/ppg/ProgramEdgeGroup.h

@@ -0,0 +1,78 @@
+#pragma once
+
+#include "defines.h"
+#include "ProgramEdge.h"
+
+namespace storm {
+    namespace ppg {
+        
+        class ProgramEdgeGroup {
+        public:
+            using const_iterator = std::vector<ProgramEdge*>::const_iterator;
+            
+            ProgramEdgeGroup(ProgramGraph* graph, ProgramEdgeGroupIdentifier id, ProgramLocationIdentifier sourceId, storm::expressions::Expression const& probability)
+            : graph(graph), groupId(id), sourceId(sourceId), probability(probability)
+            {
+                // Intentionally left empty.
+            }
+            
+            virtual ~ProgramEdgeGroup() {
+                for( auto const& e : edges) {
+                    delete e;
+                }
+            }
+            
+            ProgramEdge* addEdge(ProgramActionIdentifier action, ProgramLocationIdentifier target);
+            ProgramEdge* addEdge(ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier target);
+            
+            /**
+             * Constructs an outgoing edge in this edge group.
+             */
+            ProgramEdge* emplaceEdge(ProgramEdgeIdentifier id, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier target) {
+                edges.emplace_back(new ProgramEdge(this, id, action, condition, target));
+                return edges.back();
+            }
+            
+            const_iterator begin() const {
+                return edges.begin();
+            }
+            
+            const_iterator end() const {
+                return edges.end();
+            }
+            
+            size_t nrEdges() const {
+                return edges.size();
+            }
+            
+            storm::expressions::Expression const& getProbability() const {
+                return probability;
+            }
+            
+            ProgramGraph const& getGraph() const {
+                return *graph;
+            }
+            
+            ProgramLocationIdentifier getSourceId() const {
+                return sourceId;
+            }
+            
+            ProgramEdgeGroupIdentifier getId() const {
+                return groupId;
+            }
+            
+        private:
+            /// Pointer to the graph; not owned.
+            ProgramGraph* graph;
+            /// Own id (persistent over copy)
+            ProgramEdgeGroupIdentifier groupId;
+            /// Id of source location
+            ProgramLocationIdentifier sourceId;
+            /// Probability for this group
+            storm::expressions::Expression probability;
+            /// Outgoing edges
+            std::vector<ProgramEdge*> edges;
+            
+        };
+    }
+}

src/storage/ppg/ProgramGraph.cpp

@@ -0,0 +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

@@ -0,0 +1,236 @@
+#pragma once
+
+#include "defines.h"
+#include "src/storage/expressions/Expression.h"
+#include "src/storage/expressions/Variable.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+#include "ProgramLocation.h"
+#include "ProgramEdge.h"
+#include "ProgramEdgeGroup.h"
+#include "ProgramAction.h"
+
+namespace storm {
+    namespace ppg {
+        /**
+         *  Program graph as based on Principles of Model Checking, Def 2.13
+         *  Action effects are part of the action.
+         */
+        class ProgramGraph {
+        public:
+            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() {
+                for(auto const& v : variables) {
+                    this->variables.emplace(v.getIndex(), v);
+                }
+                // No Action:
+                deterministicActions.emplace(noActionId, DeterministicProgramAction(this, noActionId));
+            }
+            
+            ProgramGraph(ProgramGraph const&) = delete;
+            
+            virtual ~ProgramGraph() {
+            }
+            
+            DeterministicProgramAction* addDeterministicAction() {
+                ProgramActionIdentifier newId = freeActionIndex();
+                assert(!hasAction(newId));
+                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));
+                return &(locations.emplace(newId, ProgramLocation(this, newId, isInitial)).first->second);
+            }
+            
+            
+            ProgramEdgeGroup* addProgramEdgeGroup(ProgramLocation& source, storm::expressions::Expression const& probability) {
+                ProgramEdgeGroupIdentifier newId = freeEdgeGroupIndex();
+                return source.emplaceEdgeGroup(newId, probability);
+            }
+            
+            ProgramEdgeGroup* addProgramEdgeGroup(ProgramLocationIdentifier sourceId, storm::expressions::Expression const& probability) {
+                assert(hasLocation(sourceId));
+                return addProgramEdgeGroup(getLocation(sourceId), probability);
+            }
+        
+            ProgramEdge* addProgramEdge(ProgramEdgeGroup& group, ProgramActionIdentifier action, ProgramLocationIdentifier targetId) {
+                return addProgramEdge(group, action, expManager->boolean(true), targetId);
+            }
+            
+            ProgramEdge* addProgramEdge(ProgramEdgeGroup& group, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId) {
+                ProgramEdgeIdentifier newId = freeEdgeIndex();
+                return group.emplaceEdge(newId, action, condition, targetId);
+            }
+            
+            std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramLocation& source, ProgramActionIdentifier action, ProgramLocationIdentifier targetId) {
+                return addProgramEdgeToAllGroups(source, action, expManager->boolean(true), targetId);
+            }
+            
+            std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramLocation& source, ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId) {
+                assert(hasLocation(targetId));
+                assert(hasAction(action));
+                
+                if(source.nrOutgoingEdgeGroups() == 0) {
+                    addProgramEdgeGroup(source, expManager->rational(1));
+                }
+                
+                std::vector<ProgramEdge*> res;
+                for(EdgeGroupIterator eg = source.getOutgoingEdgeGroupBegin(); eg != source.getOutgoingEdgeGroupEnd(); ++eg) {
+                    ProgramEdgeIdentifier newId = freeEdgeIndex();
+                    res.push_back((*eg)->emplaceEdge(newId, action, condition, targetId));
+                    
+                }
+                
+                return res;
+                
+            }
+            
+            
+            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);
+            }
+
+            
+            ProgramVariableIdentifier getVariableId(std::string const& varName) const {
+                // TODO consider holding a map for this.
+                for(auto const& v : variables) {
+                    if(v.second.getName() == varName) {
+                        return v.first;
+                    }
+                }
+                assert(false);
+            }
+            
+            std::string const& getVariableName(ProgramVariableIdentifier id) const {
+                return variables.at(id).getName();
+            }
+            
+            bool hasVariable(std::string const& varName) const {
+                for(auto const& v : variables) {
+                    if(v.second.getName() == varName) {
+                        return true;
+                    }
+                }
+                return false;
+            }
+            
+            bool hasLocation(ProgramLocationIdentifier id) const {
+                return locations.count(id) == 1;
+            }
+            
+            bool hasAction(ProgramActionIdentifier id) const {
+                return deterministicActions.count(id) == 1 || probabilisticActions.count(id);
+            }
+            
+            ProgramAction const& getAction(ProgramActionIdentifier id) const {
+                assert(hasAction(id));
+                if(isDeterministicAction(id)) {
+                    return deterministicActions.at(id);
+                } else {
+                    return probabilisticActions.at(id);
+                }
+            }
+            
+            bool isDeterministicAction(ProgramActionIdentifier id) const {
+                assert(hasAction(id));
+                return probabilisticActions.count(id) == 0;
+            }
+            
+            size_t nrLocations() const {
+                return locations.size();
+            }
+            
+            size_t nrVariables() const {
+                return variables.size();
+            }
+            
+            size_t nrActions() const {
+                return variables.size();
+            }
+            
+            
+            ConstLocationIterator locationBegin() const {
+                return locations.begin();
+            }
+            
+            ConstLocationIterator locationEnd() const {
+                return locations.end();
+            }
+            
+            std::unordered_map<ProgramVariableIdentifier, storm::expressions::Variable> const& getVariables() const {
+                return variables;
+            }
+            
+            std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const {
+                return expManager;
+            }
+            
+            void checkValid() {
+                
+            }
+            
+            void printInfo(std::ostream& os) const {
+                os << "Number of variables: " << nrVariables() << std::endl;
+                os << "Number of locations: " << nrLocations() << std::endl;
+                os << "Number of actions: " << nrActions() << std::endl;
+            }
+            
+            void printDot(std::ostream& os) const;
+        protected:
+            
+            ProgramLocation& getLocation(ProgramLocationIdentifier id) {
+                return locations.at(id);
+            }
+            
+            /**
+             * Gets a free location index (based on whatever scheme we are using).
+             */
+            ProgramLocationIdentifier freeLocationIndex() {
+                return newLocationId++;
+            }
+            
+            ProgramActionIdentifier freeActionIndex() {
+                return newActionId++;
+            }
+            
+            ProgramEdgeIdentifier freeEdgeIndex() {
+                return newEdgeId++;
+            }
+            
+            ProgramEdgeGroupIdentifier freeEdgeGroupIndex() {
+                return newEdgeGroupId++;
+            }
+            
+            std::unordered_map<ProgramActionIdentifier, DeterministicProgramAction> deterministicActions;
+            std::unordered_map<ProgramActionIdentifier, ProbabilisticProgramAction> probabilisticActions;
+            std::unordered_map<ProgramLocationIdentifier, ProgramLocation> locations;
+            storm::expressions::Expression initialValueRestriction;
+            std::unordered_map<ProgramVariableIdentifier, storm::expressions::Variable> variables;
+            
+            std::shared_ptr<storm::expressions::ExpressionManager> expManager;
+        private:
+            // Helper for IDs, may be changed later.
+            ProgramEdgeGroupIdentifier newEdgeGroupId = 0;
+            ProgramLocationIdentifier newLocationId = 0;
+            ProgramEdgeIdentifier newEdgeId = 0;
+            ProgramActionIdentifier newActionId = 1;
+            ProgramActionIdentifier noActionId = 0;
+            
+        };
+    }
+}

src/storage/ppg/ProgramLocation.cpp

@@ -0,0 +1,21 @@
+
+#include "ProgramLocation.h"
+#include "ProgramGraph.h"
+
+namespace storm {
+    namespace ppg {
+        
+        std::vector<ProgramEdge*> ProgramLocation::addProgramEdgeToAllGroups(ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId) {
+            return graph->addProgramEdgeToAllGroups(*this, action, condition, targetId);
+        }
+        
+        std::vector<ProgramEdge*> ProgramLocation::addProgramEdgeToAllGroups(ProgramActionIdentifier action, ProgramLocationIdentifier targetId) {
+            return graph->addProgramEdgeToAllGroups(*this, action, targetId);
+        }
+        
+        ProgramEdgeGroup* ProgramLocation::addProgramEdgeGroup(storm::expressions::Expression const& probability) {
+            return graph->addProgramEdgeGroup(*this, probability);
+        }
+        
+    }
+}

src/storage/ppg/ProgramLocation.h

@@ -0,0 +1,80 @@
+#pragma once
+
+#include "defines.h"
+#include "ProgramEdgeGroup.h"
+
+namespace storm {
+    namespace ppg {
+        class ProgramLocation {
+        public:
+            using EdgeGroupIterator = std::vector<ProgramEdgeGroup*>::iterator;
+            using const_iterator = std::vector<ProgramEdgeGroup*>::const_iterator;
+            
+            ProgramLocation(ProgramGraph* graph, ProgramLocationIdentifier id, bool initial) : graph(graph), locId(id), init(initial){
+                // Intentionally left empty
+            }
+            
+            virtual ~ProgramLocation() {
+                for( auto const& e : edgeGroups) {
+                    delete e;
+                }
+            }
+            
+            
+            std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramActionIdentifier action, storm::expressions::Expression const& condition, ProgramLocationIdentifier targetId);
+            std::vector<ProgramEdge*> addProgramEdgeToAllGroups(ProgramActionIdentifier action, ProgramLocationIdentifier targetId);
+            ProgramEdgeGroup* addProgramEdgeGroup(storm::expressions::Expression const& probability);
+            
+            
+            ProgramEdgeGroup* emplaceEdgeGroup(ProgramEdgeGroupIdentifier id, storm::expressions::Expression const& probability) {
+                edgeGroups.emplace_back(new ProgramEdgeGroup(graph, id, locId, probability));
+                return edgeGroups.back();
+            }
+            
+            bool isInitial() const {
+                return init;
+            }
+            
+            size_t nrOutgoingEdgeGroups() const {
+                return edgeGroups.size();
+            }
+            
+            bool hasNonDeterminism() const {
+                for(auto const& eg : edgeGroups) {
+                    if(eg->nrEdges() > 1) return true;
+                }
+                return false;
+            }
+            
+            const_iterator begin() const {
+                return edgeGroups.begin();
+            }
+            
+            const_iterator end() const {
+                return edgeGroups.end();
+            }
+            
+            // Todo rename?
+            EdgeGroupIterator getOutgoingEdgeGroupBegin() {
+                return edgeGroups.begin();
+            }
+            
+            // Todo rename?
+            EdgeGroupIterator getOutgoingEdgeGroupEnd() {
+                return edgeGroups.end();
+            }
+            
+            ProgramLocationIdentifier id() const {
+                return locId;
+            }
+            
+        private:
+            ProgramGraph* graph;
+            ProgramLocationIdentifier locId;
+            bool init;
+            std::vector<ProgramEdgeGroup*> edgeGroups;
+            
+            
+        };
+    }
+}

src/storage/ppg/defines.h

@@ -0,0 +1,16 @@
+#pragma once
+#include <cassert>
+#include <vector>
+namespace storm {
+    namespace ppg {
+        class ProgramGraph;
+        class ProgramEdgeGroup;
+        class ProgramLocation;
+        using ProgramLocationIdentifier = uint64_t;
+        using ProgramActionIdentifier = uint64_t;
+        using ProgramEdgeGroupIdentifier =  uint64_t;
+        using ProgramEdgeIdentifier = uint64_t;
+        using ProgramVariableIdentifier = uint64_t;
+        
+    }
+}

src/storage/prism/CompositionToJaniVisitor.cpp

@@ -2,7 +2,7 @@
 #include "src/storage/prism/Compositions.h"
 
 #include "src/storage/jani/Compositions.h"
-#include "src/storage/jani/CompositionActionInformationVisitor.h"
+#include "src/storage/jani/CompositionInformationVisitor.h"
 #include "src/storage/jani/Model.h"
 
 namespace storm {
@@ -30,7 +30,7 @@ namespace storm {
         boost::any CompositionToJaniVisitor::visit(HidingComposition const& composition, boost::any const& data) {
             std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
             for (auto const& action : composition.getActionsToHide()) {
-                synchronizationVectors.push_back(storm::jani::SynchronizationVector({action}, storm::jani::Model::getSilentActionName()));
+                synchronizationVectors.push_back(storm::jani::SynchronizationVector({action}, storm::jani::Model::SILENT_ACTION_NAME));
             }
             std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::ParallelComposition>(boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getSubcomposition().accept(*this, data)), synchronizationVectors);
             return result;
@@ -41,9 +41,8 @@ namespace storm {
             auto rightSubcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getRightSubcomposition().accept(*this, data));
             
             storm::jani::Model const& model = boost::any_cast<storm::jani::Model const&>(data);
-            storm::jani::CompositionActionInformationVisitor visitor(model);
-            storm::jani::ActionInformation leftActionInformation = visitor.getActionInformation(*leftSubcomposition);
-            storm::jani::ActionInformation rightActionInformation = visitor.getActionInformation(*rightSubcomposition);
+            storm::jani::CompositionInformation leftActionInformation = storm::jani::CompositionInformationVisitor(model, *leftSubcomposition).getInformation();
+            storm::jani::CompositionInformation rightActionInformation = storm::jani::CompositionInformationVisitor(model, *rightSubcomposition).getInformation();
             
             std::set<std::string> leftActions;
             for (auto const& actionIndex : leftActionInformation.getNonSilentActionIndices()) {

src/storm-pgcl.cpp

@@ -7,22 +7,18 @@
 #include "src/exceptions/BaseException.h"
 #include "src/utility/macros.h"
 #include <boost/lexical_cast.hpp>
+#include "src/builder/ProgramGraphBuilder.h"
+#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/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"
+#include "src/settings/modules/JaniExportSettings.h"
+
 
 /*!
  * Initialize the settings manager.
@@ -35,17 +31,28 @@ 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()) {
+        // For now, we have to have a jani file
+        storm::jani::JsonExporter::toStream(model, std::cout);
+    } else {
+        storm::jani::JsonExporter::toFile(model, storm::settings::getModule<storm::settings::modules::JaniExportSettings>().getJaniFilename());
+    }
+}
+
+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) {
@@ -59,10 +66,27 @@ int main(const int argc, const char** argv) {
             return -1;
         }
         
-        if(storm::settings::getModule<storm::settings::modules::PGCLSettings>().isPgclFileSet()) {
-            storm::pgcl::PgclProgram prog = storm::parser::PgclParser::parse(storm::settings::getModule<storm::settings::modules::PGCLSettings>().getPgclFilename());
-            std::cout << prog << std::endl;
+        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());
+        storm::ppg::ProgramGraph* progGraph = storm::builder::ProgramGraphBuilder::build(prog);
+    
+        progGraph->printInfo(std::cout);
+        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;
+        } else {
+            
+        }
+        
         
         
         

src/utility/storm.cpp

@@ -17,9 +17,7 @@ namespace storm {
 
     std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& path) {
         std::pair<storm::jani::Model, std::vector<storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(path);
-        if(!modelAndFormulae.first.checkValidity(true)) {
-            STORM_LOG_THROW(false, storm::exceptions::FileIoException, "Jani file parsing yields invalid model.");
-        }
+        modelAndFormulae.first.checkValid();
         return modelAndFormulae;
     }