diff --git a/src/abstraction/AbstractionInformation.cpp b/src/abstraction/AbstractionInformation.cpp index afa80f2a0..a5500092b 100644 --- a/src/abstraction/AbstractionInformation.cpp +++ b/src/abstraction/AbstractionInformation.cpp @@ -155,24 +155,24 @@ namespace storm { } template - storm::dd::Bdd AbstractionInformation::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, 0, numberOfVariables, player1VariableBdds); + storm::dd::Bdd AbstractionInformation::encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) const { + return encodeChoice(index, 0, end, player1VariableBdds); } template - storm::dd::Bdd AbstractionInformation::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, 0, numberOfVariables, player2VariableBdds); + storm::dd::Bdd AbstractionInformation::encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const { + return encodeChoice(index, 0, end, player2VariableBdds); } template - storm::dd::Bdd AbstractionInformation::encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const { - return encodeChoice(index, offset, numberOfVariables, auxVariableBdds); + storm::dd::Bdd AbstractionInformation::encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const { + return encodeChoice(index, start, end, auxVariableBdds); } template - storm::dd::Bdd AbstractionInformation::getPlayer2ZeroCube(uint_fast64_t numberOfVariables, uint_fast64_t offset) const { + storm::dd::Bdd AbstractionInformation::getPlayer2ZeroCube(uint_fast64_t start, uint_fast64_t end) const { storm::dd::Bdd result = ddManager->getBddOne(); - for (uint_fast64_t index = offset; index < numberOfVariables; ++index) { + for (uint_fast64_t index = start; index < end; ++index) { result &= player2VariableBdds[index]; } STORM_LOG_ASSERT(!result.isZero(), "Zero cube must not be zero."); @@ -205,8 +205,8 @@ namespace storm { } template - std::set AbstractionInformation::getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const { - return std::set(auxVariables.begin() + offset, auxVariables.begin() + offset + count); + std::set AbstractionInformation::getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const { + return std::set(auxVariables.begin() + start, auxVariables.begin() + end); } template @@ -298,10 +298,9 @@ namespace storm { } template - storm::dd::Bdd AbstractionInformation::encodeChoice(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables, std::vector> const& variables) const { + storm::dd::Bdd AbstractionInformation::encodeChoice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end, std::vector> const& variables) const { storm::dd::Bdd result = ddManager->getBddOne(); - numberOfVariables += offset; - for (uint_fast64_t bitIndex = numberOfVariables; bitIndex > offset; --bitIndex) { + for (uint_fast64_t bitIndex = end; bitIndex > start; --bitIndex) { if ((index & 1) != 0) { result &= variables[bitIndex - 1]; } else { diff --git a/src/abstraction/AbstractionInformation.h b/src/abstraction/AbstractionInformation.h index 2c076daae..fab9c1526 100644 --- a/src/abstraction/AbstractionInformation.h +++ b/src/abstraction/AbstractionInformation.h @@ -174,29 +174,29 @@ namespace storm { * Encodes the given index using the indicated player 1 variables. * * @param index The index to encode. - * @param numberOfVariables The number of variables to use for encoding the index. + * @param end The index of the variable past the end of the range that is used to encode the index. * @return The index encoded as a BDD. */ - storm::dd::Bdd encodePlayer1Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const; + storm::dd::Bdd encodePlayer1Choice(uint_fast64_t index, uint_fast64_t end) const; /*! * Encodes the given index using the indicated player 2 variables. * * @param index The index to encode. - * @param numberOfVariables The number of variables to use for encoding the index. + * @param end The index of the variable past the end of the range that is used to encode the index. * @return The index encoded as a BDD. */ - storm::dd::Bdd encodePlayer2Choice(uint_fast64_t index, uint_fast64_t numberOfVariables) const; + storm::dd::Bdd encodePlayer2Choice(uint_fast64_t index, uint_fast64_t end) const; /*! * Encodes the given index using the indicated probabilistic branching variables. * * @param index The index to encode. - * @param offset The offset within the auxiliary variables at which to start encoding. - * @param numberOfVariables The number of variables to use for encoding the index. + * @param start The index of the first variable of the range that is used to encode the index. + * @param end The index of the variable past the end of the range that is used to encode the index. * @return The index encoded as a BDD. */ - storm::dd::Bdd encodeAux(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables) const; + storm::dd::Bdd encodeAux(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end) const; /*! * Retrieves the cube of player 2 variables in the given range [offset, numberOfVariables). @@ -262,11 +262,11 @@ namespace storm { /*! * Retrieves the requested set of auxiliary variables. * - * @param offset The offset at which to start gatherin the auxiliary variables. - * @param count The number of auxiliary variables to include. + * @param start The index of the first auxiliary variable to include. + * @param end The index of the auxiliary variable past the end of the range to include. * @return The set of auxiliary variables. */ - std::set getAuxVariableSet(uint_fast64_t offset, uint_fast64_t count) const; + std::set getAuxVariableSet(uint_fast64_t start, uint_fast64_t end) const; /*! * Retrieves the number of auxiliary variables. @@ -356,11 +356,11 @@ namespace storm { * Encodes the given index with the given number of variables from the given variables. * * @param index The index to encode. - * @param offset The offset at which to start encoding. - * @param numberOfVariables The total number of variables to use. + * @param start The index of the first variable to use for the encoding. + * @param end The index of the variable past the end of the range to use for the encoding. * @param variables The BDDs of the variables to use to encode the index. */ - storm::dd::Bdd encodeChoice(uint_fast64_t index, uint_fast64_t offset, uint_fast64_t numberOfVariables, std::vector> const& variables) const; + storm::dd::Bdd encodeChoice(uint_fast64_t index, uint_fast64_t start, uint_fast64_t end, std::vector> const& variables) const; // The expression related data. diff --git a/src/abstraction/BottomStateResult.cpp b/src/abstraction/BottomStateResult.cpp new file mode 100644 index 000000000..32b1417b7 --- /dev/null +++ b/src/abstraction/BottomStateResult.cpp @@ -0,0 +1,14 @@ +#include "src/abstraction/BottomStateResult.h" + +namespace storm { + namespace abstraction { + + template + BottomStateResult::BottomStateResult(storm::dd::Bdd const& states, storm::dd::Bdd const& transitions) : states(states), transitions(transitions) { + // Intentionally left empty. + } + + template class BottomStateResult; + template class BottomStateResult; + } +} \ No newline at end of file diff --git a/src/abstraction/BottomStateResult.h b/src/abstraction/BottomStateResult.h new file mode 100644 index 000000000..c3f2f69d4 --- /dev/null +++ b/src/abstraction/BottomStateResult.h @@ -0,0 +1,19 @@ +#pragma once + +#include "src/storage/dd/DdType.h" +#include "src/storage/dd/Bdd.h" + +namespace storm { + namespace abstraction { + + template + struct BottomStateResult { + public: + BottomStateResult(storm::dd::Bdd const& states, storm::dd::Bdd const& transitions); + + storm::dd::Bdd states; + storm::dd::Bdd transitions; + }; + + } +} \ No newline at end of file diff --git a/src/abstraction/MenuGame.cpp b/src/abstraction/MenuGame.cpp index 4ada7add8..10b8c2fe4 100644 --- a/src/abstraction/MenuGame.cpp +++ b/src/abstraction/MenuGame.cpp @@ -28,6 +28,7 @@ namespace storm { std::set const& probabilisticBranchingVariables, std::map> const& expressionToBddMap) : storm::models::symbolic::StochasticTwoPlayerGame(manager, reachableStates, initialStates, deadlockStates, transitionMatrix.sumAbstract(probabilisticBranchingVariables), rowVariables, nullptr, columnVariables, nullptr, rowColumnMetaVariablePairs, player1Variables, player2Variables, allNondeterminismVariables), probabilisticBranchingVariables(probabilisticBranchingVariables), expressionToBddMap(expressionToBddMap), bottomStates(bottomStates) { // Intentionally left empty. + this->getTransitionMatrix().exportToDot("trans.dot"); } template diff --git a/src/abstraction/StateSetAbstractor.cpp b/src/abstraction/StateSetAbstractor.cpp index 97874d080..35bedcd73 100644 --- a/src/abstraction/StateSetAbstractor.cpp +++ b/src/abstraction/StateSetAbstractor.cpp @@ -125,6 +125,8 @@ namespace storm { // Create a new backtracking point before adding the constraint. smtSolver->push(); + constraint.template toAdd().exportToDot("constraint.dot"); + // Create the constraint. std::pair, std::unordered_map> result = constraint.toExpression(this->getAbstractionInformation().getExpressionManager()); diff --git a/src/abstraction/prism/AbstractCommand.cpp b/src/abstraction/prism/AbstractCommand.cpp index ade2e85b7..723d67b41 100644 --- a/src/abstraction/prism/AbstractCommand.cpp +++ b/src/abstraction/prism/AbstractCommand.cpp @@ -3,6 +3,7 @@ #include #include "src/abstraction/AbstractionInformation.h" +#include "src/abstraction/BottomStateResult.h" #include "src/storage/dd/DdManager.h" #include "src/storage/dd/Add.h" @@ -17,7 +18,7 @@ namespace storm { namespace abstraction { namespace prism { template - AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0), decisionVariables(), guardIsPredicate(guardIsPredicate), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { + AbstractCommand::AbstractCommand(storm::prism::Command const& command, AbstractionInformation& abstractionInformation, std::shared_ptr const& smtSolverFactory, bool guardIsPredicate) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), command(command), localExpressionInformation(abstractionInformation.getVariables()), evaluator(abstractionInformation.getExpressionManager()), relevantPredicatesAndVariables(), cachedDd(abstractionInformation.getDdManager().getBddZero(), 0, 0), decisionVariables(), guardIsPredicate(guardIsPredicate), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) { // Make the second component of relevant predicates have the right size. relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates()); @@ -37,9 +38,6 @@ namespace storm { allPredicateIndices[index] = index; } this->refine(allPredicateIndices); - - // Refine the bottom state abstractor. - bottomStateAbstractor.refine(allPredicateIndices); } template @@ -97,8 +95,15 @@ namespace storm { // Finally, build overall result. storm::dd::Bdd resultBdd = this->getAbstractionInformation().getDdManager().getBddZero(); + if (!guardIsPredicate) { + abstractGuard = this->getAbstractionInformation().getDdManager().getBddZero(); + } uint_fast64_t sourceStateIndex = 0; for (auto const& sourceDistributionsPair : sourceToDistributionsMap) { + if (!guardIsPredicate) { + 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."); storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); @@ -236,7 +241,7 @@ namespace storm { } else { updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } - updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); + updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()); } result |= updateBdd; @@ -275,7 +280,7 @@ namespace storm { } } - result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); + result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()); } return result; } @@ -301,11 +306,32 @@ namespace storm { return cachedDd; } + template + BottomStateResult AbstractCommand::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); + + // Use the state abstractor to compute the set of abstract states that has this command enabled but + // still has a transition to a bottom state. + bottomStateAbstractor.constrain(reachableStates && abstractGuard); + result.states = bottomStateAbstractor.getAbstractStates(); + + // Now equip all these states with an actual transition to a bottom state. + result.transitions = result.states && this->getAbstractionInformation().getAllPredicateIdentities(); + + // Add the command encoding and the next free player 2 encoding. + result.transitions &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()) && this->getAbstractionInformation().encodePlayer2Choice(cachedDd.nextFreePlayer2Index, cachedDd.numberOfPlayer2Variables); + + result.states.template toAdd().exportToDot("bottom_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + result.transitions.template toAdd().exportToDot("bottom_trans_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + + return result; + } + template storm::dd::Add AbstractCommand::getCommandUpdateProbabilitiesAdd() const { storm::dd::Add result = this->getAbstractionInformation().getDdManager().template getAddZero(); for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) { - result += this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); + result += this->getAbstractionInformation().encodeAux(updateIndex, 1, this->getAbstractionInformation().getAuxVariableCount()).template toAdd() * this->getAbstractionInformation().getDdManager().getConstant(evaluator.asRational(command.get().getUpdate(updateIndex).getLikelihoodExpression())); } result *= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()).template toAdd(); return result; diff --git a/src/abstraction/prism/AbstractCommand.h b/src/abstraction/prism/AbstractCommand.h index 3000d6474..f972873e8 100644 --- a/src/abstraction/prism/AbstractCommand.h +++ b/src/abstraction/prism/AbstractCommand.h @@ -40,7 +40,10 @@ namespace storm { namespace abstraction { template class AbstractionInformation; - + + template + class BottomStateResult; + namespace prism { template struct GameBddResult; @@ -73,6 +76,15 @@ namespace storm { */ GameBddResult getAbstractBdd(); + /*! + * Retrieves the transitions to bottom states of this command. + * + * @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 getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); + /*! * Retrieves an ADD that maps the encoding of the command and its updates to their probabilities. * @@ -201,6 +213,10 @@ namespace storm { // is no need to compute bottom states. bool guardIsPredicate; + // The abstract guard of the command. 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 abstractGuard; + // A state-set abstractor used to determine the bottom states if not all guards were added. StateSetAbstractor bottomStateAbstractor; }; diff --git a/src/abstraction/prism/AbstractModule.cpp b/src/abstraction/prism/AbstractModule.cpp index 46fc41da5..ee76febf4 100644 --- a/src/abstraction/prism/AbstractModule.cpp +++ b/src/abstraction/prism/AbstractModule.cpp @@ -1,6 +1,7 @@ #include "src/abstraction/prism/AbstractModule.h" #include "src/abstraction/AbstractionInformation.h" +#include "src/abstraction/BottomStateResult.h" #include "src/abstraction/prism/GameBddResult.h" #include "src/storage/dd/DdManager.h" @@ -50,11 +51,13 @@ namespace storm { } template - storm::dd::Bdd AbstractModule::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { - storm::dd::Bdd result = this->getAbstractionInformation().getDdManager().getBddZero(); + BottomStateResult AbstractModule::getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables) { + BottomStateResult result(this->getAbstractionInformation().getDdManager().getBddZero(), this->getAbstractionInformation().getDdManager().getBddZero()); for (auto& command : commands) { - result |= command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); + BottomStateResult commandBottomStateResult = command.getBottomStateTransitions(reachableStates, numberOfPlayer2Variables); + result.states |= commandBottomStateResult.states; + result.transitions |= commandBottomStateResult.transitions; } return result; diff --git a/src/abstraction/prism/AbstractModule.h b/src/abstraction/prism/AbstractModule.h index 57f78aaf1..f8016ec61 100644 --- a/src/abstraction/prism/AbstractModule.h +++ b/src/abstraction/prism/AbstractModule.h @@ -17,12 +17,14 @@ namespace storm { namespace abstraction { template class AbstractionInformation; + + template + struct BottomStateResult; namespace prism { template struct GameBddResult; - template class AbstractModule { public: @@ -60,9 +62,9 @@ namespace storm { * * @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. + * @return The bottom states and the necessary transitions. */ - storm::dd::Bdd getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); + BottomStateResult getBottomStateTransitions(storm::dd::Bdd const& reachableStates, uint_fast64_t numberOfPlayer2Variables); /*! * Retrieves an ADD that maps the encodings of commands and their updates to their probabilities. diff --git a/src/abstraction/prism/AbstractProgram.cpp b/src/abstraction/prism/AbstractProgram.cpp index 9ca9dd9c5..c0fd0459b 100644 --- a/src/abstraction/prism/AbstractProgram.cpp +++ b/src/abstraction/prism/AbstractProgram.cpp @@ -1,5 +1,7 @@ #include "src/abstraction/prism/AbstractProgram.h" +#include "src/abstraction/BottomStateResult.h" + #include "src/storage/prism/Program.h" #include "src/storage/dd/DdManager.h" @@ -54,7 +56,7 @@ namespace storm { // 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(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount)))); + abstractionInformation.createEncodingVariables(static_cast(std::ceil(std::log2(totalNumberOfCommands))), 100, static_cast(std::ceil(std::log2(maximalUpdateCount))) + 1); // Now that we have created all other DD variables, we create the DD variables for the predicates. std::vector allPredicateIndices; @@ -127,31 +129,18 @@ namespace storm { std::set variablesToAbstract(abstractionInformation.getPlayer1VariableSet(abstractionInformation.getPlayer1VariableCount())); auto player2Variables = abstractionInformation.getPlayer2VariableSet(game.numberOfPlayer2Variables); variablesToAbstract.insert(player2Variables.begin(), player2Variables.end()); - auto probBranchingVariables = abstractionInformation.getAuxVariableSet(0, abstractionInformation.getAuxVariableCount()); - variablesToAbstract.insert(probBranchingVariables.begin(), probBranchingVariables.end()); + auto auxVariables = abstractionInformation.getAuxVariableSet(1, abstractionInformation.getAuxVariableCount()); + variablesToAbstract.insert(auxVariables.begin(), auxVariables.end()); + std::cout << "vars" << std::endl; + for (auto const& var : auxVariables) { + std::cout << var.getName() << std::endl; + } // Do a reachability analysis on the raw transition relation. storm::dd::Bdd transitionRelation = game.bdd.existsAbstract(variablesToAbstract); storm::dd::Bdd initialStates = initialStateAbstractor.getAbstractStates(); storm::dd::Bdd reachableStates = this->getReachableStates(initialStates, transitionRelation); - storm::dd::Bdd bottomStateTransitions = abstractionInformation.getDdManager().getBddZero(); - storm::dd::Bdd bottomStates = bottomStateTransitions; - if (addedAllGuards) { - bottomStateTransitions = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); - - // If there are transitions to the bottom states, add them and register the new states as well. - transitionRelation |= bottomStateTransitions; - } - - // Determine the bottom states. - if (addedAllGuards) { - bottomStates = abstractionInformation.getDdManager().getBddZero(); - } else { - bottomStateAbstractor.constrain(reachableStates); - bottomStates = bottomStateAbstractor.getAbstractStates(); - } - // 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 deadlockStates = transitionRelation.existsAbstract(abstractionInformation.getSuccessorVariables()); @@ -163,15 +152,22 @@ namespace storm { deadlockTransitions = (deadlockStates && abstractionInformation.getAllPredicateIdentities() && abstractionInformation.encodePlayer1Choice(0, abstractionInformation.getPlayer1VariableCount()) && abstractionInformation.encodePlayer2Choice(0, game.numberOfPlayer2Variables) && abstractionInformation.encodeAux(0, 0, abstractionInformation.getAuxVariableCount())).template toAdd(); } + // Compute bottom states and the appropriate transitions if necessary. + BottomStateResult bottomStateResult(abstractionInformation.getDdManager().getBddZero(), abstractionInformation.getDdManager().getBddZero()); + if (!addedAllGuards) { + bottomStateResult = modules.front().getBottomStateTransitions(reachableStates, game.numberOfPlayer2Variables); + } + // Construct the transition matrix by cutting away the transitions of unreachable states. - storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions; + storm::dd::Add transitionMatrix = (game.bdd && reachableStates).template toAdd() * commandUpdateProbabilitiesAdd + deadlockTransitions;// + bottomStateResult.transitions.template toAdd(); + transitionMatrix.exportToDot("trans_upd.dot"); std::set usedPlayer2Variables(abstractionInformation.getPlayer2Variables().begin(), abstractionInformation.getPlayer2Variables().begin() + game.numberOfPlayer2Variables); std::set allNondeterminismVariables = usedPlayer2Variables; allNondeterminismVariables.insert(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()); - return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStates, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, std::set(abstractionInformation.getAuxVariables().begin(), abstractionInformation.getAuxVariables().end()), abstractionInformation.getPredicateToBddMap()); + return std::make_unique>(abstractionInformation.getDdManagerAsSharedPointer(), reachableStates, initialStates, abstractionInformation.getDdManager().getBddZero(), transitionMatrix, bottomStateResult.states, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables(), abstractionInformation.getSourceSuccessorVariablePairs(), std::set(abstractionInformation.getPlayer1Variables().begin(), abstractionInformation.getPlayer1Variables().end()), usedPlayer2Variables, allNondeterminismVariables, auxVariables, abstractionInformation.getPredicateToBddMap()); } template diff --git a/src/abstraction/prism/GameBddResult.cpp b/src/abstraction/prism/GameBddResult.cpp index 01780ebcd..df22713d7 100644 --- a/src/abstraction/prism/GameBddResult.cpp +++ b/src/abstraction/prism/GameBddResult.cpp @@ -13,7 +13,9 @@ namespace storm { GameBddResult::GameBddResult(storm::dd::Bdd const& gameBdd, uint_fast64_t numberOfPlayer2Variables, uint_fast64_t nextFreePlayer2Index) : bdd(gameBdd), numberOfPlayer2Variables(numberOfPlayer2Variables), nextFreePlayer2Index(nextFreePlayer2Index) { // Intentionally left empty. } - + + template class GameBddResult; + template class GameBddResult; } } } \ No newline at end of file