From 45f0f1057ac0cfa19fec0140f74fa52ce84320a1 Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 14 Dec 2016 21:41:35 +0100 Subject: [PATCH] fixed a bug in quantitative computation, removed debug output --- src/storm/abstraction/MenuGameRefiner.cpp | 23 ++----------------- .../abstraction/prism/CommandAbstractor.cpp | 4 ---- .../abstraction/GameBasedMdpModelChecker.cpp | 3 +++ .../settings/modules/AbstractionSettings.cpp | 2 +- 4 files changed, 6 insertions(+), 26 deletions(-) diff --git a/src/storm/abstraction/MenuGameRefiner.cpp b/src/storm/abstraction/MenuGameRefiner.cpp index f0d02ea81..8523dc913 100644 --- a/src/storm/abstraction/MenuGameRefiner.cpp +++ b/src/storm/abstraction/MenuGameRefiner.cpp @@ -169,6 +169,7 @@ namespace storm { if (quantitativeResult) { storm::dd::Add frontierMinPivotStatesAdd = frontierMinPivotStates.template toAdd(); storm::dd::Add frontierMaxPivotStatesAdd = frontierMaxPivotStates.template toAdd(); + storm::dd::Add diffMin = frontierMinPivotStatesAdd * quantitativeResult.get().max.values - frontierMinPivotStatesAdd * quantitativeResult.get().min.values; storm::dd::Add diffMax = frontierMaxPivotStatesAdd * quantitativeResult.get().max.values - frontierMaxPivotStatesAdd * quantitativeResult.get().min.values; @@ -254,10 +255,6 @@ namespace storm { } else { STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); -// player1Choice.template toAdd().exportToDot("choice.dot"); -// lowerChoice.template toAdd().exportToDot("lower.dot"); -// upperChoice.template toAdd().exportToDot("upper.dot"); - // Decode both choices to explicit mappings. std::map> lowerChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping(lowerChoice); std::map> upperChoiceUpdateToSuccessorMapping = abstractionInformation.template decodeChoiceToUpdateSuccessorMapping(upperChoice); @@ -379,14 +376,6 @@ namespace storm { bool player1ChoicesDifferent = !(pivotState && minPlayer1Strategy).exclusiveOr(pivotState && maxPlayer1Strategy).isZero(); - pivotState.template toAdd().exportToDot("pivot.dot"); - - minPlayer1Strategy.template toAdd().exportToDot("minpl1.dot"); - maxPlayer1Strategy.template toAdd().exportToDot("maxpl1.dot"); - - (pivotState && minPlayer1Strategy).template toAdd().exportToDot("minpivot.dot"); - (pivotState && maxPlayer1Strategy).template toAdd().exportToDot("maxpivot.dot"); - boost::optional predicates; // Derive predicates from lower choice. @@ -394,9 +383,6 @@ namespace storm { storm::dd::Bdd lowerChoice1 = (lowerChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); storm::dd::Bdd lowerChoice2 = (lowerChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - lowerChoice1.template toAdd().exportToDot("lower1.dot"); - lowerChoice2.template toAdd().exportToDot("lower2.dot"); - bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); if (lowerChoicesDifferent) { STORM_LOG_TRACE("Deriving predicate based on lower choice."); @@ -411,9 +397,6 @@ namespace storm { storm::dd::Bdd upperChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && maxPlayer1Strategy; storm::dd::Bdd upperChoice1 = (upperChoice && minPlayer2Strategy).existsAbstract(variablesToAbstract); storm::dd::Bdd upperChoice2 = (upperChoice && maxPlayer2Strategy).existsAbstract(variablesToAbstract); - - upperChoice1.template toAdd().exportToDot("upper1.dot"); - upperChoice2.template toAdd().exportToDot("upper2.dot"); bool upperChoicesDifferent = !upperChoice1.exclusiveOr(upperChoice2).isZero(); if (upperChoicesDifferent) { @@ -470,8 +453,6 @@ namespace storm { predicate = predicate.changeManager(expressionManager); } -// pivotState.template toAdd().exportToDot("pivot.dot"); - // Perform a backward search for an initial state. storm::dd::Bdd currentState = pivotState; while ((currentState && game.getInitialStates()).isZero()) { @@ -643,7 +624,7 @@ namespace storm { // Now that we have the pivot state candidates, we need to pick one. PivotStateResult pivotStateResult = pickPivotState(pivotSelectionHeuristic, game, pivotStateCandidatesResult, boost::none, quantitativeResult); - + boost::optional predicates; if (useInterpolation) { predicates = derivePredicatesFromInterpolation(game, pivotStateResult, minPlayer1Strategy, minPlayer2Strategy, maxPlayer1Strategy, maxPlayer2Strategy); diff --git a/src/storm/abstraction/prism/CommandAbstractor.cpp b/src/storm/abstraction/prism/CommandAbstractor.cpp index 89829f41b..b2a79622e 100644 --- a/src/storm/abstraction/prism/CommandAbstractor.cpp +++ b/src/storm/abstraction/prism/CommandAbstractor.cpp @@ -353,8 +353,6 @@ namespace storm { auto end = std::chrono::high_resolution_clock::now(); STORM_LOG_TRACE("Enumerated " << numberOfSolutions << " solutions in " << std::chrono::duration_cast(end - start).count() << "ms."); forceRecomputation = false; - - resultBdd.template toAdd().exportToDot("cmd_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); } } @@ -650,8 +648,6 @@ namespace storm { return result; } -// abstractGuard.template toAdd().exportToDot("abstractguard_" + std::to_string(command.get().getGlobalIndex()) + ".dot"); - // Use the state abstractor to compute the set of abstract states that has this command enabled but // still has a transition to a bottom state. bottomStateAbstractor.constrain(reachableStates && abstractGuard); diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index 45534e453..a707cd972 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -276,6 +276,9 @@ namespace storm { result.player2Strategy = combinedPlayer2QualitativeStrategies.existsAbstract(game.getPlayer2Variables()).ite(combinedPlayer2QualitativeStrategies, result.player2Strategy); } else { STORM_LOG_TRACE("No maybe states."); + + // Extend the values of the maybe states by the qualitative values. + result.values += min ? qualitativeResult.prob1Min.getPlayer1States().template toAdd() : qualitativeResult.prob1Max.getPlayer1States().template toAdd(); } auto end = std::chrono::high_resolution_clock::now(); diff --git a/src/storm/settings/modules/AbstractionSettings.cpp b/src/storm/settings/modules/AbstractionSettings.cpp index 9654c5692..473062a16 100644 --- a/src/storm/settings/modules/AbstractionSettings.cpp +++ b/src/storm/settings/modules/AbstractionSettings.cpp @@ -10,7 +10,7 @@ namespace storm { namespace modules { const std::string AbstractionSettings::moduleName = "abstraction"; - const std::string AbstractionSettings::addAllGuardsOptionName = "allguards"; + const std::string AbstractionSettings::addAllGuardsOptionName = "all-guards"; const std::string AbstractionSettings::splitPredicatesOptionName = "split-preds"; const std::string AbstractionSettings::splitInitialGuardsOptionName = "split-init-guards"; const std::string AbstractionSettings::splitGuardsOptionName = "split-guards";