@ -25,6 +25,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 {
@ -260,10 +264,10 @@ 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 ( ) ;
@ -300,30 +304,13 @@ 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 : : unique_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 ) ;
STORM_LOG_ASSERT ( checkConsistent ( flexibleMatrix , flexibleBackwardTransitions ) , " The forward and backward transition matrices became inconsistent. " ) ;
} }
// 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
@ -345,11 +332,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 ) {
@ -752,21 +739,24 @@ namespace storm {
eliminationOrderNeedsReversedDistances ( order ) ) ; eliminationOrderNeedsReversedDistances ( order ) ) ;
} }
FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix ( submatrix ) ;
FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix ( submatrixTransposed , true ) ;
std : : chrono : : high_resolution_clock : : time_point conversionStart = std : : chrono : : high_resolution_clock : : now ( ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibleMatrix ( submatrix ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibleBackwardTransitions ( submatrixTransposed , true ) ;
std : : chrono : : high_resolution_clock : : time_point conversionEnd = std : : chrono : : high_resolution_clock : : now ( ) ;
std : : unique_ptr < StatePriorityQueue > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , flexibleMatrix , flexibleBackwardTransitions , oneStepProbabilities , statesToEliminate ) ;
std : : unique_ptr < StatePriorityQueue < ValueType > > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , flexibleMatrix , flexibleBackwardTransitions , oneStepProbabilities , statesToEliminate ) ;
STORM_LOG_INFO ( " Computing conditional probilities. " < < std : : endl ) ;
std : : chrono : : high_resolution_clock : : time_point modelCheckingStart = std : : chrono : : high_resolution_clock : : now ( ) ;
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
@ -797,11 +787,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 ;
} }
} }
@ -827,10 +819,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 ;
} }
} }
@ -877,7 +871,7 @@ 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 : : unique_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 ) ;
@ -921,23 +915,20 @@ namespace storm {
} }
template < typename SparseDtmcModelType > template < typename SparseDtmcModelType >
std : : unique_ptr < typename SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : StatePriorityQueue > SparseDtmcEliminationModelChecker < SparseDtmcModelType > : : createNaivePriorityQueue ( storm : : storage : : BitVector const & states ) {
std : : unique_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 : : unique_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 : : unique_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 > ( ) ;
} }
@ -946,8 +937,8 @@ namespace storm {
} }
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 : : unique_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 ) ;
@ -956,7 +947,7 @@ 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 ) ;
@ -966,7 +957,7 @@ namespace storm {
if ( storm : : settings : : sparseDtmcEliminationModelCheckerSettings ( ) . isEliminateEntryStatesLastSet ( ) ) { if ( storm : : settings : : sparseDtmcEliminationModelCheckerSettings ( ) . 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 : : unique_ptr < StatePriorityQueue < ValueType > > queuePriorities = std : : unique_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 ) ;
@ -976,8 +967,11 @@ 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 = getFlexibleSparseMatrix ( transitionMatrix ) ;
FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix ( backwardTransitions ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibleMatrix ( transitionMatrix ) ;
storm : : storage : : FlexibleSparseMatrix < ValueType > flexibleBackwardTransitions ( backwardTransitions ) ;
auto conversionEnd = 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 : : sparseDtmcEliminationModelCheckerSettings ( ) . getEliminationOrder ( ) ; storm : : settings : : modules : : SparseDtmcEliminationModelCheckerSettings : : EliminationOrder order = storm : : settings : : sparseDtmcEliminationModelCheckerSettings ( ) . getEliminationOrder ( ) ;
boost : : optional < std : : vector < uint_fast64_t > > distanceBasedPriorities ; boost : : optional < std : : vector < uint_fast64_t > > distanceBasedPriorities ;
@ -1008,7 +1002,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.
@ -1024,7 +1018,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 ( ) ) {
@ -1034,7 +1028,7 @@ namespace storm {
} }
} }
std : : unique_ptr < StatePriorityQueue > statePriorities = createStatePriorityQueue ( distanceBasedPriorities , matrix , backwardTransitions , values , statesInTrivialSccs ) ;
std : : unique_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. " ) ;
@ -1064,7 +1058,7 @@ namespace storm {
} 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 : : unique_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. " ) ;
} }
@ -1072,7 +1066,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 : : unique_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 {
@ -1085,229 +1079,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 ( ) ) ;
@ -1356,111 +1127,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 ;
@ -1487,17 +1154,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.
} }
@ -1518,7 +1185,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 ) ;
@ -1545,7 +1212,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 ) ;
@ -1574,8 +1241,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 ;
@ -1596,9 +1263,11 @@ 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 > > ;
# 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
Mavo
9 years ago