Browse Source

fixed bug in abstraction information object

Former-commit-id: 1338ecfa47
tempestpy_adaptions
dehnert 8 years ago
parent
commit
241f23f730
  1. 1
      src/abstraction/AbstractionInformation.cpp
  2. 2
      src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  3. 2
      src/utility/graph.cpp

1
src/abstraction/AbstractionInformation.cpp

@ -48,6 +48,7 @@ namespace storm {
std::pair<storm::expressions::Variable, storm::expressions::Variable> newMetaVariable = ddManager->addMetaVariable(stream.str());
predicateDdVariables.push_back(newMetaVariable);
extendedPredicateDdVariables.push_back(newMetaVariable);
predicateBdds.emplace_back(ddManager->getEncoding(newMetaVariable.first, 1), ddManager->getEncoding(newMetaVariable.second, 1));
predicateIdentities.push_back(ddManager->getEncoding(newMetaVariable.first, 1).iff(ddManager->getEncoding(newMetaVariable.second, 1)));
allPredicateIdentities &= predicateIdentities.back();

2
src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@ -95,8 +95,6 @@ namespace storm {
void GameBasedMdpModelChecker<Type, ValueType>::computeProb01States(storm::OptimizationDirection player1Direction, storm::abstraction::MenuGame<Type, ValueType> const& game, storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
storm::dd::Bdd<Type> transitionMatrixBdd = game.getTransitionMatrix().toBdd();
storm::dd::Bdd<Type> bottomStatesBdd = game.getBottomStates();
game.getTransitionMatrix().exportToDot("trans.dot");
bottomStatesBdd.template toAdd<ValueType>().exportToDot("bottom.dot");
storm::dd::Bdd<Type> targetStates = game.getStates(targetStateExpression);
if (player1Direction == storm::OptimizationDirection::Minimize) {

2
src/utility/graph.cpp

@ -955,7 +955,7 @@ namespace storm {
solution = tmp;
++iterations;
}
// Since we have determined the inverse of the desired set, we need to complement it now.
solution = !solution && model.getReachableStates();

Loading…
Cancel
Save