diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp
new file mode 100644
index 000000000..e31327157
--- /dev/null
+++ b/src/storm/abstraction/MenuGameRefiner.cpp
@@ -0,0 +1,22 @@
+#include "storm/abstraction/MenuGameRefiner.h"
+
+#include "storm/abstraction/MenuGameAbstractor.h"
+
+namespace storm {
+ namespace abstraction {
+
+ template<storm::dd::DdType Type, typename ValueType>
+ MenuGameRefiner<Type, ValueType>::MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor) : abstractor(abstractor) {
+ // Intentionally left empty.
+ }
+
+ template<storm::dd::DdType Type, typename ValueType>
+ void MenuGameRefiner<Type, ValueType>::refine(std::vector<storm::expressions::Expression> const& predicates) const {
+ abstractor.get().refine(predicates);
+ }
+
+ template class MenuGameRefiner<storm::dd::DdType::CUDD, double>;
+ template class MenuGameRefiner<storm::dd::DdType::Sylvan, double>;
+
+ }
+}
diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h
new file mode 100644
index 000000000..b6a9e7482
--- /dev/null
+++ b/src/storm/abstraction/MenuGameRefiner.h
@@ -0,0 +1,37 @@
+#pragma once
+
+#include <functional>
+#include <vector>
+
+#include "storm/storage/expressions/Expression.h"
+
+#include "storm/storage/dd/DdType.h"
+
+namespace storm {
+ namespace abstraction {
+
+ template <storm::dd::DdType DdType, typename ValueType>
+ class MenuGameAbstractor;
+
+ template<storm::dd::DdType Type, typename ValueType>
+ class MenuGameRefiner {
+ public:
+ /*!
+ * Creates a refiner for the provided abstractor.
+ */
+ MenuGameRefiner(MenuGameAbstractor<Type, ValueType>& abstractor);
+
+ /*!
+ * Refines the abstractor with the given set of predicates.
+ */
+ void refine(std::vector<storm::expressions::Expression> const& predicates) const;
+
+
+
+ private:
+ /// The underlying abstractor to refine.
+ std::reference_wrapper<MenuGameAbstractor<Type, ValueType>> abstractor;
+ };
+
+ }
+}
diff --git a/src/storm/abstraction/StateSetAbstractor.cpp b/src/storm/abstraction/StateSetAbstractor.cpp
index 0483635b6..50da8f008 100644
--- a/src/storm/abstraction/StateSetAbstractor.cpp
+++ b/src/storm/abstraction/StateSetAbstractor.cpp
@@ -14,7 +14,7 @@ namespace storm {
namespace abstraction {
template <storm::dd::DdType DdType, typename ValueType>
- StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddZero()), constraint(abstractionInformation.getDdManager().getBddOne()) {
+ StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionInformation<DdType>& abstractionInformation, std::set<storm::expressions::Variable> const& allVariables, std::vector<storm::expressions::Expression> const& statePredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : smtSolver(smtSolverFactory->create(abstractionInformation.getExpressionManager())), abstractionInformation(abstractionInformation), localExpressionInformation(allVariables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(abstractionInformation.getDdManager().getBddOne()), constraint(abstractionInformation.getDdManager().getBddOne()) {
// Assert all state predicates.
for (auto const& predicate : statePredicates) {
@@ -101,8 +101,7 @@ namespace storm {
STORM_LOG_TRACE("Recomputing BDD for state set abstraction.");
storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddZero();
- uint_fast64_t modelCounter = 0;
- smtSolver->allSat(decisionVariables, [&result,this,&modelCounter] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); ++modelCounter; return true; } );
+ smtSolver->allSat(decisionVariables, [&result,this] (storm::solver::SmtSolver::ModelReference const& model) { result |= getStateBdd(model); return true; } );
cachedBdd = result;
}
diff --git a/src/storm/abstraction/prism/AbstractCommand.cpp b/src/storm/abstraction/prism/AbstractCommand.cpp
index 63a889472..dd9b51efc 100644
--- a/src/storm/abstraction/prism/AbstractCommand.cpp
+++ b/src/storm/abstraction/prism/AbstractCommand.cpp
@@ -23,7 +23,7 @@ namespace storm {
namespace abstraction {
namespace prism {
template <storm::dd::DdType DdType, typename ValueType>
- AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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), abstractGuard(abstractionInformation.getDdManager().getBddZero()), bottomStateAbstractor(abstractionInformation, abstractionInformation.getExpressionVariables(), {!command.getGuardExpression()}, smtSolverFactory) {
+ AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionInformation<DdType>& abstractionInformation, std::shared_ptr<storm::utility::solver::SmtSolverFactory> 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), forceRecomputation(true), 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());
@@ -36,17 +36,10 @@ namespace storm {
// Assert the guard of the command.
smtSolver->add(command.getGuardExpression());
-
- // Refine the command based on all initial predicates.
- std::vector<uint_fast64_t> allPredicateIndices(abstractionInformation.getNumberOfPredicates());
- for (uint_fast64_t index = 0; index < abstractionInformation.getNumberOfPredicates(); ++index) {
- allPredicateIndices[index] = index;
- }
- this->refine(allPredicateIndices, true);
}
template <storm::dd::DdType DdType, typename ValueType>
- void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates, bool forceRecomputation) {
+ void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
// Add all predicates to the variable partition.
for (auto predicateIndex : predicates) {
localExpressionInformation.addExpression(this->getAbstractionInformation().getPredicateByIndex(predicateIndex), predicateIndex);
@@ -69,6 +62,9 @@ namespace storm {
// Finally recompute the cached BDD.
this->recomputeCachedBdd();
+
+ // Disable forcing recomputation until it is set again.
+ forceRecomputation = false;
}
// Refine bottom state abstractor. Note that this does not trigger a recomputation yet.
@@ -322,6 +318,7 @@ namespace storm {
// If the guard of this command is a predicate, there are not bottom states/transitions.
if (guardIsPredicate) {
+ STORM_LOG_TRACE("Guard is predicate, no bottom state transitions for this command.");
return result;
}
@@ -329,7 +326,7 @@ namespace storm {
// 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() && this->getAbstractionInformation().getBottomStateBdd(false, false);
diff --git a/src/storm/abstraction/prism/AbstractCommand.h b/src/storm/abstraction/prism/AbstractCommand.h
index 5a67d4a30..600693bbf 100644
--- a/src/storm/abstraction/prism/AbstractCommand.h
+++ b/src/storm/abstraction/prism/AbstractCommand.h
@@ -65,9 +65,8 @@ namespace storm {
* Refines the abstract command with the given predicates.
*
* @param predicates The new predicates.
- * @param forceRecomputation If set, the BDD is recomputed even if the relevant predicates have not changed.
*/
- void refine(std::vector<uint_fast64_t> const& predicates, bool forceRecomputation = false);
+ void refine(std::vector<uint_fast64_t> const& predicates);
/*!
* Computes the abstraction of the command wrt. to the current set of predicates.
@@ -227,6 +226,9 @@ namespace storm {
// is no need to compute bottom states.
bool guardIsPredicate;
+ // A flag remembering whether we need to force recomputation of the BDD.
+ bool forceRecomputation;
+
// 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<DdType> abstractGuard;
diff --git a/src/storm/abstraction/prism/AbstractProgram.cpp b/src/storm/abstraction/prism/AbstractProgram.cpp
index 29e627806..c6738a740 100644
--- a/src/storm/abstraction/prism/AbstractProgram.cpp
+++ b/src/storm/abstraction/prism/AbstractProgram.cpp
@@ -29,7 +29,6 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
AbstractProgram<DdType, ValueType>::AbstractProgram(storm::prism::Program const& program,
- std::vector<storm::expressions::Expression> const& initialPredicates,
std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory,
bool addAllGuards, bool splitPredicates)
: program(program), smtSolverFactory(smtSolverFactory), abstractionInformation(program.getManager()), modules(), initialStateAbstractor(abstractionInformation, program.getAllExpressionVariables(), {program.getInitialStatesExpression()}, this->smtSolverFactory), splitPredicates(splitPredicates), splitter(), equivalenceChecker(smtSolverFactory->create(abstractionInformation.getExpressionManager()), abstractionInformation.getExpressionManager().boolean(true)), addedAllGuards(addAllGuards), currentGame(nullptr) {
@@ -58,7 +57,7 @@ namespace storm {
}
maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates()));
}
-
+
totalNumberOfCommands += module.getNumberOfCommands();
}
@@ -76,23 +75,19 @@ namespace storm {
commandUpdateProbabilitiesAdd = modules.front().getCommandUpdateProbabilitiesAdd();
// Now that we have created all other DD variables, we create the DD variables for the predicates.
- std::vector<std::pair<storm::expressions::Expression, bool>> allPredicates;
- for (auto const& predicate : initialPredicates) {
- allPredicates.push_back(std::make_pair(predicate, false));
- }
+ std::vector<std::pair<storm::expressions::Expression, bool>> initialPredicates;
if (addAllGuards) {
for (auto const& guard : allGuards) {
- allPredicates.push_back(std::make_pair(guard, true));
+ initialPredicates.push_back(std::make_pair(guard, true));
}
}
+
// Finally, refine using the all predicates and build game as a by-product.
- this->refine(allPredicates);
+ this->refine(initialPredicates);
}
template <storm::dd::DdType DdType, typename ValueType>
void AbstractProgram<DdType, ValueType>::refine(std::vector<std::pair<storm::expressions::Expression, bool>> const& predicates) {
- STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates.");
-
// Add the predicates to the global list of predicates.
std::vector<uint_fast64_t> newPredicateIndices;
for (auto const& predicateAllowSplitPair : predicates) {
@@ -132,7 +127,7 @@ namespace storm {
// Refine initial state abstractor.
initialStateAbstractor.refine(newPredicateIndices);
-
+
// Finally, we rebuild the game.
currentGame = buildGame();
}
@@ -240,7 +235,7 @@ namespace storm {
#endif
std::map<uint_fast64_t, storm::storage::BitVector> upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice);
STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
-
+
#ifdef LOCAL_DEBUG
std::cout << "lower" << std::endl;
for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) {
@@ -268,6 +263,9 @@ namespace storm {
for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) {
if (lowerIt->second.get(predicateIndex) != upperIt->second.get(predicateIndex)) {
// Now we know the point of the deviation (command, update, predicate).
+ std::cout << "ref" << std::endl;
+ std::cout << abstractionInformation.getPredicateByIndex(predicateIndex) << std::endl;
+ std::cout << concreteCommand.getUpdate(updateIndex) << std::endl;
newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(concreteCommand.getUpdate(updateIndex).getAsVariableToExpressionMap()).simplify();
break;
}
@@ -298,12 +296,12 @@ namespace storm {
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>> AbstractProgram<DdType, ValueType>::buildGame() {
// As long as there is only one module, we only build its game representation.
GameBddResult<DdType> game = modules.front().getAbstractBdd();
-
+
// 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);
@@ -326,7 +324,7 @@ namespace storm {
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());
bool hasBottomStates = false;
@@ -345,17 +343,17 @@ namespace storm {
reachableStates &= abstractionInformation.getBottomStateBdd(true, true);
initialStates &= abstractionInformation.getBottomStateBdd(true, true);
- // If there are bottom transitions, exnted the transition matrix and reachable states now.
+ // 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());
@@ -363,7 +361,7 @@ namespace storm {
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 AbstractProgram<DdType, ValueType>::exportToDot(std::string const& filename, storm::dd::Bdd<DdType> const& highlightStatesBdd, storm::dd::Bdd<DdType> const& filter) const {
std::ofstream out(filename);
@@ -402,7 +400,7 @@ namespace storm {
}
highlightStates.insert(stateName.str());
}
-
+
out << "digraph game {" << std::endl;
// Create the player 1 nodes.
@@ -504,7 +502,7 @@ namespace storm {
template class AbstractProgram<storm::dd::DdType::CUDD, double>;
template class AbstractProgram<storm::dd::DdType::Sylvan, double>;
#ifdef STORM_HAVE_CARL
- template class AbstractProgram<storm::dd::DdType::Sylvan, storm::RationalFunction>;
+ template class AbstractProgram<storm::dd::DdType::Sylvan, storm::RationalFunction>;
#endif
}
}
diff --git a/src/storm/abstraction/prism/AbstractProgram.h b/src/storm/abstraction/prism/AbstractProgram.h
index 5cfca0f41..d20ca12e0 100644
--- a/src/storm/abstraction/prism/AbstractProgram.h
+++ b/src/storm/abstraction/prism/AbstractProgram.h
@@ -42,12 +42,11 @@ namespace storm {
*
* @param expressionManager The manager responsible for the expressions of the program.
* @param program The concrete program for which to build the abstraction.
- * @param initialPredicates The initial set of predicates.
* @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
* @param addAllGuards A flag that indicates whether all guards of the program should be added to the initial set of predicates.
* @param splitPredicates A flag that indicates whether the predicates are to be split into atoms before being added.
*/
- AbstractProgram(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false, bool splitPredicates = false);
+ AbstractProgram(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>(), bool addAllGuards = false, bool splitPredicates = false);
AbstractProgram(AbstractProgram const&) = default;
AbstractProgram& operator=(AbstractProgram const&) = default;
diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
index e6ce56eca..7c5a22861 100644
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
+++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
@@ -10,7 +10,7 @@ namespace storm {
namespace prism {
template <storm::dd::DdType DdType, typename ValueType>
- PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : abstractProgram(program, initialPredicates, smtSolverFactory, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet(), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitPredicatesSet()) {
+ PrismMenuGameAbstractor<DdType, ValueType>::PrismMenuGameAbstractor(storm::prism::Program const& program, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : abstractProgram(program, smtSolverFactory, storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isAddAllGuardsSet(), storm::settings::getModule<storm::settings::modules::AbstractionSettings>().isSplitPredicatesSet()) {
// Intentionally left empty.
}
diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
index 7214a380e..84fd5ec36 100644
--- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
+++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.h
@@ -11,7 +11,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
class PrismMenuGameAbstractor : public MenuGameAbstractor<DdType, ValueType> {
public:
- PrismMenuGameAbstractor(storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, 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 = std::make_shared<storm::utility::solver::MathsatSmtSolverFactory>());
virtual storm::abstraction::MenuGame<DdType, ValueType> abstract() override;
virtual void refine(std::vector<storm::expressions::Expression> const& predicates) override;
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index cf5596dfa..fc0313ab5 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/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/MenuGameRefiner.h"
#include "storm/logic/FragmentSpecification.h"
@@ -261,6 +262,7 @@ namespace storm {
if (lowerChoicesDifferent) {
STORM_LOG_TRACE("Refining based on lower choice.");
auto refinementStart = std::chrono::high_resolution_clock::now();
+
abstractor.refine(pivotState, (pivotState && minPlayer1Strategy).existsAbstract(game.getRowVariables()), lowerChoice1, lowerChoice2);
auto refinementEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Refinement completed in " << std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count() << "ms.");
@@ -466,9 +468,11 @@ namespace storm {
storm::OptimizationDirection player1Direction = getPlayer1Direction(checkTask);
// Create the abstractor.
- storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedModel.asPrismProgram(), initialPredicates, smtSolverFactory);
+ storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType> abstractor(preprocessedModel.asPrismProgram(), smtSolverFactory);
- // TODO: create refiner and move initial predicates there.
+ // Create a refiner that can be used to refine the abstraction when needed.
+ storm::abstraction::MenuGameRefiner<Type, ValueType> refiner(abstractor);
+ refiner.refine(initialPredicates);
// Enter the main-loop of abstraction refinement.
for (uint_fast64_t iterations = 0; iterations < 10000; ++iterations) {
@@ -526,6 +530,7 @@ namespace storm {
}
}
+ // (6) if we arrived at this point and no refinement was made, we need to compute the quantitative solution.
if (!qualitativeRefinement) {
// At this point, we know that we cannot answer the query without further numeric computation.
@@ -534,14 +539,14 @@ namespace storm {
STORM_LOG_TRACE("Starting numerical solution step.");
auto quantitativeStart = std::chrono::high_resolution_clock::now();
- // Solve the min values and check whether we can give the answer already.
+ // (7) Solve the min values and check whether we can give the answer already.
QuantitativeResult<Type, ValueType> minResult = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Minimize, game, qualitativeResult, initialStatesAdd, maybeMin);
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Minimize, minResult.initialStateValue);
if (result) {
return result;
}
- // Solve the max values and check whether we can give the answer already.
+ // (8) Solve the max values and check whether we can give the answer already.
QuantitativeResult<Type, ValueType> maxResult = computeQuantitativeResult(player1Direction, storm::OptimizationDirection::Maximize, game, qualitativeResult, initialStatesAdd, maybeMax, boost::make_optional(minResult));
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, storm::OptimizationDirection::Maximize, maxResult.initialStateValue);
if (result) {
@@ -551,27 +556,20 @@ namespace storm {
auto quantitativeEnd = std::chrono::high_resolution_clock::now();
STORM_LOG_DEBUG("Obtained quantitative bounds [" << minResult.initialStateValue << ", " << maxResult.initialStateValue << "] on the actual value for the initial states in " << std::chrono::duration_cast<std::chrono::milliseconds>(quantitativeEnd - quantitativeStart).count() << "ms.");
+ // (9) Check whether the lower and upper bounds are close enough to terminate with an answer.
result = checkForResultAfterQuantitativeCheck<ValueType>(checkTask, minResult.initialStateValue, maxResult.initialStateValue);
if (result) {
return result;
}
- // If we arrived at this point, it means that we have all qualitative and quantitative information
- // about the game, but we could not yet answer the query. In this case, we need to refine.
-
// Make sure that all strategies are still valid strategies.
STORM_LOG_ASSERT(minResult.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for min is illegal.");
STORM_LOG_ASSERT(maxResult.player1Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer1Variables()).getMax() <= 1, "Player 1 strategy for max is illegal.");
STORM_LOG_ASSERT(minResult.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for min is illegal.");
STORM_LOG_ASSERT(maxResult.player2Strategy.template toAdd<ValueType>().sumAbstract(game.getPlayer2Variables()).getMax() <= 1, "Player 2 strategy for max is illegal.");
-#ifdef LOCAL_DEBUG
- // Check whether the strategies coincide over the reachable parts.
-// storm::dd::Bdd<Type> tmp = game.getTransitionMatrix().toBdd() && (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy);
-// storm::dd::Bdd<Type> commonReach = storm::utility::dd::computeReachableStates(initialStates, tmp.existsAbstract(game.getNondeterminismVariables()), game.getRowVariables(), game.getColumnVariables());
-// STORM_LOG_ASSERT((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy) || (commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy), "The strategies fully coincide.");
-#endif
-
+ // (10) If we arrived at this point, it means that we have all qualitative and quantitative
+ // information about the game, but we could not yet answer the query. In this case, we need to refine.
refineAfterQuantitativeCheck(abstractor, game, transitionMatrixBdd, minResult, maxResult);
}
auto iterationEnd = std::chrono::high_resolution_clock::now();
@@ -632,7 +630,11 @@ namespace storm {
result = storm::utility::graph::performProb1(game, transitionMatrixBdd, constraintStates, targetStates, player1Direction, player2Direction, true, true);
}
- STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
+ if (prob0) {
+ STORM_LOG_ASSERT(result.hasPlayer1Strategy() && (result.getPlayer1States().isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
+ } else {
+ STORM_LOG_ASSERT(result.hasPlayer1Strategy() && ((result.getPlayer1States() && !targetStates).isZero() || !result.getPlayer1Strategy().isZero()), "Unable to proceed without strategy.");
+ }
STORM_LOG_ASSERT(result.hasPlayer2Strategy() && (result.getPlayer2States().isZero() || !result.getPlayer2Strategy().isZero()), "Unable to proceed without strategy.");
STORM_LOG_TRACE("Computed states with probability " << (prob0 ? "0" : "1") << " (player 1: " << player1Direction << ", player 2: " << player2Direction << "): " << result.getPlayer1States().getNonZeroCount() << " '" << (prob0 ? "no" : "yes") << "' states.");
diff --git a/src/storm/utility/graph.cpp b/src/storm/utility/graph.cpp
index 499817ce0..ceecdfb18 100644
--- a/src/storm/utility/graph.cpp
+++ b/src/storm/utility/graph.cpp
@@ -961,7 +961,10 @@ namespace storm {
// Since we have determined the complements of the desired sets, we need to complement it now.
player1States = !player1States && model.getReachableStates();
- player2States = !player2States && model.getReachableStates();
+
+ std::set<storm::expressions::Variable> variablesToAbstract(model.getColumnVariables());
+ variablesToAbstract.insert(model.getPlayer2Variables().begin(), model.getPlayer2Variables().end());
+ player2States = !player2States && transitionMatrix.existsAbstract(variablesToAbstract);
// Determine all transitions between prob0 states.
storm::dd::Bdd<Type> transitionsBetweenProb0States = player2States && (transitionMatrix && player1States.swapVariables(model.getRowColumnMetaVariablePairs()));