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

Added local flags in cpp files to disable std::cout flooding. 

Former-commit-id: 25789a803a
tempestpy_adaptions
PBerger 8 years ago
parent
2799412a4d
commit
9bfb41b2be
2 changed files with 38 additions and 7 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. 26
      src/abstraction/prism/AbstractProgram.cpp
  2. 17
      src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

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

@ -20,6 +20,8 @@
#include "storm-config.h" #include "storm-config.h"
#include "src/adapters/CarlAdapter.h" #include "src/adapters/CarlAdapter.h"
//#define LOCAL_DEBUG
namespace storm { namespace storm {
namespace abstraction { namespace abstraction {
namespace prism { namespace prism {
@ -122,18 +124,28 @@ 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());
#ifdef LOCAL_DEBUG
std::cout << "update idx: " << updateIndex << std::endl; std::cout << "update idx: " << updateIndex << std::endl;
#endif
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];
#ifdef LOCAL_DEBUG
std::cout << successorVariable.getName() << " has value"; std::cout << successorVariable.getName() << " has value";
#endif
if (successorValuePair.first.getBooleanValue(successorVariable)) { if (successorValuePair.first.getBooleanValue(successorVariable)) {
successor.set(index); successor.set(index);
#ifdef LOCAL_DEBUG
std::cout << " true"; std::cout << " true";
#endif
} else { } else {
#ifdef LOCAL_DEBUG
std::cout << " false"; std::cout << " false";
#endif
} }
#ifdef LOCAL_DEBUG
std::cout << std::endl; std::cout << std::endl;
#endif
} }
result[updateIndex] = successor; result[updateIndex] = successor;
@ -147,12 +159,16 @@ namespace storm {
storm::dd::Add<DdType, ValueType> player1ChoiceAsAdd = player1Choice.template toAdd<ValueType>(); storm::dd::Add<DdType, ValueType> player1ChoiceAsAdd = player1Choice.template toAdd<ValueType>();
auto pl1It = player1ChoiceAsAdd.begin(); auto pl1It = player1ChoiceAsAdd.begin();
uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount()); uint_fast64_t commandIndex = abstractionInformation.decodePlayer1Choice((*pl1It).first, abstractionInformation.getPlayer1VariableCount());
#ifdef LOCAL_DEBUG
std::cout << "command index " << commandIndex << std::endl; std::cout << "command index " << commandIndex << std::endl;
std::cout << program.get() << std::endl; std::cout << program.get() << std::endl;
#endif
storm::abstraction::prism::AbstractCommand<DdType, ValueType>& abstractCommand = modules.front().getCommands()[commandIndex]; storm::abstraction::prism::AbstractCommand<DdType, ValueType>& abstractCommand = modules.front().getCommands()[commandIndex];
storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand(); storm::prism::Command const& concreteCommand = abstractCommand.getConcreteCommand();
#ifdef LOCAL_DEBUG
player1Choice.template toAdd<ValueType>().exportToDot("pl1choice_ref.dot"); player1Choice.template toAdd<ValueType>().exportToDot("pl1choice_ref.dot");
std::cout << concreteCommand << std::endl; std::cout << concreteCommand << std::endl;
#endif
// Check whether there are bottom states in the game and whether one of the choices actually picks the // Check whether there are bottom states in the game and whether one of the choices actually picks the
// bottom state as the successor. // bottom state as the successor.
@ -172,16 +188,23 @@ 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.");
#ifdef LOCAL_DEBUG
lowerChoice.template toAdd<ValueType>().exportToDot("lowerchoice_ref.dot"); lowerChoice.template toAdd<ValueType>().exportToDot("lowerchoice_ref.dot");
upperChoice.template toAdd<ValueType>().exportToDot("upperchoice_ref.dot"); upperChoice.template toAdd<ValueType>().exportToDot("upperchoice_ref.dot");
#endif
// Decode both choices to explicit mappings. // Decode both choices to explicit mappings.
#ifdef LOCAL_DEBUG
std::cout << "lower" << std::endl; std::cout << "lower" << std::endl;
#endif
std::map<uint_fast64_t, storm::storage::BitVector> lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice); std::map<uint_fast64_t, storm::storage::BitVector> lowerChoiceUpdateToSuccessorMapping = decodeChoiceToUpdateSuccessorMapping(lowerChoice);
#ifdef LOCAL_DEBUG
std::cout << "upper" << std::endl; std::cout << "upper" << std::endl;
#endif
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 (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ")."); STORM_LOG_ASSERT(lowerChoiceUpdateToSuccessorMapping.size() == upperChoiceUpdateToSuccessorMapping.size(), "Mismatching sizes after decode (" << lowerChoiceUpdateToSuccessorMapping.size() << " vs. " << upperChoiceUpdateToSuccessorMapping.size() << ").");
#ifdef LOCAL_DEBUG
std::cout << "lower" << std::endl; std::cout << "lower" << std::endl;
for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) { for (auto const& entry : lowerChoiceUpdateToSuccessorMapping) {
std::cout << entry.first << " -> " << entry.second << std::endl; std::cout << entry.first << " -> " << entry.second << std::endl;
@ -190,6 +213,7 @@ namespace storm {
for (auto const& entry : upperChoiceUpdateToSuccessorMapping) { for (auto const& entry : upperChoiceUpdateToSuccessorMapping) {
std::cout << entry.first << " -> " << entry.second << std::endl; 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. // Now go through the mappings and find points of deviation. Currently, we take the first deviation.
storm::expressions::Expression newPredicate; storm::expressions::Expression newPredicate;
@ -199,7 +223,9 @@ namespace storm {
for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) { for (; lowerIt != lowerIte; ++lowerIt, ++upperIt) {
STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch."); STORM_LOG_ASSERT(lowerIt->first == upperIt->first, "Update indices mismatch.");
uint_fast64_t updateIndex = lowerIt->first; uint_fast64_t updateIndex = lowerIt->first;
#ifdef LOCAL_DEBUG
std::cout << "update idx " << updateIndex << std::endl; std::cout << "update idx " << updateIndex << std::endl;
#endif
bool deviates = lowerIt->second != upperIt->second; bool deviates = lowerIt->second != upperIt->second;
if (deviates) { if (deviates) {
for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) { for (uint_fast64_t predicateIndex = 0; predicateIndex < lowerIt->second.size(); ++predicateIndex) {

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

@ -28,6 +28,8 @@
#include "src/modelchecker/results/CheckResult.h" #include "src/modelchecker/results/CheckResult.h"
//#define LOCAL_DEBUG
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
namespace detail { namespace detail {
@ -337,7 +339,7 @@ namespace storm {
// //
// minResult.exportToDot("minresult.dot"); // minResult.exportToDot("minresult.dot");
// maxResult.exportToDot("maxresult.dot"); // maxResult.exportToDot("maxresult.dot");
pivotState.template toAdd<ValueType>().exportToDot("pivot.dot");
// pivotState.template toAdd<ValueType>().exportToDot("pivot.dot");
// pivotStateLower.exportToDot("pivot_lower.dot"); // pivotStateLower.exportToDot("pivot_lower.dot");
// pivotStateUpper.exportToDot("pivot_upper.dot"); // pivotStateUpper.exportToDot("pivot_upper.dot");
// pivotStateIsMinProb0.template toAdd<ValueType>().exportToDot("pivot_is_minprob0.dot"); // pivotStateIsMinProb0.template toAdd<ValueType>().exportToDot("pivot_is_minprob0.dot");
@ -363,9 +365,11 @@ namespace storm {
// lowerChoice2.template toAdd<ValueType>().exportToDot("tmp_lower.dot"); // lowerChoice2.template toAdd<ValueType>().exportToDot("tmp_lower.dot");
// lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract); // lowerChoice2 = lowerChoice2.existsAbstract(variablesToAbstract);
#ifdef LOCAL_DEBUG
lowerChoice.template toAdd<ValueType>().exportToDot("ref_lower.dot"); lowerChoice.template toAdd<ValueType>().exportToDot("ref_lower.dot");
lowerChoice1.template toAdd<ValueType>().exportToDot("ref_lower1.dot"); lowerChoice1.template toAdd<ValueType>().exportToDot("ref_lower1.dot");
lowerChoice2.template toAdd<ValueType>().exportToDot("ref_lower2.dot"); lowerChoice2.template toAdd<ValueType>().exportToDot("ref_lower2.dot");
#endif
bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero(); bool lowerChoicesDifferent = !lowerChoice1.exclusiveOr(lowerChoice2).isZero();
if (lowerChoicesDifferent) { if (lowerChoicesDifferent) {
@ -475,16 +479,16 @@ namespace storm {
targetStates |= game.getBottomStates(); targetStates |= game.getBottomStates();
} }
abstractor.exportToDot("game" + std::to_string(iterations) + ".dot");
#ifdef LOCAL_DEBUG
abstractor.exportToDot("game" + std::to_string(iterations) + ".dot", targetStates, game.getManager().getBddOne());
#endif
prob01.min = computeProb01States(player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); prob01.min = computeProb01States(player1Direction, storm::OptimizationDirection::Minimize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates);
std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Minimize, game.getInitialStates(), prob01.min.first.getPlayer1States(), prob01.min.second.getPlayer1States()); std::unique_ptr<CheckResult> result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Minimize, game.getInitialStates(), prob01.min.first.getPlayer1States(), prob01.min.second.getPlayer1States());
if (result) { if (result) {
return result; return result;
} }
/*if (iterations == 18) {
exit(-1);
}*/
prob01.max = computeProb01States(player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates); prob01.max = computeProb01States(player1Direction, storm::OptimizationDirection::Maximize, game, transitionMatrixBdd, game.getStates(constraintExpression), targetStates);
result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Maximize, game.getInitialStates(), prob01.max.first.getPlayer1States(), prob01.max.second.getPlayer1States()); result = checkForResultAfterQualitativeCheck<Type, ValueType>(checkTask, storm::OptimizationDirection::Maximize, game.getInitialStates(), prob01.max.first.getPlayer1States(), prob01.max.second.getPlayer1States());
if (result) { if (result) {
@ -608,10 +612,12 @@ namespace storm {
//std::cout << "diff one? " << ((commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy)) << std::endl; //std::cout << "diff one? " << ((commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy)) << std::endl;
STORM_LOG_ASSERT((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy) || (commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy), "The strategies fully coincide."); STORM_LOG_ASSERT((commonReach && minMaybeStateResult.player1Strategy) != (commonReach && maxMaybeStateResult.player1Strategy) || (commonReach && minMaybeStateResult.player2Strategy) != (commonReach && maxMaybeStateResult.player2Strategy), "The strategies fully coincide.");
#ifdef LOCAL_DEBUG
abstractor.exportToDot("lowerlower" + std::to_string(iterations) + ".dot", targetStates, minMaybeStateResult.player1Strategy && minMaybeStateResult.player2Strategy); abstractor.exportToDot("lowerlower" + std::to_string(iterations) + ".dot", targetStates, minMaybeStateResult.player1Strategy && minMaybeStateResult.player2Strategy);
abstractor.exportToDot("upperupper" + std::to_string(iterations) + ".dot", targetStates, maxMaybeStateResult.player1Strategy && maxMaybeStateResult.player2Strategy); abstractor.exportToDot("upperupper" + std::to_string(iterations) + ".dot", targetStates, maxMaybeStateResult.player1Strategy && maxMaybeStateResult.player2Strategy);
abstractor.exportToDot("common" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && minMaybeStateResult.player2Strategy && maxMaybeStateResult.player2Strategy); abstractor.exportToDot("common" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && minMaybeStateResult.player2Strategy && maxMaybeStateResult.player2Strategy);
abstractor.exportToDot("both" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy)); abstractor.exportToDot("both" + std::to_string(iterations) + ".dot", targetStates, (minMaybeStateResult.player1Strategy || maxMaybeStateResult.player1Strategy) && (minMaybeStateResult.player2Strategy || maxMaybeStateResult.player2Strategy));
#endif
refineAfterQuantitativeCheck(abstractor, game, minResult, maxResult, prob01, 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);
} }
@ -657,6 +663,5 @@ namespace storm {
template class GameBasedMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>; template class GameBasedMdpModelChecker<storm::dd::DdType::CUDD, storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
template class GameBasedMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>; template class GameBasedMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Dtmc<storm::dd::DdType::Sylvan, double>>;
template class GameBasedMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>; template class GameBasedMdpModelChecker<storm::dd::DdType::Sylvan, storm::models::symbolic::Mdp<storm::dd::DdType::Sylvan, double>>;
} }
} }
Write Preview
Loading…
Cancel
Save