@ -179,7 +179,6 @@ namespace storm {
}
relevantBlockPartition [ representativeBlock ] . insert ( relevantBlockPartition [ assignmentVariableBlock ] . begin ( ) , relevantBlockPartition [ assignmentVariableBlock ] . end ( ) ) ;
relevantBlockPartition [ assignmentVariableBlock ] . clear ( ) ;
}
}
}
@ -188,200 +187,235 @@ namespace storm {
// Now remove all blocks that are empty and obtain the partition.
std : : vector < std : : set < uint64_t > > cleanedRelevantBlockPartition ;
for ( auto & element : relevantBlockPartition ) {
if ( ! element . empty ( ) ) {
cleanedRelevantBlockPartition . emplace_back ( std : : move ( element ) ) ;
for ( auto & outerBlock : relevantBlockPartition ) {
if ( ! outerBlock . empty ( ) ) {
cleanedRelevantBlockPartition . emplace_back ( ) ;
for ( auto const & innerBlock : outerBlock ) {
if ( ! localExpressionInformation . getExpressionBlock ( innerBlock ) . empty ( ) ) {
cleanedRelevantBlockPartition . back ( ) . insert ( innerBlock ) ;
}
}
if ( cleanedRelevantBlockPartition . back ( ) . empty ( ) ) {
cleanedRelevantBlockPartition . pop_back ( ) ;
}
}
}
relevantBlockPartition = std : : move ( cleanedRelevantBlockPartition ) ;
// if the decomposition has size 1, use the plain technique from before
if ( relevantBlockPartition . size ( ) = = 1 ) {
STORM_LOG_TRACE ( " Relevant block partition size is one, falling back to regular computation. " ) ;
recomputeCachedBddWithoutDecomposition ( ) ;
} else {
std : : set < storm : : expressions : : Variable > variablesContainedInGuard = command . get ( ) . getGuardExpression ( ) . getVariables ( ) ;
STORM_LOG_TRACE ( " Decomposition into " < < relevantBlockPartition . size ( ) < < " blocks. " ) ;
for ( auto const & block : relevantBlockPartition ) {
STORM_LOG_TRACE ( " New block of size " < < block . size ( ) < < " : " ) ;
// Check whether we need to enumerate the guard. This is the case if the blocks related by the guard
// are not contained within a single block of our decomposition.
bool enumerateAbstractGuard = true ;
std : : set < uint64_t > guardBlocks = localExpressionInformation . getBlockIndicesOfVariables ( variablesContainedInGuard ) ;
for ( auto const & block : relevantBlockPartition ) {
bool allContained = true ;
for ( auto const & guardBlock : guardBlocks ) {
if ( block . find ( guardBlock ) = = block . end ( ) ) {
allContained = false ;
break ;
}
std : : set < uint64_t > blockPredicateIndices ;
for ( auto const & innerBlock : block ) {
blockPredicateIndices . insert ( localExpressionInformation . getExpressionBlock ( innerBlock ) . begin ( ) , localExpressionInformation . getExpressionBlock ( innerBlock ) . end ( ) ) ;
}
for ( auto const & predicateIndex : blockPredicateIndices ) {
STORM_LOG_TRACE ( abstractionInformation . get ( ) . getPredicateByIndex ( predicateIndex ) ) ;
}
}
std : : set < storm : : expressions : : Variable > variablesContainedInGuard = command . get ( ) . getGuardExpression ( ) . getVariables ( ) ;
// Check whether we need to enumerate the guard. This is the case if the blocks related by the guard
// are not contained within a single block of our decomposition.
bool enumerateAbstractGuard = true ;
std : : set < uint64_t > guardBlocks = localExpressionInformation . getBlockIndicesOfVariables ( variablesContainedInGuard ) ;
for ( auto const & block : relevantBlockPartition ) {
bool allContained = true ;
for ( auto const & guardBlock : guardBlocks ) {
if ( block . find ( guardBlock ) = = block . end ( ) ) {
allContained = false ;
break ;
}
if ( allContained ) {
enumerateAbstractGuard = false ;
}
if ( allContained ) {
enumerateAbstractGuard = false ;
}
}
uint64_t numberOfSolutions = 0 ;
uint64_t numberOfTotalSolutions = 0 ;
// If we need to enumerate the guard, do it only once now.
if ( enumerateAbstractGuard ) {
std : : set < uint64_t > relatedGuardPredicates = localExpressionInformation . getRelatedExpressions ( variablesContainedInGuard ) ;
std : : vector < storm : : expressions : : Variable > guardDecisionVariables ;
std : : vector < std : : pair < storm : : expressions : : Variable , uint_fast64_t > > guardVariablesAndPredicates ;
for ( auto const & element : relevantPredicatesAndVariables . first ) {
if ( relatedGuardPredicates . find ( element . second ) ! = relatedGuardPredicates . end ( ) ) {
guardDecisionVariables . push_back ( element . first ) ;
guardVariablesAndPredicates . push_back ( element ) ;
}
}
abstractGuard = this - > getAbstractionInformation ( ) . getDdManager ( ) . getBddZero ( ) ;
smtSolver - > allSat ( guardDecisionVariables , [ this , & guardVariablesAndPredicates , & numberOfSolutions ] ( storm : : solver : : SmtSolver : : ModelReference const & model ) {
abstractGuard | = getSourceStateBdd ( model , guardVariablesAndPredicates ) ;
+ + numberOfSolutions ;
return true ;
} ) ;
STORM_LOG_TRACE ( " Enumerated " < < numberOfSolutions < < " solutions for abstract guard. " ) ;
// now that we have the abstract guard, we can add it as an assertion to the solver before enumerating
// the other solutions.
// Create a new backtracking point before adding the guard.
smtSolver - > push ( ) ;
// Create the guard constraint.
std : : pair < std : : vector < storm : : expressions : : Expression > , std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > > result = abstractGuard . toExpression ( this - > getAbstractionInformation ( ) . getExpressionManager ( ) ) ;
// Then add it to the solver.
for ( auto const & expression : result . first ) {
smtSolver - > add ( expression ) ;
}
uint64_t numberOfSolutions = 0 ;
// Finally associate the level variables with the predicates.
for ( auto const & indexVariablePair : result . second ) {
smtSolver - > add ( storm : : expressions : : iff ( indexVariablePair . second , this - > getAbstractionInformation ( ) . getPredicateForDdVariableIndex ( indexVariablePair . first ) ) ) ;
}
}
// then enumerate the solutions for each of the blocks of the decomposition
uint64_t usedNondeterminismVariables = 0 ;
uint64_t blockCounter = 0 ;
std : : vector < storm : : dd : : Bdd < DdType > > blockBdds ;
for ( auto const & block : relevantBlockPartition ) {
std : : set < uint64_t > relevantPredicates ;
for ( auto const & innerBlock : block ) {
relevantPredicates . insert ( localExpressionInformation . getExpressionBlock ( innerBlock ) . begin ( ) , localExpressionInformation . getExpressionBlock ( innerBlock ) . end ( ) ) ;
}
if ( enumerateAbstractGuard ) {
// otherwise, enumerate the abstract guard so we do this only once
std : : set < uint64_t > relatedGuardPredicates = localExpressionInformation . getRelatedExpressions ( variablesContainedInGuard ) ;
std : : vector < storm : : expressions : : Variable > guardDecisionVariables ;
std : : vector < std : : pair < storm : : expressions : : Variable , uint_fast64_t > > guardVariablesAndPredicates ;
for ( auto const & element : relevantPredicatesAndVariables . first ) {
if ( relatedGuardPredicates . find ( element . second ) ! = relatedGuardPredicates . end ( ) ) {
guardDecisionVariables . push_back ( element . first ) ;
guardVariablesAndPredicates . push_back ( element ) ;
}
}
abstractGuard = this - > getAbstractionInformation ( ) . getDdManager ( ) . getBddZero ( ) ;
smtSolver - > allSat ( guardDecisionVariables , [ this , & guardVariablesAndPredicates , & numberOfSolutions ] ( storm : : solver : : SmtSolver : : ModelReference const & model ) {
abstractGuard | = getSourceStateBdd ( model , guardVariablesAndPredicates ) ;
+ + numberOfSolutions ;
return true ;
} ) ;
STORM_LOG_TRACE ( " Enumerated " < < numberOfSolutions < < " for abstract guard. " ) ;
// now that we have the abstract guard, we can add it as an assertion to the solver before enumerating
// the other solutions.
// Create a new backtracking point before adding the guard.
smtSolver - > push ( ) ;
// Create the guard constraint.
std : : pair < std : : vector < storm : : expressions : : Expression > , std : : unordered_map < uint_fast64_t , storm : : expressions : : Variable > > result = abstractGuard . toExpression ( this - > getAbstractionInformation ( ) . getExpressionManager ( ) ) ;
// Then add it to the solver.
for ( auto const & expression : result . first ) {
smtSolver - > add ( expression ) ;
}
// Finally associate the level variables with the predicates.
for ( auto const & indexVariablePair : result . second ) {
smtSolver - > add ( storm : : expressions : : iff ( indexVariablePair . second , this - > getAbstractionInformation ( ) . getPredicateForDdVariableIndex ( indexVariablePair . first ) ) ) ;
}
if ( relevantPredicates . empty ( ) ) {
STORM_LOG_TRACE ( " Block does not contain relevant predicates, skipping it. " ) ;
continue ;
}
// then enumerate the solutions for each of the blocks of the decomposition
uint64_t usedNondeterminismVariables = 0 ;
uint64_t blockCounter = 0 ;
std : : vector < storm : : dd : : Bdd < DdType > > blockBdds ;
for ( auto const & block : relevantBlockPartition ) {
std : : set < uint64_t > relevantPredicates ;
for ( auto const & innerBlock : block ) {
relevantPredicates . insert ( localExpressionInformation . getExpressionBlock ( innerBlock ) . begin ( ) , localExpressionInformation . getExpressionBlock ( innerBlock ) . end ( ) ) ;
}
std : : vector < storm : : expressions : : Variable > transitionDecisionVariables ;
std : : vector < std : : pair < storm : : expressions : : Variable , uint_fast64_t > > sourceVariablesAndPredicates ;
for ( auto const & element : relevantPredicatesAndVariables . first ) {
if ( relevantPredicates . find ( element . second ) ! = relevantPredicates . end ( ) ) {
transitionDecisionVariables . push_back ( element . first ) ;
sourceVariablesAndPredicates . push_back ( element ) ;
}
std : : vector < storm : : expressions : : Variable > transitionDecisionVariables ;
std : : vector < std : : pair < storm : : expressions : : Variable , uint_fast64_t > > sourceVariablesAndPredicates ;
for ( auto const & element : relevantPredicatesAndVariables . first ) {
if ( relevantPredicates . find ( element . second ) ! = relevantPredicates . end ( ) ) {
transitionDecisionVariables . push_back ( element . first ) ;
sourceVariablesAndPredicates . push_back ( element ) ;
}
std : : vector < std : : vector < std : : pair < storm : : expressions : : Variable , uint_fast64_t > > > destinationVariablesAndPredicates ;
for ( uint64_t updateIndex = 0 ; updateIndex < command . get ( ) . getNumberOfUpdates ( ) ; + + updateIndex ) {
destinationVariablesAndPredicates . emplace_back ( ) ;
for ( auto const & assignment : command . get ( ) . getUpdate ( updateIndex ) . getAssignments ( ) ) {
uint64_t assignmentVariableBlockIndex = localExpressionInformation . getBlockIndexOfVariable ( assignment . getVariable ( ) ) ;
std : : set < uint64_t > const & assignmentVariableBlock = localExpressionInformation . getExpressionBlock ( assignmentVariableBlockIndex ) ;
if ( block . find ( assignmentVariableBlockIndex ) ! = block . end ( ) ) {
for ( auto const & element : relevantPredicatesAndVariables . second [ updateIndex ] ) {
if ( assignmentVariableBlock . find ( element . second ) ! = assignmentVariableBlock . end ( ) ) {
destinationVariablesAndPredicates . back ( ) . push_back ( element ) ;
transitionDecisionVariables . push_back ( element . firs t ) ;
}
}
std : : vector < std : : vector < std : : pair < storm : : expressions : : Variable , uint_fast64_t > > > destinationVariablesAndPredicates ;
for ( uint64_t updateIndex = 0 ; updateIndex < command . get ( ) . getNumberOfUpdates ( ) ; + + updateIndex ) {
destinationVariablesAndPredicates . emplace_back ( ) ;
for ( auto const & assignment : command . get ( ) . getUpdate ( updateIndex ) . getAssignments ( ) ) {
uint64_t assignmentVariableBlockIndex = localExpressionInformation . getBlockIndexOfVariable ( assignment . getVariable ( ) ) ;
std : : set < uint64_t > const & assignmentVariableBlock = localExpressionInformation . getExpressionBlock ( assignmentVariableBlockIndex ) ;
if ( block . find ( assignmentVariableBlockIndex ) ! = block . end ( ) ) {
for ( auto const & element : relevantPredicatesAndVariables . second [ updateIndex ] ) {
if ( assignmentVariableBlock . find ( element . second ) ! = assignmentVariableBlock . end ( ) ) {
destinationVariablesAndPredicates . back ( ) . push_back ( element ) ;
transitionDecisionVariables . push_back ( element . first ) ;
}
}
}
}
std : : unordered_map < storm : : dd : : Bdd < DdType > , std : : vector < storm : : dd : : Bdd < DdType > > > sourceToDistributionsMap ;
numberOfSolutions = 0 ;
smtSolver - > allSat ( transitionDecisionVariables , [ & sourceToDistributionsMap , this , & numberOfSolutions , & sourceVariablesAndPredicates , & destinationVariablesAndPredicates ] ( storm : : solver : : SmtSolver : : ModelReference const & model ) {
sourceToDistributionsMap [ getSourceStateBdd ( model , sourceVariablesAndPredicates ) ] . push_back ( getDistributionBdd ( model , destinationVariablesAndPredicates ) ) ;
+ + numberOfSolutions ;
return true ;
} ) ;
STORM_LOG_TRACE ( " Enumerated " < < numberOfSolutions < < " solutions for block " < < blockCounter < < " . " ) ;
numberOfSolutions = 0 ;
// Now we search for the maximal number of choices of player 2 to determine how many DD variables we
// need to encode the nondeterminism.
uint_fast64_t maximalNumberOfChoices = 0 ;
for ( auto const & sourceDistributionsPair : sourceToDistributionsMap ) {
maximalNumberOfChoices = std : : max ( maximalNumberOfChoices , static_cast < uint_fast64_t > ( sourceDistributionsPair . second . size ( ) ) ) ;
}
// We now compute how many variables we need to encode the choices. We add one to the maximal number of
// choices to account for a possible transition to a bottom state.
uint_fast64_t numberOfVariablesNeeded = static_cast < uint_fast64_t > ( std : : ceil ( std : : log2 ( maximalNumberOfChoices + 1 ) ) ) ;
// Finally, build overall result.
storm : : dd : : Bdd < DdType > resultBdd = this - > getAbstractionInformation ( ) . getDdManager ( ) . getBddZero ( ) ;
uint_fast64_t sourceStateIndex = 0 ;
for ( auto const & sourceDistributionsPair : sourceToDistributionsMap ) {
STORM_LOG_ASSERT ( ! sourceDistributionsPair . first . isZero ( ) , " The source BDD must not be empty. " ) ;
STORM_LOG_ASSERT ( ! sourceDistributionsPair . second . empty ( ) , " The distributions must not be empty. " ) ;
// We start with the distribution index of 1, becase 0 is reserved for a potential bottom choice.
uint_fast64_t distributionIndex = 1 ;
storm : : dd : : Bdd < DdType > allDistributions = this - > getAbstractionInformation ( ) . getDdManager ( ) . getBddZero ( ) ;
for ( auto const & distribution : sourceDistributionsPair . second ) {
allDistributions | = distribution & & this - > getAbstractionInformation ( ) . encodePlayer2Choice ( distributionIndex , usedNondeterminismVariables , usedNondeterminismVariables + numberOfVariablesNeeded ) ;
+ + distributionIndex ;
STORM_LOG_ASSERT ( ! allDistributions . isZero ( ) , " The BDD must not be empty. " ) ;
}
resultBdd | = sourceDistributionsPair . first & & allDistributions ;
+ + sourceStateIndex ;
STORM_LOG_ASSERT ( ! resultBdd . isZero ( ) , " The BDD must not be empty. " ) ;
}
usedNondeterminismVariables + = numberOfVariablesNeeded ;
blockBdds . push_back ( resultBdd ) ;
+ + blockCounter ;
}
if ( enumerateAbstractGuard ) {
smtSolver - > pop ( ) ;
}
std : : unordered_map < storm : : dd : : Bdd < DdType > , std : : vector < storm : : dd : : Bdd < DdType > > > sourceToDistributionsMap ;
numberOfSolutions = 0 ;
smtSolver - > allSat ( transitionDecisionVariables , [ & sourceToDistributionsMap , this , & numberOfSolutions , & sourceVariablesAndPredicates , & destinationVariablesAndPredicates ] ( storm : : solver : : SmtSolver : : ModelReference const & model ) {
sourceToDistributionsMap [ getSourceStateBdd ( model , sourceVariablesAndPredicates ) ] . push_back ( getDistributionBdd ( model , destinationVariablesAndPredicates ) ) ;
+ + numberOfSolutions ;
return true ;
} ) ;
STORM_LOG_TRACE ( " Enumerated " < < numberOfSolutions < < " solutions for block " < < blockCounter < < " . " ) ;
numberOfTotalSolutions + = numberOfSolutions ;
// multiply the results
storm : : dd : : Bdd < DdType > resultBdd = getAbstractionInformation ( ) . getDdManager ( ) . getBddOne ( ) ;
for ( auto const & blockBdd : blockBdds ) {
resultBdd & = blockBdd ;
// Now we search for the maximal number of choices of player 2 to determine how many DD variables we
// need to encode the nondeterminism.
uint_fast64_t maximalNumberOfChoices = 0 ;
for ( auto const & sourceDistributionsPair : sourceToDistributionsMap ) {
maximalNumberOfChoices = std : : max ( maximalNumberOfChoices , static_cast < uint_fast64_t > ( sourceDistributionsPair . second . size ( ) ) ) ;
}
// if we did not explicitly enumerate the guard, we can construct it from the result BDD.
if ( ! enumerateAbstractGuard ) {
std : : set < storm : : expressions : : Variable > allVariables ( getAbstractionInformation ( ) . getSuccessorVariables ( ) ) ;
auto player2Variables = getAbstractionInformation ( ) . getPlayer2VariableSet ( usedNondeterminismVariables ) ;
allVariables . insert ( player2Variables . begin ( ) , player2Variables . end ( ) ) ;
auto auxVariables = getAbstractionInformation ( ) . getAuxVariableSet ( 0 , getAbstractionInformation ( ) . getAuxVariableCount ( ) ) ;
allVariables . insert ( auxVariables . begin ( ) , auxVariables . end ( ) ) ;
std : : set < storm : : expressions : : Variable > variablesToAbstract ;
std : : set_intersection ( allVariables . begin ( ) , allVariables . end ( ) , resultBdd . getContainedMetaVariables ( ) . begin ( ) , resultBdd . getContainedMetaVariables ( ) . end ( ) , std : : inserter ( variablesToAbstract , variablesToAbstract . begin ( ) ) ) ;
// We now compute how many variables we need to encode the choices. We add one to the maximal number of
// choices to account for a possible transition to a bottom state.
uint_fast64_t numberOfVariablesNeeded = static_cast < uint_fast64_t > ( std : : ceil ( std : : log2 ( maximalNumberOfChoices + ( blockCounter = = 0 ? 1 : 0 ) ) ) ) ;
std : : cout < < " need " < < numberOfVariablesNeeded < < " variables for " < < ( maximalNumberOfChoices + ( blockCounter = = 0 ? 1 : 0 ) ) < < " choices " < < std : : endl ;
// Finally, build overall result.
storm : : dd : : Bdd < DdType > resultBdd = this - > getAbstractionInformation ( ) . getDdManager ( ) . getBddZero ( ) ;
uint_fast64_t sourceStateIndex = 0 ;
for ( auto const & sourceDistributionsPair : sourceToDistributionsMap ) {
STORM_LOG_ASSERT ( ! sourceDistributionsPair . first . isZero ( ) , " The source BDD must not be empty. " ) ;
STORM_LOG_ASSERT ( ! sourceDistributionsPair . second . empty ( ) , " The distributions must not be empty. " ) ;
abstractGuard = resultBdd . existsAbstract ( variablesToAbstract ) ;
} else {
// Multiply the abstract guard as it can contain predicates that are not mentioned in the blocks.
resultBdd & = abstractGuard ;
// We start with the distribution index of 1, because 0 is reserved for a potential bottom choice.
uint_fast64_t distributionIndex = blockCounter = = 0 ? 1 : 0 ;
storm : : dd : : Bdd < DdType > allDistributions = this - > getAbstractionInformation ( ) . getDdManager ( ) . getBddZero ( ) ;
for ( auto const & distribution : sourceDistributionsPair . second ) {
allDistributions | = distribution & & this - > getAbstractionInformation ( ) . encodePlayer2Choice ( distributionIndex , usedNondeterminismVariables , usedNondeterminismVariables + numberOfVariablesNeeded ) ;
+ + distributionIndex ;
STORM_LOG_ASSERT ( ! allDistributions . isZero ( ) , " The BDD must not be empty. " ) ;
}
resultBdd | = sourceDistributionsPair . first & & allDistributions ;
+ + sourceStateIndex ;
STORM_LOG_ASSERT ( ! resultBdd . isZero ( ) , " The BDD must not be empty. " ) ;
}
usedNondeterminismVariables + = numberOfVariablesNeeded ;
// multiply with missing identities
resultBdd & = computeMissingIdentities ( ) ;
// cache and return result
resultBdd & = this - > getAbstractionInformation ( ) . encodePlayer1Choice ( command . get ( ) . getGlobalIndex ( ) , this - > getAbstractionInformation ( ) . getPlayer1VariableCount ( ) ) ;
blockBdds . push_back ( resultBdd ) ;
+ + blockCounter ;
}
if ( enumerateAbstractGuard ) {
smtSolver - > pop ( ) ;
}
// multiply the results
storm : : dd : : Bdd < DdType > resultBdd = getAbstractionInformation ( ) . getDdManager ( ) . getBddOne ( ) ;
uint64_t blockIndex = 0 ;
for ( auto const & blockBdd : blockBdds ) {
blockBdd . template toAdd < ValueType > ( ) . exportToDot ( " block " + std : : to_string ( command . get ( ) . getGlobalIndex ( ) ) + " _ " + std : : to_string ( blockIndex ) + " .dot " ) ;
resultBdd & = blockBdd ;
+ + blockIndex ;
}
// If we did not explicitly enumerate the guard, we can construct it from the result BDD.
if ( ! enumerateAbstractGuard ) {
std : : set < storm : : expressions : : Variable > allVariables ( getAbstractionInformation ( ) . getSuccessorVariables ( ) ) ;
auto player2Variables = getAbstractionInformation ( ) . getPlayer2VariableSet ( usedNondeterminismVariables ) ;
allVariables . insert ( player2Variables . begin ( ) , player2Variables . end ( ) ) ;
auto auxVariables = getAbstractionInformation ( ) . getAuxVariableSet ( 0 , getAbstractionInformation ( ) . getAuxVariableCount ( ) ) ;
allVariables . insert ( auxVariables . begin ( ) , auxVariables . end ( ) ) ;
// Cache the result.
cachedDd = GameBddResult < DdType > ( resultBdd , usedNondeterminismVariables ) ;
std : : set < storm : : expressions : : Variable > variablesToAbstract ;
std : : set_intersection ( allVariables . begin ( ) , allVariables . end ( ) , resultBdd . getContainedMetaVariables ( ) . begin ( ) , resultBdd . getContainedMetaVariables ( ) . end ( ) , std : : inserter ( variablesToAbstract , variablesToAbstract . begin ( ) ) ) ;
auto end = std : : chrono : : high_resolution_clock : : now ( ) ;
STORM_LOG_TRACE ( " Enumerated " < < numberOfSolutions < < " solutions in " < < std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( end - start ) . count ( ) < < " ms. " ) ;
forceRecomputation = false ;
abstractGuard = resultBdd . existsAbstract ( variablesToAbstract ) ;
} else {
// Multiply the abstract guard as it can contain predicates that are not mentioned in the blocks.
resultBdd & = abstractGuard ;
}
resultBdd . template toAdd < ValueType > ( ) . exportToDot ( " decomp " + std : : to_string ( command . get ( ) . getGlobalIndex ( ) ) + " .dot " ) ;
auto identities = computeMissingIdentities ( ) ;
identities . template toAdd < ValueType > ( ) . exportToDot ( " idents " + std : : to_string ( command . get ( ) . getGlobalIndex ( ) ) + " .dot " ) ;
// multiply with missing identities
resultBdd & = computeMissingIdentities ( ) ;
// cache and return result
resultBdd & = this - > getAbstractionInformation ( ) . encodePlayer1Choice ( command . get ( ) . getGlobalIndex ( ) , this - > getAbstractionInformation ( ) . getPlayer1VariableCount ( ) ) ;
// Cache the result.
cachedDd = GameBddResult < DdType > ( resultBdd , usedNondeterminismVariables ) ;
auto end = std : : chrono : : high_resolution_clock : : now ( ) ;
STORM_LOG_TRACE ( " Enumerated " < < numberOfTotalSolutions < < " solutions in " < < std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( end - start ) . count ( ) < < " ms. " ) ;
forceRecomputation = false ;
}
template < storm : : dd : : DdType DdType , typename ValueType >
@ -433,6 +467,8 @@ namespace storm {
STORM_LOG_ASSERT ( ! resultBdd . isZero ( ) , " The BDD must not be empty. " ) ;
}
resultBdd . template toAdd < ValueType > ( ) . exportToDot ( " nodecomp " + std : : to_string ( command . get ( ) . getGlobalIndex ( ) ) + " .dot " ) ;
resultBdd & = computeMissingIdentities ( ) ;
resultBdd & = this - > getAbstractionInformation ( ) . encodePlayer1Choice ( command . get ( ) . getGlobalIndex ( ) , this - > getAbstractionInformation ( ) . getPlayer1VariableCount ( ) ) ;
STORM_LOG_ASSERT ( sourceToDistributionsMap . empty ( ) | | ! resultBdd . isZero ( ) , " The BDD must not be empty, if there were distributions. " ) ;
@ -460,12 +496,12 @@ namespace storm {
auto const & leftHandSidePredicates = localExpressionInformation . getRelatedExpressions ( assignedVariable ) ;
result . second . insert ( leftHandSidePredicates . begin ( ) , leftHandSidePredicates . end ( ) ) ;
assignedVariables . insert ( assignedVariable ) ;
// // Keep track of all assigned variables, so we can find the related predicates later.
// assignedVariables.insert(assignedVariable);
}
auto c onst & predicatesRelatedToAssignedVariable = localExpressionInformation . getRelatedExpressions ( assignedVariables ) ;
result . first . insert ( predicatesRelatedToAssignedVariable . begin ( ) , predicatesRelatedToAssignedVariable . end ( ) ) ;
// auto c onst& predicatesRelatedToAssignedVariable = localExpressionInformation.getRelatedExpressions(assignedVariables);
// result.first.insert(predicatesRelatedToAssignedVariable.begin(), predicatesRelatedToAssignedVariable.end());
return result ;
}
@ -594,6 +630,7 @@ namespace storm {
for ( ; sourceRelevantIt ! = sourceRelevantIte ; + + sourceRelevantIt ) {
// If the predicates do not match, there is a predicate missing, so we need to add its identity.
if ( updateRelevantIt = = updateRelevantIte | | sourceRelevantIt - > second ! = updateRelevantIt - > second ) {
std : : cout < < " adding update identity of predicate " < < this - > getAbstractionInformation ( ) . getPredicateByIndex ( sourceRelevantIt - > second ) < < " to update " < < updateIndex < < std : : endl ;
updateIdentity & = this - > getAbstractionInformation ( ) . getPredicateIdentity ( sourceRelevantIt - > second ) ;
} else {
+ + updateRelevantIt ;
@ -614,6 +651,7 @@ namespace storm {
for ( uint_fast64_t predicateIndex = 0 ; predicateIndex < this - > getAbstractionInformation ( ) . getNumberOfPredicates ( ) ; + + predicateIndex ) {
if ( relevantIt = = relevantIte | | relevantIt - > second ! = predicateIndex ) {
std : : cout < < " adding global identity of predicate " < < this - > getAbstractionInformation ( ) . getPredicateByIndex ( predicateIndex ) < < std : : endl ;
result & = this - > getAbstractionInformation ( ) . getPredicateIdentity ( predicateIndex ) ;
} else {
+ + relevantIt ;
dehnert
7 years ago