fixed more bugs. however, a test still fails, because the abstraction is wrong

Former-commit-id: 6e326acaf3

src/storage/prism/menu_games/AbstractCommand.cpp

@@ -56,9 +56,8 @@ namespace storm {
                 bool recomputeDd = this->relevantPredicatesChanged(newRelevantPredicates);
                 if (!recomputeDd) {
                     // If the new predicates are unrelated to the BDD of this command, we need to multiply their identities.
-                    for (auto predicateIndex : predicates) {
-                        cachedDd.first &= ddInformation.predicateIdentities[predicateIndex];
-                    }
+                    cachedDd.first &= computeMissingGlobalIdentities();
+                    cachedDd.first.toAdd().exportToDot("cmd" + std::to_string(command.get().getGlobalIndex()) + ".dot");
                 } else {
                     // If the DD needs recomputation, it is because of new relevant predicates, so we need to assert the appropriate clauses in the solver.
                     addMissingPredicates(newRelevantPredicates);
@@ -71,12 +70,11 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractCommand<DdType, ValueType>::recomputeCachedBdd() {
                 STORM_LOG_TRACE("Recomputing BDD for command " << command.get());
-                std::cout << "recomputing " << command.get() << std::endl;
-                
+
                 // Create a mapping from source state DDs to their distributions.
                 std::unordered_map<storm::dd::Bdd<DdType>, std::vector<storm::dd::Bdd<DdType>>> sourceToDistributionsMap;
                 uint_fast64_t modelCounter = 0;
-                smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); ++modelCounter; std::cout << "model cnt: " << modelCounter << std::endl;  return true; } );
+                smtSolver->allSat(decisionVariables, [&sourceToDistributionsMap,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { sourceToDistributionsMap[getSourceStateBdd(model)].push_back(getDistributionBdd(model)); 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.
@@ -112,6 +110,7 @@ namespace storm {
                 STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
                 
                 // Cache the result.
+                resultBdd.toAdd().exportToDot("cmd" + std::to_string(command.get().getGlobalIndex()) + ".dot");
                 cachedDd = std::make_pair(resultBdd, numberOfVariablesNeeded);
             }
             
@@ -122,11 +121,6 @@ namespace storm {
                 // To start with, all predicates related to the guard are relevant source predicates.
                 result.first = variablePartition.getExpressionsUsingVariables(command.get().getGuardExpression().getVariables());
                 
-                std::cout << "using" << std::endl;
-                for (auto const& el : result.first) {
-                    std::cout << expressionInformation.predicates[el] << std::endl;
-                }
-                
                 std::set<storm::expressions::Variable> assignedVariables;
                 for (auto const& assignment : assignments) {
                     // Also, variables appearing on the right-hand side of an assignment are relevant for source state.
@@ -144,12 +138,6 @@ namespace storm {
                 
                 auto const& predicatesRelatedToAssignedVariable = variablePartition.getRelatedExpressions(assignedVariables);
                 
-                std::cout << variablePartition << std::endl;
-                std::cout << "related" << std::endl;
-                for (auto const& el : predicatesRelatedToAssignedVariable) {
-                    std::cout << expressionInformation.predicates[el] << std::endl;
-                }
-
                 result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
                 
                 return result;

src/storage/prism/menu_games/AbstractProgram.cpp

@@ -69,6 +69,8 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractProgram<DdType, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) {
+                std::cout << " >>>> refine <<<<<<" << std::endl;
+                
                 // Add the predicates to the global list of predicates.
                 uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size();
                 expressionInformation.predicates.insert(expressionInformation.predicates.end(), predicates.begin(), predicates.end());

src/storage/prism/menu_games/VariablePartition.cpp

@@ -15,6 +15,7 @@ namespace storm {
                     this->variableToBlockMapping[variable] = currentBlock;
                     this->variableToExpressionsMapping[variable] = std::set<uint_fast64_t>();
                     variableBlocks[currentBlock].insert(variable);
+                    ++currentBlock;
                 }
                 
                 // Add all expressions, which might relate some variables.
@@ -67,35 +68,42 @@ namespace storm {
             }
             
             void VariablePartition::mergeBlocks(std::set<uint_fast64_t> const& blocksToMerge) {
-                // Determine which block to keep (to merge the other blocks into).
-                uint_fast64_t blockToKeep = *blocksToMerge.begin();
-                
                 // Merge all blocks into the block to keep.
                 std::vector<std::set<storm::expressions::Variable>> newVariableBlocks;
                 std::vector<std::set<uint_fast64_t>> newExpressionBlocks;
+                
+                std::set<uint_fast64_t>::const_iterator blocksToMergeIt = blocksToMerge.begin();
+                std::set<uint_fast64_t>::const_iterator blocksToMergeIte = blocksToMerge.end();
+
+                // Determine which block to keep (to merge the other blocks into).
+                uint_fast64_t blockToKeep = *blocksToMergeIt;
+                ++blocksToMergeIt;
+                
                 for (uint_fast64_t blockIndex = 0; blockIndex < variableBlocks.size(); ++blockIndex) {
-                    
-                    // If the block is the one into which the others are to be merged, we do so.
-                    if (blockIndex == blockToKeep) {
-                        for (auto const& blockToMerge : blocksToMerge) {
-                            if (blockToMerge == blockToKeep) {
-                                continue;
-                            }
-                            
-                            variableBlocks[blockToKeep].insert(variableBlocks[blockToMerge].begin(), variableBlocks[blockToMerge].end());
-                            expressionBlocks[blockToKeep].insert(expressionBlocks[blockToMerge].begin(), expressionBlocks[blockToMerge].end());
+                    // If the block is the next one to merge into the block to keep, do so now.
+                    if (blocksToMergeIt != blocksToMergeIte && *blocksToMergeIt == blockIndex && blockIndex != blockToKeep) {
+                        // Adjust the mapping for all variables of the old block.
+                        for (auto const& variable : variableBlocks[blockIndex]) {
+                            variableToBlockMapping[variable] = blockToKeep;
+                        }
+                        
+                        newVariableBlocks[blockToKeep].insert(variableBlocks[blockIndex].begin(), variableBlocks[blockIndex].end());
+                        newExpressionBlocks[blockToKeep].insert(expressionBlocks[blockIndex].begin(), expressionBlocks[blockIndex].end());
+                        ++blocksToMergeIt;
+                    } else {
+                        // Otherwise just move the current block to the new partition.
+                        newVariableBlocks.emplace_back(std::move(variableBlocks[blockIndex]));
+                        newExpressionBlocks.emplace_back(std::move(expressionBlocks[blockIndex]));
+                        
+                        // Adjust the mapping for all variables of the old block.
+                        for (auto const& variable : variableBlocks[blockIndex]) {
+                            variableToBlockMapping[variable] = newVariableBlocks.size() - 1;
                         }
                     }
-                    
-                    // Adjust the mapping for all variables we are moving to the new block.
-                    for (auto const& variable : variableBlocks[blockIndex]) {
-                        variableToBlockMapping[variable] = newVariableBlocks.size();
-                    }
-                    
-                    // Move the current block to the new partition.
-                    newVariableBlocks.emplace_back(std::move(variableBlocks[blockIndex]));
-                    newExpressionBlocks.emplace_back(std::move(expressionBlocks[blockIndex]));
                 }
+                
+                variableBlocks = std::move(newVariableBlocks);
+                expressionBlocks = std::move(newExpressionBlocks);
             }
             
             std::set<storm::expressions::Variable> const& VariablePartition::getBlockOfVariable(storm::expressions::Variable const& variable) const {
@@ -157,12 +165,23 @@ namespace storm {
 
             std::ostream& operator<<(std::ostream& out, VariablePartition const& partition) {
                 std::vector<std::string> blocks;
-                for (auto const& block : partition.variableBlocks) {
+                for (uint_fast64_t index = 0; index < partition.variableBlocks.size(); ++index) {
+                    auto const& variableBlock = partition.variableBlocks[index];
+                    auto const& expressionBlock = partition.expressionBlocks[index];
+
                     std::vector<std::string> variablesInBlock;
-                    for (auto const& variable : block) {
+                    for (auto const& variable : variableBlock) {
                         variablesInBlock.push_back(variable.getName());
                     }
-                    blocks.push_back("[" + boost::algorithm::join(variablesInBlock, ", ") + "]");
+                    
+                    std::vector<std::string> expressionsInBlock;
+                    for (auto const& expression : expressionBlock) {
+                        std::stringstream stream;
+                        stream << partition.expressions[expression];
+                        expressionsInBlock.push_back(stream.str());
+                    }
+
+                    blocks.push_back("<[" + boost::algorithm::join(variablesInBlock, ", ") + "], [" + boost::algorithm::join(expressionsInBlock, ", ") + "]>");
                 }
                 
                 out << "{";

test/functional/abstraction/PrismMenuGameTest.cpp

@@ -193,12 +193,10 @@ TEST(PrismMenuGame, CrowdsFullAbstractionTest) {
     storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
     ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
     
-    EXPECT_EQ(46, abstraction.getNodeCount());
-    
     storm::dd::Bdd<storm::dd::DdType::CUDD> reachableStatesInAbstraction;
     ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates());
     
-    EXPECT_EQ(13, reachableStatesInAbstraction.getNonZeroCount());
+    EXPECT_EQ(8607, reachableStatesInAbstraction.getNonZeroCount());
 }
 
 TEST(PrismMenuGame, TwoDiceAbstractionTest) {
@@ -240,8 +238,66 @@ TEST(PrismMenuGame, TwoDiceAbstractionAndRefinementTest) {
     
     ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("d1") + manager.getVariableExpression("d2") == manager.integer(7)}));
     ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(95, abstraction.getNodeCount());
+    
+    storm::dd::Bdd<storm::dd::DdType::CUDD> reachableStatesInAbstraction;
+    ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates());
+}
 
-    EXPECT_EQ(107, abstraction.getNodeCount());
+TEST(PrismMenuGame, TwoDiceFullAbstractionTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
+
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("d1") == manager.integer(6));
+    
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
+
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("d2") == manager.integer(6));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(1635, abstraction.getNodeCount());
+    
+    storm::dd::Bdd<storm::dd::DdType::CUDD> reachableStatesInAbstraction;
+    ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates());
+    
+    EXPECT_EQ(169, reachableStatesInAbstraction.getNonZeroCount());
 }
 
 TEST(PrismMenuGame, WlanAbstractionTest) {
@@ -261,7 +317,7 @@ TEST(PrismMenuGame, WlanAbstractionTest) {
     storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
     ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
     
-    EXPECT_EQ(219, abstraction.getNodeCount());
+    EXPECT_EQ(221, abstraction.getNodeCount());
 }
 
 TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
@@ -281,12 +337,135 @@ TEST(PrismMenuGame, WlanAbstractionAndRefinementTest) {
     storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
     ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
     
-    EXPECT_EQ(219, abstraction.getNodeCount());
+    EXPECT_EQ(221, abstraction.getNodeCount());
     
     ASSERT_NO_THROW(abstractProgram.refine({manager.getVariableExpression("backoff1") < manager.integer(7)}));
     ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
     
-    EXPECT_EQ(292, abstraction.getNodeCount());
+    EXPECT_EQ(287, abstraction.getNodeCount());
+}
+
+TEST(PrismMenuGame, WlanFullAbstractionTest) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/wlan0-2-2.nm");
+    program = program.substituteConstants();
+    program = program.flattenModules(std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>());
+    
+    std::vector<storm::expressions::Expression> initialPredicates;
+    storm::expressions::ExpressionManager& manager = program.getManager();
+    
+    initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("col") == manager.integer(2));
+
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("c1") == manager.integer(2));
+
+    initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("c2") == manager.integer(2));
+    
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("x1") == manager.integer(7));
+
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(7));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(8));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(9));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(10));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(11));
+    initialPredicates.push_back(manager.getVariableExpression("s1") == manager.integer(12));
+    
+    initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("slot1") == manager.integer(1));
+
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(7));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(8));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(9));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(10));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(11));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(12));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(13));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(14));
+    initialPredicates.push_back(manager.getVariableExpression("backoff1") == manager.integer(15));
+
+    initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("bc1") == manager.integer(1));
+    
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("x2") == manager.integer(7));
+    
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(7));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(8));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(9));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(10));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(11));
+    initialPredicates.push_back(manager.getVariableExpression("s2") == manager.integer(12));
+    
+    initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("slot2") == manager.integer(1));
+    
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(1));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(2));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(3));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(4));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(5));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(6));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(7));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(8));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(9));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(10));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(11));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(12));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(13));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(14));
+    initialPredicates.push_back(manager.getVariableExpression("backoff2") == manager.integer(15));
+    
+    initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(0));
+    initialPredicates.push_back(manager.getVariableExpression("bc2") == manager.integer(1));
+    
+    storm::prism::menu_games::AbstractProgram<storm::dd::DdType::CUDD, double> abstractProgram(program.getManager(), program, initialPredicates, std::make_unique<storm::utility::solver::MathsatSmtSolverFactory>(), false);
+    
+    storm::dd::Add<storm::dd::DdType::CUDD> abstraction;
+    ASSERT_NO_THROW(abstraction = abstractProgram.getAbstractAdd());
+    
+    EXPECT_EQ(2861, abstraction.getNodeCount());
+    
+    storm::dd::Bdd<storm::dd::DdType::CUDD> reachableStatesInAbstraction;
+    ASSERT_NO_THROW(reachableStatesInAbstraction = abstractProgram.getReachableStates());
+    
+    EXPECT_EQ(37, reachableStatesInAbstraction.getNonZeroCount());
 }
 
 #endif