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

fixed bug and added tons of debug output 

Former-commit-id: 5bf2d6d82f
tempestpy_adaptions
dehnert 8 years ago
parent
a663a37e21
commit
d16e47882d
3 changed files with 75 additions and 8 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 3
      src/abstraction/prism/AbstractCommand.cpp
  2. 23
      src/abstraction/prism/AbstractProgram.cpp
  3. 57
      src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

3
src/abstraction/prism/AbstractCommand.cpp
View File

@ -69,8 +69,7 @@ namespace storm {
this->recomputeCachedBdd(); this->recomputeCachedBdd();
} }
// Refine bottom state abstractor.
// FIXME: Should this only be done if the other BDD needs recomputation?
// Refine bottom state abstractor. Note that this does not trigger a recomputation yet.
bottomStateAbstractor.refine(predicates); bottomStateAbstractor.refine(predicates);
} }

23
src/abstraction/prism/AbstractProgram.cpp
View File

@ -122,12 +122,18 @@ namespace storm {
for (auto const& successorValuePair : lowerChoiceAsAdd) { for (auto const& successorValuePair : lowerChoiceAsAdd) {
uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size()); uint_fast64_t updateIndex = abstractionInformation.decodeAux(successorValuePair.first, 0, currentGame->getProbabilisticBranchingVariables().size());
std::cout << "update idx: " << updateIndex << std::endl;
storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates()); storm::storage::BitVector successor(abstractionInformation.getNumberOfPredicates());
for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) { for (uint_fast64_t index = 0; index < abstractionInformation.getOrderedSuccessorVariables().size(); ++index) {
auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index]; auto const& successorVariable = abstractionInformation.getOrderedSuccessorVariables()[index];
std::cout << successorVariable.getName() << " has value";
if (successorValuePair.first.getBooleanValue(successorVariable)) { if (successorValuePair.first.getBooleanValue(successorVariable)) {
successor.set(index); successor.set(index);
std::cout << " true";
} else {
std::cout << " false";
} }
std::cout << std::endl;
} }
result[updateIndex] = successor; result[updateIndex] = successor;
@ -162,10 +168,24 @@ namespace storm {
} else { } else {
STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition."); STORM_LOG_TRACE("No bottom state successor. Deriving a new predicate using weakest precondition.");
lowerChoice.template toAdd<ValueType>().exportToDot("lowerchoice_ref.dot");
upperChoice.template toAdd<ValueType>().exportToDot("upperchoice_ref.dot");
// Decode both choices to explicit mappings. // Decode both choices to explicit mappings.
std::cout << "lower" << std::endl;
std::map<uint_fast64_t, storm::storage::BitVector> lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); std::map<uint_fast64_t, storm::storage::BitVector> lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice);
std::cout << "upper" << std::endl;
std::map<uint_fast64_t, storm::storage::BitVector> upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice); std::map<uint_fast64_t, storm::storage::BitVector> upperChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(upperChoice);
STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode.");
STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
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;
}
// Now go through the mappings and find points of deviation. Currently, we take the first deviation. // Now go through the mappings and find points of deviation. Currently, we take the first deviation.
storm::expressions::Expression newPredicate; storm::expressions::Expression newPredicate;
@ -186,6 +206,7 @@ namespace storm {
} }
} }
} }
STORM_LOG_ASSERT(newPredicate.isInitialized(), "Could not derive new predicate as there is no deviation.");
STORM_LOG_TRACE("Derived new predicate: " << newPredicate); STORM_LOG_TRACE("Derived new predicate: " << newPredicate);

57
src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
View File

@ -61,13 +61,15 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) { std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
storm::logic::UntilFormula const& pathFormula = checkTask.getFormula(); storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), getExpression(pathFormula.getLeftSubformula()), getExpression(pathFormula.getRightSubformula()));
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = preprocessedProgram.getLabelToExpressionMapping();
return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), pathFormula.getLeftSubformula().toExpression(preprocessedProgram.getManager(), labelToExpressionMapping), pathFormula.getRightSubformula().toExpression(preprocessedProgram.getManager(), labelToExpressionMapping));
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) { std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ValueType>::computeReachabilityProbabilities(CheckTask<storm::logic::EventuallyFormula> const& checkTask) {
storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula(); storm::logic::EventuallyFormula const& pathFormula = checkTask.getFormula();
return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), originalProgram.getManager().boolean(true), getExpression(pathFormula.getSubformula()));
std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = preprocessedProgram.getLabelToExpressionMapping();
return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), originalProgram.getManager().boolean(true), pathFormula.getSubformula().toExpression(preprocessedProgram.getManager(), labelToExpressionMapping));
} }
template<typename ValueType> template<typename ValueType>
@ -195,6 +197,7 @@ namespace storm {
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
void refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, detail::GameProb01Result<Type> const& prob01, storm::dd::Bdd<Type> const& transitionMatrixBdd) { void refineAfterQualitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, detail::GameProb01Result<Type> const& prob01, storm::dd::Bdd<Type> const& transitionMatrixBdd) {
STORM_LOG_TRACE("Refining after qualitative check.");
// Build the fragment of states that is reachable by any combination of the player 1 and player 2 strategies. // Build the fragment of states that is reachable by any combination of the player 1 and player 2 strategies.
storm::dd::Bdd<Type> reachableTransitions = prob01.min.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy(); storm::dd::Bdd<Type> reachableTransitions = prob01.min.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy();
reachableTransitions = (prob01.min.first.getPlayer1Strategy() && reachableTransitions) || (prob01.max.second.getPlayer1Strategy() && reachableTransitions); reachableTransitions = (prob01.min.first.getPlayer1Strategy() && reachableTransitions) || (prob01.max.second.getPlayer1Strategy() && reachableTransitions);
@ -236,7 +239,8 @@ namespace storm {
} }
template<storm::dd::DdType Type, typename ValueType> template<storm::dd::DdType Type, typename ValueType>
void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> const& minStrategyPair, std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> const& maxStrategyPair, storm::dd::Bdd<Type> const& transitionMatrixBdd) {
void refineAfterQuantitativeCheck(storm::abstraction::prism::PrismMenuGameAbstractor<Type, ValueType>& abstractor, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::dd::Add<Type, ValueType> const& minResult, storm::dd::Add<Type, ValueType> const& maxResult, detail::GameProb01Result<Type> const& prob01, std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> const& minStrategyPair, std::pair<storm::dd::Bdd<Type>, storm::dd::Bdd<Type>> const& maxStrategyPair, storm::dd::Bdd<Type> const& transitionMatrixBdd) {
STORM_LOG_TRACE("Refining after quantitative check.");
// Build the fragment of states that is reachable by any combination of the player 1 and player 2 strategies. // Build the fragment of states that is reachable by any combination of the player 1 and player 2 strategies.
storm::dd::Bdd<Type> reachableTransitions = minStrategyPair.second || maxStrategyPair.second; storm::dd::Bdd<Type> reachableTransitions = minStrategyPair.second || maxStrategyPair.second;
reachableTransitions = (minStrategyPair.first && reachableTransitions) || (maxStrategyPair.first && reachableTransitions); reachableTransitions = (minStrategyPair.first && reachableTransitions) || (maxStrategyPair.first && reachableTransitions);
@ -251,12 +255,48 @@ namespace storm {
// Now that we have the pivot state candidates, we need to pick one. // Now that we have the pivot state candidates, we need to pick one.
storm::dd::Bdd<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates); storm::dd::Bdd<Type> pivotState = pickPivotState<Type>(game.getInitialStates(), reachableTransitions, game.getRowVariables(), game.getColumnVariables(), pivotStates);
storm::dd::Add<Type, ValueType> pivotStateLower = pivotState.template toAdd<ValueType>() * minResult;
storm::dd::Add<Type, ValueType> pivotStateUpper = pivotState.template toAdd<ValueType>() * maxResult;
storm::dd::Bdd<Type> pivotStateIsMinProb0 = pivotState && prob01.min.first.states;
storm::dd::Bdd<Type> pivotStateIsMaxProb0 = pivotState && prob01.max.first.states;
storm::dd::Bdd<Type> pivotStateLowerStrategies = pivotState && prob01.min.first.getPlayer1Strategy() && prob01.min.first.getPlayer2Strategy();
storm::dd::Bdd<Type> pivotStateUpperStrategies = pivotState && prob01.max.first.getPlayer1Strategy() && prob01.max.first.getPlayer2Strategy();
storm::dd::Bdd<Type> pivotStateLowerPl1Strategy = pivotState && prob01.min.first.getPlayer1Strategy();
storm::dd::Bdd<Type> pivotStateUpperPl1Strategy = pivotState && prob01.max.first.getPlayer1Strategy();
storm::dd::Bdd<Type> pivotStateLowerPl2Strategy = pivotState && prob01.min.first.getPlayer2Strategy();
storm::dd::Bdd<Type> pivotStateUpperPl2Strategy = pivotState && prob01.max.first.getPlayer2Strategy();
minResult.exportToDot("minresult.dot");
maxResult.exportToDot("maxresult.dot");
pivotState.template toAdd<ValueType>().exportToDot("pivot.dot");
pivotStateLower.exportToDot("pivot_lower.dot");
pivotStateUpper.exportToDot("pivot_upper.dot");
pivotStateIsMinProb0.template toAdd<ValueType>().exportToDot("pivot_is_minprob0.dot");
pivotStateIsMaxProb0.template toAdd<ValueType>().exportToDot("pivot_is_maxprob0.dot");
pivotStateLowerStrategies.template toAdd<ValueType>().exportToDot("pivot_lower_strats.dot");
pivotStateUpperStrategies.template toAdd<ValueType>().exportToDot("pivot_upper_strats.dot");
pivotStateLowerPl1Strategy.template toAdd<ValueType>().exportToDot("pivot_lower_pl1_strat.dot");
pivotStateUpperPl1Strategy.template toAdd<ValueType>().exportToDot("pivot_upper_pl1_strat.dot");
pivotStateLowerPl2Strategy.template toAdd<ValueType>().exportToDot("pivot_lower_pl2_strat.dot");
pivotStateUpperPl2Strategy.template toAdd<ValueType>().exportToDot("pivot_upper_pl2_strat.dot");
// Compute the lower and the upper choice for the pivot state. // Compute the lower and the upper choice for the pivot state.
std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables(); std::set<storm::expressions::Variable> variablesToAbstract = game.getNondeterminismVariables();
variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end()); variablesToAbstract.insert(game.getRowVariables().begin(), game.getRowVariables().end());
storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minStrategyPair.first; storm::dd::Bdd<Type> lowerChoice = pivotState && game.getExtendedTransitionMatrix().toBdd() && minStrategyPair.first;
(pivotState && minStrategyPair.first).template toAdd<ValueType>().exportToDot("pl1_choice_in_pivot.dot");
(pivotState && minStrategyPair.first && maxStrategyPair.second).template toAdd<ValueType>().exportToDot("pl1and2_choice_in_pivot.dot");
(pivotState && maxStrategyPair.second).template toAdd<ValueType>().exportToDot("pl2_choice_in_pivot.dot");
storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minStrategyPair.second).existsAbstract(variablesToAbstract); storm::dd::Bdd<Type> lowerChoice1 = (lowerChoice && minStrategyPair.second).existsAbstract(variablesToAbstract);
storm::dd::Bdd<Type> lowerChoice2 = (lowerChoice && maxStrategyPair.second).existsAbstract(variablesToAbstract);
lowerChoice.template toAdd<ValueType>().exportToDot("lower.dot");
maxStrategyPair.second.template toAdd<ValueType>().exportToDot("max_strat.dot");
storm::dd::Bdd<Type> lowerChoice2 = (lowerChoice && maxStrategyPair.second);
lowerChoice2.template toAdd<ValueType>().exportToDot("tmp_lower.dot");
lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract);
lowerChoice.template toAdd<ValueType>().exportToDot("ref_lower.dot");
lowerChoice1.template toAdd<ValueType>().exportToDot("ref_lower1.dot");
lowerChoice2.template toAdd<ValueType>().exportToDot("ref_lower2.dot");
bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
if (lowerChoicesDifferent) { if (lowerChoicesDifferent) {
@ -377,6 +417,13 @@ namespace storm {
return result; return result;
} }
// 2.5 At this point, we need to fix the max strategy for the prob 0 states for player 2. This is because
// there may be player 2 nodes for which there is no choice in the currently computed strategy (by prob0)
// as no choice achieves probability 0. However, later we require the strategies to only differ if necessary
// so we need to force the player 2 strategy to agree with the player 2 strategy for the probability 0
// states in the min case.
prob01.max.first.player2Strategy = prob01.max.first.getPlayer2Strategy().existsAbstract(game.getPlayer1Variables()).ite(prob01.max.first.getPlayer2Strategy(), prob01.min.first.getPlayer2Strategy());
// 3. compute the states for which we know the result/for which we know there is more work to be done. // 3. compute the states for which we know the result/for which we know there is more work to be done.
storm::dd::Bdd<Type> maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates(); storm::dd::Bdd<Type> maybeMin = !(prob01.min.first.states || prob01.min.second.states) && game.getReachableStates();
storm::dd::Bdd<Type> maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates(); storm::dd::Bdd<Type> maybeMax = !(prob01.max.first.states || prob01.max.second.states) && game.getReachableStates();
@ -465,7 +512,7 @@ namespace storm {
maxMaybeStateResult.player1Strategy |= prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy(); maxMaybeStateResult.player1Strategy |= prob01.max.first.getPlayer1Strategy() || prob01.max.second.getPlayer1Strategy();
maxMaybeStateResult.player2Strategy |= prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy(); maxMaybeStateResult.player2Strategy |= prob01.max.first.getPlayer2Strategy() || prob01.max.second.getPlayer2Strategy();
refineAfterQuantitativeCheck(abstractor, game, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd);
refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, std::make_pair(minMaybeStateResult.player1Strategy, minMaybeStateResult.player2Strategy), std::make_pair(maxMaybeStateResult.player1Strategy, maxMaybeStateResult.player2Strategy), transitionMatrixBdd);
} }
} }

Write Preview
Loading…
Cancel
Save