From 0cd148c60020bf5f3adbbaf23e6aedb52e3cb331 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Fri, 18 Sep 2015 21:19:49 +0200
Subject: [PATCH] fixed more bugs. however, a test still fails, because the
abstraction is wrong
Former-commit-id: 6e326acaf3c89621f0e6861736ca6d7f60c99a85
---
.../prism/menu_games/AbstractCommand.cpp | 22 +-
.../prism/menu_games/AbstractProgram.cpp | 2 +
.../prism/menu_games/VariablePartition.cpp | 69 ++++---
.../abstraction/PrismMenuGameTest.cpp | 193 +++++++++++++++++-
4 files changed, 237 insertions(+), 49 deletions(-)
diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp
index 267ee38b6..bd019a4a9 100644
--- a/src/storage/prism/menu_games/AbstractCommand.cpp
+++ b/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;
diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp
index c515a9074..476b18aac 100644
--- a/src/storage/prism/menu_games/AbstractProgram.cpp
+++ b/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());
diff --git a/src/storage/prism/menu_games/VariablePartition.cpp b/src/storage/prism/menu_games/VariablePartition.cpp
index fc69ac1a4..f48df618f 100644
--- a/src/storage/prism/menu_games/VariablePartition.cpp
+++ b/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 << "{";
diff --git a/test/functional/abstraction/PrismMenuGameTest.cpp b/test/functional/abstraction/PrismMenuGameTest.cpp
index 8fdd03cdd..26b41e87a 100644
--- a/test/functional/abstraction/PrismMenuGameTest.cpp
+++ b/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
\ No newline at end of file