another step, debugging in progress

Former-commit-id: 41c25470a2 [formerly 10e321e3d0]
Former-commit-id: 38f405c114

src/builder/jit/ExplicitJitJaniModelBuilder.cpp

@@ -7,6 +7,8 @@
 #include "src/adapters/CarlAdapter.h"
 
 #include "src/solver/SmtSolver.h"
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/ParallelComposition.h"
 
 #include "src/models/sparse/Dtmc.h"
 #include "src/models/sparse/StandardRewardModel.h"
@@ -57,6 +59,7 @@ namespace storm {
                 
 #include "resources/3rdparty/sparsepp/sparsepp.h"
                 
+#include "src/builder/jit/StateSet.h"
 #include "src/builder/jit/JitModelBuilderInterface.h"
 #include "src/builder/jit/StateBehaviour.h"
 #include "src/builder/jit/ModelComponentsBuilder.h"
@@ -93,7 +96,7 @@ namespace storm {
                             
                             std::ostream& operator<<(std::ostream& out, StateType const& state) {
                                 out << "<";
-                                {% for variable in stateVariables.boolean %}out << "{$variable.name}=" << state.{$variable.name} << ", ";
+                                {% for variable in stateVariables.boolean %}out << "{$variable.name}=" << std::boolalpha << state.{$variable.name} << ", ";
                                 {% endfor %}
                                 {% for variable in stateVariables.boundedInteger %}out << "{$variable.name}=" << state.{$variable.name} << ", ";
                                 {% endfor %}
@@ -127,39 +130,40 @@ namespace storm {
                     namespace builder {
                         namespace jit {
                             
-                            static bool model_is_deterministic() {
+                            bool model_is_deterministic() {
                                 return {$deterministic_model};
                             }
                             
-                            static bool model_is_discrete_time() {
+                            bool model_is_discrete_time() {
                                 return {$discrete_time_model};
                             }
 
-                            class StateSet {
-                            public:
-                                StateType const& peek() const {
-                                    return storage.front();
+                            {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& state) {
+                                if ({$edge.guard}) {
+                                    return true;
                                 }
-                                
-                                StateType get() {
-                                    StateType result = std::move(storage.front());
-                                    storage.pop();
-                                    return result;
+                                return false;
                             }
                             
-                                void add(StateType const& state) {
-                                    storage.push(state);
+                            {% for destination in edge.destinations %}
+                            void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType& state) {
+                                {% for level in destination.levels %}if (level == {$level.index}) {
+                                    {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};
+                                    {% endfor %}
                                 }
-                                
-                                bool empty() const {
-                                    return storage.empty();
+                                {% endfor %}
                             }
                             
-                            private:
-                                std::queue<StateType> storage;
-                            };
+                            void destination_perform_{$edge.name}_{$destination.name}(StateType& state) {
+                                {% for level in destination.levels %}
+                                {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};
+                                {% endfor %}
+                                {% endfor %}
+                            }
+                            {% endfor %}
+                            {% endfor %}
 
-                            {% for edge in nonSynchronizingEdges %}static bool edge_enabled_{$edge.name}(StateType const& state) {
+                            {% for edge in synch_edges %}static bool edge_enabled_{$edge.name}(StateType const& state) {
                                 if ({$edge.guard}) {
                                     return true;
                                 }
@@ -167,14 +171,14 @@ namespace storm {
                             }
                             
                             {% for destination in edge.destinations %}
-                            static void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType& state) {
+                            void destination_perform_level_{$edge.name}_{$destination.name}(int_fast64_t level, StateType& state) {
                                 {% for level in destination.levels %}if (level == {$level.index}) {
                                     {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};{% endfor %}
                                 }
                                 {% endfor %}
                             }
                             
-                            static void destination_perform_{$edge.name}_{$destination.name}(StateType& state) {
+                            void destination_perform_{$edge.name}_{$destination.name}(StateType& state) {
                                 {% for level in destination.levels %}
                                 {% for assignment in level.nonTransientAssignments %}state.{$assignment.variable} = {$assignment.value};
                                 {% endfor %}
@@ -183,6 +187,7 @@ namespace storm {
                             {% endfor %}
                             {% endfor %}
 
+                            
                             typedef void (*DestinationLevelFunctionPtr)(int_fast64_t, StateType&);
                             typedef void (*DestinationFunctionPtr)(StateType&);
                             
@@ -276,7 +281,13 @@ namespace storm {
                                         {% endfor %}
                                         initialStates.push_back(state);
                                     }{% endfor %}
-                                    {% for edge in nonSynchronizingEdges %}{
+                                    {% for edge in nonsynch_edges %}{
+                                        edge_{$edge.name} = Edge(&edge_enabled_{$edge.name});
+                                        {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name});
+                                        {% endfor %}
+                                    }
+                                    {% endfor %}
+                                    {% for edge in synch_edges %}{
                                         edge_{$edge.name} = Edge(&edge_enabled_{$edge.name});
                                         {% for destination in edge.destinations %}edge_{$edge.name}.addDestination({$destination.lowestLevel}, {$destination.highestLevel}, {$destination.value}, &destination_perform_level_{$edge.name}_{$destination.name}, &destination_perform_{$edge.name}_{$destination.name});
                                         {% endfor %}
@@ -306,6 +317,7 @@ namespace storm {
                                     
                                     for (auto const& stateEntry : stateIds) {
                                         auto const& state = stateEntry.first;
+                                        std::cout << state << std::endl;
                                         {% for label in labels %}if ({$label.predicate}) {
                                             this->modelComponentsBuilder.addLabel(stateEntry.second, {$loop.index} - 1);
                                         }
@@ -331,7 +343,7 @@ namespace storm {
                                 }
                                 
                                 void explore(StateType const& initialState) {
-                                    StateSet statesToExplore;
+                                    StateSet<StateType> statesToExplore;
                                     getOrAddIndex(initialState, statesToExplore);
                                     
                                     StateBehaviour<IndexType, ValueType> behaviour;
@@ -345,7 +357,8 @@ namespace storm {
 #endif
                                         
                                             behaviour.setExpanded();
-                                            exploreNonSynchronizingEdges(currentState, currentIndex, behaviour, statesToExplore);
+                                            exploreNonSynchronizingEdges(currentState, behaviour, statesToExplore);
+                                            exploreSynchronizingEdges(currentState, behaviour, statesToExplore);
                                         }
                                             
                                         this->addStateBehaviour(currentIndex, behaviour);
@@ -361,28 +374,32 @@ namespace storm {
                                     return false;
                                 }
                                 
-                                void exploreNonSynchronizingEdges(StateType const& state, IndexType const& currentIndex, StateBehaviour<IndexType, ValueType>& behaviour, StateSet& statesToExplore) {
-                                    {% for edge in nonSynchronizingEdges %}{
-                                        {% for destination in edge.destinations %}{
+                                void exploreNonSynchronizingEdges(StateType const& state, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
+                                    {% for edge in nonsynch_edges %}{
                                         if ({$edge.guard}) {
                                             Choice<IndexType, ValueType>& choice = behaviour.addChoice();
                                             {% for destination in edge.destinations %}{
                                                 StateType targetState(state);
                                                 destination_perform_{$edge.name}_{$destination.name}(targetState);
-                                                    //for (auto const& destination : edge_{$edge.name}) {
-                                                    //destination.perform(targetState);
                                                 IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore);
                                                 choice.add(targetStateIndex, {$destination.value});
-                                                    //}
                                             }{% endfor %}
                                         }
                                     }
                                     {% endfor %}
                                 }
+                                
+                                {% for vector in synch_vectors %}{$vector.functions}
+                                {% endfor %}
+
+                                void exploreSynchronizingEdges(StateType const& state, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {
+                                    {% for vector in synch_vectors %}{
+                                        exploreSynchronizationVector_{$vector.index}(state, behaviour, statesToExplore);
+                                    }
                                     {% endfor %}
                                 }
                                 
-                                IndexType getOrAddIndex(StateType const& state, StateSet& statesToExplore) {
+                                IndexType getOrAddIndex(StateType const& state, StateSet<StateType>& statesToExplore) {
                                     auto it = stateIds.find(state);
                                     if (it != stateIds.end()) {
                                         return it->second;
@@ -423,7 +440,9 @@ namespace storm {
                                 std::vector<StateType> initialStates;
                                 std::vector<IndexType> deadlockStates;
                                 
-                                {% for edge in nonSynchronizingEdges %}Edge edge_{$edge.name};
+                                {% for edge in nonsynch_edges %}Edge edge_{$edge.name};
+                                {% endfor %}
+                                {% for edge in synch_edges %}Edge edge_{$edge.name};
                                 {% endfor %}
                             };
                             
@@ -437,8 +456,7 @@ namespace storm {
                 modelData["stateVariables"] = generateStateVariables();
                 cpptempl::data_list initialStates = generateInitialStates();
                 modelData["initialStates"] = cpptempl::make_data(initialStates);
-                cpptempl::data_list nonSynchronizingEdges = generateNonSynchronizingEdges();
-                modelData["nonSynchronizingEdges"] = cpptempl::make_data(nonSynchronizingEdges);
+                generateEdges(modelData);
                 cpptempl::data_list labels = generateLabels();
                 modelData["labels"] = cpptempl::make_data(labels);
                 cpptempl::data_list terminalExpressions = generateTerminalExpressions();
@@ -680,19 +698,218 @@ namespace storm {
             }
 
             template <typename ValueType, typename RewardModelType>
-            cpptempl::data_list ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateNonSynchronizingEdges() {
-                cpptempl::data_list edges;
-                for (auto const& automaton : this->model.getAutomata()) {
+            cpptempl::data_map ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateSynchronizationVector(storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex) {
+                std::stringstream vectorSource;
+                uint64_t numberOfActionInputs = synchronizationVector.getNumberOfActionInputs();
+                
+                vectorSource << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore, ";
+                for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
+                    vectorSource << "Destination const& destination" << index << ", ";
+                }
+                vectorSource << "Choice<IndexType, ValueType>& choice) {" << std::endl;
+                vectorSource << "StateType targetState(state);" << std::endl;
+                for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
+                    vectorSource << "destination" << index << ".perform(targetState);" << std::endl;
+                }
+                vectorSource << "IndexType targetStateIndex = getOrAddIndex(targetState, statesToExplore);" << std::endl;
+                vectorSource << "choice.add(targetStateIndex, ";
+                for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
+                    vectorSource << "destination" << index << ".value()";
+                    if (index + 1 < numberOfActionInputs) {
+                        vectorSource << " * ";
+                    }
+                }
+                vectorSource << ");" << std::endl;
+                vectorSource << "}" << std::endl;
+                
+                vectorSource << "void performSynchronizedDestinations_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore, ";
+                for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
+                    vectorSource << "Edge const& edge" << index << ", ";
+                }
+                vectorSource << "Choice<IndexType, ValueType>& choice) {" << std::endl;
+                for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
+                    vectorSource << "for (auto const& destination" << index << " : edge" << index << ") {" << std::endl;
+                }
+                vectorSource << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(state, behaviour, statesToExplore, ";
+                for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
+                    vectorSource << "destination" << index << ", ";
+                }
+                vectorSource << "choice);" << std::endl;
+                for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
+                    vectorSource << "}" << std::endl;
+                }
+                vectorSource << "}" << std::endl;
+            
+                for (uint64_t index = 0; index < numberOfActionInputs; ++index) {
+                    vectorSource << "void performSynchronizedEdges_" << synchronizationVectorIndex << "_" << index << "(StateType const& state, std::vector<std::vector<std::reference_wrapper<Edge const>>> const& edges,  StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore";
+                    if (index > 0) {
+                        vectorSource << ", ";
+                    }
+                    for (uint64_t innerIndex = 0; innerIndex < index; ++innerIndex) {
+                        vectorSource << "Edge const& edge" << innerIndex;
+                        if (innerIndex + 1 < index) {
+                            vectorSource << ", ";
+                        }
+                    }
+                    vectorSource << ") {" << std::endl;
+                    vectorSource << "for (auto const& edge" << index << " : edges[" << index << "]) {" << std::endl;
+                    if (index + 1 < numberOfActionInputs) {
+                        vectorSource << "performSynchronizedEdges_" << synchronizationVectorIndex << "_" << (index + 1) << "(state, edges, behaviour, statesToExplore, ";
+                        for (uint64_t innerIndex = 0; innerIndex <= index; ++innerIndex) {
+                            vectorSource << "edge" << innerIndex;
+                            if (innerIndex + 1 <= index) {
+                                vectorSource << ", ";
+                            }
+                        }
+                        vectorSource << ");" << std::endl;
+                    } else {
+                        vectorSource << "Choice<IndexType, ValueType>& choice = behaviour.addChoice();" << std::endl;
+                        vectorSource << "performSynchronizedDestinations_" << synchronizationVectorIndex << "(state, behaviour, statesToExplore, ";
+                        for (uint64_t innerIndex = 0; innerIndex <= index; ++innerIndex) {
+                            vectorSource << "edge" << innerIndex << ", ";
+                        }
+                        vectorSource << " choice);" << std::endl;
+
+                    }
+                    vectorSource << "}" << std::endl;
+                    vectorSource << "}" << std::endl;
+                }
+                
+                vectorSource << "void get_edges_" << synchronizationVectorIndex << "(StateType const& state, std::vector<std::reference_wrapper<Edge const>>& edges, uint64_t position) {" << std::endl;
+                uint64_t position = 0;
+                uint64_t participatingPosition = 0;
+                std::cout << "synch vector " << synchronizationVector << std::endl;
+                for (auto const& inputActionName : synchronizationVector.getInput()) {
+                    if (!storm::jani::SynchronizationVector::isNoActionInput(inputActionName)) {
+                        vectorSource << "if (position == " << participatingPosition << ") {" << std::endl;
+                        
+                        storm::jani::Automaton const& automaton = model.getAutomaton(parallelComposition.getSubcomposition(position).asAutomatonComposition().getAutomatonName());
+                        uint64_t actionIndex = model.getActionIndex(inputActionName);
                         uint64_t edgeIndex = 0;
                         for (auto const& edge : automaton.getEdges()) {
-                        if (edge.getActionIndex() == storm::jani::Model::SILENT_ACTION_INDEX) {
-                            edges.push_back(generateEdge(automaton, edgeIndex, edge));
+                            std::cout << "[" << automaton.getName() << "], edge " << edgeIndex << " with guard " << edge.getGuard() << " has action " << model.getAction(edge.getActionIndex()).getName() << "[" << edge.getActionIndex() << "]" << std::endl;
+                            if (edge.getActionIndex() == actionIndex) {
+                                std::string edgeName = automaton.getName() + "_" + std::to_string(edgeIndex);
+                                vectorSource << "if (edge_enabled_" << edgeName  << "(state)) {" << std::endl;
+                                vectorSource << "edges.emplace_back(edge_" << edgeName << ");" << std::endl;
+                                vectorSource << "}" << std::endl;
                             }
                             ++edgeIndex;
                         }
+                        
+                        vectorSource << "}" << std::endl;
+                        ++participatingPosition;
+                    }
+                    ++position;
                 }
+                vectorSource << "}" << std::endl;
                 
-                return edges;
+                vectorSource << "void exploreSynchronizationVector_" << synchronizationVectorIndex << "(StateType const& state, StateBehaviour<IndexType, ValueType>& behaviour, StateSet<StateType>& statesToExplore) {" << std::endl;
+                vectorSource << "std::vector<std::vector<std::reference_wrapper<Edge const>>> edges(" << synchronizationVector.getNumberOfActionInputs() << ");" << std::endl;
+                
+                participatingPosition = 0;
+                for (auto const& input : synchronizationVector.getInput()) {
+                    if (!storm::jani::SynchronizationVector::isNoActionInput(input)) {
+                        vectorSource << "get_edges_" << synchronizationVectorIndex << "(state, edges[" << participatingPosition << "], " << participatingPosition << ");" << std::endl;
+                        vectorSource << "if (edges[" << participatingPosition << "].empty()) {" << std::endl;
+                        vectorSource << "return;" << std::endl;
+                        vectorSource << "};" << std::endl;
+                        ++participatingPosition;
+                    }
+                }
+                vectorSource << "performSynchronizedEdges_" << synchronizationVectorIndex << "_0(state, edges, behaviour, statesToExplore);" << std::endl;
+                vectorSource << "}" << std::endl;
+                
+                cpptempl::data_map vector;
+                vector["functions"] = vectorSource.str();
+                vector["index"] = asString(synchronizationVectorIndex);
+                return vector;
+            }
+            
+            template <typename ValueType, typename RewardModelType>
+            void ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateEdges(cpptempl::data_map& modelData) {
+                STORM_LOG_THROW(model.hasStandardCompliantComposition(), storm::exceptions::WrongFormatException, "Model builder only supports non-nested parallel compositions.");
+                
+                cpptempl::data_list nonSynchronizingEdges;
+                cpptempl::data_list synchronizingEdges;
+                cpptempl::data_list vectors;
+                
+                storm::jani::Composition const& topLevelComposition = model.getSystemComposition();
+                if (topLevelComposition.isAutomatonComposition()) {
+                    storm::jani::Automaton const& automaton = model.getAutomaton(topLevelComposition.asAutomatonComposition().getAutomatonName());
+                    uint64_t edgeIndex = 0;
+                    for (auto const& edge : automaton.getEdges()) {
+                        nonSynchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge));
+                        ++edgeIndex;
+                    }
+                } else {
+                    STORM_LOG_ASSERT(topLevelComposition.isParallelComposition(), "Expected parallel composition.");
+                    storm::jani::ParallelComposition const& parallelComposition = topLevelComposition.asParallelComposition();
+                    for (auto const& composition : parallelComposition.getSubcompositions()) {
+                        STORM_LOG_ASSERT(composition->isAutomatonComposition(), "Expected flat parallel composition.");
+                    }
+
+                    std::vector<std::set<uint64_t>> synchronizingActions(parallelComposition.getNumberOfSubcompositions());
+                    uint64_t synchronizationVectorIndex = 0;
+                    for (auto const& synchronizationVector : parallelComposition.getSynchronizationVectors()) {
+                        // If the synchronization vector has at most one action input, there is no synchronization going on.
+                        if (synchronizationVector.getNumberOfActionInputs() <= 1) {
+                            continue;
+                        }
+                        
+                        bool createVector = true;
+                        uint64_t position = 0;
+                        for (auto const& inputActionName : synchronizationVector.getInput()) {
+                            if (!storm::jani::SynchronizationVector::isNoActionInput(inputActionName)) {
+                                uint64_t actionIndex = model.getActionIndex(inputActionName);
+                                synchronizingActions[position].insert(actionIndex);
+                                
+                                storm::jani::Automaton const& automaton = model.getAutomaton(parallelComposition.getSubcomposition(position).asAutomatonComposition().getAutomatonName());
+                                bool hasParticipatingEdge = false;
+                                for (auto const& edge : automaton.getEdges()) {
+                                    if (edge.getActionIndex() == actionIndex) {
+                                        hasParticipatingEdge = true;
+                                        break;
+                                    }
+                                }
+                                
+                                if (!hasParticipatingEdge) {
+                                    createVector = false;
+                                }
+                            }
+                            ++position;
+                        }
+                        
+                        if (createVector) {
+                            cpptempl::data_map vector = generateSynchronizationVector(parallelComposition, synchronizationVector, synchronizationVectorIndex);
+                            vectors.push_back(vector);
+                        }
+                        ++synchronizationVectorIndex;
+                    }
+                    
+                    uint64_t position = 0;
+                    for (auto const& composition : parallelComposition.getSubcompositions()) {
+                        storm::jani::Automaton const& automaton = model.getAutomaton(composition->asAutomatonComposition().getAutomatonName());
+                        
+                        // Add all edges with an action index that is not mentioned in any synchronization vector as
+                        // non-synchronizing edges.
+                        uint64_t edgeIndex = 0;
+                        for (auto const& edge : automaton.getEdges()) {
+                            if (synchronizingActions[position].find(edge.getActionIndex()) != synchronizingActions[position].end()) {
+                                synchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge));
+                            } else {
+                                nonSynchronizingEdges.push_back(generateEdge(automaton, edgeIndex, edge));
+                            }
+                            ++edgeIndex;
+                        }
+                        
+                        ++position;
+                    }
+                }
+                
+                modelData["nonsynch_edges"] = cpptempl::make_data(nonSynchronizingEdges);
+                modelData["synch_edges"] = cpptempl::make_data(synchronizingEdges);
+                modelData["synch_vectors"] = cpptempl::make_data(vectors);
             }
             
             template <typename ValueType, typename RewardModelType>
@@ -720,8 +937,13 @@ namespace storm {
                 destinationData["name"] = asString(destinationIndex);
                 destinationData["levels"] = cpptempl::make_data(levels);
                 destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(destination.getProbability()), storm::expressions::ToCppTranslationOptions("state.", "double"));
+                if (destination.getOrderedAssignments().empty()) {
+                    destinationData["lowestLevel"] = "0";
+                    destinationData["highestLevel"] = "0";
+                } else {
                     destinationData["lowestLevel"] = asString(destination.getOrderedAssignments().getLowestLevel());
                     destinationData["highestLevel"] = asString(destination.getOrderedAssignments().getHighestLevel());
+                }
 
                 return destinationData;
             }

src/builder/jit/ExplicitJitJaniModelBuilder.h

@@ -9,6 +9,7 @@
 #include "cpptempl.h"
 
 #include "src/storage/jani/Model.h"
+#include "src/storage/jani/ParallelComposition.h"
 #include "src/storage/expressions/ToCppVisitor.h"
 
 #include "src/builder/BuilderOptions.h"
@@ -54,7 +55,8 @@ namespace storm {
                 cpptempl::data_map generateStateVariables();
                 cpptempl::data_list generateLabels();
                 cpptempl::data_list generateTerminalExpressions();
-                cpptempl::data_list generateNonSynchronizingEdges();
+                void generateEdges(cpptempl::data_map& modelData);
+                cpptempl::data_map generateSynchronizationVector(storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex);
                 cpptempl::data_list generateLevels(storm::jani::OrderedAssignments const& assignments);
                 
                 cpptempl::data_map generateEdge(storm::jani::Automaton const& automaton, uint64_t edgeIndex, storm::jani::Edge const& edge);

src/builder/jit/ModelComponentsBuilder.cpp

@@ -2,6 +2,9 @@
 
 #include "src/models/sparse/StateLabeling.h"
 #include "src/models/sparse/Dtmc.h"
+#include "src/models/sparse/Ctmc.h"
+#include "src/models/sparse/Mdp.h"
+#include "src/models/sparse/MarkovAutomaton.h"
 #include "src/models/sparse/StandardRewardModel.h"
 
 #include "src/settings/SettingsManager.h"
@@ -67,6 +70,10 @@ namespace storm {
                 
                 if (modelType == storm::jani::ModelType::DTMC) {
                     return new storm::models::sparse::Dtmc<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(this->transitionMatrixBuilder->build(), std::move(stateLabeling));
+                } else if (modelType == storm::jani::ModelType::CTMC) {
+                    return new storm::models::sparse::Ctmc<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(this->transitionMatrixBuilder->build(), std::move(stateLabeling));
+                } else if (modelType == storm::jani::ModelType::MDP) {
+                    return new storm::models::sparse::Mdp<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(this->transitionMatrixBuilder->build(), std::move(stateLabeling));
                 } else {
                     return nullptr;
                 }

src/builder/jit/StateBehaviour.cpp

@@ -42,6 +42,10 @@ namespace storm {
                         if (modelType == storm::jani::ModelType::DTMC) {
                             choices.front().divideDistribution(static_cast<ValueType>(totalCount));
                         }
+                    } else {
+                        for (auto& choice : choices) {
+                            choice.compress();
+                        }
                     }
                 } else if (choices.size() == 1) {
                     choices.front().compress();

src/builder/jit/StateSet.h

@@ -0,0 +1,36 @@
+#pragma once
+
+#include <queue>
+
+namespace storm {
+    namespace builder {
+        namespace jit {
+            
+            template <typename StateType>
+            class StateSet {
+            public:
+                StateType const& peek() const {
+                    return storage.front();
+                }
+                
+                StateType get() {
+                    StateType result = std::move(storage.front());
+                    storage.pop();
+                    return result;
+                }
+                
+                void add(StateType const& state) {
+                    storage.push(state);
+                }
+                
+                bool empty() const {
+                    return storage.empty();
+                }
+                
+            private:
+                std::queue<StateType> storage;
+            };
+            
+        }
+    }
+}

src/generator/NextStateGenerator.cpp

@@ -107,6 +107,7 @@ namespace storm {
             }
             for (auto const& stateIndexPair : states) {
                 unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator);
+                std::cout << toValuation(stateIndexPair.first).toString(true) << std::endl;
                 
                 for (auto const& label : labelsAndExpressions) {
                     // Add label to state, if the corresponding expression is true.

src/generator/PrismNextStateGenerator.cpp

@@ -354,12 +354,13 @@ namespace storm {
                 // If there was no enabled command although the module has some command with the required action label,
                 // we must not return anything.
                 if (commands.size() == 0) {
-                    return boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>>();
+                    return boost::none;
                 }
                 
                 result.get().push_back(std::move(commands));
             }
             
+            STORM_LOG_ASSERT(!result->empty(), "Expected non-empty list.");
             return result;
         }
         
@@ -434,6 +435,8 @@ namespace storm {
             std::vector<Choice<ValueType>> result;
             
             for (uint_fast64_t actionIndex : program.getSynchronizingActionIndices()) {
+                std::cout << "got act " << actionIndex << std::endl;
+                std::cout << "name: " << program.getActionName(actionIndex) << std::endl;
                 boost::optional<std::vector<std::vector<std::reference_wrapper<storm::prism::Command const>>>> optionalActiveCommandLists = getActiveCommandsByActionIndex(actionIndex);
                 
                 // Only process this action label, if there is at least one feasible solution.
@@ -456,6 +459,7 @@ namespace storm {
                         
                         for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
                             storm::prism::Command const& command = *iteratorList[i];
+                            std::cout << command << std::endl;
                             for (uint_fast64_t j = 0; j < command.getNumberOfUpdates(); ++j) {
                                 storm::prism::Update const& update = command.getUpdate(j);
                                 

src/storage/expressions/SimpleValuation.cpp

@@ -112,8 +112,6 @@ namespace storm {
 
 
         std::string SimpleValuation::toString(bool pretty) const {
-
-
             std::stringstream sstr;
             if(pretty) {
                 sstr << "valuation {" << std::endl;

src/storage/jani/AutomatonComposition.cpp

@@ -19,7 +19,7 @@ namespace storm {
             return inputEnabledActions;
         }
         
-        bool AutomatonComposition::isAutomaton() const {
+        bool AutomatonComposition::isAutomatonComposition() const {
             return true;
         }
         

src/storage/jani/AutomatonComposition.h

@@ -25,7 +25,7 @@ namespace storm {
             
             std::set<std::string> const& getInputEnabledActions() const;
 
-            bool isAutomaton() const override;
+            virtual bool isAutomatonComposition() const override;
             
         private:
             /// The name of the automaton this composition element refers to.

src/storage/jani/Composition.cpp

@@ -1,8 +1,27 @@
 #include "src/storage/jani/Composition.h"
 
+#include "src/storage/jani/AutomatonComposition.h"
+#include "src/storage/jani/ParallelComposition.h"
+
 namespace storm {
     namespace jani {
 
+        bool Composition::isAutomatonComposition() const {
+            return false;
+        }
+        
+        bool Composition::isParallelComposition() const {
+            return false;
+        }
+        
+        AutomatonComposition const& Composition::asAutomatonComposition() const {
+            return static_cast<AutomatonComposition const&>(*this);
+        }
+        
+        ParallelComposition const& Composition::asParallelComposition() const {
+            return static_cast<ParallelComposition const&>(*this);
+        }
+        
         std::ostream& operator<<(std::ostream& stream, Composition const& composition) {
             composition.write(stream);
             return stream;

src/storage/jani/Composition.h

@@ -9,12 +9,16 @@ 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;
             
+            virtual bool isAutomatonComposition() const;
+            AutomatonComposition const& asAutomatonComposition() const;
+
+            virtual bool isParallelComposition() const;
+            ParallelComposition const& asParallelComposition() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Composition const& composition);
         };
                 

src/storage/jani/CompositionInformationVisitor.cpp

@@ -9,7 +9,7 @@
 namespace storm {
     namespace jani {
         
-        CompositionInformation::CompositionInformation() : nonStandardParallelComposition(false) {
+        CompositionInformation::CompositionInformation() : nonStandardParallelComposition(false), nestedParallelComposition(false), parallelComposition(false) {
             // Intentionally left empty.
         }
         
@@ -41,6 +41,22 @@ namespace storm {
             return nonStandardParallelComposition;
         }
         
+        void CompositionInformation::setContainsNestedParallelComposition(bool value) {
+            nestedParallelComposition = value;
+        }
+        
+        bool CompositionInformation::containsNestedParallelComposition() const {
+            return nestedParallelComposition;
+        }
+        
+        void CompositionInformation::setContainsParallelComposition(bool value) {
+            parallelComposition = value;
+        }
+        
+        bool CompositionInformation::containsParallelComposition() const {
+            return parallelComposition;
+        }
+        
         std::string const& CompositionInformation::getActionName(uint64_t index) const {
             return indexToNameMap.at(index);
         }
@@ -130,9 +146,11 @@ namespace storm {
             }
             
             bool containsNonStandardParallelComposition = false;
+            bool containsSubParallelComposition = false;
             
             for (auto const& subinfo : subinformation) {
                 containsNonStandardParallelComposition |= subinfo.containsNonStandardParallelComposition();
+                containsSubParallelComposition |= subinfo.containsParallelComposition();
                 result.addMultiplicityMap(subinfo.getAutomatonToMultiplicityMap());
             }
             
@@ -217,6 +235,8 @@ namespace storm {
             containsNonStandardParallelComposition |= !std::includes(synchVectorSet.begin(), synchVectorSet.end(), expectedSynchVectorSetUnderApprox.begin(), expectedSynchVectorSetUnderApprox.end(), SynchronizationVectorLexicographicalLess());
 
             result.setContainsNonStandardParallelComposition(containsNonStandardParallelComposition);
+            result.setContainsParallelComposition(true);
+            result.setContainsNestedParallelComposition(containsSubParallelComposition);
             
             result.addNonSilentActionIndices(nonSilentActionIndices);
             return result;

src/storage/jani/CompositionInformationVisitor.h

@@ -25,6 +25,12 @@ namespace storm {
             void setContainsNonStandardParallelComposition(bool value);
             bool containsNonStandardParallelComposition() const;
 
+            void setContainsNestedParallelComposition(bool value);
+            bool containsNestedParallelComposition() const;
+
+            void setContainsParallelComposition(bool value);
+            bool containsParallelComposition() const;
+            
             std::string const& getActionName(uint64_t index) const;
             uint64_t getActionIndex(std::string const& name) const;
 
@@ -57,6 +63,12 @@ namespace storm {
             
             /// A flag indicating whether the composition contains any non-standard parallel composition.
             bool nonStandardParallelComposition;
+            
+            /// A flag indicating whether the composition contains nested parallel compositions;
+            bool nestedParallelComposition;
+            
+            /// A flag indicating whether the composition contains a parallel composition;
+            bool parallelComposition;
         };
         
         class CompositionInformationVisitor : public CompositionVisitor {

src/storage/jani/JSONExporter.cpp

@@ -59,7 +59,7 @@ namespace storm {
                 std::vector<modernjson::json> elems;
                 for (auto const& subcomp : composition.getSubcompositions()) {
                     modernjson::json elemDecl;
-                    if (subcomp->isAutomaton()) {
+                    if (subcomp->isAutomatonComposition()) {
                         modernjson::json autDecl;
                         autDecl["automaton"] = std::static_pointer_cast<AutomatonComposition>(subcomp)->getAutomatonName();
                         std::vector<modernjson::json> elements;

src/storage/jani/Model.cpp

@@ -506,6 +506,15 @@ namespace storm {
             return true;
         }
         
+        bool Model::hasStandardCompliantComposition() const {
+            CompositionInformationVisitor visitor(*this, this->getSystemComposition());
+            CompositionInformation info = visitor.getInformation();
+            if (info.containsNestedParallelComposition()) {
+                return false;
+            }
+            return true;
+        }
+        
         bool Model::undefinedConstantsAreGraphPreserving() const {
             if (!this->hasUndefinedConstants()) {
                 return true;

src/storage/jani/Model.h

@@ -227,6 +227,7 @@ namespace storm {
              * @see getStandardSystemComposition
              */
             void setStandardSystemComposition();
+            
             /*!
              * Gets the system composition as the standard, fully-synchronizing parallel composition.
              */
@@ -314,6 +315,11 @@ namespace storm {
              */
             bool hasStandardComposition() const;
             
+            /*!
+             * Checks whether the composition has no nesting.
+             */
+            bool hasStandardCompliantComposition() const;
+            
             /*!
              * After adding all components to the model, this method has to be called. It recursively calls
              * <code>finalize</code> on all contained elements. All subsequent changes to the model require another call

src/storage/jani/OrderedAssignments.cpp

@@ -82,6 +82,10 @@ namespace storm {
             return false;
         }
         
+        bool OrderedAssignments::empty() const {
+            return allAssignments.empty();
+        }
+        
         int_fast64_t OrderedAssignments::getLowestLevel() const {
             return allAssignments.front()->getLevel();
         }

src/storage/jani/OrderedAssignments.h

@@ -42,6 +42,11 @@ namespace storm {
              */
             bool hasMultipleLevels() const;
             
+            /*!
+             * Retrieves whether this set of assignments is empty.
+             */
+            bool empty() const;
+            
             /*!
              * Retrieves the lowest level among all assignments. Note that this may only be called if there is at least
              * one assignment.

src/storage/jani/ParallelComposition.cpp

@@ -74,6 +74,16 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Synchronization vector must have at least one participating action.");
         }
         
+        uint64_t SynchronizationVector::getNumberOfActionInputs() const {
+            uint64_t result = 0;
+            for (auto const& inputEntry : input) {
+                if (!isNoActionInput(inputEntry)) {
+                    ++result;
+                }
+            }
+            return result;
+        }
+        
         bool SynchronizationVector::isNoActionInput(std::string const& action) {
             return action == NO_ACTION_INPUT;
         }
@@ -151,6 +161,10 @@ namespace storm {
             }
         }
         
+        bool ParallelComposition::isParallelComposition() const {
+            return true;
+        }
+        
         Composition const& ParallelComposition::getSubcomposition(uint64_t index) const {
             return *subcompositions[index];
         }

src/storage/jani/ParallelComposition.h

@@ -41,6 +41,10 @@ namespace storm {
              */
             uint64_t getPositionOfFirstParticipatingAction() const;
             
+            /*!
+             * Retrieves the number of action inputs, i.e. participating subcompositions.
+             */
+            uint64_t getNumberOfActionInputs() const;
             
             // A marker that can be used as one of the inputs. The semantics is that no action of the corresponding
             // automaton takes part in the synchronization.
@@ -85,6 +89,8 @@ namespace storm {
              */
             ParallelComposition(std::shared_ptr<Composition> const& leftSubcomposition, std::shared_ptr<Composition> const& rightSubcomposition, std::set<std::string> const& synchronizationAlphabet);
 
+            virtual bool isParallelComposition() const override;
+            
             /*!
              * Retrieves the subcomposition with the given index.
              */

src/storage/prism/Module.cpp

@@ -172,6 +172,18 @@ namespace storm {
             return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
         }
         
+        Module Module::restrictActionIndices(boost::container::flat_set<uint_fast64_t> const& actionIndices) const {
+            // First construct the new vector of commands.
+            std::vector<storm::prism::Command> newCommands;
+            for (auto const& command : commands) {
+                if (actionIndices.find(command.getActionIndex()) != actionIndices.end()) {
+                    newCommands.push_back(command);
+                }
+            }
+            
+            return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
+        }
+        
         Module Module::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             std::vector<BooleanVariable> newBooleanVariables;
             newBooleanVariables.reserve(this->getNumberOfBooleanVariables());

src/storage/prism/Module.h

@@ -209,6 +209,14 @@ namespace storm {
              */
             Module restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) const;
             
+            /*!
+             * Creates a new module that drops all commands whose action indices are not in the given set.
+             *
+             * @param indexSet The set of action indices for which to keep the commands.
+             * @return The module resulting from erasing all commands whose action indices are not in the given set.
+             */
+            Module restrictActionIndices(boost::container::flat_set<uint_fast64_t> const& actionIndices) const;
+            
             /*!
              * Substitutes all variables in the module according to the given map.
              *

src/storage/prism/Program.cpp

@@ -1306,7 +1306,7 @@ namespace storm {
                 std::vector<Module> cleanedModules;
                 cleanedModules.reserve(newModules.size());
                 for (auto const& module : newModules) {
-                    cleanedModules.emplace_back(module.restrictCommands(actionsToKeep));
+                    cleanedModules.emplace_back(module.restrictActionIndices(actionsToKeep));
                 }
                 newModules = std::move(cleanedModules);