Browse Source

fix in existsAbstractRepresentative

Former-commit-id: c884deaf11
tempestpy_adaptions
dehnert 8 years ago
parent
commit
5bf666be4c
  1. 3
      resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
  2. 2
      src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
  3. 2
      test/functional/utility/GraphTest.cpp

3
resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c

@ -611,11 +611,12 @@ cuddBddExistAbstractRepresentativeRecur(
if (res1 == NULL) {
return(NULL);
}
// FIXME
if (res1 == one) {
if (F->ref != 1) {
cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, one);
}
return(one);
return(cube);
}
cuddRef(res1);

2
src/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@ -100,7 +100,7 @@ namespace storm {
if (player1Direction == storm::OptimizationDirection::Minimize) {
targetStates |= game.getBottomStates();
}
transitionMatrixBdd.template toAdd<ValueType>().exportToDot("transbdd.dot");
// Start by computing the states with probability 0/1 when player 2 minimizes.

2
test/functional/utility/GraphTest.cpp

@ -258,7 +258,7 @@ TEST(GraphTest, SymbolicProb01StochasticGameDieSmall) {
EXPECT_TRUE(nonProb0StatesWithStrategy.isZero());
// Proceed by checking whether they select exactly one action in each state.
storm::dd::Add<storm::dd::DdType::CUDD, double> stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());;
storm::dd::Add<storm::dd::DdType::CUDD, double> stateDistributionsUnderStrategies = (game.getTransitionMatrix() * result.player1Strategy.get().template toAdd<double>() * result.player2Strategy.get().template toAdd<double>()).sumAbstract(game.getColumnVariables());
EXPECT_EQ(2, stateDistributionsUnderStrategies.getNonZeroCount());
// Check that the number of distributions per state is one (or zero in the case where there are no prob0 states).

Loading…
Cancel
Save