From 7ef779a8a6c5f8790911123d735661847eb7be5c Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 28 May 2018 16:38:59 +0200 Subject: [PATCH] fixing one bug in abstraction using decomposition, started tracking down more --- src/storm/abstraction/jani/EdgeAbstractor.cpp | 2 +- .../abstraction/prism/CommandAbstractor.cpp | 27 +++++++++++++++---- .../prism/PrismMenuGameAbstractor.cpp | 6 +++++ 3 files changed, 29 insertions(+), 6 deletions(-) diff --git a/src/storm/abstraction/jani/EdgeAbstractor.cpp b/src/storm/abstraction/jani/EdgeAbstractor.cpp index 2342a497f..c0592df3c 100644 --- a/src/storm/abstraction/jani/EdgeAbstractor.cpp +++ b/src/storm/abstraction/jani/EdgeAbstractor.cpp @@ -561,9 +561,9 @@ namespace storm { } else { updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } - updateBdd &= this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } + updateBdd &= this->getAbstractionInformation().encodeAux(destinationIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); result |= updateBdd; } diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index d7003a39f..929285943 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -240,6 +240,8 @@ 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 relatedGuardPredicates = localExpressionInformation.getRelatedExpressions(variablesContainedInGuard); @@ -258,8 +260,10 @@ namespace storm { return true; }); STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions for abstract guard."); + abstractGuard.template toAdd().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 + // Now that we have the abstract guard, we can add it as an assertion to the solver before enumerating // the other solutions. // Create a new backtracking point before adding the guard. @@ -288,7 +292,7 @@ namespace storm { for (auto const& innerBlock : block) { relevantPredicates.insert(localExpressionInformation.getExpressionBlock(innerBlock).begin(), localExpressionInformation.getExpressionBlock(innerBlock).end()); } - + if (relevantPredicates.empty()) { STORM_LOG_TRACE("Block does not contain relevant predicates, skipping it."); continue; @@ -297,7 +301,9 @@ namespace storm { std::vector transitionDecisionVariables; std::vector> 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); } @@ -308,10 +314,14 @@ namespace storm { destinationVariablesAndPredicates.emplace_back(); for (auto const& assignment : command.get().getUpdate(updateIndex).getAssignments()) { uint64_t assignmentVariableBlockIndex = localExpressionInformation.getBlockIndexOfVariable(assignment.getVariable()); - std::set const& assignmentVariableBlock = localExpressionInformation.getExpressionBlock(assignmentVariableBlockIndex); + std::cout << "assignment variable " << assignment.getVariable().getName() << " block index: " << assignmentVariableBlockIndex << std::endl; + if (block.find(assignmentVariableBlockIndex) != block.end()) { + std::set 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); } @@ -355,6 +365,7 @@ namespace storm { storm::dd::Bdd allDistributions = this->getAbstractionInformation().getDdManager().getBddZero(); for (auto const& distribution : sourceDistributionsPair.second) { allDistributions |= distribution && this->getAbstractionInformation().encodePlayer2Choice(distributionIndex, usedNondeterminismVariables, usedNondeterminismVariables + numberOfVariablesNeeded); + distribution.template toAdd().exportToDot("dist" + std::to_string(distributionIndex) + ".dot"); ++distributionIndex; STORM_LOG_ASSERT(!allDistributions.isZero(), "The BDD must not be empty."); } @@ -364,6 +375,9 @@ namespace storm { } usedNondeterminismVariables += numberOfVariablesNeeded; +// resultBdd.template toAdd().exportToDot("result.dot"); +// exit(-1); + blockBdds.push_back(resultBdd); ++blockCounter; } @@ -406,6 +420,8 @@ namespace storm { // multiply with missing identities resultBdd &= computeMissingIdentities(); + resultBdd.template toAdd().exportToDot("decomp_idents" + std::to_string(command.get().getGlobalIndex()) + ".dot"); + // cache and return result resultBdd &= this->getAbstractionInformation().encodePlayer1Choice(command.get().getGlobalIndex(), this->getAbstractionInformation().getPlayer1VariableCount()); @@ -595,9 +611,10 @@ namespace storm { } else { updateBdd &= !this->getAbstractionInformation().encodePredicateAsSuccessor(variableIndexPair.second); } - updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); } - + + updateBdd &= this->getAbstractionInformation().encodeAux(updateIndex, 0, this->getAbstractionInformation().getAuxVariableCount()); + result |= updateBdd; } diff --git a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp index 529ecffad..d9cbdd46e 100644 --- a/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp +++ b/src/storm/abstraction/prism/PrismMenuGameAbstractor.cpp @@ -180,6 +180,12 @@ namespace storm { } initialStates.addMetaVariables(abstractionInformation.getSourcePredicateVariables()); storm::dd::Bdd reachableStates = storm::utility::dd::computeReachableStates(initialStates, transitionRelation, abstractionInformation.getSourceVariables(), abstractionInformation.getSuccessorVariables()); + + transitionRelation.template toAdd().exportToDot("transrel.dot"); + (initialStates && transitionRelation).template toAdd().exportToDot("transrelinit.dot"); + (transitionRelation && abstractionInformation.encodePlayer1Choice(6, this->getAbstractionInformation().getPlayer1VariableCount())).template toAdd().exportToDot("trans6.dot"); + + initialStates.template toAdd().exportToDot("initial.dot"); relevantStatesWatch.start(); if (this->isRestrictToRelevantStatesSet() && this->hasTargetStateExpression()) {