more work on JANI next state generator and the corresponding tests

Former-commit-id: e170c9989c

src/builder/ExplicitModelBuilder.cpp

@@ -13,6 +13,7 @@
 #include "src/settings/modules/IOSettings.h"
 
 #include "src/generator/PrismNextStateGenerator.h"
+#include "src/generator/JaniNextStateGenerator.h"
 
 #include "src/utility/prism.h"
 #include "src/utility/constants.h"
@@ -105,6 +106,11 @@ namespace storm {
             // Intentionally left empty.
         }
         
+        template <typename ValueType, typename RewardModelType, typename StateType>
+        ExplicitModelBuilder<ValueType, RewardModelType, StateType>::ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions, Options const& builderOptions) : ExplicitModelBuilder(std::make_shared<storm::generator::JaniNextStateGenerator<ValueType, StateType>>(model, generatorOptions), builderOptions) {
+            // Intentionally left empty.
+        }
+        
         template <typename ValueType, typename RewardModelType, typename StateType>
         storm::storage::sparse::StateValuations const& ExplicitModelBuilder<ValueType, RewardModelType, StateType>::getStateValuations() const {
             STORM_LOG_THROW(static_cast<bool>(stateValuations), storm::exceptions::InvalidOperationException, "The state information was not properly build.");

src/builder/ExplicitModelBuilder.h

@@ -88,11 +88,18 @@ namespace storm {
             ExplicitModelBuilder(std::shared_ptr<storm::generator::NextStateGenerator<ValueType, StateType>> const& generator, Options const& options = Options());
 
             /*!
-             * Creates an explicit model builder for the given PRISM program..
+             * Creates an explicit model builder for the given PRISM program.
              *
              * @param program The program for which to build the model.
              */
             ExplicitModelBuilder(storm::prism::Program const& program, storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(), Options const& builderOptions = Options());
+
+            /*!
+             * Creates an explicit model builder for the given JANI model.
+             *
+             * @param model The JANI model for which to build the model.
+             */
+            ExplicitModelBuilder(storm::jani::Model const& model, storm::generator::NextStateGeneratorOptions const& generatorOptions = storm::generator::NextStateGeneratorOptions(), Options const& builderOptions = Options());
             
             /*!
              * Convert the program given at construction time to an abstract model. The type of the model is the one

src/generator/JaniNextStateGenerator.cpp

@@ -14,7 +14,7 @@
 
 namespace storm {
     namespace generator {
-     
+        
         template<typename ValueType, typename StateType>
         JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options) : JaniNextStateGenerator(model.substituteConstants(), options, false) {
             // Intentionally left empty.
@@ -22,7 +22,7 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), VariableInformation(model), options), model(model) {
-            STORM_LOG_THROW(!this->model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
+            STORM_LOG_THROW(!model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
             STORM_LOG_THROW(!this->options.isBuildAllRewardModelsSet() && this->options.getRewardModelNames().empty(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support building reward models.");
             STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
             
@@ -59,7 +59,35 @@ namespace storm {
         bool JaniNextStateGenerator<ValueType, StateType>::isDiscreteTimeModel() const {
             return model.isDiscreteTimeModel();
         }
-
+        
+        template<typename ValueType, typename StateType>
+        uint64_t JaniNextStateGenerator<ValueType, StateType>::getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const {
+            if (locationVariable.bitWidth == 0) {
+                return 0;
+            } else {
+                return state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth);
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        void JaniNextStateGenerator<ValueType, StateType>::setLocation(CompressedState& state, LocationVariableInformation const& locationVariable, uint64_t locationIndex) const {
+            if (locationVariable.bitWidth != 0) {
+                state.setFromInt(locationVariable.bitOffset, locationVariable.bitWidth, locationIndex);
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::vector<uint64_t> JaniNextStateGenerator<ValueType, StateType>::getLocations(CompressedState const& state) const {
+            std::vector<uint64_t> result(this->variableInformation.locationVariables.size());
+            
+            auto resultIt = result.begin();
+            for (auto it = this->variableInformation.locationVariables.begin(), ite = this->variableInformation.locationVariables.end(); it != ite; ++it, ++resultIt) {
+                *resultIt = getLocation(state, *it);
+            }
+            
+            return result;
+        }
+        
         template<typename ValueType, typename StateType>
         std::vector<StateType> JaniNextStateGenerator<ValueType, StateType>::getInitialStates(StateToIdCallback const& stateToIdCallback) {
             // Prepare an SMT solver to enumerate all initial states.
@@ -72,7 +100,7 @@ namespace storm {
             }
             solver->add(model.getInitialStatesExpression(true));
             
-            // Proceed ss long as the solver can still enumerate initial states.
+            // Proceed as long as the solver can still enumerate initial states.
             std::vector<StateType> initialStateIndices;
             while (solver->check() == storm::solver::SmtSolver::CheckResult::Sat) {
                 // Create fresh state.
@@ -95,11 +123,35 @@ namespace storm {
                     initialState.setFromInt(integerVariable.bitOffset, integerVariable.bitWidth, static_cast<uint_fast64_t>(variableValue - integerVariable.lowerBound));
                 }
                 
-                // FIXME: iterate through all combinations of initial locations and set them in the initial state.
+                // Gather iterators to the initial locations of all the automata.
+                std::vector<std::set<uint64_t>::const_iterator> initialLocationsIterators;
+                for (auto const& automaton : this->model.getAutomata()) {
+                    initialLocationsIterators.push_back(automaton.getInitialLocationIndices().cbegin());
+                }
                 
-                // Register initial state and return it.
-                StateType id = stateToIdCallback(initialState);
-                initialStateIndices.push_back(id);
+                // Now iterate through all combinations of initial locations.
+                while (true) {
+                    uint64_t index = 0;
+                    for (; index < initialLocationsIterators.size(); ++index) {
+                        ++initialLocationsIterators[index];
+                        if (initialLocationsIterators[index] == this->model.getAutomata()[index].getInitialLocationIndices().cend()) {
+                            initialLocationsIterators[index] = this->model.getAutomata()[index].getInitialLocationIndices().cbegin();
+                        } else {
+                            break;
+                        }
+                    }
+                    
+                    // If we are at the end, leave the loop. Otherwise, create the next initial state.
+                    if (index == initialLocationsIterators.size()) {
+                        break;
+                    } else {
+                        setLocation(initialState, this->variableInformation.locationVariables[index], *initialLocationsIterators[index]);
+
+                        // Register initial state and return it.
+                        StateType id = stateToIdCallback(initialState);
+                        initialStateIndices.push_back(id);
+                    }
+                }
                 
                 // Block the current initial state to search for the next one.
                 solver->add(blockingExpression);
@@ -107,7 +159,7 @@ namespace storm {
             
             return initialStateIndices;
         }
-
+        
         template<typename ValueType, typename StateType>
         CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination) {
             CompressedState newState(state);
@@ -161,9 +213,12 @@ namespace storm {
                 }
             }
             
+            // Retrieve the locations from the state.
+            std::vector<uint64_t> locations = getLocations(*this->state);
+            
             // Get all choices for the state.
-            std::vector<Choice<ValueType>> allChoices = getSilentActionChoices(*this->state, stateToIdCallback);
-            std::vector<Choice<ValueType>> allLabeledChoices = getNonsilentActionChoices(*this->state, stateToIdCallback);
+            std::vector<Choice<ValueType>> allChoices = getSilentActionChoices(locations, *this->state, stateToIdCallback);
+            std::vector<Choice<ValueType>> allLabeledChoices = getNonsilentActionChoices(locations, *this->state, stateToIdCallback);
             for (auto& choice : allLabeledChoices) {
                 allChoices.push_back(std::move(choice));
             }
@@ -210,18 +265,16 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+        std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getSilentActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) {
             std::vector<Choice<ValueType>> result;
             
             // Iterate over all automata.
-            auto locationVariableIt = this->variableInformation.locationVariables.begin();
+            uint64_t automatonIndex = 0;
             for (auto const& automaton : model.getAutomata()) {
-                
-                // Determine the location of the automaton in the given state.
-                uint64_t locationIndex = state.getAsInt(locationVariableIt->bitOffset, locationVariableIt->bitWidth);
+                uint64_t location = locations[automatonIndex];
                 
                 // Iterate over all edges from the source location.
-                for (auto const& edge : automaton.getEdgesFromLocation(locationIndex)) {
+                for (auto const& edge : automaton.getEdgesFromLocation(location)) {
                     // Skip the edge if it is labeled with a non-silent action.
                     if (edge.getActionIndex() != model.getSilentActionIndex()) {
                         continue;
@@ -252,16 +305,146 @@ namespace storm {
                     STORM_LOG_THROW(!this->isDiscreteTimeModel() || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for edge (actually sum to " << probabilitySum << ").");
                 }
                 
-                // After we have processed all edges of the current automaton, move to the next location variable.
-                ++locationVariableIt;
+                ++automatonIndex;
             }
             
             return result;
         }
         
         template<typename ValueType, typename StateType>
-        std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback) {
+        std::vector<Choice<ValueType>> JaniNextStateGenerator<ValueType, StateType>::getNonsilentActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback) {
+            std::vector<Choice<ValueType>> result;
             
+            for (uint64_t actionIndex : model.getNonsilentActionIndices()) {
+                std::vector<std::vector<storm::jani::Edge const*>> enabledEdges = getEnabledEdges(locations, actionIndex);
+                
+                // Only process this action, if there is at least one feasible solution.
+                if (!enabledEdges.empty()) {
+                    std::vector<std::vector<storm::jani::Edge const*>::const_iterator> iteratorList(enabledEdges.size());
+                    
+                    // Initialize the list of iterators.
+                    for (size_t i = 0; i < enabledEdges.size(); ++i) {
+                        iteratorList[i] = enabledEdges[i].cbegin();
+                    }
+                    
+                    // As long as there is one feasible combination of commands, keep on expanding it.
+                    bool done = false;
+                    while (!done) {
+                        boost::container::flat_map<CompressedState, ValueType>* currentTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+                        boost::container::flat_map<CompressedState, ValueType>* newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+                        
+                        currentTargetStates->emplace(state, storm::utility::one<ValueType>());
+                        
+                        for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
+                            storm::jani::Edge const& edge = **iteratorList[i];
+                            
+                            for (auto const& destination : edge.getDestinations()) {
+                                for (auto const& stateProbabilityPair : *currentTargetStates) {
+                                    // Compute the new state under the current update and add it to the set of new target states.
+                                    CompressedState newTargetState = applyUpdate(stateProbabilityPair.first, destination);
+                                    
+                                    // If the new state was already found as a successor state, update the probability
+                                    // and otherwise insert it.
+                                    auto targetStateIt = newTargetStates->find(newTargetState);
+                                    if (targetStateIt != newTargetStates->end()) {
+                                        targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability());
+                                    } else {
+                                        newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability()));
+                                    }
+                                }
+                            }
+                            
+                            // If there is one more command to come, shift the target states one time step back.
+                            if (i < iteratorList.size() - 1) {
+                                delete currentTargetStates;
+                                currentTargetStates = newTargetStates;
+                                newTargetStates = new boost::container::flat_map<CompressedState, ValueType>();
+                            }
+                        }
+                        
+                        // At this point, we applied all commands of the current command combination and newTargetStates
+                        // contains all target states and their respective probabilities. That means we are now ready to
+                        // add the choice to the list of transitions.
+                        result.push_back(Choice<ValueType>(actionIndex));
+                        
+                        // Now create the actual distribution.
+                        Choice<ValueType>& choice = result.back();
+                        
+                        // Add the probabilities/rates to the newly created choice.
+                        ValueType probabilitySum = storm::utility::zero<ValueType>();
+                        for (auto const& stateProbabilityPair : *newTargetStates) {
+                            StateType actualIndex = stateToIdCallback(stateProbabilityPair.first);
+                            choice.addProbability(actualIndex, stateProbabilityPair.second);
+                            probabilitySum += stateProbabilityPair.second;
+                        }
+                        
+                        // Check that the resulting distribution is in fact a distribution.
+                        STORM_LOG_THROW(!this->isDiscreteTimeModel() || !this->comparator.isConstant(probabilitySum) || this->comparator.isOne(probabilitySum), storm::exceptions::WrongFormatException, "Sum of update probabilities do not some to one for some command (actually sum to " << probabilitySum << ").");
+                        
+                        // Dispose of the temporary maps.
+                        delete currentTargetStates;
+                        delete newTargetStates;
+                        
+                        // Now, check whether there is one more command combination to consider.
+                        bool movedIterator = false;
+                        for (uint64_t j = 0; !movedIterator && j < iteratorList.size(); ++j) {
+                            ++iteratorList[j];
+                            if (iteratorList[j] != enabledEdges[j].end()) {
+                                movedIterator = true;
+                            } else {
+                                // Reset the iterator to the beginning of the list.
+                                iteratorList[j] = enabledEdges[j].begin();
+                            }
+                        }
+                        
+                        done = !movedIterator;
+                    }
+                }
+            }
+            
+            return result;
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::vector<std::vector<storm::jani::Edge const*>> JaniNextStateGenerator<ValueType, StateType>::getEnabledEdges(std::vector<uint64_t> const& locationIndices, uint64_t actionIndex) {
+            std::vector<std::vector<storm::jani::Edge const*>> result;
+            
+            // Iterate over all automata.
+            uint64_t automatonIndex = 0;
+            for (auto const& automaton : model.getAutomata()) {
+                
+                // If the automaton has no edge labeled with the given action, we can skip it.
+                if (!automaton.hasEdgeLabeledWithActionIndex(actionIndex)) {
+                    continue;
+                }
+                
+                auto edges = automaton.getEdgesFromLocation(locationIndices[automatonIndex], actionIndex);
+                
+                // If the automaton contains the action, but there is no edge available labeled with
+                // this action, we don't have any feasible command combinations.
+                if (edges.empty()) {
+                    return std::vector<std::vector<storm::jani::Edge const*>>();
+                }
+                
+                std::vector<storm::jani::Edge const*> edgePointers;
+                edgePointers.reserve(edges.size());
+                for (auto const& edge : edges) {
+                    if (this->evaluator.asBool(edge.getGuard())) {
+                        edgePointers.push_back(&edge);
+                    }
+                }
+                
+                // If there was no enabled edge although the automaton has some edge with the required action, we must
+                // not return anything.
+                if (edgePointers.size() == 0) {
+                    return std::vector<std::vector<storm::jani::Edge const*>>();
+                }
+                
+                result.emplace_back(std::move(edgePointers));
+                ++automatonIndex;
+            }
+            
+            return result;
         }
         
         template<typename ValueType, typename StateType>
@@ -279,7 +462,7 @@ namespace storm {
         storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices) {
             return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, {});
         }
-
+        
         template class JaniNextStateGenerator<double>;
         template class JaniNextStateGenerator<storm::RationalFunction>;
         

src/generator/JaniNextStateGenerator.h

@@ -27,6 +27,21 @@ namespace storm {
             virtual storm::models::sparse::StateLabeling label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices = {}) override;
             
         private:
+            /*!
+             * Retrieves the location index from the given state.
+             */
+            uint64_t getLocation(CompressedState const& state, LocationVariableInformation const& locationVariable) const;
+            
+            /*!
+             * Sets the location index from the given state.
+             */
+            void setLocation(CompressedState& state, LocationVariableInformation const& locationVariable, uint64_t locationIndex) const;
+            
+            /*!
+             * Retrieves the tuple of locations of the given state.
+             */
+            std::vector<uint64_t> getLocations(CompressedState const& state) const;
+            
             /*!
              * A delegate constructor that is used to preprocess the model before the constructor of the superclass is
              * being called. The last argument is only present to distinguish the signature of this constructor from the
@@ -46,18 +61,27 @@ namespace storm {
             /*!
              * Retrieves all choices labeled with the silent action possible from the given state.
              *
+             * @param locations The current locations of all automata.
              * @param state The state for which to retrieve the silent choices.
              * @return The silent action choices of the state.
              */
-            std::vector<Choice<ValueType>> getSilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
+            std::vector<Choice<ValueType>> getSilentActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback);
             
             /*!
              * Retrieves all choices labeled with some non-silent action possible from the given state.
              *
+             * @param locations THe current locations of all automata.
              * @param state The state for which to retrieve the non-silent choices.
              * @return The non-silent action choices of the state.
              */
-            std::vector<Choice<ValueType>> getNonsilentActionChoices(CompressedState const& state, StateToIdCallback stateToIdCallback);
+            std::vector<Choice<ValueType>> getNonsilentActionChoices(std::vector<uint64_t> const& locations, CompressedState const& state, StateToIdCallback stateToIdCallback);
+            
+            /*!
+             * Retrieves a list of lists of edges such that the list at index i are all edges of automaton i enabled in 
+             * the current state. If the list is empty, it means there was at least one automaton containing edges with
+             * the desired action, but none of them were enabled.
+             */
+            std::vector<std::vector<storm::jani::Edge const*>> getEnabledEdges(std::vector<uint64_t> const& locationIndices, uint64_t actionIndex);
             
             // The model used for the generation of next states.
             storm::jani::Model model;

src/generator/PrismNextStateGenerator.cpp

@@ -479,7 +479,7 @@ namespace storm {
                         
                         // Now, check whether there is one more command combination to consider.
                         bool movedIterator = false;
-                        for (int_fast64_t j = iteratorList.size() - 1; j >= 0; --j) {
+                        for (int_fast64_t j = iteratorList.size() - 1; !movedIterator && j >= 0; --j) {
                             ++iteratorList[j];
                             if (iteratorList[j] != activeCommandList[j].end()) {
                                 movedIterator = true;

src/storage/jani/Automaton.cpp

@@ -24,6 +24,10 @@ namespace storm {
                 return it == ite;
             }
             
+            std::size_t Edges::size() const {
+                return std::distance(it, ite);
+            }
+            
             ConstEdges::ConstEdges(const_iterator it, const_iterator ite) : it(it), ite(ite) {
                 // Intentionally left empty.
             }
@@ -39,6 +43,10 @@ namespace storm {
             bool ConstEdges::empty() const {
                 return it == ite;
             }
+
+            std::size_t ConstEdges::size() const {
+                return std::distance(it, ite);
+            }
         }
         
         Automaton::Automaton(std::string const& name) : name(name) {
@@ -138,6 +146,100 @@ namespace storm {
             return ConstEdges(it, ite);
         }
         
+        Automaton::Edges Automaton::getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) {
+            typedef std::vector<Edge>::iterator ForwardIt;
+
+            // Perform binary search for start of edges with the given action index.
+            auto first = edges.begin();
+            std::advance(first, locationToStartingIndex[locationIndex]);
+            auto last = edges.begin();
+            std::advance(last, locationToStartingIndex[locationIndex + 1]);
+            typename std::iterator_traits<ForwardIt>::difference_type count, step;
+            count = std::distance(first, last);
+            
+            ForwardIt it1;
+            while (count > 0) {
+                it1 = first;
+                step = count / 2;
+                std::advance(it1, step);
+                if (it1->getActionIndex() < actionIndex) {
+                    first = ++it1;
+                    count -= step + 1;
+                }
+                else {
+                    count = step;
+                }
+            }
+            
+            // If there is no such edge, we can return now.
+            if (it1 != last && it1->getActionIndex() > actionIndex) {
+                return Edges(last, last);
+            }
+            
+            // Otherwise, perform a binary search for the end of the edges with the given action index.
+            count = std::distance(first,last);
+            
+            ForwardIt it2;
+            while (count > 0) {
+                it2 = it1;
+                step = count / 2;
+                std::advance(it2, step);
+                if (!(actionIndex < it2->getActionIndex())) {
+                    first = ++it2;
+                    count -= step + 1;
+                } else count = step;
+            }
+            
+            return Edges(it1, it2);
+        }
+        
+        Automaton::ConstEdges Automaton::getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const {
+            typedef std::vector<Edge>::const_iterator ForwardIt;
+            
+            // Perform binary search for start of edges with the given action index.
+            auto first = edges.begin();
+            std::advance(first, locationToStartingIndex[locationIndex]);
+            auto last = edges.begin();
+            std::advance(last, locationToStartingIndex[locationIndex + 1]);
+            typename std::iterator_traits<ForwardIt>::difference_type count, step;
+            count = std::distance(first, last);
+            
+            ForwardIt it1;
+            while (count > 0) {
+                it1 = first;
+                step = count / 2;
+                std::advance(it1, step);
+                if (it1->getActionIndex() < actionIndex) {
+                    first = ++it1;
+                    count -= step + 1;
+                }
+                else {
+                    count = step;
+                }
+            }
+            
+            // If there is no such edge, we can return now.
+            if (it1 != last && it1->getActionIndex() > actionIndex) {
+                return ConstEdges(last, last);
+            }
+            
+            // Otherwise, perform a binary search for the end of the edges with the given action index.
+            count = std::distance(first,last);
+            
+            ForwardIt it2;
+            while (count > 0) {
+                it2 = it1;
+                step = count / 2;
+                std::advance(it2, step);
+                if (!(actionIndex < it2->getActionIndex())) {
+                    first = ++it2;
+                    count -= step + 1;
+                } else count = step;
+            }
+            
+            return ConstEdges(it1, it2);
+        }
+        
         void Automaton::addEdge(Edge const& edge) {
             STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'.");
             
@@ -151,6 +253,13 @@ namespace storm {
                 ++locationToStartingIndex[locationIndex];
             }
             
+            // Sort all edges form the source location of the newly introduced edge by their action indices.
+            auto it = edges.begin();
+            std::advance(it, locationToStartingIndex[edge.getSourceLocationIndex()]);
+            auto ite = edges.begin();
+            std::advance(ite, locationToStartingIndex[edge.getSourceLocationIndex() + 1]);
+            std::sort(it, ite, [] (Edge const& a, Edge const& b) { return a.getActionIndex() < b.getActionIndex(); } );
+            
             // Update the set of action indices of this automaton.
             actionIndices.insert(edge.getActionIndex());
         }

src/storage/jani/Automaton.h

@@ -3,6 +3,7 @@
 #include <string>
 #include <cstdint>
 #include <unordered_map>
+#include <boost/container/flat_set.hpp>
 
 #include "src/storage/jani/VariableSet.h"
 #include "src/storage/jani/Edge.h"
@@ -36,6 +37,11 @@ namespace storm {
                  */
                 bool empty() const;
                 
+                /*!
+                 * Retrieves the number of edges.
+                 */
+                std::size_t size() const;
+                
             private:
                 iterator it;
                 iterator ite;
@@ -62,6 +68,11 @@ namespace storm {
                  * Determines whether this set of edges is empty.
                  */
                 bool empty() const;
+
+                /*!
+                 * Retrieves the number of edges.
+                 */
+                std::size_t size() const;
                 
             private:
                 const_iterator it;
@@ -175,6 +186,16 @@ namespace storm {
              */
             ConstEdges getEdgesFromLocation(uint64_t index) const;
             
+            /*!
+             * Retrieves the edges of the location with the given index labeled with the given action index.
+             */
+            Edges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex);
+            
+            /*!
+             * Retrieves the edges of the location with the given index.
+             */
+            ConstEdges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const;
+            
             /*!
              * Adds an edge to the automaton.
              */

src/storage/jani/Model.cpp

@@ -47,6 +47,9 @@ namespace storm {
             STORM_LOG_THROW(it == actionToIndex.end(), storm::exceptions::WrongFormatException, "Action with name '" << action.getName() << "' already exists");
             actionToIndex.emplace(action.getName(), actions.size());
             actions.push_back(action);
+            if (action.getName() != SILENT_ACTION_NAME) {
+                nonsilentActionIndices.insert(actions.size() - 1);
+            }
             return actions.size() - 1;
         }
         
@@ -68,6 +71,10 @@ namespace storm {
             return actions;
         }
         
+        boost::container::flat_set<uint64_t> const& Model::getNonsilentActionIndices() const {
+            return nonsilentActionIndices;
+        }
+        
         uint64_t Model::addConstant(Constant const& constant) {
             auto it = constantToIndex.find(constant.getName());
             STORM_LOG_THROW(it == constantToIndex.end(), storm::exceptions::WrongFormatException, "Cannot add constant with name '" << constant.getName() << "', because a constant with that name already exists.");

src/storage/jani/Model.h

@@ -77,6 +77,11 @@ namespace storm {
              */
             std::vector<Action> const& getActions() const;
             
+            /*!
+             * Retrieves all non-silent action indices of the model.
+             */
+            boost::container::flat_set<uint64_t> const& getNonsilentActionIndices() const;
+            
             /*!
              * Adds the given constant to the model.
              */
@@ -288,6 +293,9 @@ namespace storm {
             /// A mapping from names to action indices.
             std::unordered_map<std::string, uint64_t> actionToIndex;
             
+            /// The set of non-silent action indices.
+            boost::container::flat_set<uint64_t> nonsilentActionIndices;
+            
             /// The index of the silent action.
             uint64_t silentActionIndex;
             

test/functional/builder/ExplicitJaniModelBuilderTest.cpp

@@ -0,0 +1,124 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+#include "src/models/sparse/StandardRewardModel.h"
+#include "src/settings/SettingMemento.h"
+#include "src/parser/PrismParser.h"
+#include "src/builder/ExplicitModelBuilder.h"
+#include "src/storage/jani/Model.h"
+
+#include "src/settings/modules/IOSettings.h"
+
+TEST(ExplicitJaniModelBuilderTest, Dtmc) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
+    storm::jani::Model janiModel = program.toJani();
+    
+    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(13ul, model->getNumberOfStates());
+    EXPECT_EQ(20ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/brp-16-2.pm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(677ul, model->getNumberOfStates());
+    EXPECT_EQ(867ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/crowds-5-5.pm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(8607ul, model->getNumberOfStates());
+    EXPECT_EQ(15113ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader-3-5.pm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(273ul, model->getNumberOfStates());
+    EXPECT_EQ(397ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/nand-5-2.pm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(1728ul, model->getNumberOfStates());
+    EXPECT_EQ(2505ul, model->getNumberOfTransitions());
+}
+
+TEST(ExplicitJaniModelBuilderTest, Ctmc) {
+    // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
+    std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
+    
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/cluster2.sm");
+    storm::jani::Model janiModel = program.toJani();
+
+    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+    EXPECT_EQ(276ul, model->getNumberOfStates());
+    EXPECT_EQ(1120ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/embedded2.sm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(3478ul, model->getNumberOfStates());
+    EXPECT_EQ(14639ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/polling2.sm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(12ul, model->getNumberOfStates());
+    EXPECT_EQ(22ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/fms2.sm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(810ul, model->getNumberOfStates());
+    EXPECT_EQ(3699ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/tandem5.sm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(66ul, model->getNumberOfStates());
+    EXPECT_EQ(189ul, model->getNumberOfTransitions());
+}
+
+TEST(ExplicitJaniModelBuilderTest, Mdp) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    storm::jani::Model janiModel = program.toJani();
+    
+    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+    EXPECT_EQ(169ul, model->getNumberOfStates());
+    EXPECT_EQ(436ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader3.nm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(364ul, model->getNumberOfStates());
+    EXPECT_EQ(654ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/coin2-2.nm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(272ul, model->getNumberOfStates());
+    EXPECT_EQ(492ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/csma2-2.nm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(1038ul, model->getNumberOfStates());
+    EXPECT_EQ(1282ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/firewire3-0.5.nm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(4093ul, model->getNumberOfStates());
+    EXPECT_EQ(5585ul, model->getNumberOfTransitions());
+    
+    program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+    janiModel = program.toJani();
+    model = storm::builder::ExplicitModelBuilder<double>(janiModel).build();
+    EXPECT_EQ(37ul, model->getNumberOfStates());
+    EXPECT_EQ(59ul, model->getNumberOfTransitions());
+}
+
+TEST(ExplicitJaniModelBuilderTest, Fail) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
+    storm::jani::Model janiModel = program.toJani();
+
+    ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(janiModel).build(), storm::exceptions::WrongFormatException);
+}

test/functional/builder/ExplicitPrismModelBuilderTest.cpp

@@ -7,7 +7,7 @@
 
 #include "src/settings/modules/IOSettings.h"
 
-TEST(ExplicitModelBuilderTest, Dtmc) {
+TEST(ExplicitPrismModelBuilderTest, Dtmc) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
@@ -35,7 +35,7 @@ TEST(ExplicitModelBuilderTest, Dtmc) {
     EXPECT_EQ(2505ul, model->getNumberOfTransitions());
 }
 
-TEST(ExplicitModelBuilderTest, Ctmc) {
+TEST(ExplicitPrismModelBuilderTest, Ctmc) {
     // Set the PRISM compatibility mode temporarily. It is set to its old value once the returned object is destructed.
     std::unique_ptr<storm::settings::SettingMemento> enablePrismCompatibility = storm::settings::mutableIOSettings().overridePrismCompatibilityMode(true);
 
@@ -66,7 +66,7 @@ TEST(ExplicitModelBuilderTest, Ctmc) {
     EXPECT_EQ(189ul, model->getNumberOfTransitions());
 }
 
-TEST(ExplicitModelBuilderTest, Mdp) {
+TEST(ExplicitPrismModelBuilderTest, Mdp) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
     
     std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
@@ -99,7 +99,7 @@ TEST(ExplicitModelBuilderTest, Mdp) {
     EXPECT_EQ(59ul, model->getNumberOfTransitions());
 }
 
-TEST(ExplicitModelBuilderTest, Fail) {
+TEST(ExplicitPrismModelBuilderTest, Fail) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/system_composition.nm");
 
     ASSERT_THROW(storm::builder::ExplicitModelBuilder<double>(program).build(), storm::exceptions::WrongFormatException);