sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

extended strategy redirection, better statistics

tempestpy_adaptions
dehnert 7 years ago
parent
8f4f5c555e
commit
e216d55320
6 changed files with 221 additions and 67 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 24
      src/storm/abstraction/MenuGameRefiner.cpp
  2. 35
      src/storm/abstraction/prism/CommandAbstractor.cpp
  3. 177
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  4. 8
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
  5. 28
      src/storm/settings/modules/AbstractionSettings.cpp
  6. 16
      src/storm/settings/modules/AbstractionSettings.h

24
src/storm/abstraction/MenuGameRefiner.cpp
View File

@ -870,14 +870,11 @@ namespace storm {
auto assertionStart = std::chrono::high_resolution_clock::now();
storm::solver::MathsatSmtSolver interpolatingSolver(interpolationManager, storm::solver::MathsatSmtSolver::Options(true, false, true));
uint64_t stepCounter = 0;
auto traceIt = trace.rbegin();
auto traceIte = trace.rend();
for (; traceIt != traceIte; ++traceIt) {
auto const& step = *traceIt;
interpolatingSolver.push();
for (auto const& traceElement : trace) {
// interpolatingSolver.push();
interpolatingSolver.setInterpolationGroup(stepCounter);
for (auto const& predicate : step) {
for (auto const& predicate : traceElement) {
interpolatingSolver.add(predicate);
}
@ -898,6 +895,7 @@ namespace storm {
storm::expressions::Expression interpolant = interpolatingSolver.getInterpolant(prefix).substitute(variableSubstitution).changeManager(abstractionInformation.getExpressionManager());
if (interpolant.isFalse()) {
// If the interpolant is false, it means that the prefix has become unsatisfiable.
STORM_LOG_TRACE("Trace formula became unsatisfiable at position " << step << " of " << stepCounter << ".");
break;
}
if (!interpolant.isTrue()) {
@ -1231,16 +1229,18 @@ namespace storm {
}
}
if (currentLower) {
performDijkstraStep(dijkstraQueue, probabilityDistances, lowerDistances, lowerPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, minStrategyPair, maxStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates);
} else {
performDijkstraStep(dijkstraQueue, probabilityDistances, upperDistances, upperPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, maxStrategyPair, minStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates);
// We only need to search further if the state has some value deviation.
if (!lowerValues || !upperValues || (*lowerValues)[currentState] < (*upperValues)[currentState]) {
if (currentLower) {
performDijkstraStep(dijkstraQueue, probabilityDistances, lowerDistances, lowerPredecessors, generatePredecessors, true, currentState, currentDistance, isPivotState, minStrategyPair, maxStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates);
} else {
performDijkstraStep(dijkstraQueue, probabilityDistances, upperDistances, upperPredecessors, generatePredecessors, false, currentState, currentDistance, isPivotState, maxStrategyPair, minStrategyPair, player1Labeling, player2Grouping, transitionMatrix, targetStates, relevantStates);
}
}
}
if (foundPivotState) {
ExplicitPivotStateResult<ValueType> result;
return result;
return ExplicitPivotStateResult<ValueType>(pivotState.state, pivotState.distance, pivotState.lower ? std::move(lowerPredecessors) : std::move(upperPredecessors));
}
// If we arrived at this point, we have explored all relevant states, but none of them was a pivot state,

35
src/storm/abstraction/prism/CommandAbstractor.cpp
View File

@ -565,7 +565,8 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::getSourceStateBdd(storm::solver::SmtSolver::ModelReference const& model, std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> const& variablePredicates) const {
storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
for (auto const& variableIndexPair : variablePredicates) {
for (auto variableIndexPairIt = variablePredicates.rbegin(), variableIndexPairIte = variablePredicates.rend(); variableIndexPairIt != variableIndexPairIte; ++variableIndexPairIt) {
auto const& variableIndexPair = *variableIndexPairIt;
if (model.getBooleanValue(variableIndexPair.first)) {
result &= this->getAbstractionInformation().encodePredicateAsSource(variableIndexPair.second);
} else {
@ -585,7 +586,8 @@ namespace storm {
storm::dd::Bdd<DdType> updateBdd = this->getAbstractionInformation().getDdManager().getBddOne();
// Translate block variables for this update into a successor block.
for (auto const& variableIndexPair : variablePredicates[updateIndex]) {
for (auto variableIndexPairIt = variablePredicates[updateIndex].rbegin(), variableIndexPairIte = variablePredicates[updateIndex].rend(); variableIndexPairIt != variableIndexPairIte; ++variableIndexPairIt) {
auto const& variableIndexPair = *variableIndexPairIt;
if (model.getBooleanValue(variableIndexPair.first)) {
updateBdd &= this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second);
} else {
@ -613,17 +615,21 @@ namespace storm {
for (uint_fast64_t updateIndex = 0; updateIndex < command.get().getNumberOfUpdates(); ++updateIndex) {
// Compute the identities that are missing for this update.
auto updateRelevantIt = relevantPredicatesAndVariables.second[updateIndex].begin();
auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end();
auto updateRelevantIt = relevantPredicatesAndVariables.second[updateIndex].rbegin();
auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].rend();
storm::dd::Bdd<DdType> updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne();
for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
for (uint_fast64_t predicateIndex = this->getAbstractionInformation().getNumberOfPredicates() - 1;; --predicateIndex) {
if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) {
updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
} else {
++updateRelevantIt;
}
if (predicateIndex == 0) {
break;
}
}
result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
@ -631,25 +637,6 @@ namespace storm {
return result;
}
// template <storm::dd::DdType DdType, typename ValueType>
// storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::computeMissingGlobalIdentities() const {
// storm::dd::Bdd<DdType> result = this->getAbstractionInformation().getDdManager().getBddOne();
//
// auto relevantIt = relevantPredicatesAndVariables.first.begin();
// auto relevantIte = relevantPredicatesAndVariables.first.end();
//
// for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
// if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
// std::cout << "adding global identity of predicate " << this->getAbstractionInformation().getPredicateByIndex(predicateIndex) << std::endl;
// result &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
// } else {
// ++relevantIt;
// }
// }
//
// return result;
// }
template <storm::dd::DdType DdType, typename ValueType>
GameBddResult<DdType> CommandAbstractor<DdType, ValueType>::abstract() {
if (forceRecomputation) {

177
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -91,6 +91,8 @@ namespace storm {
reuseQualitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Qualitative;
reuseQuantitativeResults = reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::All || reuseMode == storm::settings::modules::AbstractionSettings::ReuseMode::Quantitative;
maximalNumberOfAbstractions = abstractionSettings.getMaximalAbstractionCount();
fixPlayer1Strategy = abstractionSettings.isFixPlayer1StrategySet();
fixPlayer2Strategy = abstractionSettings.isFixPlayer2StrategySet();
}
template<storm::dd::DdType Type, typename ModelType>
@ -560,6 +562,8 @@ namespace storm {
boost::optional<SymbolicQualitativeGameResultMinMax<Type>> previousSymbolicQualitativeResult = boost::none;
boost::optional<SymbolicQuantitativeGameResult<Type, ValueType>> previousSymbolicMinQuantitativeResult = boost::none;
boost::optional<PreviousExplicitResult<ValueType>> previousExplicitResult = boost::none;
uint64_t peakPlayer1States = 0;
uint64_t peakTransitions = 0;
for (iteration = 0; iteration < maximalNumberOfAbstractions; ++iteration) {
auto iterationStart = std::chrono::high_resolution_clock::now();
STORM_LOG_TRACE("Starting iteration " << iteration << ".");
@ -569,7 +573,12 @@ namespace storm {
storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract();
abstractionWatch.stop();
totalAbstractionWatch.add(abstractionWatch);
STORM_LOG_INFO("Abstraction in iteration " << iteration << " has " << game.getNumberOfStates() << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << game.getNumberOfTransitions() << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << abstractionWatch.getTimeInMilliseconds() << "ms).");
uint64_t numberOfPlayer1States = game.getNumberOfStates();
peakPlayer1States = std::max(peakPlayer1States, numberOfPlayer1States);
uint64_t numberOfTransitions = game.getNumberOfTransitions();
peakTransitions = std::max(peakTransitions, numberOfTransitions);
STORM_LOG_INFO("Abstraction in iteration " << iteration << " has " << numberOfPlayer1States << " player 1 states (" << game.getInitialStates().getNonZeroCount() << " initial), " << game.getNumberOfPlayer2States() << " player 2 states, " << numberOfTransitions << " transitions, " << game.getBottomStates().getNonZeroCount() << " bottom states, " << abstractor->getNumberOfPredicates() << " predicate(s), " << game.getTransitionMatrix().getNodeCount() << " nodes (transition matrix) (computed in " << abstractionWatch.getTimeInMilliseconds() << "ms).");
// (2) Prepare initial, constraint and target state BDDs for later use.
storm::dd::Bdd<Type> initialStates = game.getInitialStates();
@ -596,7 +605,7 @@ namespace storm {
if (result) {
totalWatch.stop();
printStatistics(*abstractor, game, iteration);
printStatistics(*abstractor, game, iteration, peakPlayer1States, peakTransitions);
return result;
}
@ -712,54 +721,169 @@ namespace storm {
}
template <typename ValueType>
void postProcessStrategies(abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, bool sanityCheck) {
void postProcessStrategies(storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQualitativeGameResultMinMax const& qualitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck) {
if (!redirectPlayer1 && !redirectPlayer2) {
return;
}
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
bool isProb0Min = qualitativeResult.getProb0Min().getStates().get(state);
bool hasMinPlayer1Choice = false;
uint64_t lowerPlayer1Choice = 0;
bool hasMaxPlayer1Choice = false;
uint64_t upperPlayer1Choice = 0;
if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
hasMinPlayer1Choice = true;
lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state);
if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) {
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
if (lowerPlayer2Choice == upperPlayer2Choice) {
continue;
}
bool redirect = true;
if (isProb0Min) {
for (auto const& entry : transitionMatrix.getRow(upperPlayer2Choice)) {
if (!qualitativeResult.getProb0Min().getStates().get(entry.getColumn())) {
redirect = false;
break;
}
}
}
if (redirectPlayer2 && redirect) {
minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice);
}
}
}
bool lowerChoiceUnderUpperIsProb0 = false;
if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state);
if (lowerPlayer1Choice != upperPlayer1Choice && minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) {
hasMaxPlayer1Choice = true;
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (lowerPlayer2Choice == upperPlayer2Choice) {
continue;
}
lowerChoiceUnderUpperIsProb0 = true;
for (auto const& entry : transitionMatrix.getRow(lowerPlayer2Choice)) {
if (!qualitativeResult.getProb0Min().getStates().get(entry.getColumn())) {
lowerChoiceUnderUpperIsProb0 = false;
break;
}
}
bool redirect = true;
if (lowerChoiceUnderUpperIsProb0) {
for (auto const& entry : transitionMatrix.getRow(upperPlayer2Choice)) {
if (!qualitativeResult.getProb0Min().getStates().get(entry.getColumn())) {
redirect = false;
break;
}
}
}
if (redirectPlayer2 && redirect) {
minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice);
}
}
}
if (redirectPlayer1 && player1Direction == storm::OptimizationDirection::Minimize) {
if (hasMinPlayer1Choice && hasMaxPlayer1Choice && lowerPlayer1Choice != upperPlayer1Choice) {
if (!isProb0Min || lowerChoiceUnderUpperIsProb0) {
minStrategyPair.getPlayer1Strategy().setChoice(state, upperPlayer1Choice);
}
}
}
}
}
template <typename ValueType>
void postProcessStrategies(storm::OptimizationDirection const& player1Direction, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair, std::vector<uint64_t> const& player1Groups, std::vector<uint64_t> const& player2Groups, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, ExplicitQuantitativeResultMinMax<ValueType> const& quantitativeResult, bool redirectPlayer1, bool redirectPlayer2, bool sanityCheck) {
if (!redirectPlayer1 && !redirectPlayer2) {
return;
}
for (uint64_t state = 0; state < player1Groups.size() - 1; ++state) {
STORM_LOG_ASSERT(targetStates.get(state) || minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected lower player 1 choice in state " << state << ".");
STORM_LOG_ASSERT(targetStates.get(state) || maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state), "Expected upper player 1 choice in state " << state << ".");
bool hasMinPlayer1Choice = false;
uint64_t lowerPlayer1Choice = 0;
ValueType lowerValueUnderMinChoicePlayer1 = storm::utility::zero<ValueType>();
bool hasMaxPlayer1Choice = false;
uint64_t upperPlayer1Choice = 0;
ValueType lowerValueUnderMaxChoicePlayer1 = storm::utility::zero<ValueType>();
if (minStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
uint64_t lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state);
hasMinPlayer1Choice = true;
lowerPlayer1Choice = minStrategyPair.getPlayer1Strategy().getChoice(state);
STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (upper player 1 choice " << lowerPlayer1Choice << ").");
STORM_LOG_ASSERT(minStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice), "Expected lower player 2 choice for state " << state << " (lower player 1 choice " << lowerPlayer1Choice << ").");
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
lowerValueUnderMinChoicePlayer1 = lowerValueUnderLowerChoicePlayer2;
if (maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(lowerPlayer1Choice)) {
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(lowerPlayer1Choice);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) {
if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) {
lowerValueUnderMinChoicePlayer1 = lowerValueUnderUpperChoicePlayer2;
minStrategyPair.getPlayer2Strategy().setChoice(lowerPlayer1Choice, upperPlayer2Choice);
if (sanityCheck) {
STORM_LOG_TRACE("[min] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice);
}
}
}
}
}
if (maxStrategyPair.getPlayer1Strategy().hasDefinedChoice(state)) {
uint64_t upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state);
upperPlayer1Choice = maxStrategyPair.getPlayer1Strategy().getChoice(state);
STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ").");
uint64_t upperPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) {
if (upperPlayer1Choice != lowerPlayer1Choice && minStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice)) {
hasMaxPlayer1Choice = true;
uint64_t lowerPlayer2Choice = minStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
ValueType lowerValueUnderLowerChoicePlayer2 = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
lowerValueUnderMaxChoicePlayer1 = lowerValueUnderLowerChoicePlayer2;
STORM_LOG_ASSERT(maxStrategyPair.getPlayer2Strategy().hasDefinedChoice(upperPlayer1Choice), "Expected upper player 2 choice for state " << state << " (upper player 1 choice " << upperPlayer1Choice << ").");
uint64_t upperPlayer2Choice = maxStrategyPair.getPlayer2Strategy().getChoice(upperPlayer1Choice);
if (lowerPlayer2Choice != upperPlayer2Choice) {
ValueType lowerValueUnderLowerChoice = transitionMatrix.multiplyRowWithVector(lowerPlayer2Choice, quantitativeResult.getMin().getValues());
ValueType lowerValueUnderUpperChoice = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
ValueType lowerValueUnderUpperChoicePlayer2 = transitionMatrix.multiplyRowWithVector(upperPlayer2Choice, quantitativeResult.getMin().getValues());
if (lowerValueUnderUpperChoice <= lowerValueUnderLowerChoice) {
if (redirectPlayer2 && lowerValueUnderUpperChoicePlayer2 <= lowerValueUnderLowerChoicePlayer2) {
minStrategyPair.getPlayer2Strategy().setChoice(upperPlayer1Choice, upperPlayer2Choice);
STORM_LOG_TRACE("[max] redirecting choice of state " << state << ": " << lowerValueUnderLowerChoice << " vs. " << lowerValueUnderUpperChoice);
}
}
}
}
if (redirectPlayer1 && player1Direction == storm::OptimizationDirection::Minimize) {
if (hasMinPlayer1Choice && hasMaxPlayer1Choice && lowerPlayer1Choice != upperPlayer1Choice) {
if (lowerValueUnderMaxChoicePlayer1 <= lowerValueUnderMinChoicePlayer1) {
minStrategyPair.getPlayer1Strategy().setChoice(state, upperPlayer1Choice);
}
}
}
}
if (sanityCheck) {
@ -894,6 +1018,9 @@ namespace storm {
STORM_LOG_INFO("Obtained qualitative bounds [0, 1] on the actual value for the initial states. Refining abstraction based on qualitative check.");
// Post-process strategies for better refinements.
postProcessStrategies(player1Direction, minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, qualitativeResult, this->fixPlayer1Strategy, this->fixPlayer2Strategy, this->debug);
// If we get here, the initial states were all identified as prob0/1 states, but the value (0 or 1)
// depends on whether player 2 is minimizing or maximizing. Therefore, we need to find a place to refine.
storm::utility::Stopwatch refinementWatch(true);
@ -937,7 +1064,8 @@ namespace storm {
return result;
}
postProcessStrategies(minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, quantitativeResult, this->debug);
// Post-process strategies for better refinements.
postProcessStrategies(player1Direction, minStrategyPair, maxStrategyPair, player1Groups, player2RowGrouping, transitionMatrix, constraintStates, targetStates, quantitativeResult, this->fixPlayer1Strategy, this->fixPlayer2Strategy, this->debug);
// Make sure that all strategies are still valid strategies.
STORM_LOG_ASSERT(minStrategyPair.getNumberOfUndefinedPlayer1States() <= targetStates.getNumberOfSetBits(), "Expected at most " << targetStates.getNumberOfSetBits() << " (number of target states) player 1 states with undefined choice but got " << minStrategyPair.getNumberOfUndefinedPlayer1States() << ".");
@ -1128,7 +1256,7 @@ namespace storm {
}
template<storm::dd::DdType Type, typename ModelType>
void GameBasedMdpModelChecker<Type, ModelType>::printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, uint64_t refinements) const {
void GameBasedMdpModelChecker<Type, ModelType>::printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, uint64_t refinements, uint64_t peakPlayer1States, uint64_t peakTransitions) const {
if (storm::settings::getModule<storm::settings::modules::CoreSettings>().isShowStatisticsSet()) {
storm::abstraction::AbstractionInformation<Type> const& abstractionInformation = abstractor.getAbstractionInformation();
@ -1137,10 +1265,11 @@ namespace storm {
std::cout << std::endl;
std::cout << "Statistics:" << std::endl;
std::cout << " * size of final game: " << game.getReachableStates().getNonZeroCount() << " player 1 states" << std::endl;
std::cout << " * size of final game: " << game.getReachableStates().getNonZeroCount() << " player 1 states, " << game.getTransitionMatrix().getNonZeroCount() << " transitions" << std::endl;
std::cout << " * peak size of game: " << peakPlayer1States << " player 1 states, " << peakTransitions << " transitions" << std::endl;
std::cout << " * transitions (final game): " << game.getTransitionMatrix().getNonZeroCount() << std::endl;
std::cout << " * refinements: " << refinements << std::endl;
std::cout << " * predicates used in abstraction: " << abstractionInformation.getNumberOfPredicates() << std::endl << std::endl;
std::cout << " * predicates: " << abstractionInformation.getNumberOfPredicates() << std::endl << std::endl;
uint64_t totalAbstractionTimeMillis = totalAbstractionWatch.getTimeInMilliseconds();
uint64_t totalTranslationTimeMillis = totalTranslationWatch.getTimeInMilliseconds();

8
src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.h
View File

@ -115,7 +115,7 @@ namespace storm {
ExplicitQualitativeGameResultMinMax computeProb01States(boost::optional<detail::PreviousExplicitResult<ValueType>> const& previousResult, storm::dd::Odd const& odd, storm::OptimizationDirection player1Direction, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint64_t> const& player1RowGrouping, storm::storage::SparseMatrix<ValueType> const& player1BackwardTransitions, std::vector<uint64_t> const& player2BackwardTransitions, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, abstraction::ExplicitGameStrategyPair& minStrategyPair, abstraction::ExplicitGameStrategyPair& maxStrategyPair);
void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, uint64_t refinements) const;
void printStatistics(storm::abstraction::MenuGameAbstractor<Type, ValueType> const& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, uint64_t refinements, uint64_t peakPlayer1States, uint64_t peakTransitions) const;
/*
* Retrieves the expression characterized by the formula. The formula needs to be propositional.
@ -150,6 +150,12 @@ namespace storm {
/// The performed number of refinement iterations.
uint64_t iteration;
/// A flag indicating whether to fix player 1 strategies.
bool fixPlayer1Strategy;
/// A flag indicating whether to fix player 2 strategies.
bool fixPlayer2Strategy;
/// A flag that indicates whether debug mode is enabled.
bool debug;

28
src/storm/settings/modules/AbstractionSettings.cpp
View File

@ -29,7 +29,9 @@ namespace storm {
const std::string AbstractionSettings::constraintsOptionName = "constraints";
const std::string AbstractionSettings::useEagerRefinementOptionName = "eagerref";
const std::string AbstractionSettings::debugOptionName = "debug";
const std::string AbstractionSettings::injectRefinementPredicatesOption = "injectref";
const std::string AbstractionSettings::injectRefinementPredicatesOptionName = "injectref";
const std::string AbstractionSettings::fixPlayer1StrategyOptionName = "fixpl1strat";
const std::string AbstractionSettings::fixPlayer2StrategyOptionName = "fixpl2strat";
AbstractionSettings::AbstractionSettings() : ModuleSettings(moduleName) {
std::vector<std::string> methods = {"games", "bisimulation", "bisim"};
@ -106,10 +108,20 @@ namespace storm {
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("constraints", "The constraints to use.").build())
.build());
this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOption, true, "Specifies predicates used by the refinement instead of the derived predicates.")
this->addOption(storm::settings::OptionBuilder(moduleName, injectRefinementPredicatesOptionName, true, "Specifies predicates used by the refinement instead of the derived predicates.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("predicates", "The (semicolon-separated) refinement predicates to use.").build())
.build());
this->addOption(storm::settings::OptionBuilder(moduleName, fixPlayer1StrategyOptionName, true, "Sets whether to fix player 1 strategies.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
.setDefaultValueString("on").build())
.build());
this->addOption(storm::settings::OptionBuilder(moduleName, fixPlayer2StrategyOptionName, true, "Sets whether to fix player 2 strategies.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
.setDefaultValueString("on").build())
.build());
this->addOption(storm::settings::OptionBuilder(moduleName, debugOptionName, true, "Sets whether to enable debug mode.")
.addArgument(storm::settings::ArgumentBuilder::createStringArgument("value", "The value of the flag.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(onOff))
.setDefaultValueString("off").build())
@ -225,11 +237,19 @@ namespace storm {
}
bool AbstractionSettings::isInjectRefinementPredicatesSet() const {
return this->getOption(injectRefinementPredicatesOption).getHasOptionBeenSet();
return this->getOption(injectRefinementPredicatesOptionName).getHasOptionBeenSet();
}
std::string AbstractionSettings::getInjectedRefinementPredicates() const {
return this->getOption(injectRefinementPredicatesOption).getArgumentByName("predicates").getValueAsString();
return this->getOption(injectRefinementPredicatesOptionName).getArgumentByName("predicates").getValueAsString();
}
bool AbstractionSettings::isFixPlayer1StrategySet() const {
return this->getOption(fixPlayer1StrategyOptionName).getArgumentByName("value").getValueAsString() == "on";
}
bool AbstractionSettings::isFixPlayer2StrategySet() const {
return this->getOption(fixPlayer2StrategyOptionName).getArgumentByName("value").getValueAsString() == "on";
}
}

16
src/storm/settings/modules/AbstractionSettings.h
View File

@ -161,7 +161,17 @@ namespace storm {
* Retrieves a string containing refinement predicates to inject (if there are any).
*/
std::string getInjectedRefinementPredicates() const;
/*!
* Retrieves whether player 1 strategies are to be fixed.
*/
bool isFixPlayer1StrategySet() const;
/*!
* Retrieves whether player 2 strategies are to be fixed.
*/
bool isFixPlayer2StrategySet() const;
const static std::string moduleName;
private:
@ -181,7 +191,9 @@ namespace storm {
const static std::string constraintsOptionName;
const static std::string useEagerRefinementOptionName;
const static std::string debugOptionName;
const static std::string injectRefinementPredicatesOption;
const static std::string injectRefinementPredicatesOptionName;
const static std::string fixPlayer1StrategyOptionName;
const static std::string fixPlayer2StrategyOptionName;
};
}

Write Preview
Loading…
Cancel
Save