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

changing command decomposition of game-based abstraction and further debugging

main
dehnert 8 years ago
parent
7ef779a8a6
commit
e780572560
5 changed files with 52 additions and 87 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. 4
      src/storm/abstraction/MenuGameRefiner.cpp
  2. 108
      src/storm/abstraction/prism/CommandAbstractor.cpp
  3. 14
      src/storm/abstraction/prism/CommandAbstractor.h
  4. 11
      src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
  5. 2
      src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

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

@ -279,6 +279,10 @@ namespace storm {
// Decode both choices to explicit mappings.
std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping<ValueType>(lowerChoice);
std::map<uint64_t, std::pair<storm::storage::BitVector, ValueType>> upperChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping<ValueType>(upperChoice);
lowerChoice.template toAdd<ValueType>().exportToDot("lower.dot");
upperChoice.template toAdd<ValueType>().exportToDot("upper.dot");
STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
// First, sort updates according to probability mass.

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

@ -98,7 +98,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
void CommandAbstractor<DdType, ValueType>::recomputeCachedBddWithDecomposition() {
STORM_LOG_TRACE("Recomputing BDD for command " << command.get() << " using the decomposition.");
STORM_LOG_TRACE("Recomputing BDD for command with index " << command.get().getGlobalIndex() << " (" << command.get() << ") using the decomposition.");
auto start = std::chrono::high_resolution_clock::now();
// compute a decomposition of the command
@ -205,18 +205,16 @@ namespace storm {
relevantBlockPartition = std::move(cleanedRelevantBlockPartition);
STORM_LOG_TRACE("Decomposition into " << relevantBlockPartition.size() << " blocks.");
for (auto const& block : relevantBlockPartition) {
STORM_LOG_TRACE("New block of size " << block.size() << ":");
std::set<uint64_t> blockPredicateIndices;
for (auto const& innerBlock : block) {
blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end());
}
for (auto const& predicateIndex : blockPredicateIndices) {
STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex));
}
}
// for (auto const& block : relevantBlockPartition) {
// std::set<uint64_t> blockPredicateIndices;
// for (auto const& innerBlock : block) {
// blockPredicateIndices.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end());
// }
//
// for (auto const& predicateIndex : blockPredicateIndices) {
// STORM_LOG_TRACE(abstractionInformation.get().getPredicateByIndex(predicateIndex));
// }
// }
std::set<storm::expressions::Variable> variablesContainedInGuard = command.get().getGuardExpression().getVariables();
@ -240,8 +238,6 @@ namespace storm {
uint64_t numberOfSolutions = 0;
uint64_t numberOfTotalSolutions = 0;
std::cout << localExpressionInformation << std::endl;
// If we need to enumerate the guard, do it only once now.
if (enumerateAbstractGuard) {
std::set<uint64_t> relatedGuardPredicates = localExpressionInformation.getRelatedExpressions(variablesContainedInGuard);
@ -260,8 +256,6 @@ namespace storm {
return true;
});
STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions for abstract guard.");
abstractGuard.template toAdd<ValueType>().exportToDot("abstractguard" + std::to_string(command.get().getGlobalIndex()) + ".dot");
// Now that we have the abstract guard, we can add it as an assertion to the solver before enumerating
// the other solutions.
@ -301,9 +295,7 @@ namespace storm {
std::vector<storm::expressions::Variable> transitionDecisionVariables;
std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> sourceVariablesAndPredicates;
for (auto const& element : relevantPredicatesAndVariables.first) {
std::cout << "1-querying " << abstractionInformation.get().getPredicateByIndex(element.second) << std::endl;
if (relevantPredicates.find(element.second) != relevantPredicates.end()) {
std::cout << "1-is relevant!" << std::endl;
transitionDecisionVariables.push_back(element.first);
sourceVariablesAndPredicates.push_back(element);
}
@ -314,14 +306,11 @@ namespace storm {
destinationVariablesAndPredicates.emplace_back();
for (auto const& assignment : command.get().getUpdate(updateIndex).getAssignments()) {
uint64_t assignmentVariableBlockIndex = localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable());
std::cout << "assignment variable " << assignment.getVariable().getName() << " block index: " << assignmentVariableBlockIndex << std::endl;
if (block.find(assignmentVariableBlockIndex) != block.end()) {
std::set<uint64_t> const& assignmentVariableBlock = localExpressionInformation.getExpressionBlock(assignmentVariableBlockIndex);
for (auto const& element : relevantPredicatesAndVariables.second[updateIndex]) {
std::cout << "2-querying " << abstractionInformation.get().getPredicateByIndex(element.second) << std::endl;
if (assignmentVariableBlock.find(element.second) != assignmentVariableBlock.end()) {
std::cout << "2-is relevant!" << std::endl;
destinationVariablesAndPredicates.back().push_back(element);
transitionDecisionVariables.push_back(element.first);
}
@ -350,7 +339,6 @@ namespace storm {
// We now compute how many variables we need to encode the choices. We add one to the maximal number of
// choices to account for a possible transition to a bottom state.
uint_fast64_t numberOfVariablesNeeded = static_cast<uint_fast64_t>(std::ceil(std::log2(maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0))));
std::cout << "need " << numberOfVariablesNeeded << " variables for " << (maximalNumberOfChoices + (blockCounter == 0 ? 1 : 0)) << " choices" << std::endl;
// Finally, build overall result.
storm::dd::Bdd<DdType> resultBdd = this->getAbstractionInformation().getDdManager().getBddZero();
@ -365,7 +353,6 @@ namespace storm {
storm::dd::Bdd<DdType> allDistributions = this->getAbstractionInformation().getDdManager().getBddZero();
for (auto const& distribution : sourceDistributionsPair.second) {
allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, usedNondeterminismVariables, usedNondeterminismVariables + numberOfVariablesNeeded);
distribution.template toAdd<ValueType>().exportToDot("dist" + std::to_string(distributionIndex) + ".dot");
++distributionIndex;
STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty.");
}
@ -375,9 +362,6 @@ namespace storm {
}
usedNondeterminismVariables += numberOfVariablesNeeded;
// resultBdd.template toAdd<ValueType>().exportToDot("result.dot");
// exit(-1);
blockBdds.push_back(resultBdd);
++blockCounter;
}
@ -390,7 +374,6 @@ namespace storm {
storm::dd::Bdd<DdType> resultBdd = getAbstractionInformation().getDdManager().getBddOne();
uint64_t blockIndex = 0;
for (auto const& blockBdd : blockBdds) {
blockBdd.template toAdd<ValueType>().exportToDot("block" + std::to_string(command.get().getGlobalIndex()) + "_" + std::to_string(blockIndex) + ".dot");
resultBdd &= blockBdd;
++blockIndex;
}
@ -412,16 +395,9 @@ namespace storm {
resultBdd &= abstractGuard;
}
resultBdd.template toAdd<ValueType>().exportToDot("decomp" + std::to_string(command.get().getGlobalIndex()) + ".dot");
auto identities = computeMissingIdentities();
identities.template toAdd<ValueType>().exportToDot("idents" + std::to_string(command.get().getGlobalIndex()) + ".dot");
// multiply with missing identities
resultBdd &= computeMissingIdentities();
resultBdd.template toAdd<ValueType>().exportToDot("decomp_idents" + std::to_string(command.get().getGlobalIndex()) + ".dot");
// cache and return result
resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount());
@ -483,8 +459,6 @@ namespace storm {
STORM_LOG_ASSERT(!resultBdd.isZero(), "The BDD must not be empty.");
}
resultBdd.template toAdd<ValueType>().exportToDot("nodecomp" + std::to_string(command.get().getGlobalIndex()) + ".dot");
resultBdd &= computeMissingIdentities();
resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount());
STORM_LOG_ASSERT(sourceToDistributionsMap.empty() || !resultBdd.isZero(), "The BDD must not be empty, if there were distributions.");
@ -504,12 +478,12 @@ namespace storm {
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.
auto const& rightHandSidePredicates = localExpressionInformation.getRelatedExpressions(assignment.getExpression().getVariables());
auto const& rightHandSidePredicates = localExpressionInformation.getExpressionsUsingVariables(assignment.getExpression().getVariables());
result.first.insert(rightHandSidePredicates.begin(), rightHandSidePredicates.end());
// Variables that are being assigned are relevant for the successor state.
storm::expressions::Variable const& assignedVariable = assignment.getVariable();
auto const& leftHandSidePredicates = localExpressionInformation.getRelatedExpressions(assignedVariable);
auto const& leftHandSidePredicates = localExpressionInformation.getExpressionsUsingVariable(assignedVariable);
result.second.insert(leftHandSidePredicates.begin(), leftHandSidePredicates.end());
// // Keep track of all assigned variables, so we can find the related predicates later.
@ -624,9 +598,7 @@ namespace storm {
template <storm::dd::DdType DdType, typename ValueType>
storm::dd::Bdd<DdType> CommandAbstractor<DdType, ValueType>::computeMissingIdentities() const {
storm::dd::Bdd<DdType> identities = computeMissingGlobalIdentities();
identities &= computeMissingUpdateIdentities();
return identities;
return computeMissingUpdateIdentities();
}
template <storm::dd::DdType DdType, typename ValueType>
@ -639,51 +611,45 @@ namespace storm {
auto updateRelevantIte = relevantPredicatesAndVariables.second[updateIndex].end();
storm::dd::Bdd<DdType> updateIdentity = this->getAbstractionInformation().getDdManager().getBddOne();
auto sourceRelevantIt = relevantPredicatesAndVariables.first.begin();
auto sourceRelevantIte = relevantPredicatesAndVariables.first.end();
// Go through all relevant source predicates. This is guaranteed to be a superset of the set of
// relevant successor predicates for any update.
for (; sourceRelevantIt != sourceRelevantIte; ++sourceRelevantIt) {
// If the predicates do not match, there is a predicate missing, so we need to add its identity.
if (updateRelevantIt == updateRelevantIte || sourceRelevantIt->second != updateRelevantIt->second) {
std::cout << "adding update identity of predicate " << this->getAbstractionInformation().getPredicateByIndex(sourceRelevantIt->second) << " to update " << updateIndex << std::endl;
updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(sourceRelevantIt->second);
for (uint_fast64_t predicateIndex = 0; predicateIndex < this->getAbstractionInformation().getNumberOfPredicates(); ++predicateIndex) {
if (updateRelevantIt == updateRelevantIte || updateRelevantIt->second != predicateIndex) {
updateIdentity &= this->getAbstractionInformation().getPredicateIdentity(predicateIndex);
} else {
++updateRelevantIt;
}
}
result |= updateIdentity && this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount());
}
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>
// 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) {
this->recomputeCachedBdd();
} else {
cachedDd.bdd &= computeMissingGlobalIdentities();
cachedDd.bdd &= computeMissingUpdateIdentities();
}
STORM_LOG_TRACE("Command produces " << cachedDd.bdd.getNonZeroCount() << " transitions.");

14
src/storm/abstraction/prism/CommandAbstractor.h
View File

@ -213,13 +213,13 @@ namespace storm {
*/
AbstractionInformation<DdType>& getAbstractionInformation();
/*!
* Computes the globally missing state identities.
*
* @return A BDD that represents the global state identities for predicates that are irrelevant for the
* source and successor states.
*/
storm::dd::Bdd<DdType> computeMissingGlobalIdentities() const;
// /*!
// * Computes the globally missing state identities.
// *
// * @return A BDD that represents the global state identities for predicates that are irrelevant for the
// * source and successor states.
// */
// storm::dd::Bdd<DdType> computeMissingGlobalIdentities() const;
// An SMT responsible for this abstract command.
std::unique_ptr<storm::solver::SmtSolver> smtSolver;

11
src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp
View File

@ -172,20 +172,17 @@ namespace storm {
}
relevantStatesWatch.stop();
storm::dd::Bdd<DdType> validBlocks = validBlockAbstractor.getValidBlocks();
// Do a reachability analysis on the raw transition relation.
storm::dd::Bdd<DdType> transitionRelation = nonTerminalStates && game.bdd.existsAbstract(variablesToAbstract);
storm::dd::Bdd<DdType> initialStates = initialStateAbstractor.getAbstractStates();
if (program.get().hasInitialConstruct()) {
initialStates &= validBlockAbstractor.getValidBlocks();
initialStates &= validBlocks;
}
initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables());
storm::dd::Bdd<DdType> reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables());
transitionRelation.template toAdd<ValueType>().exportToDot("transrel.dot");
(initialStates && transitionRelation).template toAdd<ValueType>().exportToDot("transrelinit.dot");
(transitionRelation && abstractionInformation.encodePlayer1Choice(6, this->getAbstractionInformation().getPlayer1VariableCount())).template toAdd<ValueType>().exportToDot("trans6.dot");
initialStates.template toAdd<ValueType>().exportToDot("initial.dot");
reachableStates &= validBlocks;
relevantStatesWatch.start();
if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) {

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

@ -573,8 +573,6 @@ namespace storm {
targetStates |= game.getBottomStates();
}
exit(-1);
// #ifdef LOCAL_DEBUG
// initialStates.template toAdd<ValueType>().exportToDot("init" + std::to_string(iteration) + ".dot");
// targetStates.template toAdd<ValueType>().exportToDot("target" + std::to_string(iteration) + ".dot");

Write Preview
Loading…
Cancel
Save