@ -4,13 +4,17 @@
# include "storm/storage/dd/bisimulation/PreservationInformation.h"
# include "storm/logic/Formula.h"
# include "storm/logic/Formulas .h"
# include "storm/logic/AtomicExpressionFormula.h"
# include "storm/logic/AtomicLabelFormula.h"
# include "storm/logic/FragmentSpecification.h"
# include "storm/models/symbolic/Mdp.h"
# include "storm/models/symbolic/StandardRewardModel.h"
# include "storm/modelchecker/propositional/SymbolicPropositionalModelChecker.h"
# include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
# include "storm/settings/SettingsManager.h"
# include "storm/settings/modules/BisimulationSettings.h"
@ -52,6 +56,50 @@ namespace storm {
return Partition < DdType , ValueType > ( newPartitionBdd , blockVariables , numberOfBlocks , nextFreeBlockIndex ) ;
}
template < storm : : dd : : DdType DdType , typename ValueType >
boost : : optional < std : : pair < std : : shared_ptr < storm : : logic : : Formula const > , std : : shared_ptr < storm : : logic : : Formula const > > > Partition < DdType , ValueType > : : extractConstraintTargetFormulas ( storm : : logic : : Formula const & formula ) {
boost : : optional < std : : pair < std : : shared_ptr < storm : : logic : : Formula const > , std : : shared_ptr < storm : : logic : : Formula const > > > result ;
if ( formula . isProbabilityOperatorFormula ( ) ) {
return extractConstraintTargetFormulas ( formula . asProbabilityOperatorFormula ( ) . getSubformula ( ) ) ;
} else if ( formula . isRewardOperatorFormula ( ) ) {
return extractConstraintTargetFormulas ( formula . asRewardOperatorFormula ( ) . getSubformula ( ) ) ;
} else if ( formula . isUntilFormula ( ) ) {
storm : : logic : : UntilFormula const & untilFormula = formula . asUntilFormula ( ) ;
storm : : logic : : FragmentSpecification propositional = storm : : logic : : propositional ( ) ;
if ( untilFormula . getLeftSubformula ( ) . isInFragment ( propositional ) & & untilFormula . getRightSubformula ( ) . isInFragment ( propositional ) ) {
result = std : : pair < std : : shared_ptr < storm : : logic : : Formula const > , std : : shared_ptr < storm : : logic : : Formula const > > ( ) ;
result . get ( ) . first = untilFormula . getLeftSubformula ( ) . asSharedPointer ( ) ;
result . get ( ) . second = untilFormula . getRightSubformula ( ) . asSharedPointer ( ) ;
}
} else if ( formula . isEventuallyFormula ( ) ) {
storm : : logic : : EventuallyFormula const & eventuallyFormula = formula . asEventuallyFormula ( ) ;
storm : : logic : : FragmentSpecification propositional = storm : : logic : : propositional ( ) ;
if ( eventuallyFormula . getSubformula ( ) . isInFragment ( propositional ) ) {
result = std : : pair < std : : shared_ptr < storm : : logic : : Formula const > , std : : shared_ptr < storm : : logic : : Formula const > > ( ) ;
result . get ( ) . first = std : : make_shared < storm : : logic : : BooleanLiteralFormula > ( true ) ;
result . get ( ) . second = eventuallyFormula . getSubformula ( ) . asSharedPointer ( ) ;
}
}
return result ;
}
template < storm : : dd : : DdType DdType , typename ValueType >
Partition < DdType , ValueType > Partition < DdType , ValueType > : : create ( storm : : models : : symbolic : : Model < DdType , ValueType > const & model , storm : : storage : : BisimulationType const & bisimulationType , std : : vector < std : : shared_ptr < storm : : logic : : Formula const > > const & formulas ) {
auto const & bisimulationSettings = storm : : settings : : getModule < storm : : settings : : modules : : BisimulationSettings > ( ) ;
boost : : optional < std : : pair < std : : shared_ptr < storm : : logic : : Formula const > , std : : shared_ptr < storm : : logic : : Formula const > > > constraintTargetFormulas ;
if ( bisimulationSettings . getInitialPartitionMode ( ) = = storm : : settings : : modules : : BisimulationSettings : : InitialPartitionMode : : Finer & & formulas . size ( ) = = 1 ) {
constraintTargetFormulas = extractConstraintTargetFormulas ( * formulas . front ( ) ) ;
}
if ( constraintTargetFormulas & & bisimulationType = = storm : : storage : : BisimulationType : : Strong ) {
return createDistanceBased ( model , * constraintTargetFormulas . get ( ) . first , * constraintTargetFormulas . get ( ) . second ) ;
} else {
return create ( model , bisimulationType , PreservationInformation < DdType , ValueType > ( model , formulas ) ) ;
}
}
template < storm : : dd : : DdType DdType , typename ValueType >
Partition < DdType , ValueType > Partition < DdType , ValueType > : : create ( storm : : models : : symbolic : : Model < DdType , ValueType > const & model , storm : : storage : : BisimulationType const & bisimulationType , PreservationInformation < DdType , ValueType > const & preservationInformation ) {
@ -64,15 +112,58 @@ namespace storm {
}
template < storm : : dd : : DdType DdType , typename ValueType >
Partition < DdType , ValueType > Partition < DdType , ValueType > : : create ( storm : : models : : symbolic : : Model < DdType , ValueType > const & model , std : : vector < storm : : expressions : : Expression > const & expressions , storm : : storage : : BisimulationType const & bisimulationType ) {
STORM_LOG_THROW ( bisimulationType = = storm : : storage : : BisimulationType : : Strong , storm : : exceptions : : NotSupportedException , " Currently only strong bisimulation is supported. " ) ;
Partition < DdType , ValueType > Partition < DdType , ValueType > : : createDistanceBased ( storm : : models : : symbolic : : Model < DdType , ValueType > const & model , storm : : logic : : Formula const & constraintFormula , storm : : logic : : Formula const & targetFormula ) {
storm : : modelchecker : : SymbolicPropositionalModelChecker < storm : : models : : symbolic : : Model < DdType , ValueType > > propositionalChecker ( model ) ;
std : : unique_ptr < storm : : modelchecker : : CheckResult > subresult = propositionalChecker . check ( constraintFormula ) ;
storm : : dd : : Bdd < DdType > constraintStates = subresult - > asSymbolicQualitativeCheckResult < DdType > ( ) . getTruthValuesVector ( ) ;
subresult = propositionalChecker . check ( targetFormula ) ;
storm : : dd : : Bdd < DdType > targetStates = subresult - > asSymbolicQualitativeCheckResult < DdType > ( ) . getTruthValuesVector ( ) ;
return createDistanceBased ( model , constraintStates , targetStates ) ;
}
template < storm : : dd : : DdType DdType , typename ValueType >
Partition < DdType , ValueType > Partition < DdType , ValueType > : : createDistanceBased ( storm : : models : : symbolic : : Model < DdType , ValueType > const & model , storm : : dd : : Bdd < DdType > const & constraintStates , storm : : dd : : Bdd < DdType > const & targetStates ) {
STORM_LOG_TRACE ( " Creating distance-based partition. " ) ;
std : : pair < storm : : expressions : : Variable , storm : : expressions : : Variable > blockVariables = createBlockVariables ( model ) ;
// Set up the construction.
storm : : dd : : DdManager < DdType > & manager = model . getManager ( ) ;
storm : : dd : : Bdd < DdType > partitionBdd = manager . getBddZero ( ) ;
storm : : dd : : Bdd < DdType > transitionMatrixBdd = model . getTransitionMatrix ( ) . notZero ( ) . existsAbstract ( model . getNondeterminismVariables ( ) ) ;
storm : : dd : : Bdd < DdType > coveredStates = manager . getBddZero ( ) ;
uint64_t blockCount = 0 ;
// Backward BFS.
storm : : dd : : Bdd < DdType > backwardFrontier = targetStates ;
while ( ! backwardFrontier . isZero ( ) ) {
partitionBdd | = backwardFrontier & & manager . getEncoding ( blockVariables . first , blockCount + + , false ) ;
coveredStates | = backwardFrontier ;
backwardFrontier = backwardFrontier . inverseRelationalProduct ( transitionMatrixBdd , model . getRowVariables ( ) , model . getColumnVariables ( ) ) & & ! coveredStates & & constraintStates ;
}
// If there are states that cannot reach the target states (via only constraint states) at all, put them in one block.
if ( coveredStates ! = model . getReachableStates ( ) ) {
partitionBdd | = ( model . getReachableStates ( ) & & ! coveredStates ) & & manager . getEncoding ( blockVariables . first , blockCount + + , false ) ;
}
std : : vector < storm : : dd : : Bdd < DdType > > stateSets ;
for ( auto const & expression : expressions ) {
stateSets . emplace_back ( model . getStates ( expression ) ) ;
// Move the partition over to the primed variables.
partitionBdd = partitionBdd . swapVariables ( model . getRowColumnMetaVariablePairs ( ) ) ;
// Store the partition as an ADD only in the case of CUDD.
if ( DdType = = storm : : dd : : DdType : : CUDD ) {
return Partition < DdType , ValueType > ( partitionBdd . template toAdd < ValueType > ( ) , blockVariables , blockCount , blockCount ) ;
} else {
return Partition < DdType , ValueType > ( partitionBdd , blockVariables , blockCount , blockCount ) ;
}
}
template < storm : : dd : : DdType DdType , typename ValueType >
std : : pair < storm : : expressions : : Variable , storm : : expressions : : Variable > Partition < DdType , ValueType > : : createBlockVariables ( storm : : models : : symbolic : : Model < DdType , ValueType > const & model ) {
storm : : dd : : DdManager < DdType > & manager = model . getManager ( ) ;
uint64_t numberOfDdVariables = 0 ;
for ( auto const & metaVariable : model . getRowVariables ( ) ) {
@ -87,8 +178,20 @@ namespace storm {
}
}
std : : pair < storm : : expressions : : Variable , storm : : expressions : : Variable > blockVariables = createBlockVariables ( manager , numberOfDdVariables ) ;
std : : pair < storm : : dd : : Bdd < DdType > , uint64_t > partitionBddAndBlockCount = createPartitionBdd ( manager , model , stateSets , blockVariables . first ) ;
return createBlockVariables ( manager , numberOfDdVariables ) ;
}
template < storm : : dd : : DdType DdType , typename ValueType >
Partition < DdType , ValueType > Partition < DdType , ValueType > : : create ( storm : : models : : symbolic : : Model < DdType , ValueType > const & model , std : : vector < storm : : expressions : : Expression > const & expressions , storm : : storage : : BisimulationType const & bisimulationType ) {
STORM_LOG_THROW ( bisimulationType = = storm : : storage : : BisimulationType : : Strong , storm : : exceptions : : NotSupportedException , " Currently only strong bisimulation is supported. " ) ;
std : : pair < storm : : expressions : : Variable , storm : : expressions : : Variable > blockVariables = createBlockVariables ( model ) ;
std : : vector < storm : : dd : : Bdd < DdType > > stateSets ;
for ( auto const & expression : expressions ) {
stateSets . emplace_back ( model . getStates ( expression ) ) ;
}
std : : pair < storm : : dd : : Bdd < DdType > , uint64_t > partitionBddAndBlockCount = createPartitionBdd ( model . getManager ( ) , model , stateSets , blockVariables . first ) ;
// Store the partition as an ADD only in the case of CUDD.
if ( DdType = = storm : : dd : : DdType : : CUDD ) {
dehnert
8 years ago