diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index 3f809fb2b..6c9ff1bce 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -21,8 +21,8 @@ namespace storm { abstractor.get().refine(predicates); } - template - storm::dd::Bdd pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates) { + template + storm::dd::Bdd pickPivotState(storm::dd::Bdd const& initialStates, storm::dd::Bdd const& transitions, std::set const& rowVariables, std::set const& columnVariables, storm::dd::Bdd const& pivotStates, boost::optional> const& quantitativeResult = boost::none) { // Perform a BFS and pick the first pivot state we encounter. storm::dd::Bdd pivotState; @@ -40,9 +40,17 @@ namespace storm { frontierPivotStates = frontier && pivotStates; if (!frontierPivotStates.isZero()) { - STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); - pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); - foundPivotState = true; + if (quantitativeResult) { + storm::dd::Add frontierPivotStatesAdd = frontierPivotStates.template toAdd(); + storm::dd::Add diff = frontierPivotStatesAdd * quantitativeResult.get().max.values - frontierPivotStatesAdd * quantitativeResult.get().min.values; + pivotState = diff.maxAbstractRepresentative(rowVariables); + STORM_LOG_TRACE("Picked pivot state with difference " << diff.getMax() << " from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + foundPivotState = true; + } else { + pivotState = frontierPivotStates.existsAbstractRepresentative(rowVariables); + STORM_LOG_TRACE("Picked pivot state from " << frontierPivotStates.getNonZeroCount() << " candidates on level " << level << ", " << pivotStates.getNonZeroCount() << " candidates in total."); + foundPivotState = true; + } } ++level; } @@ -59,32 +67,6 @@ namespace storm { storm::dd::Add player1ChoiceAsAdd = player1Choice.template toAdd(); auto pl1It = player1ChoiceAsAdd.begin(); uint_fast64_t player1Index = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); -#ifdef LOCAL_DEBUG - std::cout << "command index " << commandIndex << std::endl; - std::cout << program.get() << std::endl; - - for (auto stateValue : pivotState.template toAdd()) { - std::stringstream stateName; - stateName << "\tpl1_"; - for (auto const& var : currentGame->getRowVariables()) { - std::cout << "var " << var.getName() << std::endl; - if (stateValue.first.getBooleanValue(var)) { - stateName << "1"; - } else { - stateName << "0"; - } - } - std::cout << "pivot is " << stateName.str() << std::endl; - } -#endif - // storm::abstraction::prism::AbstractCommand& abstractCommand = modules.front().getCommands()[commandIndex]; - // storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); -#ifdef LOCAL_DEBUG - player1Choice.template toAdd().exportToDot("pl1choice_ref.dot"); - std::cout << concreteCommand << std::endl; - - (currentGame->getTransitionMatrix() * player1Choice.template toAdd()).exportToDot("cuttrans.dot"); -#endif // Check whether there are bottom states in the game and whether one of the choices actually picks the // bottom state as the successor. @@ -100,33 +82,11 @@ namespace storm { } else { STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); -#ifdef LOCAL_DEBUG - lowerChoice.template toAdd().exportToDot("lowerchoice_ref.dot"); - upperChoice.template toAdd().exportToDot("upperchoice_ref.dot"); -#endif - // Decode both choices to explicit mappings. -#ifdef LOCAL_DEBUG - std::cout << "lower" << std::endl; -#endif std::map lowerChoiceUpdateToSuccessorMapping = abstractionInformation.decodeChoiceToUpdateSuccessorMapping(lowerChoice); -#ifdef LOCAL_DEBUG - std::cout << "upper" << std::endl; -#endif std::map upperChoiceUpdateToSuccessorMapping = abstractionInformation.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) { - std::cout << entry.first << " -> " << entry.second << std::endl; - } - std::cout << "upper" << std::endl; - for (auto const& entry : upperChoiceUpdateToSuccessorMapping) { - std::cout << entry.first << " -> " << entry.second << std::endl; - } -#endif - // Now go through the mappings and find points of deviation. Currently, we take the first deviation. storm::expressions::Expression newPredicate; auto lowerIt = lowerChoiceUpdateToSuccessorMapping.begin(); @@ -135,16 +95,11 @@ namespace storm { for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) { STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch."); uint_fast64_t updateIndex = lowerIt->first; -#ifdef LOCAL_DEBUG - std::cout << "update idx " << updateIndex << std::endl; -#endif bool deviates = lowerIt->second != upperIt->second; if (deviates) { 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; newPredicate = abstractionInformation.getPredicateByIndex(predicateIndex).substitute(abstractor.get().getVariableUpdates(player1Index, updateIndex)).simplify(); break; } @@ -208,7 +163,7 @@ namespace storm { STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to proceed without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. - storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); + storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); // Compute the lower and the upper choice for the pivot state. std::set variablesToAbstract = game.getNondeterminismVariables(); @@ -283,7 +238,7 @@ namespace storm { STORM_LOG_ASSERT(!pivotStates.isZero(), "Unable to refine without pivot state candidates."); // Now that we have the pivot state candidates, we need to pick one. - storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); + storm::dd::Bdd pivotState = pickPivotState(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates, quantitativeResult); // Compute the lower and the upper choice for the pivot state. std::set variablesToAbstract = game.getNondeterminismVariables(); @@ -315,8 +270,8 @@ namespace storm { STORM_LOG_ASSERT(false, "Did not find choices from which to derive predicates."); } } + return true; } - template bool MenuGameRefiner::performRefinement(std::vector const& predicates) const { @@ -331,6 +286,8 @@ namespace storm { // Check which of the atoms are redundant in the sense that they are equivalent to a predicate we already have. for (auto const& atom : atoms) { + // Check whether the newly found atom is equivalent to an atom we already have in the predicate + // set or in the set that is to be added. bool addAtom = true; for (auto const& oldPredicate : abstractionInformation.getPredicates()) { if (equivalenceChecker.areEquivalent(atom, oldPredicate)) { @@ -338,6 +295,12 @@ namespace storm { break; } } + for (auto const& addedAtom : cleanedAtoms) { + if (equivalenceChecker.areEquivalent(addedAtom, atom)) { + addAtom = false; + break; + } + } if (addAtom) { cleanedAtoms.push_back(atom); @@ -347,8 +310,11 @@ namespace storm { abstractor.get().refine(cleanedAtoms); } else { + // If no splitting of the predicates is required, just forward the refinement request to the abstractor. abstractor.get().refine(predicates); } + + return true; } template class MenuGameRefiner;