first version of jani menu-game abstraction

src/storm/abstraction/GameBddResult.cpp

@@ -2,20 +2,19 @@
 
 namespace storm {
     namespace abstraction {
-        namespace prism {
-         
-            template <storm::dd::DdType DdType>
-            GameBddResult<DdType>::GameBddResult() : bdd(), numberOfPlayer2Variables(0) {
-                // Intentionally left empty.
-            }
-            
-            template <storm::dd::DdType DdType>
-            GameBddResult<DdType>::GameBddResult(storm::dd::Bdd<DdType> const& gameBdd, uint_fast64_t numberOfPlayer2Variables) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables) {
-                // Intentionally left empty.
-            }
-         
-            template class GameBddResult<storm::dd::DdType::CUDD>;
-            template class GameBddResult<storm::dd::DdType::Sylvan>;
+        
+        template <storm::dd::DdType DdType>
+        GameBddResult<DdType>::GameBddResult() : bdd(), numberOfPlayer2Variables(0) {
+            // Intentionally left empty.
         }
+        
+        template <storm::dd::DdType DdType>
+        GameBddResult<DdType>::GameBddResult(storm::dd::Bdd<DdType> const& gameBdd, uint_fast64_t numberOfPlayer2Variables) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables) {
+            // Intentionally left empty.
+        }
+        
+        template class GameBddResult<storm::dd::DdType::CUDD>;
+        template class GameBddResult<storm::dd::DdType::Sylvan>;
+        
     }
 }

src/storm/abstraction/GameBddResult.h

@@ -4,17 +4,15 @@
 
 namespace storm {
     namespace abstraction {
-        namespace prism {
+        
+        template <storm::dd::DdType DdType>
+        struct GameBddResult {
+            GameBddResult();
+            GameBddResult(storm::dd::Bdd<DdType> const& gameBdd, uint_fast64_t numberOfPlayer2Variables);
             
-            template <storm::dd::DdType DdType>
-            struct GameBddResult {
-                GameBddResult();
-                GameBddResult(storm::dd::Bdd<DdType> const& gameBdd, uint_fast64_t numberOfPlayer2Variables);
-                
-                storm::dd::Bdd<DdType> bdd;
-                uint_fast64_t numberOfPlayer2Variables;
-            };
-            
-        }
+            storm::dd::Bdd<DdType> bdd;
+            uint_fast64_t numberOfPlayer2Variables;
+        };
+        
     }
 }

src/storm/abstraction/jani/AutomatonAbstractor.cpp

@@ -0,0 +1,127 @@
+#include "storm/abstraction/jani/AutomatonAbstractor.h"
+
+#include "storm/abstraction/AbstractionInformation.h"
+#include "storm/abstraction/BottomStateResult.h"
+#include "storm/abstraction/GameBddResult.h"
+
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Add.h"
+
+#include "storm/storage/jani/Automaton.h"
+
+#include "storm/settings/SettingsManager.h"
+
+#include "storm-config.h"
+#include "storm/adapters/CarlAdapter.h"
+
+#include "storm/utility/macros.h"
+
+namespace storm {
+    namespace abstraction {
+        namespace jani {
+            
+            using storm::settings::modules::AbstractionSettings;
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            AutomatonAbstractor<DdType, ValueType>::AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy) : smtSolverFactory(smtSolverFactory), abstractionInformation(abstractionInformation), edges(), automaton(automaton) {
+                
+                bool allowInvalidSuccessorsInCommands = false;
+                if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::None || invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) {
+                    allowInvalidSuccessorsInCommands = true;
+                }
+                
+                // For each concrete command, we create an abstract counterpart.
+                uint64_t edgeId = 0;
+                for (auto const& edge : automaton.getEdges()) {
+                    edges.emplace_back(edgeId, edge, abstractionInformation, smtSolverFactory, allowInvalidSuccessorsInCommands);
+                    ++edgeId;
+                }
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void AutomatonAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
+                for (uint_fast64_t index = 0; index < edges.size(); ++index) {
+                    STORM_LOG_TRACE("Refining edge with index " << index << ".");
+                    edges[index].refine(predicates);
+                }
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::expressions::Expression const& AutomatonAbstractor<DdType, ValueType>::getGuard(uint64_t player1Choice) const {
+                return edges[player1Choice].getGuard();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::map<storm::expressions::Variable, storm::expressions::Expression> AutomatonAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
+                return edges[player1Choice].getVariableUpdates(auxiliaryChoice);
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            GameBddResult<DdType> AutomatonAbstractor<DdType, ValueType>::abstract() {
+                // First, we retrieve the abstractions of all commands.
+                std::vector<GameBddResult<DdType>> edgeDdsAndUsedOptionVariableCounts;
+                uint_fast64_t maximalNumberOfUsedOptionVariables = 0;
+                for (auto& edge : edges) {
+                    edgeDdsAndUsedOptionVariableCounts.push_back(edge.abstract());
+                    maximalNumberOfUsedOptionVariables = std::max(maximalNumberOfUsedOptionVariables, edgeDdsAndUsedOptionVariableCounts.back().numberOfPlayer2Variables);
+                }
+                
+                // Then, we build the module BDD by adding the single command DDs. We need to make sure that all command
+                // DDs use the same amount DD variable encoding the choices of player 2.
+                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
+                for (auto const& edgeDd : edgeDdsAndUsedOptionVariableCounts) {
+                    result |= edgeDd.bdd && this->getAbstractionInformation().getPlayer2ZeroCube(edgeDd.numberOfPlayer2Variables, maximalNumberOfUsedOptionVariables);
+                }
+                return GameBddResult<DdType>(result, maximalNumberOfUsedOptionVariables);
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            BottomStateResult<DdType> AutomatonAbstractor<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
+                BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
+                
+                for (auto& edge : edges) {
+                    BottomStateResult<DdType> commandBottomStateResult = edge.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables);
+                    result.states |= commandBottomStateResult.states;
+                    result.transitions |= commandBottomStateResult.transitions;
+                }
+                
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Add<DdType, ValueType> AutomatonAbstractor<DdType, ValueType>::getEdgeUpdateProbabilitiesAdd() const {
+                storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
+                for (auto const& edge : edges) {
+                    result += edge.getEdgeUpdateProbabilitiesAdd();
+                }
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::vector<EdgeAbstractor<DdType, ValueType>> const& AutomatonAbstractor<DdType, ValueType>::getEdges() const {
+                return edges;
+            }
+
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::vector<EdgeAbstractor<DdType, ValueType>>& AutomatonAbstractor<DdType, ValueType>::getEdges() {
+                return edges;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::size_t AutomatonAbstractor<DdType, ValueType>::getNumberOfEdges() const {
+                return edges.size();
+            }
+
+            template <storm::dd::DdType DdType, typename ValueType>
+            AbstractionInformation<DdType> const& AutomatonAbstractor<DdType, ValueType>::getAbstractionInformation() const {
+                return abstractionInformation.get();
+            }
+            
+            template class AutomatonAbstractor<storm::dd::DdType::CUDD, double>;
+            template class AutomatonAbstractor<storm::dd::DdType::Sylvan, double>;
+#ifdef STORM_HAVE_CARL
+			template class AutomatonAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+#endif
+        }
+    }
+}

src/storm/abstraction/jani/AutomatonAbstractor.h

@@ -0,0 +1,131 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/abstraction/jani/EdgeAbstractor.h"
+
+#include "storm/settings/modules/AbstractionSettings.h"
+
+#include "storm/storage/expressions/Expression.h"
+
+#include "storm/utility/solver.h"
+
+namespace storm {
+    namespace jani {
+        // Forward-declare concrete automaton class.
+        class Automaton;
+    }
+    
+    namespace abstraction {
+        template <storm::dd::DdType DdType>
+        class AbstractionInformation;
+
+        template<storm::dd::DdType DdType>
+        struct BottomStateResult;
+
+        namespace jani {
+            template <storm::dd::DdType DdType, typename ValueType>
+            class AutomatonAbstractor {
+            public:
+                /*!
+                 * Constructs an abstract module from the given automaton.
+                 *
+                 * @param automaton The concrete automaton for which to build the abstraction.
+                 * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
+                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
+                 */
+                AutomatonAbstractor(storm::jani::Automaton const& automaton, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy);
+                
+                AutomatonAbstractor(AutomatonAbstractor const&) = default;
+                AutomatonAbstractor& operator=(AutomatonAbstractor const&) = default;
+                AutomatonAbstractor(AutomatonAbstractor&&) = default;
+                AutomatonAbstractor& operator=(AutomatonAbstractor&&) = default;
+                
+                /*!
+                 * Refines the abstract automaton with the given predicates.
+                 *
+                 * @param predicates The new predicate indices.
+                 */
+                void refine(std::vector<uint_fast64_t> const& predicates);
+                
+                /*!
+                 * Retrieves the guard of the given player 1 choice.
+                 *
+                 * @param player1Choice The choice of player 1.
+                 * @return The guard of the player 1 choice.
+                 */
+                storm::expressions::Expression const& getGuard(uint64_t player1Choice) const;
+                
+                /*!
+                 * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player
+                 * 1 choice and auxiliary choice.
+                 */
+                std::map<storm::expressions::Variable, storm::expressions::Expression> getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const;
+                
+                /*!
+                 * Computes the abstraction of the module wrt. to the current set of predicates.
+                 *
+                 * @return The abstraction of the module in the form of a BDD together with how many option variables were used.
+                 */
+                GameBddResult<DdType> abstract();
+                
+                /*!
+                 * Retrieves the transitions to bottom states of this automaton.
+                 *
+                 * @param reachableStates A BDD representing the reachable states.
+                 * @param numberOfPlayer2Variables The number of variables used to encode the choices of player 2.
+                 * @return The bottom states and the necessary transitions.
+                 */
+                BottomStateResult<DdType> getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables);
+                
+                /*!
+                 * Retrieves an ADD that maps the encodings of edges and their updates to their probabilities.
+                 *
+                 * @return The edge-update probability ADD.
+                 */
+                storm::dd::Add<DdType, ValueType> getEdgeUpdateProbabilitiesAdd() const;
+                
+                /*!
+                 * Retrieves the abstract edges of this abstract automton.
+                 *
+                 * @return The abstract edges.
+                 */
+                std::vector<EdgeAbstractor<DdType, ValueType>> const& getEdges() const;
+
+                /*!
+                 * Retrieves the abstract edges of this abstract automaton.
+                 *
+                 * @return The abstract edges.
+                 */
+                std::vector<EdgeAbstractor<DdType, ValueType>>& getEdges();
+
+                /*!
+                 * Retrieves the number of abstract edges of this abstract automaton.
+                 *
+                 * @param The number of edges.
+                 */
+                std::size_t getNumberOfEdges() const;
+                
+            private:
+                /*!
+                 * Retrieves the abstraction information.
+                 *
+                 * @return The abstraction information.
+                 */
+                AbstractionInformation<DdType> const& getAbstractionInformation() const;
+                
+                // A factory that can be used to create new SMT solvers.
+                std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
+                
+                // The DD-related information.
+                std::reference_wrapper<AbstractionInformation<DdType> const> abstractionInformation;
+                
+                // The abstract edge of the abstract automaton.
+                std::vector<EdgeAbstractor<DdType, ValueType>> edges;
+                
+                // The concrete module this abstract automaton refers to.
+                std::reference_wrapper<storm::jani::Automaton const> automaton;
+            };
+        }
+    }
+}

src/storm/abstraction/jani/EdgeAbstractor.cpp

@@ -0,0 +1,415 @@
+#include "storm/abstraction/jani/EdgeAbstractor.h"
+
+#include <chrono>
+
+#include <boost/iterator/transform_iterator.hpp>
+
+#include "storm/abstraction/AbstractionInformation.h"
+#include "storm/abstraction/BottomStateResult.h"
+
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Add.h"
+
+#include "storm/storage/jani/Edge.h"
+#include "storm/storage/jani/EdgeDestination.h"
+
+#include "storm/utility/solver.h"
+#include "storm/utility/macros.h"
+
+#include "storm-config.h"
+#include "storm/adapters/CarlAdapter.h"
+
+namespace storm {
+    namespace abstraction {
+        namespace jani {
+            template <storm::dd::DdType DdType, typename ValueType>
+            EdgeAbstractor<DdType, ValueType>::EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool allowInvalidSuccessors) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), edgeId(edgeId), edge(edge), localExpressionInformation(abstractionInformation), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), allowInvalidSuccessors(allowInvalidSuccessors), skipBottomStates(false), forceRecomputation(true), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, {!edge.getGuard()}, smtSolverFactory) {
+
+                // Make the second component of relevant predicates have the right size.
+                relevantPredicatesAndVariables.second.resize(edge.getNumberOfDestinations());
+                
+                // Assert all constraints to enforce legal variable values.
+                for (auto const& constraint : abstractionInformation.getConstraints()) {
+                    smtSolver->add(constraint);
+                    bottomStateAbstractor.constrain(constraint);
+                }
+                
+                // Assert the guard of the command.
+                smtSolver->add(edge.getGuard());
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void EdgeAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
+                // Add all predicates to the variable partition.
+                for (auto predicateIndex : predicates) {
+                    localExpressionInformation.addExpression(predicateIndex);
+                }
+                                
+                // Next, we check whether there is work to be done by recomputing the relevant predicates and checking
+                // whether they changed.
+                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> newRelevantPredicates = this->computeRelevantPredicates();
+                
+                // Check whether we need to recompute the abstraction.
+                bool relevantPredicatesChanged = this->relevantPredicatesChanged(newRelevantPredicates);
+                if (relevantPredicatesChanged) {
+                    addMissingPredicates(newRelevantPredicates);
+                }
+                forceRecomputation |= relevantPredicatesChanged;
+                
+                // Refine bottom state abstractor. Note that this does not trigger a recomputation yet.
+                bottomStateAbstractor.refine(predicates);
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::expressions::Expression const& EdgeAbstractor<DdType, ValueType>::getGuard() const {
+                return edge.get().getGuard();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::map<storm::expressions::Variable, storm::expressions::Expression> EdgeAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t auxiliaryChoice) const {
+                return edge.get().getDestination(auxiliaryChoice).getAsVariableToExpressionMap();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void EdgeAbstractor<DdType, ValueType>::recomputeCachedBdd() {
+                STORM_LOG_TRACE("Recomputing BDD for edge with guard " << edge.get().getGuard());
+                auto start = std::chrono::high_resolution_clock::now();
+                
+                // Create a mapping from source state DDs to their distributions.
+                std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
+                uint64_t numberOfSolutions = 0;
+                smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&numberOfSolutions] (storm::solver::SmtSolver::ModelReference const& model) {
+                    sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model));
+                    ++numberOfSolutions;
+                    return true;
+                });
+                
+                // Now we search for the maximal number of choices of player 2 to determine how many DD variables we
+                // need to encode the nondeterminism.
+                uint_fast64_t maximalNumberOfChoices = 0;
+                for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
+                    maximalNumberOfChoices = std::max(maximalNumberOfChoices, static_cast<uint_fast64_t>(sourceDistributionsPair.second.size()));
+                }
+                
+                // We now compute how many variables we need to encode the choices. We add one to the maximal number of
+                // choices to account for a possible transition to a bottom state.
+                uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices + 1)));
+                
+                // Finally, build overall result.
+                storm::dd::Bdd<DdType> resultBdd = this->getAbstractionInformation().getDdManager().getBddZero();
+                if (!skipBottomStates) {
+                    abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero();
+                }
+                uint_fast64_t sourceStateIndex = 0;
+                for (auto const& sourceDistributionsPair : sourceToDistributionsMap) {
+                    if (!skipBottomStates) {
+                        abstractGuard |= sourceDistributionsPair.first;
+                    }
+                    
+                    STORM_LOG_ASSERT(!sourceDistributionsPair.first.isZero(), "The source BDD must not be empty.");
+                    STORM_LOG_ASSERT(!sourceDistributionsPair.second.empty(), "The distributions must not be empty.");
+                    // We start with the distribution index of 1, becase 0 is reserved for a potential bottom choice.
+                    uint_fast64_t distributionIndex = 1;
+                    storm::dd::Bdd<DdType> allDistributions = this->getAbstractionInformation().getDdManager().getBddZero();
+                    for (auto const& distribution : sourceDistributionsPair.second) {
+                        allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, numberOfVariablesNeeded);
+                        ++distributionIndex;
+                        STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty.");
+                    }
+                    resultBdd |= sourceDistributionsPair.first && allDistributions;
+                    ++sourceStateIndex;
+                    STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty.");
+                }
+                
+                resultBdd &= computeMissingIdentities();
+                resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount());
+                STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
+                
+                // Cache the result.
+                cachedDd = GameBddResult<DdType>(resultBdd, numberOfVariablesNeeded);
+                auto end = std::chrono::high_resolution_clock::now();
+                
+                STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions in " << std::chrono::duration_cast<std::chrono::milliseconds>(end - start).count() << "ms.");
+                forceRecomputation = false;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> EdgeAbstractor<DdType, ValueType>::computeRelevantPredicates(storm::jani::OrderedAssignments const& assignments) const {
+                std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> result;
+                
+                std::set<storm::expressions::Variable> assignedVariables;
+                for (auto const& assignment : assignments.getAllAssignments()) {
+                    // Also, variables appearing on the right-hand side of an assignment are relevant for source state.
+                    auto const& rightHandSidePredicates = localExpressionInformation.getExpressionsUsingVariables(assignment.getAssignedExpression().getVariables());
+                    result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end());
+                    
+                    // Variables that are being assigned are relevant for the successor state.
+                    storm::expressions::Variable const& assignedVariable = assignment.getExpressionVariable();
+                    auto const& leftHandSidePredicates = localExpressionInformation.getExpressionsUsingVariable(assignedVariable);
+                    result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end());
+                    
+                    // Keep track of all assigned variables, so we can find the related predicates later.
+                    assignedVariables.insert(assignedVariable);
+                }
+                
+                if (!allowInvalidSuccessors) {
+                    auto const& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
+                    result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
+                }
+                
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> EdgeAbstractor<DdType, ValueType>::computeRelevantPredicates() const {
+                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> result;
+
+                // To start with, all predicates related to the guard are relevant source predicates.
+                result.first = localExpressionInformation.getExpressionsUsingVariables(edge.get().getGuard().getVariables());
+                
+                // Then, we add the predicates that become relevant, because of some update.
+                for (auto const& destination : edge.get().getDestinations()) {
+                    std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> relevantUpdatePredicates = computeRelevantPredicates(destination.getOrderedAssignments());
+                    result.first.insert(relevantUpdatePredicates.first.begin(), relevantUpdatePredicates.first.end());
+                    result.second.push_back(relevantUpdatePredicates.second);
+                }
+                
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            bool EdgeAbstractor<DdType, ValueType>::relevantPredicatesChanged(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) const {
+                if (newRelevantPredicates.first.size() > relevantPredicatesAndVariables.first.size()) {
+                    return true;
+                }
+                
+                for (uint_fast64_t index = 0; index < edge.get().getNumberOfDestinations(); ++index) {
+                    if (newRelevantPredicates.second[index].size() > relevantPredicatesAndVariables.second[index].size()) {
+                        return true;
+                    }
+                }
+                
+                return false;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void EdgeAbstractor<DdType, ValueType>::addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) {
+                // Determine and add new relevant source predicates.
+                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.first, newRelevantPredicates.first);
+                for (auto const& element : newSourceVariables) {
+                    allRelevantPredicates.insert(element.second);
+                    smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second)));
+                    decisionVariables.push_back(element.first);
+                }
+                
+                // Insert the new variables into the record of relevant source variables.
+                relevantPredicatesAndVariables.first.insert(relevantPredicatesAndVariables.first.end(), newSourceVariables.begin(), newSourceVariables.end());
+                std::sort(relevantPredicatesAndVariables.first.begin(), relevantPredicatesAndVariables.first.end(), [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) { return first.second < second.second; } );
+                
+                // Do the same for every update.
+                for (uint_fast64_t index = 0; index < edge.get().getNumberOfDestinations(); ++index) {
+                    std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSuccessorVariables = this->getAbstractionInformation().declareNewVariables(relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
+                    for (auto const& element : newSuccessorVariables) {
+                        allRelevantPredicates.insert(element.second);
+                        smtSolver->add(storm::expressions::iff(element.first, this->getAbstractionInformation().getPredicateByIndex(element.second).substitute(edge.get().getDestination(index).getAsVariableToExpressionMap())));
+                        decisionVariables.push_back(element.first);
+                    }
+                    
+                    relevantPredicatesAndVariables.second[index].insert(relevantPredicatesAndVariables.second[index].end(), newSuccessorVariables.begin(), newSuccessorVariables.end());
+                    std::sort(relevantPredicatesAndVariables.second[index].begin(), relevantPredicatesAndVariables.second[index].end(), [] (std::pair<storm::expressions::Variable, uint_fast64_t> const& first, std::pair<storm::expressions::Variable, uint_fast64_t> const& second) { return first.second < second.second; } );
+                }
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const {
+                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
+                for (auto const& variableIndexPair : relevantPredicatesAndVariables.first) {
+                    if (model.getBooleanValue(variableIndexPair.first)) {
+                        result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
+                    } else {
+                        result &= !this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
+                    }
+                }
+                
+                STORM_LOG_ASSERT(!result.isZero(), "Source must not be empty.");
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const {
+                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
+                
+                for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) {
+                    storm::dd::Bdd<DdType> updateBdd = this->getAbstractionInformation().getDdManager().getBddOne();
+
+                    // Translate block variables for this update into a successor block.
+                    for (auto const& variableIndexPair : relevantPredicatesAndVariables.second[updateIndex]) {
+                        if (model.getBooleanValue(variableIndexPair.first)) {
+                            updateBdd &= this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
+                        } else {
+                            updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
+                        }
+                        updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
+                    }
+                    
+                    result |= updateBdd;
+                }
+                
+                STORM_LOG_ASSERT(!result.isZero(), "Distribution must not be empty.");
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::computeMissingIdentities() const {
+                storm::dd::Bdd<DdType> identities = computeMissingGlobalIdentities();
+                identities &= computeMissingUpdateIdentities();
+                return identities;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::computeMissingUpdateIdentities() const {
+                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
+                
+                for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) {
+                    // Compute the identities that are missing for this update.
+                    auto updateRelevantIt = relevantPredicatesAndVariables.second[updateIndex].begin();
+                    auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end();
+                    
+                    storm::dd::Bdd<DdType> updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne();
+                    if (allowInvalidSuccessors) {
+                        for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
+                            if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) {
+                                updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
+                            } else {
+                                ++updateRelevantIt;
+                            }
+                        }
+                    } else {
+                        auto sourceRelevantIt = relevantPredicatesAndVariables.first.begin();
+                        auto sourceRelevantIte = relevantPredicatesAndVariables.first.end();
+                        
+                        // Go through all relevant source predicates. This is guaranteed to be a superset of the set of
+                        // relevant successor predicates for any update.
+                        for (; sourceRelevantIt != sourceRelevantIte; ++sourceRelevantIt) {
+                            // If the predicates do not match, there is a predicate missing, so we need to add its identity.
+                            if (updateRelevantIt == updateRelevantIte || sourceRelevantIt->second != updateRelevantIt->second) {
+                                updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second);
+                            } else {
+                                ++updateRelevantIt;
+                            }
+                        }
+                    }
+                    
+                    result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
+                }
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> EdgeAbstractor<DdType, ValueType>::computeMissingGlobalIdentities() const {
+                storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
+
+                if (allowInvalidSuccessors) {
+                    auto allRelevantIt = allRelevantPredicates.cbegin();
+                    auto allRelevantIte = allRelevantPredicates.cend();
+                    
+                    for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
+                        if (allRelevantIt == allRelevantIte || *allRelevantIt != predicateIndex) {
+                            result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
+                        } else {
+                            ++allRelevantIt;
+                        }
+                    }
+                } else {
+                    auto relevantIt = relevantPredicatesAndVariables.first.begin();
+                    auto relevantIte = relevantPredicatesAndVariables.first.end();
+                    
+                    for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
+                        if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
+                            result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
+                        } else {
+                            ++relevantIt;
+                        }
+                    }
+                }
+                
+                return result;
+            }
+
+            template <storm::dd::DdType DdType, typename ValueType>
+            GameBddResult<DdType> EdgeAbstractor<DdType, ValueType>::abstract() {
+                if (forceRecomputation) {
+                    this->recomputeCachedBdd();
+                } else {
+                    cachedDd.bdd &= computeMissingGlobalIdentities();
+                }
+                
+                return cachedDd;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            BottomStateResult<DdType> EdgeAbstractor<DdType, ValueType>::getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables) {
+                STORM_LOG_TRACE("Computing bottom state transitions of edge with guard " << edge.get().getGuard());
+                BottomStateResult<DdType> result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero());
+
+                // If the guard of this edge is a predicate, there are not bottom states/transitions.
+                if (skipBottomStates) {
+                    STORM_LOG_TRACE("Skipping bottom state computation for this edge.");
+                    return result;
+                }
+                
+                // Use the state abstractor to compute the set of abstract states that has this edge enabled but still
+                // has a transition to a bottom state.
+                bottomStateAbstractor.constrain(reachableStates && abstractGuard);
+                result.states = bottomStateAbstractor.getAbstractStates();
+                
+                // If the result is empty one time, we can skip the bottom state computation from now on.
+                if (result.states.isZero()) {
+                    skipBottomStates = true;
+                }
+
+                // Now equip all these states with an actual transition to a bottom state.
+                result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities() && this->getAbstractionInformation().getBottomStateBdd(false, false);
+                
+                // Mark the states as bottom states.
+                result.states &= this->getAbstractionInformation().getBottomStateBdd(true, false);
+                
+                // Add the edge encoding and the next free player 2 encoding.
+                result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(0, numberOfPlayer2Variables) && this->getAbstractionInformation().encodeAux(0, 0, this->getAbstractionInformation().getAuxVariableCount());
+                
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Add<DdType, ValueType> EdgeAbstractor<DdType, ValueType>::getEdgeUpdateProbabilitiesAdd() const {
+                storm::dd::Add<DdType, ValueType> result = this->getAbstractionInformation().getDdManager().template getAddZero<ValueType>();
+                for (uint_fast64_t updateIndex = 0; updateIndex < edge.get().getNumberOfDestinations(); ++updateIndex) {
+                    result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd<ValueType>() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(edge.get().getDestination(updateIndex).getProbability()));
+                }
+                result *= this->getAbstractionInformation().encodePlayer1Choice(edgeId, this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd<ValueType>();
+                return result;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::jani::Edge const& EdgeAbstractor<DdType, ValueType>::getConcreteEdge() const {
+                return edge.get();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            AbstractionInformation<DdType> const& EdgeAbstractor<DdType, ValueType>::getAbstractionInformation() const {
+                return abstractionInformation.get();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            AbstractionInformation<DdType>& EdgeAbstractor<DdType, ValueType>::getAbstractionInformation() {
+                return abstractionInformation.get();
+            }
+            
+            template class EdgeAbstractor<storm::dd::DdType::CUDD, double>;
+            template class EdgeAbstractor<storm::dd::DdType::Sylvan, double>;
+#ifdef STORM_HAVE_CARL
+			template class EdgeAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+#endif
+        }
+    }
+}

src/storm/abstraction/jani/EdgeAbstractor.h

@@ -0,0 +1,256 @@
+#pragma once
+
+#include <memory>
+#include <vector>
+#include <set>
+#include <map>
+
+#include "storm/abstraction/LocalExpressionInformation.h"
+#include "storm/abstraction/StateSetAbstractor.h"
+#include "storm/abstraction/GameBddResult.h"
+
+#include "storm/storage/expressions/ExpressionEvaluator.h"
+
+#include "storm/storage/dd/DdType.h"
+#include "storm/storage/expressions/Expression.h"
+
+#include "storm/solver/SmtSolver.h"
+
+namespace storm {
+    namespace utility {
+        namespace solver {
+            class SmtSolverFactory;
+        }
+    }
+    
+    namespace dd {
+        template <storm::dd::DdType DdType>
+        class Bdd;
+
+        template <storm::dd::DdType DdType, typename ValueType>
+        class Add;
+    }
+    
+    namespace jani {
+        // Forward-declare concrete edge and assignment classes.
+        class Edge;
+        class Assignment;
+        class OrderedAssignments;
+    }
+    
+    namespace abstraction {
+        template <storm::dd::DdType DdType>
+        class AbstractionInformation;
+
+        template <storm::dd::DdType DdType>
+        class BottomStateResult;
+
+        namespace jani {
+            template <storm::dd::DdType DdType, typename ValueType>
+            class EdgeAbstractor {
+            public:
+                /*!
+                 * Constructs an abstract edge from the given command and the initial predicates.
+                 *
+                 * @param edgeId The ID to assign to the edge.
+                 * @param edge The concrete edge for which to build the abstraction.
+                 * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
+                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
+                 * @param allowInvalidSuccessors A flag indicating whether it is allowed to enumerate invalid successors.
+                 */
+                EdgeAbstractor(uint64_t edgeId, storm::jani::Edge const& edge, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, bool allowInvalidSuccessors);
+                               
+                /*!
+                 * Refines the abstract edge with the given predicates.
+                 *
+                 * @param predicates The new predicates.
+                 */
+                void refine(std::vector<uint_fast64_t> const& predicates);
+                
+                /*!
+                 * Retrieves the guard of this edge.
+                 */
+                storm::expressions::Expression const& getGuard() const;
+                
+                /*!
+                 * Retrieves a mapping from variables to expressions that define their updates wrt. to the given
+                 * auxiliary choice.
+                 */
+                std::map<storm::expressions::Variable, storm::expressions::Expression> getVariableUpdates(uint64_t auxiliaryChoice) const;
+                
+                /*!
+                 * Computes the abstraction of the edge wrt. to the current set of predicates.
+                 *
+                 * @return The abstraction of the edge in the form of a BDD together with the number of DD variables
+                 * used to encode the choices of player 2.
+                 */
+                GameBddResult<DdType> abstract();
+                
+                /*!
+                 * Retrieves the transitions to bottom states of this edge.
+                 *
+                 * @param reachableStates A BDD representing the reachable states.
+                 * @param numberOfPlayer2Variables The number of variables used to encode the choices of player 2.
+                 * @return The bottom state transitions in the form of a BDD.
+                 */
+                BottomStateResult<DdType> getBottomStateTransitions(storm::dd::Bdd<DdType> const& reachableStates, uint_fast64_t numberOfPlayer2Variables);
+
+                /*!
+                 * Retrieves an ADD that maps the encoding of the edge and its updates to their probabilities.
+                 *
+                 * @return The edge-update probability ADD.
+                 */
+                storm::dd::Add<DdType, ValueType> getEdgeUpdateProbabilitiesAdd() const;
+                
+                /*!
+                 * Retrieves the concrete edge that is abstracted by this abstract edge.
+                 *
+                 * @return The concrete edge.
+                 */
+                storm::jani::Edge const& getConcreteEdge() const;
+                
+            private:
+                /*!
+                 * Determines the relevant predicates for source as well as successor states wrt. to the given assignments
+                 * (that, for example, form an update).
+                 *
+                 * @param assignments The assignments that are to be considered.
+                 * @return A pair whose first component represents the relevant source predicates and whose second
+                 * component represents the relevant successor state predicates.
+                 */
+                std::pair<std::set<uint_fast64_t>, std::set<uint_fast64_t>> computeRelevantPredicates(storm::jani::OrderedAssignments const& assignments) const;
+                
+                /*!
+                 * Determines the relevant predicates for source as well as successor states.
+                 *
+                 * @return A pair whose first component represents the relevant source predicates and whose second
+                 * component represents the relevant successor state predicates.
+                 */
+                std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> computeRelevantPredicates() const;
+
+                /*!
+                 * Checks whether the relevant predicates changed.
+                 *
+                 * @param newRelevantPredicates The new relevant predicates.
+                 */
+                bool relevantPredicatesChanged(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) const;
+                                
+                /*!
+                 * Takes the new relevant predicates and creates the appropriate variables and assertions for the ones
+                 * that are currently missing.
+                 *
+                 * @param newRelevantPredicates The new relevant predicates.
+                 */
+                void addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates);
+                
+                /*!
+                 * Translates the given model to a source state DD.
+                 *
+                 * @param model The model to translate.
+                 * @return The source state encoded as a DD.
+                 */
+                storm::dd::Bdd<DdType> getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model) const;
+
+                /*!
+                 * Translates the given model to a distribution over successor states.
+                 *
+                 * @param model The model to translate.
+                 * @return The source state encoded as a DD.
+                 */
+                storm::dd::Bdd<DdType> getDistributionBdd(storm::solver::SmtSolver::ModelReference const& model) const;
+                
+                /*!
+                 * Recomputes the cached BDD. This needs to be triggered if any relevant predicates change.
+                 */
+                void recomputeCachedBdd();
+
+                /*!
+                 * Computes the missing state identities.
+                 *
+                 * @return A BDD that represents the all missing state identities.
+                 */
+                storm::dd::Bdd<DdType> computeMissingIdentities() const;
+                
+                /*!
+                 * Computes the missing state identities for the updates.
+                 *
+                 * @return A BDD that represents the state identities for predicates that are irrelevant for the
+                 * successor states.
+                 */
+                storm::dd::Bdd<DdType> computeMissingUpdateIdentities() const;
+                
+                /*!
+                 * Retrieves the abstraction information object.
+                 *
+                 * @return The abstraction information object.
+                 */
+                AbstractionInformation<DdType> const& getAbstractionInformation() const;
+
+                /*!
+                 * Retrieves the abstraction information object.
+                 *
+                 * @return The abstraction information object.
+                 */
+                AbstractionInformation<DdType>& getAbstractionInformation();
+                
+                /*!
+                 * Computes the globally missing state identities.
+                 *
+                 * @return A BDD that represents the global state identities for predicates that are irrelevant for the
+                 * source and successor states.
+                 */
+                storm::dd::Bdd<DdType> computeMissingGlobalIdentities() const;
+                
+                // An SMT responsible for this abstract command.
+                std::unique_ptr<storm::solver::SmtSolver> smtSolver;
+
+                // The abstraction-related information.
+                std::reference_wrapper<AbstractionInformation<DdType>> abstractionInformation;
+                
+                // The ID of the edge.
+                uint64_t edgeId;
+                
+                // The concrete edge this abstract command refers to.
+                std::reference_wrapper<storm::jani::Edge const> edge;
+                
+                // The local expression-related information.
+                LocalExpressionInformation<DdType> localExpressionInformation;
+                
+                // The evaluator used to translate the probability expressions.
+                storm::expressions::ExpressionEvaluator<ValueType> evaluator;
+                
+                // The currently relevant source/successor predicates and the corresponding variables.
+                std::pair<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>, std::vector<std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>>>> relevantPredicatesAndVariables;
+                
+                // The set of all relevant predicates.
+                std::set<uint64_t> allRelevantPredicates;
+                
+                // The most recent result of a call to computeDd. If nothing has changed regarding the relevant
+                // predicates, this result may be reused.
+                GameBddResult<DdType> cachedDd;
+                
+                // All relevant decision variables over which to perform AllSat.
+                std::vector<storm::expressions::Variable> decisionVariables;
+                
+                // A flag indicating whether it is allowed to enumerate invalid successors. Invalid successors may be
+                // enumerated if the predicates that are (indirectly) related to an assignment variable are not
+                // considered as source predicates.
+                bool allowInvalidSuccessors;
+                
+                // A flag indicating whether the computation of bottom states can be skipped (for example, if the bottom
+                // states become empty at some point).
+                bool skipBottomStates;
+                
+                // A flag remembering whether we need to force recomputation of the BDD.
+                bool forceRecomputation;
+                
+                // The abstract guard of the edge. This is only used if the guard is not a predicate, because it can
+                // then be used to constrain the bottom state abstractor.
+                storm::dd::Bdd<DdType> abstractGuard;
+                
+                // A state-set abstractor used to determine the bottom states if not all guards were added.
+                StateSetAbstractor<DdType, ValueType> bottomStateAbstractor;
+            };
+        }
+    }
+}

src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp

@@ -0,0 +1,349 @@
+#include "storm/abstraction/jani/JaniMenuGameAbstractor.h"
+
+#include "storm/abstraction/BottomStateResult.h"
+#include "storm/abstraction/GameBddResult.h"
+
+#include "storm/storage/BitVector.h"
+
+#include "storm/storage/jani/Model.h"
+
+#include "storm/storage/dd/DdManager.h"
+#include "storm/storage/dd/Add.h"
+
+#include "storm/models/symbolic/StandardRewardModel.h"
+
+#include "storm/settings/SettingsManager.h"
+
+#include "storm/utility/dd.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/solver.h"
+#include "storm/exceptions/WrongFormatException.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/NotSupportedException.h"
+
+#include "storm-config.h"
+#include "storm/adapters/CarlAdapter.h"
+
+namespace storm {
+    namespace abstraction {
+        namespace jani {
+            
+            using storm::settings::modules::AbstractionSettings;
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false), invalidBlockDetectionStrategy(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getInvalidBlockDetectionStrategy()) {
+                
+                // For now, we assume that there is a single module. If the program has more than one module, it needs
+                // to be flattened before the procedure.
+                STORM_LOG_THROW(model.getNumberOfAutomata() == 1, storm::exceptions::WrongFormatException, "Cannot create abstract model from program containing more than one automaton.");
+                
+                // Add all variables range expressions to the information object.
+                for (auto const& range : this->model.get().getAllRangeExpressions()) {
+                    abstractionInformation.addConstraint(range);
+                    initialStateAbstractor.constrain(range);
+                }
+                
+                uint_fast64_t totalNumberOfCommands = 0;
+                uint_fast64_t maximalUpdateCount = 0;
+                std::vector<storm::expressions::Expression> allGuards;
+                for (auto const& automaton : model.getAutomata()) {
+                    for (auto const& edge : automaton.getEdges()) {
+                        maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(edge.getNumberOfDestinations()));
+                    }
+                    
+                    totalNumberOfCommands += automaton.getNumberOfEdges();
+                }
+                
+                // NOTE: currently we assume that 100 player 2 variables suffice, which corresponds to 2^100 possible
+                // choices. If for some reason this should not be enough, we could grow this vector dynamically, but
+                // odds are that it's impossible to treat such models in any event.
+                abstractionInformation.createEncodingVariables(static_cast<uint_fast64_t>(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast<uint_fast64_t>(std::ceil(std::log2(maximalUpdateCount))));
+                
+                // For each module of the concrete program, we create an abstract counterpart.
+                for (auto const& automaton : model.getAutomata()) {
+                    automata.emplace_back(automaton, abstractionInformation, this->smtSolverFactory, invalidBlockDetectionStrategy);
+                }
+                
+                // Retrieve the edge-update probability ADD, so we can multiply it with the abstraction BDD later.
+                edgeUpdateProbabilitiesAdd = automata.front().getEdgeUpdateProbabilitiesAdd();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void JaniMenuGameAbstractor<DdType, ValueType>::refine(RefinementCommand const& command) {
+                // Add the predicates to the global list of predicates and gather their indices.
+                std::vector<uint_fast64_t> predicateIndices;
+                for (auto const& predicate : command.getPredicates()) {
+                    STORM_LOG_THROW(predicate.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expecting a predicate of type bool.");
+                    predicateIndices.push_back(abstractionInformation.getOrAddPredicate(predicate));
+                }
+                
+                // Refine all abstract automata.
+                for (auto& automaton : automata) {
+                    automaton.refine(predicateIndices);
+                }
+                
+                // Refine initial state abstractor.
+                initialStateAbstractor.refine(predicateIndices);
+                
+                // Refine the valid blocks.
+                validBlockAbstractor.refine(predicateIndices);
+
+                refinementPerformed |= !command.getPredicates().empty();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            MenuGame<DdType, ValueType> JaniMenuGameAbstractor<DdType, ValueType>::abstract() {
+                if (refinementPerformed) {
+                    currentGame = buildGame();
+                    refinementPerformed = true;
+                }
+                return *currentGame;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            AbstractionInformation<DdType> const& JaniMenuGameAbstractor<DdType, ValueType>::getAbstractionInformation() const {
+                return abstractionInformation;
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::expressions::Expression const& JaniMenuGameAbstractor<DdType, ValueType>::getGuard(uint64_t player1Choice) const {
+                return automata.front().getGuard(player1Choice);
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::map<storm::expressions::Variable, storm::expressions::Expression> JaniMenuGameAbstractor<DdType, ValueType>::getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const {
+                return automata.front().getVariableUpdates(player1Choice, auxiliaryChoice);
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::pair<uint64_t, uint64_t> JaniMenuGameAbstractor<DdType, ValueType>::getPlayer1ChoiceRange() const {
+                return std::make_pair(0, automata.front().getNumberOfEdges());
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::expressions::Expression JaniMenuGameAbstractor<DdType, ValueType>::getInitialExpression() const {
+                return model.get().getInitialStatesExpression();
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            storm::dd::Bdd<DdType> JaniMenuGameAbstractor<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) {
+                STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
+                return abstractionInformation.getPredicateSourceVariable(predicate);
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            std::unique_ptr<MenuGame<DdType, ValueType>> JaniMenuGameAbstractor<DdType, ValueType>::buildGame() {
+                // As long as there is only one module, we only build its game representation.
+                GameBddResult<DdType> game = automata.front().abstract();
+                
+                if (invalidBlockDetectionStrategy == AbstractionSettings::InvalidBlockDetectionStrategy::Global) {
+                    auto validBlockStart = std::chrono::high_resolution_clock::now();
+                    storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
+                    // Cut away all invalid successor blocks.
+                    game.bdd &= validBlocks.swapVariables(abstractionInformation.getExtendedSourceSuccessorVariablePairs());
+                    auto validBlockEnd = std::chrono::high_resolution_clock::now();
+                    STORM_LOG_DEBUG("Global invalid block detection completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(validBlockEnd - validBlockStart).count() << "ms.");
+                }
+                
+                // Construct a set of all unnecessary variables, so we can abstract from it.
+                std::set<storm::expressions::Variable> variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount()));
+                auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables);
+                variablesToAbstract.insert(player2Variables.begin(), player2Variables.end());
+                auto auxVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount());
+                variablesToAbstract.insert(auxVariables.begin(), auxVariables.end());
+                
+                // Do a reachability analysis on the raw transition relation.
+                storm::dd::Bdd<DdType> transitionRelation = game.bdd.existsAbstract(variablesToAbstract);
+                storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
+                storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
+                
+                // Find the deadlock states in the model. Note that this does not find the 'deadlocks' in bottom states,
+                // as the bottom states are not contained in the reachable states.
+                storm::dd::Bdd<DdType> deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables());
+                deadlockStates = reachableStates && !deadlockStates;
+                
+                // If there are deadlock states, we fix them now.
+                storm::dd::Add<DdType, ValueType> deadlockTransitions = abstractionInformation.getDdManager().template getAddZero<ValueType>();
+                if (!deadlockStates.isZero()) {
+                    deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd<ValueType>();
+                }
+                
+                // Compute bottom states and the appropriate transitions if necessary.
+                BottomStateResult<DdType> bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero());
+                bottomStateResult = automata.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables);
+                bool hasBottomStates = !bottomStateResult.states.isZero();
+                
+                // Construct the transition matrix by cutting away the transitions of unreachable states.
+                storm::dd::Add<DdType, ValueType> transitionMatrix = (game.bdd && reachableStates).template toAdd<ValueType>();
+                transitionMatrix *= edgeUpdateProbabilitiesAdd;
+                transitionMatrix += deadlockTransitions;
+                
+                // Extend the current game information with the 'non-bottom' tag before potentially adding bottom state transitions.
+                transitionMatrix *= (abstractionInformation.getBottomStateBdd(true, true) && abstractionInformation.getBottomStateBdd(false, true)).template toAdd<ValueType>();
+                reachableStates &= abstractionInformation.getBottomStateBdd(true, true);
+                initialStates &= abstractionInformation.getBottomStateBdd(true, true);
+                
+                // If there are bottom transitions, exnted the transition matrix and reachable states now.
+                if (hasBottomStates) {
+                    transitionMatrix += bottomStateResult.transitions.template toAdd<ValueType>();
+                    reachableStates |= bottomStateResult.states;
+                }
+                
+                std::set<storm::expressions::Variable> usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables);
+                
+                std::set<storm::expressions::Variable> allNondeterminismVariables = usedPlayer2Variables;
+                allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end());
+                
+                std::set<storm::expressions::Variable> allSourceVariables(abstractionInformation.getSourceVariables());
+                allSourceVariables.insert(abstractionInformation.getBottomStateVariable(true));
+                std::set<storm::expressions::Variable> allSuccessorVariables(abstractionInformation.getSuccessorVariables());
+                allSuccessorVariables.insert(abstractionInformation.getBottomStateVariable(false));
+                
+                return std::make_unique<MenuGame<DdType, ValueType>>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, allSourceVariables, allSuccessorVariables, abstractionInformation.getExtendedSourceSuccessorVariablePairs(), std::set<storm::expressions::Variable>(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap());
+            }
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            void JaniMenuGameAbstractor<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
+                std::ofstream out(filename);
+                
+                storm::dd::Add<DdType, ValueType> filteredTransitions = filter.template toAdd<ValueType>() * currentGame->getTransitionMatrix();
+                storm::dd::Bdd<DdType> filteredTransitionsBdd = filteredTransitions.toBdd().existsAbstract(currentGame->getNondeterminismVariables());
+                storm::dd::Bdd<DdType> filteredReachableStates = storm::utility::dd::computeReachableStates(currentGame->getInitialStates(), filteredTransitionsBdd, currentGame->getRowVariables(), currentGame->getColumnVariables());
+                filteredTransitions *= filteredReachableStates.template toAdd<ValueType>();
+                
+                // Determine all initial states so we can color them blue.
+                std::unordered_set<std::string> initialStates;
+                storm::dd::Add<DdType, ValueType> initialStatesAsAdd = currentGame->getInitialStates().template toAdd<ValueType>();
+                for (auto stateValue : initialStatesAsAdd) {
+                    std::stringstream stateName;
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            stateName << "1";
+                        } else {
+                            stateName << "0";
+                        }
+                    }
+                    initialStates.insert(stateName.str());
+                }
+                
+                // Determine all highlight states so we can color them red.
+                std::unordered_set<std::string> highlightStates;
+                storm::dd::Add<DdType, ValueType> highlightStatesAdd = highlightStatesBdd.template toAdd<ValueType>();
+                for (auto stateValue : highlightStatesAdd) {
+                    std::stringstream stateName;
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            stateName << "1";
+                        } else {
+                            stateName << "0";
+                        }
+                    }
+                    highlightStates.insert(stateName.str());
+                }
+                
+                out << "digraph game {" << std::endl;
+                
+                // Create the player 1 nodes.
+                storm::dd::Add<DdType, ValueType> statesAsAdd = filteredReachableStates.template toAdd<ValueType>();
+                for (auto stateValue : statesAsAdd) {
+                    out << "\tpl1_";
+                    std::stringstream stateName;
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            stateName << "1";
+                        } else {
+                            stateName << "0";
+                        }
+                    }
+                    std::string stateNameAsString = stateName.str();
+                    out << stateNameAsString;
+                    out << " [ label=\"";
+                    if (stateValue.first.getBooleanValue(abstractionInformation.getBottomStateVariable(true))) {
+                        out << "*\", margin=0, width=0, height=0, shape=\"none\"";
+                    } else {
+                        out << stateName.str() << "\", margin=0, width=0, height=0, shape=\"oval\"";
+                    }
+                    bool isInitial = initialStates.find(stateNameAsString) != initialStates.end();
+                    bool isHighlight = highlightStates.find(stateNameAsString) != highlightStates.end();
+                    if (isInitial && isHighlight) {
+                        out << ", style=\"filled\", fillcolor=\"yellow\"";
+                    } else if (isInitial) {
+                        out << ", style=\"filled\", fillcolor=\"blue\"";
+                    } else if (isHighlight) {
+                        out << ", style=\"filled\", fillcolor=\"red\"";
+                    }
+                    out << " ];" << std::endl;
+                }
+                
+                // Create the nodes of the second player.
+                storm::dd::Add<DdType, ValueType> player2States = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).existsAbstract(currentGame->getPlayer2Variables()).template toAdd<ValueType>();
+                for (auto stateValue : player2States) {
+                    out << "\tpl2_";
+                    std::stringstream stateName;
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            stateName << "1";
+                        } else {
+                            stateName << "0";
+                        }
+                    }
+                    uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
+                    out << stateName.str() << "_" << index;
+                    out << " [ shape=\"square\", width=0, height=0, margin=0, label=\"" << index << "\" ];" << std::endl;
+                    out << "\tpl1_" << stateName.str() << " -> " << "pl2_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
+                }
+                
+                // Create the nodes of the probabilistic player.
+                storm::dd::Add<DdType, ValueType> playerPStates = filteredTransitions.toBdd().existsAbstract(currentGame->getColumnVariables()).template toAdd<ValueType>();
+                for (auto stateValue : playerPStates) {
+                    out << "\tplp_";
+                    std::stringstream stateName;
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            stateName << "1";
+                        } else {
+                            stateName << "0";
+                        }
+                    }
+                    uint_fast64_t index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
+                    stateName << "_" << index;
+                    index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size());
+                    out << stateName.str() << "_" << index;
+                    out << " [ shape=\"point\", label=\"\" ];" << std::endl;
+                    out << "\tpl2_" << stateName.str() << " -> " << "plp_" << stateName.str() << "_" << index << " [ label=\"" << index << "\" ];" << std::endl;
+                }
+                
+                for (auto stateValue : filteredTransitions) {
+                    std::stringstream sourceStateName;
+                    std::stringstream successorStateName;
+                    for (auto const& var : currentGame->getRowVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            sourceStateName << "1";
+                        } else {
+                            sourceStateName << "0";
+                        }
+                    }
+                    for (auto const& var : currentGame->getColumnVariables()) {
+                        if (stateValue.first.getBooleanValue(var)) {
+                            successorStateName << "1";
+                        } else {
+                            successorStateName << "0";
+                        }
+                    }
+                    uint_fast64_t pl1Index = abstractionInformation.decodePlayer1Choice(stateValue.first, abstractionInformation.getPlayer1VariableCount());
+                    uint_fast64_t pl2Index = abstractionInformation.decodePlayer2Choice(stateValue.first, currentGame->getPlayer2Variables().size());
+                    out << "\tplp_" << sourceStateName.str() << "_" << pl1Index << "_" << pl2Index << " -> pl1_" << successorStateName.str() << " [ label=\"" << stateValue.second << "\"];" << std::endl;
+                }
+                
+                out << "}" << std::endl;
+            }
+            
+            // Explicitly instantiate the class.
+            template class JaniMenuGameAbstractor<storm::dd::DdType::CUDD, double>;
+            template class JaniMenuGameAbstractor<storm::dd::DdType::Sylvan, double>;
+#ifdef STORM_HAVE_CARL
+            template class JaniMenuGameAbstractor<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+#endif
+        }
+    }
+}

src/storm/abstraction/jani/JaniMenuGameAbstractor.h

@@ -0,0 +1,167 @@
+#pragma once
+
+#include "storm/storage/dd/DdType.h"
+
+#include "storm/abstraction/MenuGameAbstractor.h"
+#include "storm/abstraction/AbstractionInformation.h"
+#include "storm/abstraction/MenuGame.h"
+#include "storm/abstraction/RefinementCommand.h"
+#include "storm/abstraction/ValidBlockAbstractor.h"
+#include "storm/abstraction/jani/AutomatonAbstractor.h"
+
+#include "storm/storage/dd/Add.h"
+
+#include "storm/storage/expressions/Expression.h"
+
+#include "storm/settings/modules/AbstractionSettings.h"
+
+namespace storm {
+    namespace utility {
+        namespace solver {
+            class SmtSolverFactory;
+        }
+    }
+    
+    namespace models {
+        namespace symbolic {
+            template<storm::dd::DdType Type, typename ValueType>
+            class StochasticTwoPlayerGame;
+        }
+    }
+    
+    namespace jani {
+        // Forward-declare concrete Model class.
+        class Model;
+    }
+    
+    namespace abstraction {
+        namespace jani {
+            
+            template <storm::dd::DdType DdType, typename ValueType>
+            class JaniMenuGameAbstractor : public MenuGameAbstractor<DdType, ValueType> {
+            public:
+                /*!
+                 * Constructs an abstractor for the given model.
+                 *
+                 * @param model The concrete model for which to build the abstraction.
+                 * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
+                 */
+                JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory);
+                
+                JaniMenuGameAbstractor(JaniMenuGameAbstractor const&) = default;
+                JaniMenuGameAbstractor& operator=(JaniMenuGameAbstractor const&) = default;
+                JaniMenuGameAbstractor(JaniMenuGameAbstractor&&) = default;
+                JaniMenuGameAbstractor& operator=(JaniMenuGameAbstractor&&) = default;
+                
+                /*!
+                 * Uses the current set of predicates to derive the abstract menu game in the form of an ADD.
+                 *
+                 * @return The abstract stochastic two player game.
+                 */
+                MenuGame<DdType, ValueType> abstract() override;
+                
+                /*!
+                 * Retrieves information about the abstraction.
+                 *
+                 * @return The abstraction information object.
+                 */
+                AbstractionInformation<DdType> const& getAbstractionInformation() const override;
+                
+                /*!
+                 * Retrieves the guard predicate of the given player 1 choice.
+                 *
+                 * @param player1Choice The choice for which to retrieve the guard.
+                 * @return The guard of the player 1 choice.
+                 */
+                storm::expressions::Expression const& getGuard(uint64_t player1Choice) const override;
+                
+                /*!
+                 * Retrieves a mapping from variables to expressions that define their updates wrt. to the given player
+                 * 1 choice and auxiliary choice.
+                 */
+                std::map<storm::expressions::Variable, storm::expressions::Expression> getVariableUpdates(uint64_t player1Choice, uint64_t auxiliaryChoice) const override;
+                
+                /*!
+                 * Retrieves the range of player 1 choices.
+                 */
+                std::pair<uint64_t, uint64_t> getPlayer1ChoiceRange() const override;
+                
+                /*!
+                 * Retrieves the expression that characterizes the initial states.
+                 */
+                storm::expressions::Expression getInitialExpression() const override;
+                
+                /*!
+                 * Retrieves the set of states (represented by a BDD) satisfying the given predicate, assuming that it
+                 * was either given as an initial predicate or used as a refining predicate later.
+                 *
+                 * @param predicate The predicate for which to retrieve the states.
+                 * @return The BDD representing the set of states.
+                 */
+                storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& predicate);
+                
+                /*!
+                 * Performs the given refinement command.
+                 *
+                 * @param command The command to perform.
+                 */
+                virtual void refine(RefinementCommand const& command) override;
+
+                /*!
+                 * Exports the current state of the abstraction in the dot format to the given file.
+                 *
+                 * @param filename The name of the file to which to write the dot output.
+                 * @param highlightStates A BDD characterizing states that will be highlighted.
+                 * @param filter A filter that is applied to select which part of the game to export.
+                 */
+                void exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStates, storm::dd::Bdd<DdType> const& filter) const override;
+                
+            private:                
+                /*!
+                 * Builds the stochastic game representing the abstraction of the program.
+                 *
+                 * @return The stochastic game.
+                 */
+                std::unique_ptr<MenuGame<DdType, ValueType>> buildGame();
+                
+                /*!
+                 * Decodes the given choice over the auxiliary and successor variables to a mapping from update indices
+                 * to bit vectors representing the successors under these updates.
+                 *
+                 * @param choice The choice to decode.
+                 */
+                std::map<uint_fast64_t, storm::storage::BitVector> decodeChoiceToUpdateSuccessorMapping(storm::dd::Bdd<DdType> const& choice) const;
+                
+                // The concrete model this abstractor refers to.
+                std::reference_wrapper<storm::jani::Model const> model;
+
+                // A factory that can be used to create new SMT solvers.
+                std::shared_ptr<storm::utility::solver::SmtSolverFactory> smtSolverFactory;
+                
+                // An object containing all information about the abstraction like predicates and the corresponding DDs.
+                AbstractionInformation<DdType> abstractionInformation;
+                
+                // The abstract modules of the abstract program.
+                std::vector<AutomatonAbstractor<DdType, ValueType>> automata;
+                
+                // A state-set abstractor used to determine the initial states of the abstraction.
+                StateSetAbstractor<DdType, ValueType> initialStateAbstractor;
+                
+                // An object that is used to compute the valid blocks.
+                ValidBlockAbstractor<DdType> validBlockAbstractor;
+                                
+                // An ADD characterizing the probabilities of edges and their updates.
+                storm::dd::Add<DdType, ValueType> edgeUpdateProbabilitiesAdd;
+                
+                // The current game-based abstraction.
+                std::unique_ptr<MenuGame<DdType, ValueType>> currentGame;
+                
+                // A flag storing whether a refinement was performed.
+                bool refinementPerformed;
+                
+                // The strategy to use for detecting invalid blocks.
+                storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy;
+            };
+        }
+    }
+}

src/storm/abstraction/prism/CommandAbstractor.h

@@ -44,9 +44,6 @@ namespace storm {
         template <storm::dd::DdType DdType>
         class BottomStateResult;
 
-        template<storm::dd::DdType DdType>
-        struct GameBddResult;
-
         namespace prism {
             template <storm::dd::DdType DdType, typename ValueType>
             class CommandAbstractor {

src/storm/abstraction/prism/ModuleAbstractor.h

@@ -31,13 +31,13 @@ namespace storm {
             class ModuleAbstractor {
             public:
                 /*!
-                 * Constructs an abstract module from the given module and the initial predicates.
+                 * Constructs an abstract module from the given module.
                  *
                  * @param module The concrete module for which to build the abstraction.
                  * @param abstractionInformation An object holding information about the abstraction such as predicates and BDDs.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  */
-                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy = storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy::Command);
+                ModuleAbstractor(storm::prism::Module const& module, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory, storm::settings::modules::AbstractionSettings::InvalidBlockDetectionStrategy invalidBlockDetectionStrategy);
                 
                 ModuleAbstractor(ModuleAbstractor const&) = default;
                 ModuleAbstractor& operator=(ModuleAbstractor const&) = default;

src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp

@@ -27,9 +27,7 @@
 namespace storm {
     namespace abstraction {
         namespace prism {
-            
-#undef LOCAL_DEBUG
-            
+                        
             using storm::settings::modules::AbstractionSettings;
             
             template <storm::dd::DdType DdType, typename ValueType>
@@ -51,7 +49,6 @@ namespace storm {
                 uint_fast64_t maximalUpdateCount = 0;
                 std::vector<storm::expressions::Expression> allGuards;
                 for (auto const& module : program.getModules()) {
-                    // If we were requested to add all guards to the set of predicates, we do so now.
                     for (auto const& command : module.getCommands()) {
                         maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates()));
                     }

src/storm/abstraction/prism/PrismMenuGameAbstractor.h

@@ -41,13 +41,12 @@ namespace storm {
             class PrismMenuGameAbstractor : public MenuGameAbstractor<DdType, ValueType> {
             public:
                 /*!
-                 * Constructs an abstract program from the given program and the initial predicates.
+                 * Constructs an abstractor for the given program.
                  *
-                 * @param expressionManager The manager responsible for the expressions of the program.
                  * @param program The concrete program for which to build the abstraction.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  */
-                PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
+                PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory);
                 
                 PrismMenuGameAbstractor(PrismMenuGameAbstractor const&) = default;
                 PrismMenuGameAbstractor& operator=(PrismMenuGameAbstractor const&) = default;

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -12,6 +12,7 @@
 #include "storm/storage/dd/DdManager.h"
 
 #include "storm/abstraction/prism/PrismMenuGameAbstractor.h"
+#include "storm/abstraction/jani/JaniMenuGameAbstractor.h"
 #include "storm/abstraction/MenuGameRefiner.h"
 
 #include "storm/logic/FragmentSpecification.h"
@@ -32,8 +33,6 @@
 
 #include "storm/modelchecker/results/CheckResult.h"
 
-//#define LOCAL_DEBUG
-
 namespace storm {
     namespace modelchecker {
         
@@ -42,16 +41,22 @@ namespace storm {
         
         template<storm::dd::DdType Type, typename ModelType>
         GameBasedMdpModelChecker<Type, ModelType>::GameBasedMdpModelChecker(storm::storage::SymbolicModelDescription const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), comparator(storm::settings::getModule<storm::settings::modules::AbstractionSettings>().getPrecision()), reuseQualitativeResults(false), reuseQuantitativeResults(false) {
-            STORM_LOG_THROW(model.isPrismProgram(), storm::exceptions::NotSupportedException, "Currently only PRISM models are supported by the game-based model checker.");
-            storm::prism::Program const& originalProgram = model.asPrismProgram();
-            STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
-            storm::utility::prism::requireNoUndefinedConstants(originalProgram);
-            
-            // Start by preparing the program. That is, we flatten the modules if there is more than one.
-            if (originalProgram.getNumberOfModules() > 1) {
-                preprocessedModel = originalProgram.flattenModules(this->smtSolverFactory);
+            model.requireNoUndefinedConstants();
+            if (model.isPrismProgram()) {
+                storm::prism::Program const& originalProgram = model.asPrismProgram();
+                STORM_LOG_THROW(originalProgram.getModelType() == storm::prism::Program::ModelType::DTMC || originalProgram.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
+                
+                // Flatten the modules if there is more than one.
+                if (originalProgram.getNumberOfModules() > 1) {
+                    preprocessedModel = originalProgram.flattenModules(this->smtSolverFactory);
+                } else {
+                    preprocessedModel = originalProgram;
+                }
             } else {
-                preprocessedModel = originalProgram;
+                storm::jani::Model const& originalModel = model.asJaniModel();
+                STORM_LOG_THROW(originalModel.getModelType() == storm::jani::ModelType::DTMC || originalModel.getModelType() == storm::jani::ModelType::MDP, storm::exceptions::NotSupportedException, "Currently only DTMCs/MDPs are supported by the game-based model checker.");
+                
+                preprocessedModel = model;
             }
             
             bool reuseAll = storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isReuseAllResultsSet();
@@ -76,7 +81,10 @@ namespace storm {
         template<storm::dd::DdType Type, typename ModelType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
             storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
-            std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping();
+            std::map<std::string, storm::expressions::Expression> labelToExpressionMapping;
+            if (preprocessedModel.isPrismProgram()) {
+                labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping();
+            }
             return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), preprocessedModel.getManager().boolean(true), pathFormula.getSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping));
         }
         
@@ -286,10 +294,15 @@ namespace storm {
             storm::OptimizationDirection player1Direction = getPlayer1Direction(checkTask);
             
             // Create the abstractor.
-            storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedModel.asPrismProgram(), smtSolverFactory);
+            std::shared_ptr<storm::abstraction::MenuGameAbstractor<Type, ValueType>> abstractor;
+            if (preprocessedModel.isPrismProgram()) {
+                abstractor = std::make_shared<storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>>(preprocessedModel.asPrismProgram(), smtSolverFactory);
+            } else {
+                abstractor = std::make_shared<storm::abstraction::jani::JaniMenuGameAbstractor<Type, ValueType>>(preprocessedModel.asJaniModel(), smtSolverFactory);
+            }
             
             // Create a refiner that can be used to refine the abstraction when needed.
-            storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(abstractor, smtSolverFactory->create(preprocessedModel.getManager()));
+            storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(*abstractor, smtSolverFactory->create(preprocessedModel.getManager()));
             refiner.refine(initialPredicates);
             
             // Enter the main-loop of abstraction refinement.
@@ -301,7 +314,7 @@ namespace storm {
 
                 // (1) build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
                 auto abstractionStart = std::chrono::high_resolution_clock::now();
-                storm::abstraction::MenuGame<Type, ValueType> game = abstractor.abstract();
+                storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract();
                 auto abstractionEnd = std::chrono::high_resolution_clock::now();
                 STORM_LOG_DEBUG("Abstraction in iteration " << iterations << " has " << game.getNumberOfStates() << " (player 1) states and " << game.getNumberOfTransitions() << " transitions (computed in " << std::chrono::duration_cast<std::chrono::milliseconds>(abstractionEnd - abstractionStart).count() << "ms).");
                 STORM_LOG_THROW(game.getInitialStates().getNonZeroCount(), storm::exceptions::InvalidModelException, "Cannot treat models with more than one (abstract) initial state.");
@@ -324,7 +337,7 @@ namespace storm {
                 QualitativeResultMinMax<Type> qualitativeResult;
                 std::unique_ptr<CheckResult> result = computeProb01States(checkTask, qualitativeResult, previousQualitativeResult, game, player1Direction, transitionMatrixBdd, initialStates, constraintStates, targetStates, refiner.addedAllGuards());
                 if (result) {
-                    printStatistics(abstractor, game);
+                    printStatistics(*abstractor, game);
                     return result;
                 }
                 previousQualitativeResult = qualitativeResult;
@@ -344,7 +357,7 @@ namespace storm {
                     
                     result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, initialStates, qualitativeResult);
                     if (result) {
-                        printStatistics(abstractor, game);
+                        printStatistics(*abstractor, game);
                         return result;
                     } else {
                         STORM_LOG_DEBUG("Obtained qualitative bounds [0, 1] on the actual value for the initial states.");
@@ -374,7 +387,7 @@ namespace storm {
                     previousMinQuantitativeResult = quantitativeResult.min;
                     result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, quantitativeResult.min.initialStateValue);
                     if (result) {
-                        printStatistics(abstractor, game);
+                        printStatistics(*abstractor, game);
                         return result;
                     }
                     
@@ -382,7 +395,7 @@ namespace storm {
                     quantitativeResult.max = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(quantitativeResult.min));
                     result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, quantitativeResult.max.initialStateValue);
                     if (result) {
-                        printStatistics(abstractor, game);
+                        printStatistics(*abstractor, game);
                         return result;
                     }
 
@@ -392,7 +405,7 @@ namespace storm {
                     // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
                     result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, quantitativeResult.min.initialStateValue, quantitativeResult.max.initialStateValue, comparator);
                     if (result) {
-                        printStatistics(abstractor, game);
+                        printStatistics(*abstractor, game);
                         return result;
                     }
 

src/storm/settings/modules/AbstractionSettings.cpp

@@ -37,9 +37,9 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, pivotHeuristicOptionName, true, "Sets the pivot selection heuristic.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available heuristic. Available are: 'nearest-max-dev', 'most-prob-path' and 'max-weighted-dev'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(pivotHeuristic)).setDefaultValueString("nearest-max-dev").build()).build());
 
-                std::vector<std::string> invalidBlockStrategies = {"none", "command", "global"};
+                std::vector<std::string> invalidBlockStrategies = {"none", "local", "global"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, invalidBlockStrategyOptionName, true, "Sets the strategy to detect invalid blocks.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'command' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("global").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of an available strategy. Available are: 'none', 'local' and 'global'.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(invalidBlockStrategies)).setDefaultValueString("global").build()).build());
                 
                 this->addOption(storm::settings::OptionBuilder(moduleName, reuseQualitativeResultsOptionName, true, "Sets whether to reuse qualitative results.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, reuseQuantitativeResultsOptionName, true, "Sets whether to reuse quantitative results.").build());
@@ -90,8 +90,8 @@ namespace storm {
                 std::string strategyName = this->getOption(invalidBlockStrategyOptionName).getArgumentByName("name").getValueAsString();
                 if (strategyName == "none") {
                     return AbstractionSettings::InvalidBlockDetectionStrategy::None;
-                } else if (strategyName == "command") {
-                    return AbstractionSettings::InvalidBlockDetectionStrategy::Command;
+                } else if (strategyName == "local") {
+                    return AbstractionSettings::InvalidBlockDetectionStrategy::Local;
                 } else if (strategyName == "global") {
                     return AbstractionSettings::InvalidBlockDetectionStrategy::Global;
                 }

src/storm/settings/modules/AbstractionSettings.h

@@ -16,7 +16,7 @@ namespace storm {
                 };
                 
                 enum class InvalidBlockDetectionStrategy {
-                    None, Command, Global
+                    None, Local, Global
                 };
                 
                 /*!

src/storm/storage/SymbolicModelDescription.cpp

@@ -127,5 +127,12 @@ namespace storm {
             return *this;
         }
         
+        void SymbolicModelDescription::requireNoUndefinedConstants() const {
+            if (this->isJaniModel()) {
+                storm::utility::jani::requireNoUndefinedConstants(this->asJaniModel());
+            } else {
+                storm::utility::prism::requireNoUndefinedConstants(this->asPrismProgram());
+            }
+        }
     }
 }

src/storm/storage/SymbolicModelDescription.h

@@ -40,6 +40,8 @@ namespace storm {
             
             SymbolicModelDescription preprocess(std::string const& constantDefinitionString = "") const;
             
+            void requireNoUndefinedConstants() const;
+            
         private:
             boost::optional<boost::variant<storm::jani::Model, storm::prism::Program>> modelDescription;
         };

src/storm/storage/jani/Automaton.cpp

@@ -97,6 +97,14 @@ namespace storm {
             return variables;
         }
         
+        std::set<storm::expressions::Variable> Automaton::getAllExpressionVariables() const {
+            std::set<storm::expressions::Variable> result;
+            for (auto const& variable : this->getVariables()) {
+                result.insert(variable.getExpressionVariable());
+            }
+            return result;
+        }
+        
         bool Automaton::hasTransientVariable() const {
             return variables.hasTransientVariable();
         }

src/storm/storage/jani/Automaton.h

@@ -135,6 +135,13 @@ namespace storm {
              */
             VariableSet const& getVariables() const;
             
+            /*!
+             * Retrieves all expression variables used by this automaton.
+             *
+             * @return The set of expression variables used by this automaton.
+             */
+            std::set<storm::expressions::Variable> getAllExpressionVariables() const;
+            
             /*!
              * Retrieves whether this automaton has a transient variable.
              */

src/storm/storage/jani/Edge.cpp

@@ -44,6 +44,10 @@ namespace storm {
             this->guard = guard;
         }
         
+        EdgeDestination const& Edge::getDestination(uint64_t index) const {
+            return destinations[index];
+        }
+        
         std::vector<EdgeDestination> const& Edge::getDestinations() const {
             return destinations;
         }
@@ -52,6 +56,10 @@ namespace storm {
             return destinations;
         }
         
+        std::size_t Edge::getNumberOfDestinations() const {
+            return destinations.size();
+        }
+        
         void Edge::addDestination(EdgeDestination const& destination) {
             destinations.push_back(destination);
         }

src/storm/storage/jani/Edge.h

@@ -61,6 +61,11 @@ namespace storm {
              * Sets a new guard for this edge.
              */
             void setGuard(storm::expressions::Expression const& guard);
+
+            /*!
+             * Retrieves the destination with the given index.
+             */
+            EdgeDestination const& getDestination(uint64_t index) const;
             
             /*!
              * Retrieves the destinations of this edge.
@@ -72,6 +77,11 @@ namespace storm {
              */
             std::vector<EdgeDestination>& getDestinations();
             
+            /*!
+             * Retrieves the number of destinations of this edge.
+             */
+            std::size_t getNumberOfDestinations() const;
+            
             /*!
              * Adds the given destination to the destinations of this edge.
              */

src/storm/storage/jani/EdgeDestination.cpp

@@ -34,6 +34,16 @@ namespace storm {
             this->probability = probability;
         }
         
+        std::map<storm::expressions::Variable, storm::expressions::Expression> EdgeDestination::getAsVariableToExpressionMap() const {
+            std::map<storm::expressions::Variable, storm::expressions::Expression> result;
+            
+            for (auto const& assignment : this->getOrderedAssignments()) {
+                result[assignment.getExpressionVariable()] = assignment.getAssignedExpression();
+            }
+            
+            return result;
+        }
+        
         OrderedAssignments const& EdgeDestination::getOrderedAssignments() const {
             return assignments;
         }

src/storm/storage/jani/EdgeDestination.h

@@ -39,6 +39,12 @@ namespace storm {
              */
             void setProbability(storm::expressions::Expression const& probability);
 
+            /*!
+             * Retrieves the mapping from variables to their assigned expressions that corresponds to the assignments
+             * of this destination.
+             */
+            std::map<storm::expressions::Variable, storm::expressions::Expression> getAsVariableToExpressionMap() const;
+            
             /*!
              * Retrieves the assignments to make when choosing this destination.
              */

src/storm/storage/jani/Model.cpp

@@ -154,6 +154,23 @@ namespace storm {
             return globalVariables;
         }
         
+        std::set<storm::expressions::Variable> Model::getAllExpressionVariables() const {
+            std::set<storm::expressions::Variable> result;
+            
+            for (auto const& constant : constants) {
+                result.insert(constant.getExpressionVariable());
+            }
+            for (auto const& variable : this->getGlobalVariables()) {
+                result.insert(variable.getExpressionVariable());
+            }
+            for (auto const& automaton : automata) {
+                auto const& automatonVariables = automaton.getAllExpressionVariables();
+                result.insert(automatonVariables.begin(), automatonVariables.end());
+            }
+            
+            return result;
+        }
+        
         bool Model::hasGlobalVariable(std::string const& name) const {
             return globalVariables.hasVariable(name);
         }

src/storm/storage/jani/Model.h

@@ -156,6 +156,13 @@ namespace storm {
              * Retrieves the variables of this automaton.
              */
             VariableSet const& getGlobalVariables() const;
+            
+            /*!
+             * Retrieves all expression variables used by this model.
+             *
+             * @return The set of expression variables used by this model.
+             */
+            std::set<storm::expressions::Variable> getAllExpressionVariables() const;
 
             /*!
              * Retrieves whether this model has a global variable with the given name.

src/storm/utility/jani.cpp

@@ -66,7 +66,24 @@ namespace storm {
                 
                 return constantDefinitions;
             }
-            
+         
+            void requireNoUndefinedConstants(storm::jani::Model const& model) {
+                if (model.hasUndefinedConstants()) {
+                    std::vector<std::reference_wrapper<storm::jani::Constant const>> undefinedConstants = model.getUndefinedConstants();
+                    std::stringstream stream;
+                    bool printComma = false;
+                    for (auto const& constant : undefinedConstants) {
+                        if (printComma) {
+                            stream << ", ";
+                        } else {
+                            printComma = true;
+                        }
+                        stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+                    }
+                    stream << ".";
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Model still contains these undefined constants: " + stream.str());
+                }
+            }
         }
     }
 }

src/storm/utility/jani.h

@@ -17,6 +17,7 @@ namespace storm {
             
             std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::jani::Model const& model, std::string const& constantDefinitionString);
             
+            void requireNoUndefinedConstants(storm::jani::Model const& model);
         }
     }
 }