@ -7,7 +7,7 @@
# include "src/adapters/CarlAdapter.h"
# include "src/adapters/CarlAdapter.h"
# include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
# include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
# include "src/settings/modules/General Settings.h"
# include "src/settings/modules/MarkovChain Settings.h"
# include "src/settings/SettingsManager.h"
# include "src/settings/SettingsManager.h"
# include "src/storage/StronglyConnectedComponentDecomposition.h"
# include "src/storage/StronglyConnectedComponentDecomposition.h"
@ -27,6 +27,10 @@
# include "src/exceptions/InvalidSettingsException.h"
# include "src/exceptions/InvalidSettingsException.h"
# include "src/exceptions/IllegalArgumentException.h"
# include "src/exceptions/IllegalArgumentException.h"
# include "src/solver/stateelimination/LongRunAverageEliminator.h"
# include "src/solver/stateelimination/ConditionalEliminator.h"
# include "src/solver/stateelimination/PrioritizedEliminator.h"
namespace storm { namespace storm {
namespace modelchecker { namespace modelchecker {
@ -221,15 +225,15 @@ namespace storm {
std : : chrono : : high_resolution_clock : : time_point conversionStart = std : : chrono : : high_resolution_clock : : now ( ) ; std : : chrono : : high_resolution_clock : : time_point conversionStart = std : : chrono : : high_resolution_clock : : now ( ) ;
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
FlexibleSparseMatrix flexibleMatrix = getFlexibleSpars eMatrix( transitionMatrix ) ;
flexibleMatrix . filter ( maybeStates , maybeStates ) ;
FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix ( backwardTransitions ) ;
flexibleBackwardTransitions . filter ( maybeStates , maybeStates ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibl eMatrix( transitionMatrix ) ;
flexibleMatrix . createSubmatrix ( maybeStates , maybeStates ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibleBackwardTransitions ( backwardTransitions ) ;
flexibleBackwardTransitions . createSubmatrix ( maybeStates , maybeStates ) ;
auto conversionEnd = std : : chrono : : high_resolution_clock : : now ( ) ; auto conversionEnd = std : : chrono : : high_resolution_clock : : now ( ) ;
std : : chrono : : high_resolution_clock : : time_point modelCheckingStart = std : : chrono : : high_resolution_clock : : now ( ) ; std : : chrono : : high_resolution_clock : : time_point modelCheckingStart = std : : chrono : : high_resolution_clock : : now ( ) ;
storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder order = storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . getEliminationOrder ( ) ;
storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder order = storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . getEliminationOrder ( ) ;
boost : : optional < std : : vector < uint_fast64_t > > distanceBasedPriorities ; boost : : optional < std : : vector < uint_fast64_t > > distanceBasedPriorities ;
if ( eliminationOrderNeedsDistances ( order ) ) { if ( eliminationOrderNeedsDistances ( order ) ) {
distanceBasedPriorities = getDistanceBasedPriorities ( transitionMatrix , backwardTransitions , initialStates , stateValues , distanceBasedPriorities = getDistanceBasedPriorities ( transitionMatrix , backwardTransitions , initialStates , stateValues ,
@ -261,30 +265,15 @@ namespace storm {
std : : vector < ValueType > averageTimeInStates ( stateValues . size ( ) , storm : : utility : : one < ValueType > ( ) ) ; std : : vector < ValueType > averageTimeInStates ( stateValues . size ( ) , storm : : utility : : one < ValueType > ( ) ) ;
// First, we eliminate all states in BSCCs (except for the representative states).
// First, we eliminate all states in BSCCs (except for the representative states).
{
std : : unique_ptr < StatePriorityQueue > priorityQueue = createStatePriorityQueue ( distanceBasedPriorities , flexibleMatrix , flexibleBackwardTransitions , stateValues , regularStatesInBsccs ) ;
ValueUpdateCallback valueUpdateCallback = [ & stateValues , & averageTimeInStates ] ( storm : : storage : : sparse : : state_type const & state , ValueType const & loopProbability ) {
stateValues [ state ] = storm : : utility : : simplify ( loopProbability * stateValues [ state ] ) ;
averageTimeInStates [ state ] = storm : : utility : : simplify ( loopProbability * averageTimeInStates [ state ] ) ;
} ;
PredecessorUpdateCallback predecessorCallback = [ & stateValues , & averageTimeInStates ] ( storm : : storage : : sparse : : state_type const & predecessor , ValueType const & probability , storm : : storage : : sparse : : state_type const & state ) {
stateValues [ predecessor ] = storm : : utility : : simplify ( stateValues [ predecessor ] + storm : : utility : : simplify ( probability * stateValues [ state ] ) ) ;
averageTimeInStates [ predecessor ] = storm : : utility : : simplify ( averageTimeInStates [ predecessor ] + storm : : utility : : simplify ( probability * averageTimeInStates [ state ] ) ) ;
} ;
boost : : optional < PriorityUpdateCallback > priorityUpdateCallback = PriorityUpdateCallback ( [ & flexibleMatrix , & flexibleBackwardTransitions , & stateValues , & priorityQueue ] ( storm : : storage : : sparse : : state_type const & state ) {
priorityQueue - > update ( state , flexibleMatrix , flexibleBackwardTransitions , stateValues ) ;
} ) ;
boost : : optional < PredecessorFilterCallback > predecessorFilterCallback = boost : : none ;
while ( priorityQueue - > hasNextState ( ) ) {
storm : : storage : : sparse : : state_type state = priorityQueue - > popNextState ( ) ;
eliminateState ( state , flexibleMatrix , flexibleBackwardTransitions , valueUpdateCallback , predecessorCallback , priorityUpdateCallback , predecessorFilterCallback , true ) ;
STORM_LOG_ASSERT ( checkConsistent ( flexibleMatrix , flexibleBackwardTransitions ) , " The forward and backward transition matrices became inconsistent. " ) ;
}
std : : shared_ptr < StatePriorityQueue < ValueType > > priorityQueue = createStatePriorityQueue ( distanceBasedPriorities , flexibleMatrix , flexibleBackwardTransitions , stateValues , regularStatesInBsccs ) ;
storm : : solver : : stateelimination : : LongRunAverageEliminator < SparseDtmcModelType > stateEliminator ( flexibleMatrix , flexibleBackwardTransitions , priorityQueue , stateValues , averageTimeInStates ) ;
while ( priorityQueue - > hasNextState ( ) ) {
storm : : storage : : sparse : : state_type state = priorityQueue - > popNextState ( ) ;
stateEliminator . eliminateState ( state , true ) ;
# ifdef STORM_DEV
STORM_LOG_ASSERT ( checkConsistent ( flexibleMatrix , flexibleBackwardTransitions ) , " The forward and backward transition matrices became inconsistent. " ) ;
# endif
} }
// Now, we set the values of all states in BSCCs to that of the representative value (and clear the
// Now, we set the values of all states in BSCCs to that of the representative value (and clear the
@ -306,11 +295,11 @@ namespace storm {
stateValues [ * representativeIt ] = bsccValue ; stateValues [ * representativeIt ] = bsccValue ;
} }
typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : row_t ype& representativeForwardRow = flexibleMatrix . getRow ( * representativeIt ) ;
FlexibleRowT ype& representativeForwardRow = flexibleMatrix . getRow ( * representativeIt ) ;
representativeForwardRow . clear ( ) ; representativeForwardRow . clear ( ) ;
representativeForwardRow . shrink_to_fit ( ) ; representativeForwardRow . shrink_to_fit ( ) ;
typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : row_t ype& representativeBackwardRow = flexibleBackwardTransitions . getRow ( * representativeIt ) ;
FlexibleRowT ype& representativeBackwardRow = flexibleBackwardTransitions . getRow ( * representativeIt ) ;
auto it = representativeBackwardRow . begin ( ) , ite = representativeBackwardRow . end ( ) ; auto it = representativeBackwardRow . begin ( ) , ite = representativeBackwardRow . end ( ) ;
for ( ; it ! = ite ; + + it ) { for ( ; it ! = ite ; + + it ) {
if ( it - > getColumn ( ) = = * representativeIt ) { if ( it - > getColumn ( ) = = * representativeIt ) {
@ -343,7 +332,7 @@ namespace storm {
std : : chrono : : high_resolution_clock : : time_point modelCheckingEnd = std : : chrono : : high_resolution_clock : : now ( ) ; std : : chrono : : high_resolution_clock : : time_point modelCheckingEnd = std : : chrono : : high_resolution_clock : : now ( ) ;
std : : chrono : : high_resolution_clock : : time_point totalTimeEnd = std : : chrono : : high_resolution_clock : : now ( ) ; std : : chrono : : high_resolution_clock : : time_point totalTimeEnd = std : : chrono : : high_resolution_clock : : now ( ) ;
if ( storm : : settings : : generalSettings ( ) . isShowStatisticsSet ( ) ) {
if ( storm : : settings : : getModule < storm : : settings : : modules : : MarkovChainSettings > ( ) . isShowStatisticsSet ( ) ) {
std : : chrono : : high_resolution_clock : : duration sccDecompositionTime = sccDecompositionEnd - sccDecompositionStart ; std : : chrono : : high_resolution_clock : : duration sccDecompositionTime = sccDecompositionEnd - sccDecompositionStart ;
std : : chrono : : milliseconds sccDecompositionTimeInMilliseconds = std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( sccDecompositionTime ) ; std : : chrono : : milliseconds sccDecompositionTimeInMilliseconds = std : : chrono : : duration_cast < std : : chrono : : milliseconds > ( sccDecompositionTime ) ;
std : : chrono : : high_resolution_clock : : duration conversionTime = conversionEnd - conversionStart ; std : : chrono : : high_resolution_clock : : duration conversionTime = conversionEnd - conversionStart ;
@ -482,46 +471,56 @@ namespace storm {
std : : unique_ptr < CheckResult > rightResultPointer = this - > check ( pathFormula . getRightSubformula ( ) ) ; std : : unique_ptr < CheckResult > rightResultPointer = this - > check ( pathFormula . getRightSubformula ( ) ) ;
storm : : storage : : BitVector const & phiStates = leftResultPointer - > asExplicitQualitativeCheckResult ( ) . getTruthValuesVector ( ) ; storm : : storage : : BitVector const & phiStates = leftResultPointer - > asExplicitQualitativeCheckResult ( ) . getTruthValuesVector ( ) ;
storm : : storage : : BitVector const & psiStates = rightResultPointer - > asExplicitQualitativeCheckResult ( ) . getTruthValuesVector ( ) ; storm : : storage : : BitVector const & psiStates = rightResultPointer - > asExplicitQualitativeCheckResult ( ) . getTruthValuesVector ( ) ;
std : : vector < ValueType > result = computeUntilProbabilities ( this - > getModel ( ) . getTransitionMatrix ( ) , this - > getModel ( ) . getBackwardTransitions ( ) , this - > getModel ( ) . getInitialStates ( ) , phiStates , psiStates , checkTask . isOnlyInitialStatesRelevantSet ( ) ) ;
// Construct check result.
std : : unique_ptr < CheckResult > checkResult ( new ExplicitQuantitativeCheckResult < ValueType > ( result ) ) ;
return checkResult ;
}
template < typename SparseDtmcModelType >
std : : vector < typename SparseDtmcModelType : : ValueType > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : computeUntilProbabilities ( storm : : storage : : SparseMatrix < ValueType > const & probabilityMatrix , storm : : storage : : SparseMatrix < ValueType > const & backwardTransitions , storm : : storage : : BitVector const & initialStates , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates , bool computeForInitialStatesOnly ) {
// Then, compute the subset of states that has a probability of 0 or 1, respectively.
// Then, compute the subset of states that has a probability of 0 or 1, respectively.
std : : pair < storm : : storage : : BitVector , storm : : storage : : BitVector > statesWithProbability01 = storm : : utility : : graph : : performProb01 ( this - > getModel ( ) , phiStates , psiStates ) ;
std : : pair < storm : : storage : : BitVector , storm : : storage : : BitVector > statesWithProbability01 = storm : : utility : : graph : : performProb01 ( backwardTransitions , phiStates , psiStates ) ;
storm : : storage : : BitVector statesWithProbability0 = statesWithProbability01 . first ; storm : : storage : : BitVector statesWithProbability0 = statesWithProbability01 . first ;
storm : : storage : : BitVector statesWithProbability1 = statesWithProbability01 . second ; storm : : storage : : BitVector statesWithProbability1 = statesWithProbability01 . second ;
storm : : storage : : BitVector maybeStates = ~ ( statesWithProbability0 | statesWithProbability1 ) ; storm : : storage : : BitVector maybeStates = ~ ( statesWithProbability0 | statesWithProbability1 ) ;
// Determine whether we need to perform some further computation.
// Determine whether we need to perform some further computation.
bool furtherComputationNeeded = true ; bool furtherComputationNeeded = true ;
if ( checkTask . isOnlyInitialStatesRelevantSet ( ) & & this - > getModel ( ) . getInitialStates ( ) . isDisjointFrom ( maybeStates ) ) {
if ( computeForInitialStatesOnly & & initialStates . isDisjointFrom ( maybeStates ) ) {
STORM_LOG_DEBUG ( " The probability for all initial states was found in a preprocessing step. " ) ; STORM_LOG_DEBUG ( " The probability for all initial states was found in a preprocessing step. " ) ;
furtherComputationNeeded = false ; furtherComputationNeeded = false ;
} else if ( maybeStates . empty ( ) ) { } else if ( maybeStates . empty ( ) ) {
STORM_LOG_DEBUG ( " The probability for all states was found in a preprocessing step. " ) ; STORM_LOG_DEBUG ( " The probability for all states was found in a preprocessing step. " ) ;
furtherComputationNeeded = false ; furtherComputationNeeded = false ;
} }
std : : vector < ValueType > result ( maybeStates . size ( ) ) ; std : : vector < ValueType > result ( maybeStates . size ( ) ) ;
if ( furtherComputationNeeded ) { if ( furtherComputationNeeded ) {
// If we compute the results for the initial states only, we can cut off all maybe state that are not
// If we compute the results for the initial states only, we can cut off all maybe state that are not
// reachable from them.
// reachable from them.
if ( checkTask . isOnlyInitialStatesRelevantSet ( ) ) {
if ( computeForInitialStatesOnly ) {
// Determine the set of states that is reachable from the initial state without jumping over a target state.
// Determine the set of states that is reachable from the initial state without jumping over a target state.
storm : : storage : : BitVector reachableStates = storm : : utility : : graph : : getReachableStates ( this - > getModel ( ) . getTransitionMatrix ( ) , this - > getModel ( ) . getInitialStates ( ) , maybeStates , statesWithProbability1 ) ;
storm : : storage : : BitVector reachableStates = storm : : utility : : graph : : getReachableStates ( probabilityMatrix , initialStates , maybeStates , statesWithProbability1 ) ;
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
maybeStates & = reachableStates ; maybeStates & = reachableStates ;
} }
// Create a vector for the probabilities to go to a state with probability 1 in one step.
// Create a vector for the probabilities to go to a state with probability 1 in one step.
std : : vector < ValueType > oneStepProbabilities = this - > getModel ( ) . getTransitionMatrix ( ) . getConstrainedRowSumVector ( maybeStates , statesWithProbability1 ) ;
std : : vector < ValueType > oneStepProbabilities = probabilityMatrix . getConstrainedRowSumVector ( maybeStates , statesWithProbability1 ) ;
// Determine the set of initial states of the sub-model.
// Determine the set of initial states of the sub-model.
storm : : storage : : BitVector newInitialStates = this - > getModel ( ) . getInitialStates ( ) % maybeStates ;
storm : : storage : : BitVector newInitialStates = initialStates % maybeStates ;
// We then build the submatrix that only has the transitions of the maybe states.
// We then build the submatrix that only has the transitions of the maybe states.
storm : : storage : : SparseMatrix < ValueType > submatrix = this - > getModel ( ) . getTransitionMatrix ( ) . getSubmatrix ( false , maybeStates , maybeStates ) ;
storm : : storage : : SparseMatrix < ValueType > submatrix = probabilityMatrix . getSubmatrix ( false , maybeStates , maybeStates ) ;
storm : : storage : : SparseMatrix < ValueType > submatrixTransposed = submatrix . transpose ( ) ; storm : : storage : : SparseMatrix < ValueType > submatrixTransposed = submatrix . transpose ( ) ;
std : : vector < ValueType > subresult = computeReachabilityValues ( submatrix , oneStepProbabilities , submatrixTransposed , newInitialStates , checkTask . isOnlyInitialStatesRelevantSet ( ) , phiStates , psiStates , oneStepProbabilities ) ;
std : : vector < ValueType > subresult = computeReachabilityValues ( submatrix , oneStepProbabilities , submatrixTransposed , newInitialStates , computeForInitialStatesOnly , phiStates , psiStates , oneStepProbabilities ) ;
storm : : utility : : vector : : setVectorValues < ValueType > ( result , maybeStates , subresult ) ; storm : : utility : : vector : : setVectorValues < ValueType > ( result , maybeStates , subresult ) ;
} }
@ -529,14 +528,12 @@ namespace storm {
storm : : utility : : vector : : setVectorValues < ValueType > ( result , statesWithProbability0 , storm : : utility : : zero < ValueType > ( ) ) ; storm : : utility : : vector : : setVectorValues < ValueType > ( result , statesWithProbability0 , storm : : utility : : zero < ValueType > ( ) ) ;
storm : : utility : : vector : : setVectorValues < ValueType > ( result , statesWithProbability1 , storm : : utility : : one < ValueType > ( ) ) ; storm : : utility : : vector : : setVectorValues < ValueType > ( result , statesWithProbability1 , storm : : utility : : one < ValueType > ( ) ) ;
// Construct check result based on whether we have computed values for all states or just the initial states.
std : : unique_ptr < CheckResult > checkResult ( new ExplicitQuantitativeCheckResult < ValueType > ( result ) ) ;
if ( checkTask . isOnlyInitialStatesRelevantSet ( ) ) {
if ( computeForInitialStatesOnly ) {
// If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the
// If we computed the results for the initial (and prob 0 and prob1) states only, we need to filter the
// result to only communicate these results.
// result to only communicate these results.
checkResult - > filter ( ExplicitQualitativeCheckResult ( ~ maybeStates | this - > getModel ( ) . getInitialStates ( ) ) ) ;
result = storm : : utility : : vector : : filterVector ( result , ~ maybeStates | initialStates ) ;
} }
return checkR esult;
return r esult;
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
@ -545,27 +542,54 @@ namespace storm {
// Retrieve the appropriate bitvectors by model checking the subformulas.
// Retrieve the appropriate bitvectors by model checking the subformulas.
std : : unique_ptr < CheckResult > subResultPointer = this - > check ( eventuallyFormula . getSubformula ( ) ) ; std : : unique_ptr < CheckResult > subResultPointer = this - > check ( eventuallyFormula . getSubformula ( ) ) ;
storm : : storage : : BitVector phi States( this - > getModel ( ) . getNumberOfStates ( ) , true ) ;
storm : : storage : : BitVector const & psi States= subResultPointer - > asExplicitQualitativeCheckResult ( ) . getTruthValuesVector ( ) ;
storm : : storage : : BitVector true States( this - > getModel ( ) . getNumberOfStates ( ) , true ) ;
storm : : storage : : BitVector const & target States= subResultPointer - > asExplicitQualitativeCheckResult ( ) . getTruthValuesVector ( ) ;
// Do some sanity checks to establish some required properties.
// Do some sanity checks to establish some required properties.
RewardModelType const & rewardModel = this - > getModel ( ) . getRewardModel ( checkTask . isRewardModelSet ( ) ? checkTask . getRewardModel ( ) : " " ) ; RewardModelType const & rewardModel = this - > getModel ( ) . getRewardModel ( checkTask . isRewardModelSet ( ) ? checkTask . getRewardModel ( ) : " " ) ;
STORM_LOG_THROW ( ! rewardModel . empty ( ) , storm : : exceptions : : IllegalArgumentException , " Input model does not have a reward model. " ) ; STORM_LOG_THROW ( ! rewardModel . empty ( ) , storm : : exceptions : : IllegalArgumentException , " Input model does not have a reward model. " ) ;
std : : vector < ValueType > result = computeReachabilityRewards ( this - > getModel ( ) . getTransitionMatrix ( ) , this - > getModel ( ) . getBackwardTransitions ( ) , this - > getModel ( ) . getInitialStates ( ) , targetStates ,
[ & ] ( uint_fast64_t numberOfRows , storm : : storage : : SparseMatrix < ValueType > const & transitionMatrix , storm : : storage : : BitVector const & maybeStates ) {
return rewardModel . getTotalRewardVector ( numberOfRows , transitionMatrix , maybeStates ) ;
} ,
checkTask . isOnlyInitialStatesRelevantSet ( ) ) ;
// Construct check result.
std : : unique_ptr < CheckResult > checkResult ( new ExplicitQuantitativeCheckResult < ValueType > ( result ) ) ;
return checkResult ;
}
template < typename SparseDtmcModelType >
std : : vector < typename SparseDtmcModelType : : ValueType > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : computeReachabilityRewards ( storm : : storage : : SparseMatrix < ValueType > const & probabilityMatrix , storm : : storage : : SparseMatrix < ValueType > const & backwardTransitions , storm : : storage : : BitVector const & initialStates , storm : : storage : : BitVector const & targetStates , std : : vector < ValueType > & stateRewardValues , bool computeForInitialStatesOnly ) {
return computeReachabilityRewards ( probabilityMatrix , backwardTransitions , initialStates , targetStates ,
[ & ] ( uint_fast64_t numberOfRows , storm : : storage : : SparseMatrix < ValueType > const & transitionMatrix , storm : : storage : : BitVector const & maybeStates ) {
std : : vector < ValueType > result ( numberOfRows ) ;
storm : : utility : : vector : : selectVectorValues ( result , maybeStates , stateRewardValues ) ;
return result ;
} ,
computeForInitialStatesOnly ) ;
}
template < typename SparseDtmcModelType >
std : : vector < typename SparseDtmcModelType : : ValueType > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : computeReachabilityRewards ( storm : : storage : : SparseMatrix < ValueType > const & probabilityMatrix , storm : : storage : : SparseMatrix < ValueType > const & backwardTransitions , storm : : storage : : BitVector const & initialStates , storm : : storage : : BitVector const & targetStates , std : : function < std : : vector < ValueType > ( uint_fast64_t , storm : : storage : : SparseMatrix < ValueType > const & , storm : : storage : : BitVector const & ) > const & totalStateRewardVectorGetter , bool computeForInitialStatesOnly ) {
uint_fast64_t numberOfStates = probabilityMatrix . getRowCount ( ) ;
// Then, compute the subset of states that has a reachability reward less than infinity.
storm : : storage : : BitVector trueStates ( this - > getModel ( ) . getNumberOfStates ( ) , true ) ;
storm : : storage : : BitVector infinityStates = storm : : utility : : graph : : performProb1 ( this - > getModel ( ) . getBackwardTransitions ( ) , trueStates , psiStates ) ;
// C ompute the subset of states that has a reachability reward less than infinity.
storm : : storage : : BitVector trueStates ( n umberOfStates, true ) ;
storm : : storage : : BitVector infinityStates = storm : : utility : : graph : : performProb1 ( backwardTransitions , trueStates , target States) ;
infinityStates . complement ( ) ; infinityStates . complement ( ) ;
storm : : storage : : BitVector maybeStates = ~ psiStates & ~ infinityStates ;
storm : : storage : : BitVector maybeStates = ~ target States& ~ infinityStates ;
// Determine whether we need to perform some further computation.
// Determine whether we need to perform some further computation.
bool furtherComputationNeeded = true ; bool furtherComputationNeeded = true ;
if ( checkTask . isOnlyInitialStatesRelevantSet ( ) ) {
if ( this - > getModel ( ) . getInitialStates ( ) . isSubsetOf ( infinityStates ) ) {
if ( computeForInitialStatesOnly ) {
if ( initialStates . isSubsetOf ( infinityStates ) ) {
STORM_LOG_DEBUG ( " The reward of all initial states was found in a preprocessing step. " ) ; STORM_LOG_DEBUG ( " The reward of all initial states was found in a preprocessing step. " ) ;
furtherComputationNeeded = false ; furtherComputationNeeded = false ;
} }
if ( this - > getModel ( ) . getInitialStates ( ) . isSubsetOf ( psiStates ) ) {
if ( initialStates . isSubsetOf ( target States) ) {
STORM_LOG_DEBUG ( " The reward of all initial states was found in a preprocessing step. " ) ; STORM_LOG_DEBUG ( " The reward of all initial states was found in a preprocessing step. " ) ;
furtherComputationNeeded = false ; furtherComputationNeeded = false ;
} }
@ -575,40 +599,37 @@ namespace storm {
if ( furtherComputationNeeded ) { if ( furtherComputationNeeded ) {
// If we compute the results for the initial states only, we can cut off all maybe state that are not
// If we compute the results for the initial states only, we can cut off all maybe state that are not
// reachable from them.
// reachable from them.
if ( checkTask . isOnlyInitialStatesRelevantSet ( ) ) {
if ( computeForInitialStatesOnly ) {
// Determine the set of states that is reachable from the initial state without jumping over a target state.
// Determine the set of states that is reachable from the initial state without jumping over a target state.
storm : : storage : : BitVector reachableStates = storm : : utility : : graph : : getReachableStates ( this - > getModel ( ) . getTransitionMatrix ( ) , this - > getModel ( ) . getInitialStates ( ) , maybeStates , psi States) ;
storm : : storage : : BitVector reachableStates = storm : : utility : : graph : : getReachableStates ( probabilityMatrix , initialStates , maybeStates , target States) ;
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
// Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
maybeStates & = reachableStates ; maybeStates & = reachableStates ;
} }
// Determine the set of initial states of the sub-model.
// Determine the set of initial states of the sub-model.
storm : : storage : : BitVector newInitialStates = this - > getModel ( ) . getInitialStates ( ) % maybeStates ;
storm : : storage : : BitVector newInitialStates = initialStates % maybeStates ;
// We then build the submatrix that only has the transitions of the maybe states.
// We then build the submatrix that only has the transitions of the maybe states.
storm : : storage : : SparseMatrix < ValueType > submatrix = this - > getModel ( ) . getTransitionMatrix ( ) . getSubmatrix ( false , maybeStates , maybeStates ) ;
storm : : storage : : SparseMatrix < ValueType > submatrix = probabilityMatrix . getSubmatrix ( false , maybeStates , maybeStates ) ;
storm : : storage : : SparseMatrix < ValueType > submatrixTransposed = submatrix . transpose ( ) ; storm : : storage : : SparseMatrix < ValueType > submatrixTransposed = submatrix . transpose ( ) ;
// Project the state reward vector to all maybe-states.
// Project the state reward vector to all maybe-states.
std : : vector < ValueType > stateRewardValues = rewardModel . getTotalRewardVector ( maybeStates . getNumberOfSetBits ( ) , this - > getModel ( ) . getTransitionMatrix ( ) , maybeStates ) ;
std : : vector < ValueType > stateRewardValues = totalStateRewardVectorGetter ( submatrix . getRowCount ( ) , probabilityMatrix , maybeStates ) ;
std : : vector < ValueType > subresult = computeReachabilityValues ( submatrix , stateRewardValues , submatrixTransposed , newInitialStates , checkTask . isOnlyInitialStatesRelevantSet ( ) , phiStates , psiStates , this - > getModel ( ) . getTransitionMatrix ( ) . getConstrainedRowSumVector ( maybeStates , psi States) ) ;
std : : vector < ValueType > subresult = computeReachabilityValues ( submatrix , stateRewardValues , submatrixTransposed , newInitialStates , computeForInitialStatesOnly , trueStates , targetStates , probabilityMatrix . getConstrainedRowSumVector ( maybeStates , target States) ) ;
storm : : utility : : vector : : setVectorValues < ValueType > ( result , maybeStates , subresult ) ; storm : : utility : : vector : : setVectorValues < ValueType > ( result , maybeStates , subresult ) ;
} }
// Construct full result.
// Construct full result.
storm : : utility : : vector : : setVectorValues < ValueType > ( result , infinityStates , storm : : utility : : infinity < ValueType > ( ) ) ; storm : : utility : : vector : : setVectorValues < ValueType > ( result , infinityStates , storm : : utility : : infinity < ValueType > ( ) ) ;
storm : : utility : : vector : : setVectorValues < ValueType > ( result , psiStates , storm : : utility : : zero < ValueType > ( ) ) ;
// Construct check result based on whether we have computed values for all states or just the initial states.
std : : unique_ptr < CheckResult > checkResult ( new ExplicitQuantitativeCheckResult < ValueType > ( result ) ) ;
if ( checkTask . isOnlyInitialStatesRelevantSet ( ) ) {
storm : : utility : : vector : : setVectorValues < ValueType > ( result , targetStates , storm : : utility : : zero < ValueType > ( ) ) ;
if ( computeForInitialStatesOnly ) {
// If we computed the results for the initial (and inf) states only, we need to filter the result to
// If we computed the results for the initial (and inf) states only, we need to filter the result to
// only communicate these results.
// only communicate these results.
checkResult - > filter ( ExplicitQualitativeCheckResult ( ~ maybeStates | this - > getModel ( ) . getInitialStates ( ) ) ) ;
result = storm : : utility : : vector : : filterVector ( result , ~ maybeStates | initialStates ) ;
} }
return checkR esult;
return r esult;
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
@ -626,7 +647,7 @@ namespace storm {
storm : : storage : : BitVector trueStates ( this - > getModel ( ) . getNumberOfStates ( ) , true ) ; storm : : storage : : BitVector trueStates ( this - > getModel ( ) . getNumberOfStates ( ) , true ) ;
// Do some sanity checks to establish some required properties.
// Do some sanity checks to establish some required properties.
// STORM_LOG_WARN_COND(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination.");
// STORM_LOG_WARN_COND(storm::settings::getModule< storm::settings::modules::S parseDtmcEliminationModelCheckerSettings> ().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, "The chosen elimination method is not available for computing conditional probabilities. Falling back to regular state elimination.");
STORM_LOG_THROW ( this - > getModel ( ) . getInitialStates ( ) . getNumberOfSetBits ( ) = = 1 , storm : : exceptions : : IllegalArgumentException , " Input model is required to have exactly one initial state. " ) ; STORM_LOG_THROW ( this - > getModel ( ) . getInitialStates ( ) . getNumberOfSetBits ( ) = = 1 , storm : : exceptions : : IllegalArgumentException , " Input model is required to have exactly one initial state. " ) ;
STORM_LOG_THROW ( checkTask . isOnlyInitialStatesRelevantSet ( ) , storm : : exceptions : : IllegalArgumentException , " Cannot compute conditional probabilities for all states. " ) ; STORM_LOG_THROW ( checkTask . isOnlyInitialStatesRelevantSet ( ) , storm : : exceptions : : IllegalArgumentException , " Cannot compute conditional probabilities for all states. " ) ;
storm : : storage : : sparse : : state_type initialState = * this - > getModel ( ) . getInitialStates ( ) . begin ( ) ; storm : : storage : : sparse : : state_type initialState = * this - > getModel ( ) . getInitialStates ( ) . begin ( ) ;
@ -687,28 +708,28 @@ namespace storm {
// Before starting the model checking process, we assign priorities to states so we can use them to
// Before starting the model checking process, we assign priorities to states so we can use them to
// impose ordering constraints later.
// impose ordering constraints later.
boost : : optional < std : : vector < uint_fast64_t > > distanceBasedPriorities ; boost : : optional < std : : vector < uint_fast64_t > > distanceBasedPriorities ;
storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder order = storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . getEliminationOrder ( ) ;
storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder order = storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . getEliminationOrder ( ) ;
if ( eliminationOrderNeedsDistances ( order ) ) { if ( eliminationOrderNeedsDistances ( order ) ) {
distanceBasedPriorities = getDistanceBasedPriorities ( submatrix , submatrixTransposed , newInitialStates , oneStepProbabilities , distanceBasedPriorities = getDistanceBasedPriorities ( submatrix , submatrixTransposed , newInitialStates , oneStepProbabilities ,
eliminationOrderNeedsForwardDistances ( order ) , eliminationOrderNeedsForwardDistances ( order ) ,
eliminationOrderNeedsReversedDistances ( order ) ) ; eliminationOrderNeedsReversedDistances ( order ) ) ;
} }
FlexibleSparseMatrix flexibleMatrix = getFlexibleSpars eMatrix( submatrix ) ;
FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix ( submatrixTransposed , true ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibl eMatrix( submatrix ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibleBackwardTransitions ( submatrixTransposed , true ) ;
std : : unique_ptr < StatePriorityQueue > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , flexibleMatrix , flexibleBackwardTransitions , oneStepProbabilities , statesToEliminate ) ;
std : : shared_ptr < StatePriorityQueue < ValueType > > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , flexibleMatrix , flexibleBackwardTransitions , oneStepProbabilities , statesToEliminate ) ;
STORM_LOG_INFO ( " Computing conditional probilities. " < < std : : endl ) ;
uint_fast64_t numberOfStatesToEliminate = statePriorities - > size ( ) ;
STORM_LOG_INFO ( " Eliminating " < < numberOfStatesToEliminate < < " states using the state elimination technique. " < < std : : endl ) ;
performPrioritizedStateElimination ( statePriorities , flexibleMatrix , flexibleBackwardTransitions , oneStepProbabilities , this - > getModel ( ) . getInitialStates ( ) , true ) ; performPrioritizedStateElimination ( statePriorities , flexibleMatrix , flexibleBackwardTransitions , oneStepProbabilities , this - > getModel ( ) . getInitialStates ( ) , true ) ;
// Prepare some callbacks for the elimination procedure.
ValueUpdateCallback valueUpdateCallback = [ & oneStepProbabilities ] ( storm : : storage : : sparse : : state_type const & state , ValueType const & loopProbability ) { oneStepProbabilities [ state ] = storm : : utility : : simplify ( loopProbability * oneStepProbabilities [ state ] ) ; } ;
PredecessorUpdateCallback predecessorUpdateCallback = [ & oneStepProbabilities ] ( storm : : storage : : sparse : : state_type const & predecessor , ValueType const & probability , storm : : storage : : sparse : : state_type const & state ) { oneStepProbabilities [ predecessor ] = storm : : utility : : simplify ( oneStepProbabilities [ predecessor ] * storm : : utility : : simplify ( probability * oneStepProbabilities [ state ] ) ) ; } ;
boost : : optional < PredecessorFilterCallback > phiFilterCallback = PredecessorFilterCallback ( [ & phiStates ] ( storm : : storage : : sparse : : state_type const & state ) { return phiStates . get ( state ) ; } ) ;
boost : : optional < PredecessorFilterCallback > psiFilterCallback = PredecessorFilterCallback ( [ & psiStates ] ( storm : : storage : : sparse : : state_type const & state ) { return psiStates . get ( state ) ; } ) ;
storm : : solver : : stateelimination : : ConditionalEliminator < SparseDtmcModelType > stateEliminator = storm : : solver : : stateelimination : : ConditionalEliminator < SparseDtmcModelType > ( flexibleMatrix , flexibleBackwardTransitions , oneStepProbabilities , phiStates , psiStates ) ;
// Eliminate the transitions going into the initial state (if there are any).
// Eliminate the transitions going into the initial state (if there are any).
if ( ! flexibleBackwardTransitions . getRow ( * newInitialStates . begin ( ) ) . empty ( ) ) { if ( ! flexibleBackwardTransitions . getRow ( * newInitialStates . begin ( ) ) . empty ( ) ) {
eliminateState ( * newInitialStates . begin ( ) , flexibleMatrix , flexibleBackwardTransitions , valueUpdateCallback , predecessorUpdateCallback , boost : : none , boost : : none , false ) ;
stateEliminator . eliminateState ( * newInitialStates . begin ( ) , false ) ;
} }
// Now we need to basically eliminate all chains of not-psi states after phi states and chains of not-phi
// Now we need to basically eliminate all chains of not-psi states after phi states and chains of not-phi
@ -739,11 +760,13 @@ namespace storm {
for ( auto const & element : currentRow ) { for ( auto const & element : currentRow ) {
// If any of the successors is a phi state, we eliminate it (wrt. all its phi predecessors).
// If any of the successors is a phi state, we eliminate it (wrt. all its phi predecessors).
if ( ! psiStates . get ( element . getColumn ( ) ) ) { if ( ! psiStates . get ( element . getColumn ( ) ) ) {
typename FlexibleSparseMatrix : : row_t ypeconst & successorRow = flexibleMatrix . getRow ( element . getColumn ( ) ) ;
FlexibleRowT ypeconst & successorRow = flexibleMatrix . getRow ( element . getColumn ( ) ) ;
// Eliminate the successor only if there possibly is a psi state reachable through it.
// Eliminate the successor only if there possibly is a psi state reachable through it.
if ( successorRow . size ( ) > 1 | | ( ! successorRow . empty ( ) & & successorRow . front ( ) . getColumn ( ) ! = element . getColumn ( ) ) ) { if ( successorRow . size ( ) > 1 | | ( ! successorRow . empty ( ) & & successorRow . front ( ) . getColumn ( ) ! = element . getColumn ( ) ) ) {
STORM_LOG_TRACE ( " Found non-psi successor " < < element . getColumn ( ) < < " that needs to be eliminated. " ) ; STORM_LOG_TRACE ( " Found non-psi successor " < < element . getColumn ( ) < < " that needs to be eliminated. " ) ;
eliminateState ( element . getColumn ( ) , flexibleMatrix , flexibleBackwardTransitions , valueUpdateCallback , predecessorUpdateCallback , boost : : none , phiFilterCallback , false ) ;
stateEliminator . setStatePhi ( ) ;
stateEliminator . eliminateState ( element . getColumn ( ) , false ) ;
stateEliminator . clearState ( ) ;
hasNonPsiSuccessor = true ; hasNonPsiSuccessor = true ;
} }
} }
@ -769,10 +792,12 @@ namespace storm {
for ( auto const & element : currentRow ) { for ( auto const & element : currentRow ) {
// If any of the successors is a psi state, we eliminate it (wrt. all its psi predecessors).
// If any of the successors is a psi state, we eliminate it (wrt. all its psi predecessors).
if ( ! phiStates . get ( element . getColumn ( ) ) ) { if ( ! phiStates . get ( element . getColumn ( ) ) ) {
typename FlexibleSparseMatrix : : row_t ypeconst & successorRow = flexibleMatrix . getRow ( element . getColumn ( ) ) ;
FlexibleRowT ypeconst & successorRow = flexibleMatrix . getRow ( element . getColumn ( ) ) ;
if ( successorRow . size ( ) > 1 | | ( ! successorRow . empty ( ) & & successorRow . front ( ) . getColumn ( ) ! = element . getColumn ( ) ) ) { if ( successorRow . size ( ) > 1 | | ( ! successorRow . empty ( ) & & successorRow . front ( ) . getColumn ( ) ! = element . getColumn ( ) ) ) {
STORM_LOG_TRACE ( " Found non-phi successor " < < element . getColumn ( ) < < " that needs to be eliminated. " ) ; STORM_LOG_TRACE ( " Found non-phi successor " < < element . getColumn ( ) < < " that needs to be eliminated. " ) ;
eliminateState ( element . getColumn ( ) , flexibleMatrix , flexibleBackwardTransitions , valueUpdateCallback , predecessorUpdateCallback , boost : : none , psiFilterCallback , false ) ;
stateEliminator . setStatePsi ( ) ;
stateEliminator . eliminateState ( element . getColumn ( ) , false ) ;
stateEliminator . clearState ( ) ;
hasNonPhiSuccessor = true ; hasNonPhiSuccessor = true ;
} }
} }
@ -819,12 +844,12 @@ namespace storm {
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
std : : unique_ptr < typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : StatePriorityQueue > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : createStatePriorityQueue ( boost : : optional < std : : vector < uint_fast64_t > > const & distanceBasedStatePriorities , FlexibleSparseMatrix const & transitionMatrix , FlexibleSparseMatrix const & backwardTransitions , std : : vector < typename SparseDtmcModelType : : ValueType > & oneStepProbabilities , storm : : storage : : BitVector const & states ) {
std : : shared_ptr < StatePriorityQueue < typename SparseDtmcModelType : : ValueType > > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : createStatePriorityQueue ( boost : : optional < std : : vector < uint_fast64_t > > const & distanceBasedStatePriorities , storm : : storage : : FlexibleSparseMatrix < ValueType > const & transitionMatrix , storm : : storage : : FlexibleSparseMatrix < ValueType > const & backwardTransitions , std : : vector < ValueType > & oneStepProbabilities , storm : : storage : : BitVector const & states ) {
STORM_LOG_TRACE ( " Creating state priority queue for states " < < states ) ; STORM_LOG_TRACE ( " Creating state priority queue for states " < < states ) ;
// Get the settings to customize the priority queue.
// Get the settings to customize the priority queue.
storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder order = storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . getEliminationOrder ( ) ;
storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder order = storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . getEliminationOrder ( ) ;
std : : vector < storm : : storage : : sparse : : state_type > sortedStates ( states . begin ( ) , states . end ( ) ) ; std : : vector < storm : : storage : : sparse : : state_type > sortedStates ( states . begin ( ) , states . end ( ) ) ;
@ -859,37 +884,36 @@ namespace storm {
} }
} }
} }
STORM_LOG_THROW ( false , storm : : exceptions : : InvalidSettingsException , " Illl egal elimination order selected. " ) ;
STORM_LOG_THROW ( false , storm : : exceptions : : InvalidSettingsException , " Illegal elimination order selected. " ) ;
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
std : : unique_ptr < typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : StatePriorityQueue > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : createNaivePriorityQueue ( storm : : storage : : BitVector const & states ) {
std : : shared_ptr < StatePriorityQueue < typename SparseDtmcModelType : : ValueType > > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : createNaivePriorityQueue ( storm : : storage : : BitVector const & states ) {
std : : vector < storm : : storage : : sparse : : state_type > sortedStates ( states . begin ( ) , states . end ( ) ) ; std : : vector < storm : : storage : : sparse : : state_type > sortedStates ( states . begin ( ) , states . end ( ) ) ;
return std : : unique _ptr< StatePriorityQueue > ( new StaticStatePriorityQueue ( sortedStates ) ) ;
return std : : shared _ptr< StatePriorityQueue < ValueType > > ( new StaticStatePriorityQueue ( sortedStates ) ) ;
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : performPrioritizedStateElimination ( std : : unique _ptr< StatePriorityQueue > & priorityQueue , FlexibleSparseMatrix & transitionMatrix , FlexibleSparseMatrix & backwardTransitions , std : : vector < ValueType > & values , storm : : storage : : BitVector const & initialStates , bool computeResultsForInitialStatesOnly ) {
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : performPrioritizedStateElimination ( std : : shared _ptr< StatePriorityQueue < ValueType > > & priorityQueue , storm : : storage : : FlexibleSparseMatrix < ValueType > & transitionMatrix , storm : : storage : : FlexibleSparseMatrix < ValueType > & backwardTransitions , std : : vector < ValueType > & values , storm : : storage : : BitVector const & initialStates , bool computeResultsForInitialStatesOnly ) {
ValueUpdateCallback valueUpdateCallback = [ & values ] ( storm : : storage : : sparse : : state_type const & state , ValueType const & loopProbability ) { values [ state ] = storm : : utility : : simplify ( loopProbability * values [ state ] ) ; } ;
PredecessorUpdateCallback predecessorCallback = [ & values ] ( storm : : storage : : sparse : : state_type const & predecessor , ValueType const & probability , storm : : storage : : sparse : : state_type const & state ) { values [ predecessor ] = storm : : utility : : simplify ( values [ predecessor ] + storm : : utility : : simplify ( probability * values [ state ] ) ) ; } ;
boost : : optional < PriorityUpdateCallback > priorityUpdateCallback = PriorityUpdateCallback ( [ & transitionMatrix , & backwardTransitions , & values , & priorityQueue ] ( storm : : storage : : sparse : : state_type const & state ) { priorityQueue - > update ( state , transitionMatrix , backwardTransitions , values ) ; } ) ;
boost : : optional < PredecessorFilterCallback > predecessorFilterCallback = boost : : none ;
storm : : solver : : stateelimination : : PrioritizedEliminator < SparseDtmcModelType > stateEliminator ( transitionMatrix , backwardTransitions , priorityQueue , values ) ;
while ( priorityQueue - > hasNextState ( ) ) { while ( priorityQueue - > hasNextState ( ) ) {
storm : : storage : : sparse : : state_type state = priorityQueue - > popNextState ( ) ; storm : : storage : : sparse : : state_type state = priorityQueue - > popNextState ( ) ;
bool removeForwardTransitions = computeResultsForInitialStatesOnly & & ! initialStates . get ( state ) ; bool removeForwardTransitions = computeResultsForInitialStatesOnly & & ! initialStates . get ( state ) ;
eliminateState ( state , transitionMatrix , backwardTransitions , valueUpdateCallback , predecessorCallback , priorityUpdateCallback , predecessorFilterCallback , removeForwardTransitions ) ;
stateEliminator . eliminateState ( state , removeForwardTransitions ) ;
if ( removeForwardTransitions ) { if ( removeForwardTransitions ) {
values [ state ] = storm : : utility : : zero < ValueType > ( ) ; values [ state ] = storm : : utility : : zero < ValueType > ( ) ;
} }
# ifdef STORM_DEV
STORM_LOG_ASSERT ( checkConsistent ( transitionMatrix , backwardTransitions ) , " The forward and backward transition matrices became inconsistent. " ) ; STORM_LOG_ASSERT ( checkConsistent ( transitionMatrix , backwardTransitions ) , " The forward and backward transition matrices became inconsistent. " ) ;
# endif
} }
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : performOrdinaryStateElimination ( FlexibleSparseMatrix & transitionMatrix , FlexibleSparseMatrix & backwardTransitions , storm : : storage : : BitVector const & subsystem , storm : : storage : : BitVector const & initialStates , bool computeResultsForInitialStatesOnly , std : : vector < ValueType > & values , boost : : optional < std : : vector < uint_fast64_t > > const & distanceBasedPriorities ) {
std : : unique _ptr< StatePriorityQueue > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , transitionMatrix , backwardTransitions , values , subsystem ) ;
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : performOrdinaryStateElimination ( storm : : storage : : FlexibleSparseMatrix < ValueType > & transitionMatrix , storm : : storage : : FlexibleSparseMatrix < ValueType > & backwardTransitions , storm : : storage : : BitVector const & subsystem , storm : : storage : : BitVector const & initialStates , bool computeResultsForInitialStatesOnly , std : : vector < ValueType > & values , boost : : optional < std : : vector < uint_fast64_t > > const & distanceBasedPriorities ) {
std : : shared _ptr< StatePriorityQueue < ValueType > > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , transitionMatrix , backwardTransitions , values , subsystem ) ;
std : : size_t numberOfStatesToEliminate = statePriorities - > size ( ) ; std : : size_t numberOfStatesToEliminate = statePriorities - > size ( ) ;
STORM_LOG_DEBUG ( " Eliminating " < < numberOfStatesToEliminate < < " states using the state elimination technique. " < < std : : endl ) ; STORM_LOG_DEBUG ( " Eliminating " < < numberOfStatesToEliminate < < " states using the state elimination technique. " < < std : : endl ) ;
@ -898,17 +922,17 @@ namespace storm {
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
uint_fast64_t SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : performHybridStateElimination ( storm : : storage : : SparseMatrix < ValueType > const & forwardTransitions , FlexibleSparseMatrix & transitionMatrix , FlexibleSparseMatrix & backwardTransitions , storm : : storage : : BitVector const & subsystem , storm : : storage : : BitVector const & initialStates , bool computeResultsForInitialStatesOnly , std : : vector < ValueType > & values , boost : : optional < std : : vector < uint_fast64_t > > const & distanceBasedPriorities ) {
uint_fast64_t SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : performHybridStateElimination ( storm : : storage : : SparseMatrix < ValueType > const & forwardTransitions , storm : : storage : : FlexibleSparseMatrix < ValueType > & transitionMatrix , storm : : storage : : FlexibleSparseMatrix < ValueType > & backwardTransitions , storm : : storage : : BitVector const & subsystem , storm : : storage : : BitVector const & initialStates , bool computeResultsForInitialStatesOnly , std : : vector < ValueType > & values , boost : : optional < std : : vector < uint_fast64_t > > const & distanceBasedPriorities ) {
// When using the hybrid technique, we recursively treat the SCCs up to some size.
// When using the hybrid technique, we recursively treat the SCCs up to some size.
std : : vector < storm : : storage : : sparse : : state_type > entryStateQueue ; std : : vector < storm : : storage : : sparse : : state_type > entryStateQueue ;
STORM_LOG_DEBUG ( " Eliminating " < < subsystem . size ( ) < < " states using the hybrid elimination technique. " < < std : : endl ) ; STORM_LOG_DEBUG ( " Eliminating " < < subsystem . size ( ) < < " states using the hybrid elimination technique. " < < std : : endl ) ;
uint_fast64_t maximalDepth = treatScc ( transitionMatrix , values , initialStates , subsystem , initialStates , forwardTransitions , backwardTransitions , false , 0 , storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . getMaximalSccSize ( ) , entryStateQueue , computeResultsForInitialStatesOnly , distanceBasedPriorities ) ;
uint_fast64_t maximalDepth = treatScc ( transitionMatrix , values , initialStates , subsystem , initialStates , forwardTransitions , backwardTransitions , false , 0 , storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . getMaximalSccSize ( ) , entryStateQueue , computeResultsForInitialStatesOnly , distanceBasedPriorities ) ;
// If the entry states were to be eliminated last, we need to do so now.
// If the entry states were to be eliminated last, we need to do so now.
if ( storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . isEliminateEntryStatesLastSet ( ) ) {
if ( storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . isEliminateEntryStatesLastSet ( ) ) {
STORM_LOG_DEBUG ( " Eliminating " < < entryStateQueue . size ( ) < < " entry states as a last step. " ) ; STORM_LOG_DEBUG ( " Eliminating " < < entryStateQueue . size ( ) < < " entry states as a last step. " ) ;
std : : vector < storm : : storage : : sparse : : state_type > sortedStates ( entryStateQueue . begin ( ) , entryStateQueue . end ( ) ) ; std : : vector < storm : : storage : : sparse : : state_type > sortedStates ( entryStateQueue . begin ( ) , entryStateQueue . end ( ) ) ;
std : : unique _ptr< StatePriorityQueue > queuePriorities = std : : unique _ptr< StatePriorityQueue > ( new StaticStatePriorityQueue ( sortedStates ) ) ;
std : : shared _ptr< StatePriorityQueue < ValueType > > queuePriorities = std : : shared _ptr< StatePriorityQueue < ValueType > > ( new StaticStatePriorityQueue ( sortedStates ) ) ;
performPrioritizedStateElimination ( queuePriorities , transitionMatrix , backwardTransitions , values , initialStates , computeResultsForInitialStatesOnly ) ; performPrioritizedStateElimination ( queuePriorities , transitionMatrix , backwardTransitions , values , initialStates , computeResultsForInitialStatesOnly ) ;
} }
STORM_LOG_DEBUG ( " Eliminated " < < subsystem . size ( ) < < " states. " < < std : : endl ) ; STORM_LOG_DEBUG ( " Eliminated " < < subsystem . size ( ) < < " states. " < < std : : endl ) ;
@ -918,10 +942,10 @@ namespace storm {
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
std : : vector < typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : ValueType > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : computeReachabilityValues ( storm : : storage : : SparseMatrix < ValueType > const & transitionMatrix , std : : vector < ValueType > & values , storm : : storage : : SparseMatrix < ValueType > const & backwardTransitions , storm : : storage : : BitVector const & initialStates , bool computeResultsForInitialStatesOnly , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates , std : : vector < ValueType > const & oneStepProbabilitiesToTarget ) { std : : vector < typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : ValueType > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : computeReachabilityValues ( storm : : storage : : SparseMatrix < ValueType > const & transitionMatrix , std : : vector < ValueType > & values , storm : : storage : : SparseMatrix < ValueType > const & backwardTransitions , storm : : storage : : BitVector const & initialStates , bool computeResultsForInitialStatesOnly , storm : : storage : : BitVector const & phiStates , storm : : storage : : BitVector const & psiStates , std : : vector < ValueType > const & oneStepProbabilitiesToTarget ) {
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
// Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
FlexibleSparseMatrix flexibleMatrix = getFlexibleSpars eMatrix( transitionMatrix ) ;
FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix ( backwardTransitions ) ;
storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder order = storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . getEliminationOrder ( ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibl eMatrix( transitionMatrix ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibleBackwardTransitions ( backwardTransitions ) ;
storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder order = storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . getEliminationOrder ( ) ;
boost : : optional < std : : vector < uint_fast64_t > > distanceBasedPriorities ; boost : : optional < std : : vector < uint_fast64_t > > distanceBasedPriorities ;
if ( eliminationOrderNeedsDistances ( order ) ) { if ( eliminationOrderNeedsDistances ( order ) ) {
distanceBasedPriorities = getDistanceBasedPriorities ( transitionMatrix , backwardTransitions , initialStates , oneStepProbabilitiesToTarget , distanceBasedPriorities = getDistanceBasedPriorities ( transitionMatrix , backwardTransitions , initialStates , oneStepProbabilitiesToTarget ,
@ -932,9 +956,9 @@ namespace storm {
storm : : storage : : BitVector subsystem = storm : : storage : : BitVector ( transitionMatrix . getRowCount ( ) , true ) ; storm : : storage : : BitVector subsystem = storm : : storage : : BitVector ( transitionMatrix . getRowCount ( ) , true ) ;
uint_fast64_t maximalDepth = 0 ; uint_fast64_t maximalDepth = 0 ;
if ( storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . getEliminationMethod ( ) = = storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationMethod : : State ) {
if ( storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . getEliminationMethod ( ) = = storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationMethod : : State ) {
performOrdinaryStateElimination ( flexibleMatrix , flexibleBackwardTransitions , subsystem , initialStates , computeResultsForInitialStatesOnly , values , distanceBasedPriorities ) ; performOrdinaryStateElimination ( flexibleMatrix , flexibleBackwardTransitions , subsystem , initialStates , computeResultsForInitialStatesOnly , values , distanceBasedPriorities ) ;
} else if ( storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . getEliminationMethod ( ) = = storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationMethod : : Hybrid ) {
} else if ( storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . getEliminationMethod ( ) = = storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationMethod : : Hybrid ) {
maximalDepth = performHybridStateElimination ( transitionMatrix , flexibleMatrix , flexibleBackwardTransitions , subsystem , initialStates , computeResultsForInitialStatesOnly , values , distanceBasedPriorities ) ; maximalDepth = performHybridStateElimination ( transitionMatrix , flexibleMatrix , flexibleBackwardTransitions , subsystem , initialStates , computeResultsForInitialStatesOnly , values , distanceBasedPriorities ) ;
} }
@ -950,7 +974,7 @@ namespace storm {
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
uint_fast64_t SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : treatScc ( FlexibleSparseMatrix & matrix , std : : vector < ValueType > & values , storm : : storage : : BitVector const & entryStates , storm : : storage : : BitVector const & scc , storm : : storage : : BitVector const & initialStates , storm : : storage : : SparseMatrix < ValueType > const & forwardTransitions , FlexibleSparseMatrix & backwardTransitions , bool eliminateEntryStates , uint_fast64_t level , uint_fast64_t maximalSccSize , std : : vector < storm : : storage : : sparse : : state_type > & entryStateQueue , bool computeResultsForInitialStatesOnly , boost : : optional < std : : vector < uint_fast64_t > > const & distanceBasedPriorities ) {
uint_fast64_t SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : treatScc ( storm : : storage : : FlexibleSparseMatrix < ValueType > & matrix , std : : vector < ValueType > & values , storm : : storage : : BitVector const & entryStates , storm : : storage : : BitVector const & scc , storm : : storage : : BitVector const & initialStates , storm : : storage : : SparseMatrix < ValueType > const & forwardTransitions , storm : : storage : : FlexibleSparseMatrix < ValueType > & backwardTransitions , bool eliminateEntryStates , uint_fast64_t level , uint_fast64_t maximalSccSize , std : : vector < storm : : storage : : sparse : : state_type > & entryStateQueue , bool computeResultsForInitialStatesOnly , boost : : optional < std : : vector < uint_fast64_t > > const & distanceBasedPriorities ) {
uint_fast64_t maximalDepth = level ; uint_fast64_t maximalDepth = level ;
// If the SCCs are large enough, we try to split them further.
// If the SCCs are large enough, we try to split them further.
@ -966,7 +990,7 @@ namespace storm {
storm : : storage : : BitVector remainingSccs ( decomposition . size ( ) , true ) ; storm : : storage : : BitVector remainingSccs ( decomposition . size ( ) , true ) ;
// First, get rid of the trivial SCCs.
// First, get rid of the trivial SCCs.
storm : : storage : : BitVector statesInTrivialSccs ( matrix . getNumberOfRows ( ) ) ;
storm : : storage : : BitVector statesInTrivialSccs ( matrix . getRowCount ( ) ) ;
for ( uint_fast64_t sccIndex = 0 ; sccIndex < decomposition . size ( ) ; + + sccIndex ) { for ( uint_fast64_t sccIndex = 0 ; sccIndex < decomposition . size ( ) ; + + sccIndex ) {
storm : : storage : : StronglyConnectedComponent const & scc = decomposition . getBlock ( sccIndex ) ; storm : : storage : : StronglyConnectedComponent const & scc = decomposition . getBlock ( sccIndex ) ;
if ( scc . isTrivial ( ) ) { if ( scc . isTrivial ( ) ) {
@ -976,7 +1000,7 @@ namespace storm {
} }
} }
std : : unique _ptr< StatePriorityQueue > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , matrix , backwardTransitions , values , statesInTrivialSccs ) ;
std : : shared _ptr< StatePriorityQueue < ValueType > > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , matrix , backwardTransitions , values , statesInTrivialSccs ) ;
STORM_LOG_TRACE ( " Eliminating " < < statePriorities - > size ( ) < < " trivial SCCs. " ) ; STORM_LOG_TRACE ( " Eliminating " < < statePriorities - > size ( ) < < " trivial SCCs. " ) ;
performPrioritizedStateElimination ( statePriorities , matrix , backwardTransitions , values , initialStates , computeResultsForInitialStatesOnly ) ; performPrioritizedStateElimination ( statePriorities , matrix , backwardTransitions , values , initialStates , computeResultsForInitialStatesOnly ) ;
STORM_LOG_TRACE ( " Eliminated all trivial SCCs. " ) ; STORM_LOG_TRACE ( " Eliminated all trivial SCCs. " ) ;
@ -1000,13 +1024,13 @@ namespace storm {
} }
// Recursively descend in SCC-hierarchy.
// Recursively descend in SCC-hierarchy.
uint_fast64_t depth = treatScc ( matrix , values , entryStates , newSccAsBitVector , initialStates , forwardTransitions , backwardTransitions , eliminateEntryStates | | ! storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . isEliminateEntryStatesLastSet ( ) , level + 1 , maximalSccSize , entryStateQueue , computeResultsForInitialStatesOnly , distanceBasedPriorities ) ;
uint_fast64_t depth = treatScc ( matrix , values , entryStates , newSccAsBitVector , initialStates , forwardTransitions , backwardTransitions , eliminateEntryStates | | ! storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . isEliminateEntryStatesLastSet ( ) , level + 1 , maximalSccSize , entryStateQueue , computeResultsForInitialStatesOnly , distanceBasedPriorities ) ;
maximalDepth = std : : max ( maximalDepth , depth ) ; maximalDepth = std : : max ( maximalDepth , depth ) ;
} }
} else { } else {
// In this case, we perform simple state elimination in the current SCC.
// In this case, we perform simple state elimination in the current SCC.
STORM_LOG_TRACE ( " SCC of size " < < scc . getNumberOfSetBits ( ) < < " is small enough to be eliminated directly. " ) ; STORM_LOG_TRACE ( " SCC of size " < < scc . getNumberOfSetBits ( ) < < " is small enough to be eliminated directly. " ) ;
std : : unique _ptr< StatePriorityQueue > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , matrix , backwardTransitions , values , scc & ~ entryStates ) ;
std : : shared _ptr< StatePriorityQueue < ValueType > > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , matrix , backwardTransitions , values , scc & ~ entryStates ) ;
performPrioritizedStateElimination ( statePriorities , matrix , backwardTransitions , values , initialStates , computeResultsForInitialStatesOnly ) ; performPrioritizedStateElimination ( statePriorities , matrix , backwardTransitions , values , initialStates , computeResultsForInitialStatesOnly ) ;
STORM_LOG_TRACE ( " Eliminated all states of SCC. " ) ; STORM_LOG_TRACE ( " Eliminated all states of SCC. " ) ;
} }
@ -1014,7 +1038,7 @@ namespace storm {
// Finally, eliminate the entry states (if we are required to do so).
// Finally, eliminate the entry states (if we are required to do so).
if ( eliminateEntryStates ) { if ( eliminateEntryStates ) {
STORM_LOG_TRACE ( " Finally, eliminating entry states. " ) ; STORM_LOG_TRACE ( " Finally, eliminating entry states. " ) ;
std : : unique _ptr< StatePriorityQueue > naivePriorities = createNaivePriorityQueue ( entryStates ) ;
std : : shared _ptr< StatePriorityQueue < ValueType > > naivePriorities = createNaivePriorityQueue ( entryStates ) ;
performPrioritizedStateElimination ( naivePriorities , matrix , backwardTransitions , values , initialStates , computeResultsForInitialStatesOnly ) ; performPrioritizedStateElimination ( naivePriorities , matrix , backwardTransitions , values , initialStates , computeResultsForInitialStatesOnly ) ;
STORM_LOG_TRACE ( " Eliminated/added entry states. " ) ; STORM_LOG_TRACE ( " Eliminated/added entry states. " ) ;
} else { } else {
@ -1027,229 +1051,6 @@ namespace storm {
return maximalDepth ; return maximalDepth ;
} }
template < typename SparseDtmcModelType >
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : eliminateState ( storm : : storage : : sparse : : state_type state , FlexibleSparseMatrix & matrix , FlexibleSparseMatrix & backwardTransitions ,
ValueUpdateCallback const & callback , PredecessorUpdateCallback const & predecessorCallback ,
boost : : optional < PriorityUpdateCallback > const & priorityUpdateCallback ,
boost : : optional < PredecessorFilterCallback > const & predecessorFilterCallback , bool removeForwardTransitions ) {
STORM_LOG_TRACE ( " Eliminating state " < < state < < " . " ) ;
// Start by finding loop probability.
bool hasSelfLoop = false ;
ValueType loopProbability = storm : : utility : : zero < ValueType > ( ) ;
typename FlexibleSparseMatrix : : row_type & currentStateSuccessors = matrix . getRow ( state ) ;
for ( auto entryIt = currentStateSuccessors . begin ( ) , entryIte = currentStateSuccessors . end ( ) ; entryIt ! = entryIte ; + + entryIt ) {
if ( entryIt - > getColumn ( ) > = state ) {
if ( entryIt - > getColumn ( ) = = state ) {
loopProbability = entryIt - > getValue ( ) ;
hasSelfLoop = true ;
// If we do not clear the forward transitions completely, we need to remove the self-loop,
// because we scale all the other outgoing transitions with it anyway.
if ( ! removeForwardTransitions ) {
currentStateSuccessors . erase ( entryIt ) ;
}
}
break ;
}
}
// Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop.
STORM_LOG_TRACE ( ( hasSelfLoop ? " State has self-loop. " : " State does not have a self-loop. " ) ) ;
if ( hasSelfLoop ) {
STORM_LOG_ASSERT ( loopProbability ! = storm : : utility : : one < ValueType > ( ) , " Must not eliminate state with probability 1 self-loop. " ) ;
loopProbability = storm : : utility : : simplify ( storm : : utility : : one < ValueType > ( ) / ( storm : : utility : : one < ValueType > ( ) - loopProbability ) ) ;
for ( auto & entry : matrix . getRow ( state ) ) {
// Only scale the non-diagonal entries.
if ( entry . getColumn ( ) ! = state ) {
entry . setValue ( storm : : utility : : simplify ( entry . getValue ( ) * loopProbability ) ) ;
}
}
callback ( state , loopProbability ) ;
}
// Now connect the predecessors of the state being eliminated with its successors.
typename FlexibleSparseMatrix : : row_type & currentStatePredecessors = backwardTransitions . getRow ( state ) ;
// In case we have a constrained elimination, we need to keep track of the new predecessors.
typename FlexibleSparseMatrix : : row_type newCurrentStatePredecessors ;
std : : vector < typename FlexibleSparseMatrix : : row_type > newBackwardProbabilities ( currentStateSuccessors . size ( ) ) ;
for ( auto & backwardProbabilities : newBackwardProbabilities ) {
backwardProbabilities . reserve ( currentStatePredecessors . size ( ) ) ;
}
// Now go through the predecessors and eliminate the ones (satisfying the constraint if given).
for ( auto const & predecessorEntry : currentStatePredecessors ) {
uint_fast64_t predecessor = predecessorEntry . getColumn ( ) ;
STORM_LOG_TRACE ( " Found predecessor " < < predecessor < < " . " ) ;
// Skip the state itself as one of its predecessors.
if ( predecessor = = state ) {
assert ( hasSelfLoop ) ;
continue ;
}
// Skip the state if the elimination is constrained, but the predecessor is not in the constraint.
if ( predecessorFilterCallback & & ! predecessorFilterCallback . get ( ) ( predecessor ) ) {
newCurrentStatePredecessors . emplace_back ( predecessorEntry ) ;
STORM_LOG_TRACE ( " Not eliminating predecessor " < < predecessor < < " , because it does not fit the filter. " ) ;
continue ;
}
STORM_LOG_TRACE ( " Eliminating predecessor " < < predecessor < < " . " ) ;
// First, find the probability with which the predecessor can move to the current state, because
// the forward probabilities of the state to be eliminated need to be scaled with this factor.
typename FlexibleSparseMatrix : : row_type & predecessorForwardTransitions = matrix . getRow ( predecessor ) ;
typename FlexibleSparseMatrix : : row_type : : iterator multiplyElement = std : : find_if ( predecessorForwardTransitions . begin ( ) , predecessorForwardTransitions . end ( ) , [ & ] ( storm : : storage : : MatrixEntry < typename FlexibleSparseMatrix : : index_type , typename FlexibleSparseMatrix : : value_type > const & a ) { return a . getColumn ( ) = = state ; } ) ;
// Make sure we have found the probability and set it to zero.
STORM_LOG_THROW ( multiplyElement ! = predecessorForwardTransitions . end ( ) , storm : : exceptions : : InvalidStateException , " No probability for successor found. " ) ;
ValueType multiplyFactor = multiplyElement - > getValue ( ) ;
multiplyElement - > setValue ( storm : : utility : : zero < ValueType > ( ) ) ;
// At this point, we need to update the (forward) transitions of the predecessor.
typename FlexibleSparseMatrix : : row_type : : iterator first1 = predecessorForwardTransitions . begin ( ) ;
typename FlexibleSparseMatrix : : row_type : : iterator last1 = predecessorForwardTransitions . end ( ) ;
typename FlexibleSparseMatrix : : row_type : : iterator first2 = currentStateSuccessors . begin ( ) ;
typename FlexibleSparseMatrix : : row_type : : iterator last2 = currentStateSuccessors . end ( ) ;
typename FlexibleSparseMatrix : : row_type newSuccessors ;
newSuccessors . reserve ( ( last1 - first1 ) + ( last2 - first2 ) ) ;
std : : insert_iterator < typename FlexibleSparseMatrix : : row_type > result ( newSuccessors , newSuccessors . end ( ) ) ;
uint_fast64_t successorOffsetInNewBackwardTransitions = 0 ;
// Now we merge the two successor lists. (Code taken from std::set_union and modified to suit our needs).
for ( ; first1 ! = last1 ; + + result ) {
// Skip the transitions to the state that is currently being eliminated.
if ( first1 - > getColumn ( ) = = state | | ( first2 ! = last2 & & first2 - > getColumn ( ) = = state ) ) {
if ( first1 - > getColumn ( ) = = state ) {
+ + first1 ;
}
if ( first2 ! = last2 & & first2 - > getColumn ( ) = = state ) {
+ + first2 ;
}
continue ;
}
if ( first2 = = last2 ) {
std : : copy_if ( first1 , last1 , result , [ & ] ( storm : : storage : : MatrixEntry < typename FlexibleSparseMatrix : : index_type , typename FlexibleSparseMatrix : : value_type > const & a ) { return a . getColumn ( ) ! = state ; } ) ;
break ;
}
if ( first2 - > getColumn ( ) < first1 - > getColumn ( ) ) {
auto successorEntry = storm : : utility : : simplify ( std : : move ( * first2 * multiplyFactor ) ) ;
* result = successorEntry ;
newBackwardProbabilities [ successorOffsetInNewBackwardTransitions ] . emplace_back ( predecessor , successorEntry . getValue ( ) ) ;
+ + first2 ;
+ + successorOffsetInNewBackwardTransitions ;
} else if ( first1 - > getColumn ( ) < first2 - > getColumn ( ) ) {
* result = * first1 ;
+ + first1 ;
} else {
auto probability = storm : : utility : : simplify ( first1 - > getValue ( ) + storm : : utility : : simplify ( multiplyFactor * first2 - > getValue ( ) ) ) ;
* result = storm : : storage : : MatrixEntry < typename FlexibleSparseMatrix : : index_type , typename FlexibleSparseMatrix : : value_type > ( first1 - > getColumn ( ) , probability ) ;
newBackwardProbabilities [ successorOffsetInNewBackwardTransitions ] . emplace_back ( predecessor , probability ) ;
+ + first1 ;
+ + first2 ;
+ + successorOffsetInNewBackwardTransitions ;
}
}
for ( ; first2 ! = last2 ; + + first2 ) {
if ( first2 - > getColumn ( ) ! = state ) {
auto stateProbability = storm : : utility : : simplify ( std : : move ( * first2 * multiplyFactor ) ) ;
* result = stateProbability ;
newBackwardProbabilities [ successorOffsetInNewBackwardTransitions ] . emplace_back ( predecessor , stateProbability . getValue ( ) ) ;
+ + successorOffsetInNewBackwardTransitions ;
}
}
// Now move the new transitions in place.
predecessorForwardTransitions = std : : move ( newSuccessors ) ;
STORM_LOG_TRACE ( " Fixed new next-state probabilities of predecessor state " < < predecessor < < " . " ) ;
predecessorCallback ( predecessor , multiplyFactor , state ) ;
if ( priorityUpdateCallback ) {
STORM_LOG_TRACE ( " Updating priority of predecessor. " ) ;
priorityUpdateCallback . get ( ) ( predecessor ) ;
}
}
// Finally, we need to add the predecessor to the set of predecessors of every successor.
uint_fast64_t successorOffsetInNewBackwardTransitions = 0 ;
for ( auto const & successorEntry : currentStateSuccessors ) {
if ( successorEntry . getColumn ( ) = = state ) {
continue ;
}
typename FlexibleSparseMatrix : : row_type & successorBackwardTransitions = backwardTransitions . getRow ( successorEntry . getColumn ( ) ) ;
// Delete the current state as a predecessor of the successor state only if we are going to remove the
// current state's forward transitions.
if ( removeForwardTransitions ) {
typename FlexibleSparseMatrix : : row_type : : iterator elimIt = std : : find_if ( successorBackwardTransitions . begin ( ) , successorBackwardTransitions . end ( ) , [ & ] ( storm : : storage : : MatrixEntry < typename FlexibleSparseMatrix : : index_type , typename FlexibleSparseMatrix : : value_type > const & a ) { return a . getColumn ( ) = = state ; } ) ;
STORM_LOG_ASSERT ( elimIt ! = successorBackwardTransitions . end ( ) , " Expected a proper backward transition from " < < successorEntry . getColumn ( ) < < " to " < < state < < " , but found none. " ) ;
successorBackwardTransitions . erase ( elimIt ) ;
}
typename FlexibleSparseMatrix : : row_type : : iterator first1 = successorBackwardTransitions . begin ( ) ;
typename FlexibleSparseMatrix : : row_type : : iterator last1 = successorBackwardTransitions . end ( ) ;
typename FlexibleSparseMatrix : : row_type : : iterator first2 = newBackwardProbabilities [ successorOffsetInNewBackwardTransitions ] . begin ( ) ;
typename FlexibleSparseMatrix : : row_type : : iterator last2 = newBackwardProbabilities [ successorOffsetInNewBackwardTransitions ] . end ( ) ;
typename FlexibleSparseMatrix : : row_type newPredecessors ;
newPredecessors . reserve ( ( last1 - first1 ) + ( last2 - first2 ) ) ;
std : : insert_iterator < typename FlexibleSparseMatrix : : row_type > result ( newPredecessors , newPredecessors . end ( ) ) ;
for ( ; first1 ! = last1 ; + + result ) {
if ( first2 = = last2 ) {
std : : copy ( first1 , last1 , result ) ;
break ;
}
if ( first2 - > getColumn ( ) < first1 - > getColumn ( ) ) {
if ( first2 - > getColumn ( ) ! = state ) {
* result = * first2 ;
}
+ + first2 ;
} else if ( first1 - > getColumn ( ) = = first2 - > getColumn ( ) ) {
if ( estimateComplexity ( first1 - > getValue ( ) ) > estimateComplexity ( first2 - > getValue ( ) ) ) {
* result = * first1 ;
} else {
* result = * first2 ;
}
+ + first1 ;
+ + first2 ;
} else {
* result = * first1 ;
+ + first1 ;
}
}
if ( predecessorFilterCallback ) {
std : : copy_if ( first2 , last2 , result , [ & ] ( storm : : storage : : MatrixEntry < typename FlexibleSparseMatrix : : index_type , typename FlexibleSparseMatrix : : value_type > const & a ) { return a . getColumn ( ) ! = state & & predecessorFilterCallback . get ( ) ( a . getColumn ( ) ) ; } ) ;
} else {
std : : copy_if ( first2 , last2 , result , [ & ] ( storm : : storage : : MatrixEntry < typename FlexibleSparseMatrix : : index_type , typename FlexibleSparseMatrix : : value_type > const & a ) { return a . getColumn ( ) ! = state ; } ) ;
}
// Now move the new predecessors in place.
successorBackwardTransitions = std : : move ( newPredecessors ) ;
+ + successorOffsetInNewBackwardTransitions ;
}
STORM_LOG_TRACE ( " Fixed predecessor lists of successor states. " ) ;
if ( removeForwardTransitions ) {
// Clear the eliminated row to reduce memory consumption.
currentStateSuccessors . clear ( ) ;
currentStateSuccessors . shrink_to_fit ( ) ;
}
if ( predecessorFilterCallback ) {
currentStatePredecessors = std : : move ( newCurrentStatePredecessors ) ;
} else {
currentStatePredecessors . clear ( ) ;
currentStatePredecessors . shrink_to_fit ( ) ;
}
}
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
std : : vector < uint_fast64_t > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : getDistanceBasedPriorities ( storm : : storage : : SparseMatrix < ValueType > const & transitionMatrix , storm : : storage : : SparseMatrix < ValueType > const & transitionMatrixTransposed , storm : : storage : : BitVector const & initialStates , std : : vector < ValueType > const & oneStepProbabilities , bool forward , bool reverse ) { std : : vector < uint_fast64_t > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : getDistanceBasedPriorities ( storm : : storage : : SparseMatrix < ValueType > const & transitionMatrix , storm : : storage : : SparseMatrix < ValueType > const & transitionMatrixTransposed , storm : : storage : : BitVector const & initialStates , std : : vector < ValueType > const & oneStepProbabilities , bool forward , bool reverse ) {
std : : vector < uint_fast64_t > statePriorities ( transitionMatrix . getRowCount ( ) ) ; std : : vector < uint_fast64_t > statePriorities ( transitionMatrix . getRowCount ( ) ) ;
@ -1259,8 +1060,8 @@ namespace storm {
} }
std : : vector < std : : size_t > distances = getStateDistances ( transitionMatrix , transitionMatrixTransposed , initialStates , oneStepProbabilities , std : : vector < std : : size_t > distances = getStateDistances ( transitionMatrix , transitionMatrixTransposed , initialStates , oneStepProbabilities ,
storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . getEliminationOrder ( ) = = storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder : : Forward | |
storm : : settings : : spa rseDtmcEliminationModelCheckerSettings( ) . getEliminationOrder ( ) = = storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder : : ForwardReversed ) ;
storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . getEliminationOrder ( ) = = storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder : : Forward | |
storm : : settings : : getModule < storm : : settings : : modules : : Spa rseDtmcEliminationModelCheckerSettings> ( ) . getEliminationOrder ( ) = = storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder : : ForwardReversed ) ;
// In case of the forward or backward ordering, we can sort the states according to the distances.
// In case of the forward or backward ordering, we can sort the states according to the distances.
if ( forward ^ reverse ) { if ( forward ^ reverse ) {
@ -1298,111 +1099,7 @@ namespace storm {
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : FlexibleSparseMatrix ( index_type rows ) : data ( rows ) {
// Intentionally left empty.
}
template < typename SparseDtmcModelType >
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : reserveInRow ( index_type row , index_type numberOfElements ) {
this - > data [ row ] . reserve ( numberOfElements ) ;
}
template < typename SparseDtmcModelType >
typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : row_type & SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : getRow ( index_type index ) {
return this - > data [ index ] ;
}
template < typename SparseDtmcModelType >
typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : row_type const & SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : getRow ( index_type index ) const {
return this - > data [ index ] ;
}
template < typename SparseDtmcModelType >
typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : index_type SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : getNumberOfRows ( ) const {
return this - > data . size ( ) ;
}
template < typename SparseDtmcModelType >
bool SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : hasSelfLoop ( storm : : storage : : sparse : : state_type state ) {
for ( auto const & entry : this - > getRow ( state ) ) {
if ( entry . getColumn ( ) < state ) {
continue ;
} else if ( entry . getColumn ( ) > state ) {
return false ;
} else if ( entry . getColumn ( ) = = state ) {
return true ;
}
}
return false ;
}
template < typename SparseDtmcModelType >
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : print ( ) const {
for ( uint_fast64_t index = 0 ; index < this - > data . size ( ) ; + + index ) {
std : : cout < < index < < " - " ;
for ( auto const & element : this - > getRow ( index ) ) {
std : : cout < < " ( " < < element . getColumn ( ) < < " , " < < element . getValue ( ) < < " ) " ;
}
std : : cout < < std : : endl ;
}
}
template < typename SparseDtmcModelType >
bool SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : empty ( ) const {
for ( auto const & row : this - > data ) {
if ( ! row . empty ( ) ) {
return false ;
}
}
return true ;
}
template < typename SparseDtmcModelType >
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix : : filter ( storm : : storage : : BitVector const & rowFilter , storm : : storage : : BitVector const & columnFilter ) {
for ( uint_fast64_t rowIndex = 0 ; rowIndex < this - > data . size ( ) ; + + rowIndex ) {
auto & row = this - > data [ rowIndex ] ;
if ( ! rowFilter . get ( rowIndex ) ) {
row . clear ( ) ;
row . shrink_to_fit ( ) ;
continue ;
}
row_type newRow ;
for ( auto const & element : row ) {
if ( columnFilter . get ( element . getColumn ( ) ) ) {
newRow . push_back ( element ) ;
}
}
row = std : : move ( newRow ) ;
}
}
template < typename SparseDtmcModelType >
typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : FlexibleSparseMatrix SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : getFlexibleSparseMatrix ( storm : : storage : : SparseMatrix < ValueType > const & matrix , bool setAllValuesToOne ) {
FlexibleSparseMatrix flexibleMatrix ( matrix . getRowCount ( ) ) ;
for ( typename FlexibleSparseMatrix : : index_type rowIndex = 0 ; rowIndex < matrix . getRowCount ( ) ; + + rowIndex ) {
typename storm : : storage : : SparseMatrix < ValueType > : : const_rows row = matrix . getRow ( rowIndex ) ;
flexibleMatrix . reserveInRow ( rowIndex , row . getNumberOfEntries ( ) ) ;
for ( auto const & element : row ) {
// If the probability is zero, we skip this entry.
if ( storm : : utility : : isZero ( element . getValue ( ) ) ) {
continue ;
}
if ( setAllValuesToOne ) {
flexibleMatrix . getRow ( rowIndex ) . emplace_back ( element . getColumn ( ) , storm : : utility : : one < ValueType > ( ) ) ;
} else {
flexibleMatrix . getRow ( rowIndex ) . emplace_back ( element ) ;
}
}
}
return flexibleMatrix ;
}
template < typename SparseDtmcModelType >
uint_fast64_t SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : computeStatePenalty ( storm : : storage : : sparse : : state_type const & state , FlexibleSparseMatrix const & transitionMatrix , FlexibleSparseMatrix const & backwardTransitions , std : : vector < ValueType > const & oneStepProbabilities ) {
uint_fast64_t SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : computeStatePenalty ( storm : : storage : : sparse : : state_type const & state , storm : : storage : : FlexibleSparseMatrix < ValueType > const & transitionMatrix , storm : : storage : : FlexibleSparseMatrix < ValueType > const & backwardTransitions , std : : vector < ValueType > const & oneStepProbabilities ) {
uint_fast64_t penalty = 0 ; uint_fast64_t penalty = 0 ;
bool hasParametricSelfLoop = false ; bool hasParametricSelfLoop = false ;
@ -1429,17 +1126,17 @@ namespace storm {
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
uint_fast64_t SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : computeStatePenaltyRegularExpression ( storm : : storage : : sparse : : state_type const & state , FlexibleSparseMatrix const & transitionMatrix , FlexibleSparseMatrix const & backwardTransitions , std : : vector < ValueType > const & oneStepProbabilities ) {
uint_fast64_t SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : computeStatePenaltyRegularExpression ( storm : : storage : : sparse : : state_type const & state , storm : : storage : : FlexibleSparseMatrix < ValueType > const & transitionMatrix , storm : : storage : : FlexibleSparseMatrix < ValueType > const & backwardTransitions , std : : vector < ValueType > const & oneStepProbabilities ) {
return backwardTransitions . getRow ( state ) . size ( ) * transitionMatrix . getRow ( state ) . size ( ) ; return backwardTransitions . getRow ( state ) . size ( ) * transitionMatrix . getRow ( state ) . size ( ) ;
} }
template < typename SparseDtmcModel Type>
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : StatePriorityQueue : : update ( storm : : storage : : sparse : : state_type , FlexibleSparseMatrix const & transitionMatrix , FlexibleSparseMatrix const & backwardTransitions , std : : vector < ValueType > const & oneStepProbabilities ) {
template < typename Value Type>
void StatePriorityQueue < ValueType > : : update ( storm : : storage : : sparse : : state_type , storm : : storage : : FlexibleSparseMatrix < ValueType > const & transitionMatrix , storm : : storage : : FlexibleSparseMatrix < ValueType > const & backwardTransitions , std : : vector < ValueType > const & oneStepProbabilities ) {
// Intentionally left empty.
// Intentionally left empty.
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : StaticStatePriorityQueue : : StaticStatePriorityQueue ( std : : vector < storm : : storage : : sparse : : state_type > const & sortedStates ) : StatePriorityQueue ( ) , sortedStates ( sortedStates ) , currentPosition ( 0 ) {
SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : StaticStatePriorityQueue : : StaticStatePriorityQueue ( std : : vector < storm : : storage : : sparse : : state_type > const & sortedStates ) : StatePriorityQueue < ValueType > ( ) , sortedStates ( sortedStates ) , currentPosition ( 0 ) {
// Intentionally left empty.
// Intentionally left empty.
} }
@ -1460,7 +1157,7 @@ namespace storm {
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : DynamicPenaltyStatePriorityQueue : : DynamicPenaltyStatePriorityQueue ( std : : vector < std : : pair < storm : : storage : : sparse : : state_type , uint_fast64_t > > const & sortedStatePenaltyPairs , PenaltyFunctionType const & penaltyFunction ) : StatePriorityQueue ( ) , priorityQueue ( ) , stateToPriorityMapping ( ) , penaltyFunction ( penaltyFunction ) {
SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : DynamicPenaltyStatePriorityQueue : : DynamicPenaltyStatePriorityQueue ( std : : vector < std : : pair < storm : : storage : : sparse : : state_type , uint_fast64_t > > const & sortedStatePenaltyPairs , PenaltyFunctionType const & penaltyFunction ) : StatePriorityQueue < ValueType > ( ) , priorityQueue ( ) , stateToPriorityMapping ( ) , penaltyFunction ( penaltyFunction ) {
// Insert all state-penalty pairs into our priority queue.
// Insert all state-penalty pairs into our priority queue.
for ( auto const & statePenalty : sortedStatePenaltyPairs ) { for ( auto const & statePenalty : sortedStatePenaltyPairs ) {
priorityQueue . insert ( priorityQueue . end ( ) , statePenalty ) ; priorityQueue . insert ( priorityQueue . end ( ) , statePenalty ) ;
@ -1487,7 +1184,7 @@ namespace storm {
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : DynamicPenaltyStatePriorityQueue : : update ( storm : : storage : : sparse : : state_type state , FlexibleSparseMatrix const & transitionMatrix , FlexibleSparseMatrix const & backwardTransitions , std : : vector < ValueType > const & oneStepProbabilities ) {
void SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : DynamicPenaltyStatePriorityQueue : : update ( storm : : storage : : sparse : : state_type state , storm : : storage : : FlexibleSparseMatrix < ValueType > const & transitionMatrix , storm : : storage : : FlexibleSparseMatrix < ValueType > const & backwardTransitions , std : : vector < ValueType > const & oneStepProbabilities ) {
// First, we need to find the priority until now.
// First, we need to find the priority until now.
auto priorityIt = stateToPriorityMapping . find ( state ) ; auto priorityIt = stateToPriorityMapping . find ( state ) ;
@ -1516,8 +1213,8 @@ namespace storm {
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
bool SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : checkConsistent ( FlexibleSparseMatrix & transitionMatrix , FlexibleSparseMatrix & backwardTransitions ) {
for ( uint_fast64_t forwardIndex = 0 ; forwardIndex < transitionMatrix . getNumberOfRows ( ) ; + + forwardIndex ) {
bool SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : checkConsistent ( storm : : storage : : FlexibleSparseMatrix < ValueType > & transitionMatrix , storm : : storage : : FlexibleSparseMatrix < ValueType > & backwardTransitions ) {
for ( uint_fast64_t forwardIndex = 0 ; forwardIndex < transitionMatrix . getRowCount ( ) ; + + forwardIndex ) {
for ( auto const & forwardEntry : transitionMatrix . getRow ( forwardIndex ) ) { for ( auto const & forwardEntry : transitionMatrix . getRow ( forwardIndex ) ) {
if ( forwardEntry . getColumn ( ) = = forwardIndex ) { if ( forwardEntry . getColumn ( ) = = forwardIndex ) {
continue ; continue ;
@ -1538,9 +1235,13 @@ namespace storm {
return true ; return true ;
} }
template class StatePriorityQueue < double > ;
template class SparseDtmcEliminationModelChecker < storm : : models : : sparse : : Dtmc < double > > ; template class SparseDtmcEliminationModelChecker < storm : : models : : sparse : : Dtmc < double > > ;
template uint_fast64_t estimateComplexity ( double const & value ) ;
# ifdef STORM_HAVE_CARL
# ifdef STORM_HAVE_CARL
template class StatePriorityQueue < storm : : RationalFunction > ;
template class SparseDtmcEliminationModelChecker < storm : : models : : sparse : : Dtmc < storm : : RationalFunction > > ; template class SparseDtmcEliminationModelChecker < storm : : models : : sparse : : Dtmc < storm : : RationalFunction > > ;
# endif
# endif
} // namespace modelchecker
} // namespace modelchecker
sjunges
10 years ago