JANI choice origins and MILP-based high-level cex for JANI

src/storm-cli-utilities/model-handling.h

@@ -377,8 +377,6 @@ namespace storm {
             
             auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
             if (counterexampleSettings.isMinimalCommandSetGenerationSet()) {
-                STORM_LOG_THROW(input.model && input.model.get().isPrismProgram(), storm::exceptions::NotSupportedException, "Minimal command set counterexamples are only supported for PRISM model input.");
-                storm::prism::Program const& program = input.model.get().asPrismProgram();
                 
                 bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet();
                 for (auto const& property : input.properties) {
@@ -387,13 +385,17 @@ namespace storm {
                     storm::utility::Stopwatch watch(true);
                     if (useMilp) {
                         STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MILP is currently only supported for MDPs.");
-                        counterexample = storm::api::computePrismHighLevelCounterexampleMilp(program, sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
+                        counterexample = storm::api::computeHighLevelCounterexampleMilp(input.model.get(), sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
                     } else {
                         STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MaxSAT is currently only supported for discrete-time models.");
+
+                        STORM_LOG_THROW(input.model && input.model.get().isPrismProgram(), storm::exceptions::NotSupportedException, "Minimal command set counterexamples are only supported for PRISM model input.");
+                        storm::prism::Program const& program = input.model.get().asPrismProgram();
+                        
                         if (sparseModel->isOfType(storm::models::ModelType::Dtmc)) {
-                            counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>(), property.getRawFormula());
+                            counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(program, sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>(), property.getRawFormula());
                         } else {
-                            counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
+                            counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(program, sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
                         }
                     }
                     watch.stop();

src/storm/api/counterexamples.cpp

@@ -5,12 +5,12 @@
 namespace storm {
     namespace api {
         
-        std::shared_ptr<storm::counterexamples::Counterexample> computePrismHighLevelCounterexampleMilp(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, std::shared_ptr<storm::logic::Formula const> const& formula) {
+        std::shared_ptr<storm::counterexamples::Counterexample> computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, std::shared_ptr<storm::logic::Formula const> const& formula) {
             Environment env;
-            return storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(env, program, *mdp, formula);
+            return storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(env, symbolicModel, *mdp, formula);
         }
         
-        std::shared_ptr<storm::counterexamples::Counterexample> computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
+        std::shared_ptr<storm::counterexamples::Counterexample> computeHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
             Environment env;
             return storm::counterexamples::SMTMinimalLabelSetGenerator<double>::computeCounterexample(env, program, *model, formula);
         }

src/storm/api/counterexamples.h

@@ -6,9 +6,9 @@
 namespace storm {
     namespace api {
         
-        std::shared_ptr<storm::counterexamples::Counterexample> computePrismHighLevelCounterexampleMilp(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, std::shared_ptr<storm::logic::Formula const> const& formula);
+        std::shared_ptr<storm::counterexamples::Counterexample> computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, std::shared_ptr<storm::logic::Formula const> const& formula);
         
-        std::shared_ptr<storm::counterexamples::Counterexample> computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula);
+        std::shared_ptr<storm::counterexamples::Counterexample> computeHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula);
         
     }
 }

src/storm/builder/ChoiceInformationBuilder.cpp

@@ -10,7 +10,7 @@ namespace storm {
         }
         
         void ChoiceInformationBuilder::addOriginData(boost::any const& originData, uint_fast64_t choiceIndex) {
-            if(dataOfOrigins.size() != choiceIndex) {
+            if (dataOfOrigins.size() != choiceIndex) {
                 dataOfOrigins.resize(choiceIndex);
             }
             dataOfOrigins.push_back(originData);

src/storm/builder/ChoiceInformationBuilder.h

@@ -31,7 +31,6 @@ namespace storm {
             
             std::vector<boost::any> buildDataOfChoiceOrigins(uint_fast64_t totalNumberOfChoices);
             
-            
         private:
             std::unordered_map<std::string, storm::storage::BitVector> labels;
             std::vector<boost::any> dataOfOrigins;

src/storm/counterexamples/HighLevelCounterexample.cpp

@@ -0,0 +1,28 @@
+#include "storm/counterexamples/HighLevelCounterexample.h"
+
+namespace storm {
+    namespace counterexamples {
+        
+        HighLevelCounterexample::HighLevelCounterexample(storm::storage::SymbolicModelDescription const& model) : model(model) {
+            // Intentionally left empty.
+        }
+        
+        bool HighLevelCounterexample::isPrismHighLevelCounterexample() const {
+            return model.isPrismProgram();
+        }
+        
+        bool HighLevelCounterexample::isJaniHighLevelCounterexample() const {
+            return model.isJaniModel();
+        }
+        
+        storm::storage::SymbolicModelDescription const& HighLevelCounterexample::getModelDescription() const {
+            return model;
+        }
+        
+        void HighLevelCounterexample::writeToStream(std::ostream& out) const {
+            out << "High-level counterexample: " << std::endl;
+            out << model;
+        }
+        
+    }
+}

src/storm/counterexamples/HighLevelCounterexample.h

@@ -0,0 +1,26 @@
+#pragma once
+
+#include "storm/counterexamples/Counterexample.h"
+
+#include "storm/storage/SymbolicModelDescription.h"
+
+namespace storm {
+    namespace counterexamples {
+        
+        class HighLevelCounterexample : public Counterexample {
+        public:
+            HighLevelCounterexample(storm::storage::SymbolicModelDescription const& model);
+
+            void writeToStream(std::ostream& out) const override;
+            
+            bool isPrismHighLevelCounterexample() const;
+            bool isJaniHighLevelCounterexample() const;
+
+            storm::storage::SymbolicModelDescription const& getModelDescription() const;
+            
+        private:
+            storm::storage::SymbolicModelDescription model;
+        };
+        
+    }
+}

src/storm/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -1,5 +1,4 @@
-#ifndef STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_
-#define STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_
+#pragma once
 
 #include <chrono>
 #include <boost/container/flat_set.hpp>
@@ -18,7 +17,7 @@
 
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 
-#include "storm/counterexamples/PrismHighLevelCounterexample.h"
+#include "storm/counterexamples/HighLevelCounterexample.h"
 
 #include "storm/utility/graph.h"
 #include "storm/utility/counterexamples.h"
@@ -26,6 +25,7 @@
 #include "storm/solver/LpSolver.h"
 
 #include "storm/storage/sparse/PrismChoiceOrigins.h"
+#include "storm/storage/sparse/JaniChoiceOrigins.h"
 
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/GeneralSettings.h"
@@ -976,12 +976,12 @@ namespace storm {
              * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested
              * formula can be either an unbounded until formula or an eventually formula.
              */
-            static std::shared_ptr<PrismHighLevelCounterexample> computeCounterexample(Environment const& env, storm::prism::Program const& program, storm::models::sparse::Mdp<T> const& mdp, std::shared_ptr<storm::logic::Formula const> const& formula) {
+            static std::shared_ptr<HighLevelCounterexample> computeCounterexample(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Mdp<T> const& mdp, std::shared_ptr<storm::logic::Formula const> const& formula) {
                 std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl;
                 
                 // Check whether there are choice origins available
                 STORM_LOG_THROW(mdp.hasChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to minimal command set is impossible for model without choice origns.");
-                STORM_LOG_THROW(mdp.getChoiceOrigins()->isPrismChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without prism choice origins.");
+                STORM_LOG_THROW(mdp.getChoiceOrigins()->isPrismChoiceOrigins() || mdp.getChoiceOrigins()->isJaniChoiceOrigins(), storm::exceptions::InvalidArgumentException, "Restriction to command set is impossible for model without PRISM or JANI choice origins.");
                 
                 STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException, "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
                 storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula();
@@ -1020,21 +1020,34 @@ namespace storm {
                 }
                 
                 // Obtain the label sets for each choice.
-                // The label set of a choice corresponds to the set of prism commands that induce the choice.
-                storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins();
-                std::vector<boost::container::flat_set<uint_fast64_t>> labelSets;
-                labelSets.reserve(mdp.getNumberOfChoices());
-                for (uint_fast64_t choice = 0; choice < mdp.getNumberOfChoices(); ++choice) {
-                    labelSets.push_back(choiceOrigins.getCommandSet(choice));
+                std::vector<boost::container::flat_set<uint_fast64_t>> labelSets(mdp.getNumberOfChoices());
+                if (mdp.getChoiceOrigins()->isPrismChoiceOrigins()) {
+                    storm::storage::sparse::PrismChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asPrismChoiceOrigins();
+                    for (uint_fast64_t choice = 0; choice < mdp.getNumberOfChoices(); ++choice) {
+                        labelSets[choice] = choiceOrigins.getCommandSet(choice);
+                    }
+                } else {
+                    storm::storage::sparse::JaniChoiceOrigins const& choiceOrigins = mdp.getChoiceOrigins()->asJaniChoiceOrigins();
+
+                    // The choice origins are known to be JANI ones at this point.
+                    for (uint_fast64_t choice = 0; choice < mdp.getNumberOfChoices(); ++choice) {
+                        labelSets[choice] = choiceOrigins.getEdgeIndexSet(choice);
+                    }
                 }
                 
                 // Delegate the actual computation work to the function of equal name.
                 auto startTime = std::chrono::high_resolution_clock::now();
-                boost::container::flat_set<uint_fast64_t> usedCommandSet = getMinimalLabelSet(env, mdp, labelSets, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isUseSchedulerCutsSet());
+                boost::container::flat_set<uint_fast64_t> usedLabelSet = getMinimalLabelSet(env, mdp, labelSets, phiStates, psiStates, threshold, strictBound, true, storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>().isUseSchedulerCutsSet());
                 auto endTime = std::chrono::high_resolution_clock::now();
-                std::cout << std::endl << "Computed minimal command set of size " << usedCommandSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
+                std::cout << std::endl << "Computed minimal command set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
 
-                return std::make_shared<PrismHighLevelCounterexample>(program.restrictCommands(usedCommandSet));
+                
+                if (symbolicModel.isPrismProgram()) {
+                    return std::make_shared<HighLevelCounterexample>(symbolicModel.asPrismProgram().restrictCommands(usedLabelSet));
+                } else {
+                    STORM_LOG_ASSERT(symbolicModel.isJaniModel(), "Unknown symbolic model description type.");
+                    return std::make_shared<HighLevelCounterexample>(symbolicModel.asJaniModel().restrictEdges(usedLabelSet));
+                }
             }
             
         };
@@ -1042,4 +1055,3 @@ namespace storm {
     } // namespace counterexamples
 } // namespace storm
 
-#endif /* STORM_COUNTEREXAMPLES_MILPMINIMALLABELSETGENERATOR_MDP_H_ */

src/storm/counterexamples/PrismHighLevelCounterexample.cpp

@@ -1,16 +0,0 @@
-#include "storm/counterexamples/PrismHighLevelCounterexample.h"
-
-namespace storm {
-    namespace counterexamples {
-        
-        PrismHighLevelCounterexample::PrismHighLevelCounterexample(storm::prism::Program const& program) : program(program) {
-            // Intentionally left empty.
-        }
-        
-        void PrismHighLevelCounterexample::writeToStream(std::ostream& out) const {
-            out << "High-level counterexample (PRISM program): " << std::endl;
-            out << program;
-        }
-        
-    }
-}

src/storm/counterexamples/PrismHighLevelCounterexample.h

@@ -1,21 +0,0 @@
-#pragma once
-
-#include "storm/counterexamples/Counterexample.h"
-
-#include "storm/storage/prism/Program.h"
-
-namespace storm {
-    namespace counterexamples {
-        
-        class PrismHighLevelCounterexample : public Counterexample {
-        public:
-            PrismHighLevelCounterexample(storm::prism::Program const& program);
-
-            void writeToStream(std::ostream& out) const override;
-            
-        private:
-            storm::prism::Program program;
-        };
-        
-    }
-}

src/storm/counterexamples/SMTMinimalLabelSetGenerator.h

@@ -5,7 +5,7 @@
 
 #include "storm/solver/Z3SmtSolver.h"
 
-#include "storm/counterexamples/PrismHighLevelCounterexample.h"
+#include "storm/counterexamples/HighLevelCounterexample.h"
 
 #include "storm/storage/prism/Program.h"
 #include "storm/storage/expressions/Expression.h"
@@ -1875,11 +1875,11 @@ namespace storm {
                 return commandSet;
             }
 
-            static std::shared_ptr<PrismHighLevelCounterexample> computeCounterexample(Environment const& env, storm::prism::Program program, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula) {
+            static std::shared_ptr<HighLevelCounterexample> computeCounterexample(Environment const& env, storm::prism::Program program, storm::models::sparse::Model<T> const& model, std::shared_ptr<storm::logic::Formula const> const& formula) {
 #ifdef STORM_HAVE_Z3
                 auto commandSet = computeCounterexampleCommandSet(env, program, model, formula);
                 
-                return std::make_shared<PrismHighLevelCounterexample>(program.restrictCommands(commandSet));
+                return std::make_shared<HighLevelCounterexample>(program.restrictCommands(commandSet));
 
 #else
                 throw storm::exceptions::NotImplementedException() << "This functionality is unavailable since storm has been compiled without support for Z3.";

src/storm/generator/JaniNextStateGenerator.cpp

@@ -15,6 +15,8 @@
 #include "storm/storage/jani/ParallelComposition.h"
 #include "storm/storage/jani/CompositionInformationVisitor.h"
 
+#include "storm/storage/sparse/JaniChoiceOrigins.h"
+
 #include "storm/builder/jit/Distribution.h"
 
 #include "storm/utility/constants.h"
@@ -338,6 +340,10 @@ namespace storm {
                     for (uint_fast64_t rewardVariableIndex = 0; rewardVariableIndex < rewardVariables.size(); ++rewardVariableIndex) {
                         stateActionRewards[rewardVariableIndex] += choice.getRewards()[rewardVariableIndex] * choice.getTotalMass() / totalExitRate;
                     }
+                    
+                    if (this->options.isBuildChoiceOriginsSet() && choice.hasOriginData()) {
+                        globalChoice.addOriginData(choice.getOriginData());
+                    }
                 }
                 globalChoice.addRewards(std::move(stateActionRewards));
                 
@@ -408,7 +414,7 @@ namespace storm {
                 checkGlobalVariableWritesValid(edgeCombination);
             }
             
-            std::vector<EdgeSet::const_iterator> iteratorList(edgeCombination.size());
+            std::vector<EdgeSetWithIndices::const_iterator> iteratorList(edgeCombination.size());
             
             // Initialize the list of iterators.
             for (size_t i = 0; i < edgeCombination.size(); ++i) {
@@ -425,8 +431,15 @@ namespace storm {
                 
                 currentDistribution.add(state, storm::utility::one<ValueType>());
                 
+                EdgeIndexSet edgeIndices;
                 for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
-                    storm::jani::Edge const& edge = **iteratorList[i];
+                    auto const& indexAndEdge = *iteratorList[i];
+                    
+                    if (this->getOptions().isBuildChoiceOriginsSet()) {
+                        edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[i].first, indexAndEdge.first));
+                    }
+                    
+                    storm::jani::Edge const& edge = *indexAndEdge.second;
                     
                     for (auto const& destination : edge.getDestinations()) {
                         for (auto const& stateProbability : currentDistribution) {
@@ -465,6 +478,11 @@ namespace storm {
                 // Now create the actual distribution.
                 Choice<ValueType>& choice = result.back();
                 
+                // Add the edge indices if requested.
+                if (this->getOptions().isBuildChoiceOriginsSet()) {
+                    choice.addOriginData(boost::any(std::move(edgeIndices)));
+                }
+                
                 // Add the rewards to the choice.
                 choice.addRewards(std::move(stateActionRewards));
                 
@@ -515,12 +533,17 @@ namespace storm {
 
                     auto edgesIt = nonsychingEdges.second.find(locations[automatonIndex]);
                     if (edgesIt != nonsychingEdges.second.end()) {
-                        for (auto const& edge : edgesIt->second) {
-                            if (!this->evaluator->asBool(edge->getGuard())) {
+                        for (auto const& indexAndEdge : edgesIt->second) {
+                            if (!this->evaluator->asBool(indexAndEdge.second->getGuard())) {
                                 continue;
                             }
                         
-                            Choice<ValueType> choice = expandNonSynchronizingEdge(*edge, outputAndEdges.first ? outputAndEdges.first.get() : edge->getActionIndex(), automatonIndex, state, stateToIdCallback);
+                            Choice<ValueType> choice = expandNonSynchronizingEdge(*indexAndEdge.second, outputAndEdges.first ? outputAndEdges.first.get() : indexAndEdge.second->getActionIndex(), automatonIndex, state, stateToIdCallback);
+
+                            if (this->getOptions().isBuildChoiceOriginsSet()) {
+                                EdgeIndexSet edgeIndex { model.encodeAutomatonAndEdgeIndices(automatonIndex, indexAndEdge.first) };
+                                choice.addOriginData(boost::any(std::move(edgeIndex)));
+                            }
                             result.emplace_back(std::move(choice));
                         }
                     }
@@ -534,18 +557,18 @@ namespace storm {
                     bool productiveCombination = true;
                     for (auto const& automatonAndEdges : outputAndEdges.second) {
                         uint64_t automatonIndex = automatonAndEdges.first;
-                        EdgeSet enabledEdgesOfAutomaton;
+                        EdgeSetWithIndices enabledEdgesOfAutomaton;
                         
                         bool atLeastOneEdge = false;
                         auto edgesIt = automatonAndEdges.second.find(locations[automatonIndex]);
                         if (edgesIt != automatonAndEdges.second.end()) {
-                            for (auto const& edge : edgesIt->second) {
-                                if (!this->evaluator->asBool(edge->getGuard())) {
+                            for (auto const& indexAndEdge : edgesIt->second) {
+                                if (!this->evaluator->asBool(indexAndEdge.second->getGuard())) {
                                     continue;
                                 }
                             
                                 atLeastOneEdge = true;
-                                enabledEdgesOfAutomaton.emplace_back(edge);
+                                enabledEdgesOfAutomaton.emplace_back(indexAndEdge);
                             }
                         }
 
@@ -575,8 +598,8 @@ namespace storm {
         void JaniNextStateGenerator<ValueType, StateType>::checkGlobalVariableWritesValid(AutomataEdgeSets const& enabledEdges) const {
             std::map<storm::expressions::Variable, uint64_t> writtenGlobalVariables;
             for (auto edgeSetIt = enabledEdges.begin(), edgeSetIte = enabledEdges.end(); edgeSetIt != edgeSetIte; ++edgeSetIt) {
-                for (auto const& edge : edgeSetIt->second) {
-                    for (auto const& globalVariable : edge->getWrittenGlobalVariables()) {
+                for (auto const& indexAndEdge : edgeSetIt->second) {
+                    for (auto const& globalVariable : indexAndEdge.second->getWrittenGlobalVariables()) {
                         auto it = writtenGlobalVariables.find(globalVariable);
                         
                         auto index = std::distance(enabledEdges.begin(), edgeSetIt);
@@ -707,8 +730,10 @@ namespace storm {
                 this->parallelAutomata.push_back(automaton);
                 
                 LocationsAndEdges locationsAndEdges;
+                uint64_t edgeIndex = 0;
                 for (auto const& edge : automaton.getEdges()) {
-                    locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(&edge);
+                    locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(std::make_pair(edgeIndex, &edge));
+                    ++edgeIndex;
                 }
                 
                 AutomataAndEdges automataAndEdges;
@@ -726,10 +751,12 @@ namespace storm {
                 
                     // Add edges with silent action.
                     LocationsAndEdges locationsAndEdges;
+                    uint64_t edgeIndex = 0;
                     for (auto const& edge : parallelAutomata.back().get().getEdges()) {
                         if (edge.getActionIndex() == storm::jani::Model::SILENT_ACTION_INDEX) {
-                            locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(&edge);
+                            locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(std::make_pair(edgeIndex, &edge));
                         }
+                        ++edgeIndex;
                     }
 
                     if (!locationsAndEdges.empty()) {
@@ -750,10 +777,12 @@ namespace storm {
                         if (!storm::jani::SynchronizationVector::isNoActionInput(element)) {
                             LocationsAndEdges locationsAndEdges;
                             uint64_t actionIndex = this->model.getActionIndex(element);
+                            uint64_t edgeIndex = 0;
                             for (auto const& edge : parallelAutomata[automatonIndex].get().getEdges()) {
                                 if (edge.getActionIndex() == actionIndex) {
-                                    locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(&edge);
+                                    locationsAndEdges[edge.getSourceLocationIndex()].emplace_back(std::make_pair(edgeIndex, &edge));
                                 }
+                                ++edgeIndex;
                             }
                             if (locationsAndEdges.empty()) {
                                 atLeastOneEdge = false;
@@ -773,6 +802,39 @@ namespace storm {
             STORM_LOG_TRACE("Number of synchronizations: " << this->edges.size() << ".");
         }
         
+        template<typename ValueType, typename StateType>
+        std::shared_ptr<storm::storage::sparse::ChoiceOrigins> JaniNextStateGenerator<ValueType, StateType>::generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const {
+            if (!this->getOptions().isBuildChoiceOriginsSet()) {
+                return nullptr;
+            }
+            
+            std::vector<uint_fast64_t> identifiers;
+            identifiers.reserve(dataForChoiceOrigins.size());
+            
+            std::map<EdgeIndexSet, uint_fast64_t> edgeIndexSetToIdentifierMap;
+            // The empty edge set (i.e., the choices without origin) always has to get identifier getIdentifierForChoicesWithNoOrigin() -- which is assumed to be 0
+            STORM_LOG_ASSERT(storm::storage::sparse::ChoiceOrigins::getIdentifierForChoicesWithNoOrigin() == 0, "The no origin identifier is assumed to be zero");
+            edgeIndexSetToIdentifierMap.insert(std::make_pair(EdgeIndexSet(), 0));
+            uint_fast64_t currentIdentifier = 1;
+            for (boost::any& originData : dataForChoiceOrigins) {
+                STORM_LOG_ASSERT(originData.empty() || boost::any_cast<EdgeIndexSet>(&originData) != nullptr, "Origin data has unexpected type: " << originData.type().name() << ".");
+                
+                EdgeIndexSet currentEdgeIndexSet = originData.empty() ? EdgeIndexSet() : boost::any_cast<EdgeIndexSet>(std::move(originData));
+                auto insertionRes = edgeIndexSetToIdentifierMap.emplace(std::move(currentEdgeIndexSet), currentIdentifier);
+                identifiers.push_back(insertionRes.first->second);
+                if (insertionRes.second) {
+                    ++currentIdentifier;
+                }
+            }
+            
+            std::vector<EdgeIndexSet> identifierToEdgeIndexSetMapping(currentIdentifier);
+            for (auto const& setIdPair : edgeIndexSetToIdentifierMap) {
+                identifierToEdgeIndexSetMapping[setIdPair.second] = setIdPair.first;
+            }
+            
+            return std::make_shared<storm::storage::sparse::JaniChoiceOrigins>(std::make_shared<storm::jani::Model>(model), std::move(identifiers), std::move(identifierToEdgeIndexSetMapping));
+        }
+        
         template<typename ValueType, typename StateType>
         void JaniNextStateGenerator<ValueType, StateType>::checkValid() const {
             // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.

src/storm/generator/JaniNextStateGenerator.h

@@ -1,5 +1,7 @@
 #pragma once
 
+#include <boost/container/flat_set.hpp>
+
 #include "storm/generator/NextStateGenerator.h"
 
 #include "storm/storage/jani/Model.h"
@@ -17,6 +19,7 @@ namespace storm {
         class JaniNextStateGenerator : public NextStateGenerator<ValueType, StateType> {
         public:
             typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
+            typedef boost::container::flat_set<uint_fast64_t> EdgeIndexSet;
             
             JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options = NextStateGeneratorOptions());
             
@@ -32,6 +35,8 @@ namespace storm {
                         
             virtual storm::models::sparse::StateLabeling label(storm::storage::sparse::StateStorage<StateType> const& stateStorage, std::vector<StateType> const& initialStateIndices = {}, std::vector<StateType> const& deadlockStateIndices = {}) override;
             
+            virtual std::shared_ptr<storm::storage::sparse::ChoiceOrigins> generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const override;
+            
         private:
             /*!
              * Retrieves the location index from the given state.
@@ -79,12 +84,12 @@ namespace storm {
              */
             Choice<ValueType> expandNonSynchronizingEdge(storm::jani::Edge const& edge, uint64_t outputActionIndex, uint64_t automatonIndex, CompressedState const& state, StateToIdCallback stateToIdCallback);
             
-            typedef std::vector<storm::jani::Edge const*> EdgeSet;
-            typedef std::unordered_map<uint64_t, EdgeSet> LocationsAndEdges;
+            typedef std::vector<std::pair<uint64_t, storm::jani::Edge const*>> EdgeSetWithIndices;
+            typedef std::unordered_map<uint64_t, EdgeSetWithIndices> LocationsAndEdges;
             typedef std::vector<std::pair<uint64_t, LocationsAndEdges>> AutomataAndEdges;
             typedef std::pair<boost::optional<uint64_t>, AutomataAndEdges> OutputAndEdges;
 
-            typedef std::pair<uint64_t, EdgeSet> AutomatonAndEdgeSet;
+            typedef std::pair<uint64_t, EdgeSetWithIndices> AutomatonAndEdgeSet;
             typedef std::vector<AutomatonAndEdgeSet> AutomataEdgeSets;
             
             std::vector<Choice<ValueType>> expandSynchronizingEdgeCombination(AutomataEdgeSets const& edgeCombination, uint64_t outputActionIndex, CompressedState const& state, StateToIdCallback stateToIdCallback);

src/storm/generator/PrismNextStateGenerator.cpp

@@ -601,7 +601,6 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         std::shared_ptr<storm::storage::sparse::ChoiceOrigins> PrismNextStateGenerator<ValueType, StateType>::generateChoiceOrigins(std::vector<boost::any>& dataForChoiceOrigins) const {
-            
             if (!this->getOptions().isBuildChoiceOriginsSet()) {
                 return nullptr;
             }

src/storm/storage/SymbolicModelDescription.cpp

@@ -178,5 +178,16 @@ namespace storm {
                 storm::utility::prism::requireNoUndefinedConstants(this->asPrismProgram());
             }
         }
+        
+        std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model) {
+            if (model.isPrismProgram()) {
+                out << model.asPrismProgram();
+            } else if (model.isJaniModel()) {
+                out << model.asJaniModel();
+            } else {
+                out << "unkown symbolic model description";
+            }
+            return out;
+        }
     }
 }

src/storm/storage/SymbolicModelDescription.h

@@ -52,5 +52,7 @@ namespace storm {
             boost::optional<boost::variant<storm::jani::Model, storm::prism::Program>> modelDescription;
         };
         
+        std::ostream& operator<<(std::ostream& out, SymbolicModelDescription const& model);
+        
     }
 }

src/storm/storage/jani/Automaton.cpp

@@ -301,8 +301,6 @@ namespace storm {
             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() << "'.");
             
@@ -529,6 +527,20 @@ namespace storm {
             return result;
         }
 
+        void Automaton::restrictToEdges(boost::container::flat_set<uint_fast64_t> const& edgeIndices) {
+            std::vector<Edge> oldEdges = this->edges;
+            
+            this->edges.clear();
+            actionIndices.clear();
+            for (auto& e : locationToStartingIndex) {
+                e = 0;
+            }
+
+            for (auto const& index : edgeIndices) {
+                this->addEdge(oldEdges[index]);
+            }
+        }
+        
         void Automaton::writeDotToStream(std::ostream& outStream, std::vector<std::string> const& actionNames) const {
             outStream << "\tsubgraph " << name << " {" << std::endl;
 

src/storm/storage/jani/Automaton.h

@@ -374,6 +374,11 @@ namespace storm {
 
             void writeDotToStream(std::ostream& outStream, std::vector<std::string> const& actionNames) const;
             
+            /*!
+             * Restricts the automaton to the edges given by the indices. All other edges are deleted.
+             */
+            void restrictToEdges(boost::container::flat_set<uint_fast64_t> const& edgeIndices);
+            
         private:
             /// The name of the automaton.
             std::string name;

src/storm/storage/jani/Model.cpp

@@ -15,6 +15,7 @@
 #include "storm/storage/jani/ParallelComposition.h"
 #include "storm/storage/jani/CompositionInformationVisitor.h"
 #include "storm/storage/jani/Compositions.h"
+#include "storm/storage/jani/JSONExporter.h"
 
 #include "storm/storage/expressions/LinearityCheckVisitor.h"
 
@@ -1155,6 +1156,35 @@ namespace storm {
             return false;
         }
         
+        uint64_t Model::encodeAutomatonAndEdgeIndices(uint64_t automatonIndex, uint64_t edgeIndex) const {
+            return automatonIndex << 32 | edgeIndex;
+        }
+        
+        std::pair<uint64_t, uint64_t> Model::decodeAutomatonAndEdgeIndices(uint64_t index) const {
+            return std::make_pair(index >> 32, index & ((1ull << 32) - 1));
+        }
+
+        Model Model::restrictEdges(boost::container::flat_set<uint_fast64_t> const& automataAndEdgeIndices) const {
+            Model result(*this);
+
+            // Restrict all automata.
+            for (uint64_t automatonIndex = 0; automatonIndex < result.automata.size(); ++automatonIndex) {
+                
+                // Compute the set of edges that is to be kept for this automaton.
+                boost::container::flat_set<uint_fast64_t> automatonEdgeIndices;
+                for (auto const& e : automataAndEdgeIndices) {
+                    auto automatonAndEdgeIndex = decodeAutomatonAndEdgeIndices(e);
+                    if (automatonAndEdgeIndex.first == automatonIndex) {
+                        automatonEdgeIndices.insert(automatonAndEdgeIndex.second);
+                    }
+                }
+                
+                result.automata[automatonIndex].restrictToEdges(automatonEdgeIndices);
+            }
+            
+            return result;
+        }
+        
         Model Model::createModelFromAutomaton(Automaton const& automaton) const {
             // Copy the full model
             Model newModel(*this);
@@ -1194,5 +1224,10 @@ namespace storm {
 
             outStream << "}";
         }
+        
+        std::ostream& operator<<(std::ostream& out, Model const& model) {
+            JsonExporter::toStream(model, std::vector<storm::jani::Property>(), out);
+            return out;
+        }
     }
 }

src/storm/storage/jani/Model.h

@@ -449,6 +449,18 @@ namespace storm {
              */
             bool reusesActionsInComposition() const;
 
+            /*!
+             * Encode and decode a tuple of automaton and edge index in one 64-bit index.
+             */
+            uint64_t encodeAutomatonAndEdgeIndices(uint64_t automatonIndex, uint64_t edgeIndex) const;
+            std::pair<uint64_t, uint64_t> decodeAutomatonAndEdgeIndices(uint64_t index) const;
+
+            /*!
+             * Creates a new model that only contains the selected edges. The edge indices encode the automata and
+             * (local) indices of the edges within the automata.
+             */
+            Model restrictEdges(boost::container::flat_set<uint_fast64_t> const& automataAndEdgeIndices) const;
+            
             void writeDotToStream(std::ostream& outStream = std::cout) const;
             
             /// The name of the silent action.
@@ -505,6 +517,8 @@ namespace storm {
             // The expression restricting the legal initial values of the global variables.
             storm::expressions::Expression initialStatesRestriction;
         };
+        
+        std::ostream& operator<<(std::ostream& out, Model const& model);
     }
 }
 

src/storm/storage/sparse/JaniChoiceOrigins.cpp

@@ -1,14 +1,16 @@
 #include "storm/storage/sparse/JaniChoiceOrigins.h"
 
+#include "storm/storage/jani/Model.h"
+
 #include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidArgumentException.h"
 
 namespace storm {
     namespace storage {
         namespace sparse {
             
-            JaniChoiceOrigins::JaniChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping) : ChoiceOrigins(indexToIdentifierMapping) {
-				// Intentionally left empty
-                STORM_LOG_ASSERT(false, "Jani choice origins not properly implemented");
+            JaniChoiceOrigins::JaniChoiceOrigins(std::shared_ptr<storm::jani::Model const> const& janiModel, std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<EdgeIndexSet> const& identifierToEdgeIndexSetMapping) : ChoiceOrigins(indexToIdentifierMapping), model(janiModel), identifierToEdgeIndexSet(identifierToEdgeIndexSetMapping) {
+                STORM_LOG_THROW(identifierToEdgeIndexSet[this->getIdentifierForChoicesWithNoOrigin()].empty(), storm::exceptions::InvalidArgumentException, "The given edge set for the choices without origin is non-empty");
 			}
 
             bool JaniChoiceOrigins::isJaniChoiceOrigins() const  {
@@ -16,15 +18,25 @@ namespace storm {
             }
             
             uint_fast64_t JaniChoiceOrigins::getNumberOfIdentifiers() const {
-                return 0;
+                return identifierToEdgeIndexSet.size();
+            }
+            
+            storm::jani::Model const& JaniChoiceOrigins::getModel() const {
+                return *model;
+            }
+            
+            JaniChoiceOrigins::EdgeIndexSet const& JaniChoiceOrigins::getEdgeIndexSet(uint_fast64_t choiceIndex) const {
+                return identifierToEdgeIndexSet[this->getIdentifier(choiceIndex)];
             }
             
             std::shared_ptr<ChoiceOrigins> JaniChoiceOrigins::cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const {
-                return std::make_shared<JaniChoiceOrigins>(std::move(indexToIdentifierMapping));
+                auto result = std::make_shared<JaniChoiceOrigins>(this->model, std::move(indexToIdentifierMapping), std::move(identifierToEdgeIndexSet));
+                result->identifierToInfo = this->identifierToInfo;
+                return result;
             }
             
             void JaniChoiceOrigins::computeIdentifierInfos() const {
-                
+                STORM_LOG_ASSERT(false, "Jani choice origins not properly implemented");
             }
             
         }

src/storm/storage/sparse/JaniChoiceOrigins.h

@@ -3,25 +3,30 @@
 #include <memory>
 #include <string>
 
-#include "storm/storage/sparse/ChoiceOrigins.h"
+#include <boost/container/flat_set.hpp>
 
+#include "storm/storage/sparse/ChoiceOrigins.h"
 
 namespace storm {
+    namespace jani {
+        class Model;
+    }
+    
     namespace storage {
         namespace sparse {
             
-            
             /*!
              * This class represents for each choice the origin in the jani specification
              * // TODO complete this
              */
             class JaniChoiceOrigins : public ChoiceOrigins {
             public:
+                typedef boost::container::flat_set<uint_fast64_t> EdgeIndexSet;
 
                 /*!
                  * Creates a new representation of the choice indices to their origin in the Jani specification
                  */
-                JaniChoiceOrigins(std::vector<uint_fast64_t> const& indexToIdentifierMapping);
+                JaniChoiceOrigins(std::shared_ptr<storm::jani::Model const> const& janiModel, std::vector<uint_fast64_t> const& indexToIdentifierMapping, std::vector<EdgeIndexSet> const& identifierToEdgeIndexSetMapping);
                 
                 virtual ~JaniChoiceOrigins() = default;
                 
@@ -33,6 +38,18 @@ namespace storm {
                  */
                 virtual uint_fast64_t getNumberOfIdentifiers() const override;
                 
+                /*!
+                 * Retrieves the associated JANI model.
+                 */
+                storm::jani::Model const& getModel() const;
+                
+                /*
+                 * Returns the set of edges that induced the choice with the given index.
+                 * The edges set is represented by a set of indices that encode an automaton index and its local edge index.
+                 */
+                EdgeIndexSet const& getEdgeIndexSet(uint_fast64_t choiceIndex) const;
+                
+            private:
                 /*
                  * Returns a copy of this object where the mapping of choice indices to origin identifiers is replaced by the given one.
                  */
@@ -43,8 +60,8 @@ namespace storm {
                  */
                 virtual void computeIdentifierInfos() const override;
                 
-            private:
-                
+                std::shared_ptr<storm::jani::Model const> model;
+                std::vector<EdgeIndexSet> identifierToEdgeIndexSet;
             };
         }
     }

src/storm/storage/sparse/PrismChoiceOrigins.cpp

@@ -35,8 +35,7 @@ namespace storm {
 			}
             
             std::shared_ptr<ChoiceOrigins> PrismChoiceOrigins::cloneWithNewIndexToIdentifierMapping(std::vector<uint_fast64_t>&& indexToIdentifierMapping) const {
-                std::vector<CommandSet> identifierToCommandSetMapping = this->identifierToCommandSet;
-                auto result = std::make_shared<PrismChoiceOrigins>(this->program, std::move(indexToIdentifierMapping), std::move(identifierToCommandSetMapping));
+                auto result = std::make_shared<PrismChoiceOrigins>(this->program, std::move(indexToIdentifierMapping), std::move(this->identifierToCommandSet));
                 result->identifierToInfo = this->identifierToInfo;
                 return result;
             }

src/storm/storage/sparse/PrismChoiceOrigins.h

@@ -32,7 +32,7 @@ namespace storm {
                 
                 virtual ~PrismChoiceOrigins() = default;
                 
-                virtual bool isPrismChoiceOrigins() const override ;
+                virtual bool isPrismChoiceOrigins() const override;
                 
                 /*
                  * Returns the number of identifier that are used by this object.