@ -17,17 +17,29 @@
namespace storm {
namespace storage {
template < typename ValueType >
SparseModelMemoryProduct < ValueType > : : SparseModelMemoryProduct ( storm : : models : : sparse : : Model < ValueType > const & sparseModel , storm : : storage : : MemoryStructure const & memoryStructure ) : model ( sparseModel ) , memory ( memoryStructure ) {
// intentionally left empty
template < typename ValueType , typename RewardModelType >
SparseModelMemoryProduct < ValueType , RewardModelType > : : SparseModelMemoryProduct ( storm : : models : : sparse : : Model < ValueType , RewardModel Type > const & sparseModel , storm : : storage : : MemoryStructure const & memoryStructure ) : model ( sparseModel ) , memory ( memoryStructure ) {
reachableStates = storm : : storage : : BitVector ( model . getNumberOfStates ( ) * memory . getNumberOfStates ( ) , false ) ;
}
template < typename ValueType , typename RewardModelType >
void SparseModelMemoryProduct < ValueType , RewardModelType > : : addReachableState ( uint64_t const & modelState , uint64_t const & memoryState ) {
reachableStates . set ( modelState * memory . getNumberOfStates ( ) + memoryState , true ) ;
}
template < typename ValueType , typename RewardModelType >
void SparseModelMemoryProduct < ValueType , RewardModelType > : : setBuildFullProduct ( ) {
reachableStates . clear ( ) ;
reachableStates . complement ( ) ;
}
template < typename ValueType , typename RewardModelType >
std : : shared_ptr < storm : : models : : sparse : : Model < ValueType , RewardModelType > > SparseModelMemoryProduct < ValueType , RewardModelType > : : build ( boost : : optional < storm : : storage : : Scheduler < ValueType > > const & scheduler ) {
template < typename ValueType >
std : : shared_ptr < storm : : models : : sparse : : Model < ValueType > > SparseModelMemoryProduct < ValueType > : : build ( ) {
uint_fast64_t modelStateCount = model . getNumberOfStates ( ) ;
uint_fast64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint64_t modelStateCount = model . getNumberOfStates ( ) ;
uint64_t memoryStateCount = memory . getNumberOfStates ( ) ;
std : : vector < uint_fast64_t > memorySuccessors = computeMemorySuccessors ( ) ;
std : : vector < uint64_t > memorySuccessors = computeMemorySuccessors ( ) ;
// Get the initial states and reachable states. A stateIndex s corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
storm : : storage : : BitVector initialStates ( modelStateCount * memoryStateCount , false ) ;
@ -38,44 +50,49 @@ namespace storm {
}
STORM_LOG_ASSERT ( memoryInitIt = = memory . getInitialMemoryStates ( ) . end ( ) , " Unexpected number of initial states. " ) ;
storm : : storage : : BitVector reachableStates = computeReachableStates ( memorySuccessors , initialStates ) ;
computeReachableStates ( memorySuccessors , initialStates , scheduler ) ;
// Compute the mapping to the states of the result
uint_fast 64_t reachableStateCount = 0 ;
toResultStateMapping = std : : vector < uint_fast 64_t > ( model . getNumberOfStates ( ) * memory . getNumberOfStates ( ) , std : : numeric_limits < uint_fas t64_t > : : max ( ) ) ;
uint64_t reachableStateCount = 0 ;
toResultStateMapping = std : : vector < uint64_t > ( model . getNumberOfStates ( ) * memory . getNumberOfStates ( ) , std : : numeric_limits < uint64_t > : : max ( ) ) ;
for ( auto const & reachableState : reachableStates ) {
toResultStateMapping [ reachableState ] = reachableStateCount ;
+ + reachableStateCount ;
}
// Build the model components
storm : : storage : : SparseMatrix < ValueType > transitionMatrix = model . getTransitionMatrix ( ) . hasTrivialRowGrouping ( ) ?
buildDeterministicTransitionMatrix ( reachableStates , memorySuccessors ) :
buildNondeterministicTransitionMatrix ( reachableStates , memorySuccessors ) ;
storm : : storage : : SparseMatrix < ValueType > transitionMatrix ;
if ( scheduler ) {
transitionMatrix = buildTransitionMatrixForScheduler ( memorySuccessors , scheduler . get ( ) ) ;
} else if ( model . getTransitionMatrix ( ) . hasTrivialRowGrouping ( ) ) {
transitionMatrix = buildDeterministicTransitionMatrix ( memorySuccessors ) ;
} else {
transitionMatrix = buildNondeterministicTransitionMatrix ( memorySuccessors ) ;
}
storm : : models : : sparse : : StateLabeling labeling = buildStateLabeling ( transitionMatrix ) ;
std : : unordered_map < std : : string , storm : : models : : sparse : : StandardRewardModel < ValueType > > rewardModels = buildRewardModels ( transitionMatrix , memorySuccessors ) ;
std : : unordered_map < std : : string , RewardModelType > rewardModels = buildRewardModels ( transitionMatrix , memorySuccessors , scheduler ) ;
// Add the label for the initial states. We need to translate the state indices w.r.t. the set of reachable states.
labeling . addLabel ( " init " , initialStates % reachableStates ) ;
return buildResult ( std : : move ( transitionMatrix ) , std : : move ( labeling ) , std : : move ( rewardModels ) ) ;
return buildResult ( std : : move ( transitionMatrix ) , std : : move ( labeling ) , std : : move ( rewardModels ) , scheduler ) ;
}
template < typename ValueType >
uint_fast 64_t const & SparseModelMemoryProduct < ValueType > : : getResultState ( uint_fast 64_t const & modelState , uint_fas t64_t const & memoryState ) const {
template < typename ValueType , typename RewardModelType >
uint64_t const & SparseModelMemoryProduct < ValueType , RewardModelType > : : getResultState ( uint64_t const & modelState , uint64_t const & memoryState ) const {
return toResultStateMapping [ modelState * memory . getNumberOfStates ( ) + memoryState ] ;
}
template < typename ValueType >
std : : vector < uint_fast 64_t > SparseModelMemoryProduct < ValueType > : : computeMemorySuccessors ( ) const {
uint_fast 64_t modelTransitionCount = model . getTransitionMatrix ( ) . getEntryCount ( ) ;
uint_fast 64_t memoryStateCount = memory . getNumberOfStates ( ) ;
std : : vector < uint_fast 64_t > result ( modelTransitionCount * memoryStateCount , std : : numeric_limits < uint_fas t64_t > : : max ( ) ) ;
template < typename ValueType , typename RewardModelType >
std : : vector < uint64_t > SparseModelMemoryProduct < ValueType , RewardModel Type > : : computeMemorySuccessors ( ) const {
uint64_t modelTransitionCount = model . getTransitionMatrix ( ) . getEntryCount ( ) ;
uint64_t memoryStateCount = memory . getNumberOfStates ( ) ;
std : : vector < uint64_t > result ( modelTransitionCount * memoryStateCount , std : : numeric_limits < uint64_t > : : max ( ) ) ;
for ( uint_fast 64_t memoryState = 0 ; memoryState < memoryStateCount ; + + memoryState ) {
for ( uint_fast 64_t transitionGoal = 0 ; transitionGoal < memoryStateCount ; + + transitionGoal ) {
for ( uint64_t memoryState = 0 ; memoryState < memoryStateCount ; + + memoryState ) {
for ( uint64_t transitionGoal = 0 ; transitionGoal < memoryStateCount ; + + transitionGoal ) {
auto const & memoryTransition = memory . getTransitionMatrix ( ) [ memoryState ] [ transitionGoal ] ;
if ( memoryTransition ) {
for ( auto const & modelTransitionIndex : memoryTransition . get ( ) ) {
@ -87,54 +104,76 @@ namespace storm {
return result ;
}
template < typename ValueType >
storm : : storage : : BitVector SparseModelMemoryProduct < ValueType > : : computeReachableStates ( std : : vector < uint_fast64_t > const & memorySuccessors , storm : : storage : : BitVector const & initialStates ) const {
uint_fast 64_t memoryStateCount = memory . getNumberOfStates ( ) ;
template < typename ValueType , typename RewardModelType >
void SparseModelMemoryProduct < ValueType , RewardModelType > : : computeReachableStates ( std : : vector < uint64_t > const & memorySuccessors , storm : : storage : : BitVector const & initialStates , boost : : optional < storm : : storage : : Scheduler < ValueType > > const & scheduler ) {
uint64_t memoryStateCount = memory . getNumberOfStates ( ) ;
// Explore the reachable states via DFS.
// A state s on the stack corresponds to the model state (s / memoryStateCount) and memory state (s % memoryStateCount)
storm : : storage : : BitVector reachableStates = initialStates ;
std : : vector < uint_fast64_t > stack ( reachableStates . begin ( ) , reachableStates . end ( ) ) ;
while ( ! stack . empty ( ) ) {
uint_fast64_t stateIndex = stack . back ( ) ;
stack . pop_back ( ) ;
uint_fast64_t modelState = stateIndex / memoryStateCount ;
uint_fast64_t memoryState = stateIndex % memoryStateCount ;
auto const & rowGroup = model . getTransitionMatrix ( ) . getRowGroup ( modelState ) ;
for ( auto modelTransitionIt = rowGroup . begin ( ) ; modelTransitionIt ! = rowGroup . end ( ) ; + + modelTransitionIt ) {
if ( ! storm : : utility : : isZero ( modelTransitionIt - > getValue ( ) ) ) {
uint_fast64_t successorModelState = modelTransitionIt - > getColumn ( ) ;
uint_fast64_t modelTransitionId = modelTransitionIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint_fast64_t successorMemoryState = memorySuccessors [ modelTransitionId * memoryStateCount + memoryState ] ;
uint_fast64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState ;
if ( ! reachableStates . get ( successorStateIndex ) ) {
reachableStates . set ( successorStateIndex , true ) ;
stack . push_back ( successorStateIndex ) ;
reachableStates | = initialStates ;
if ( ! reachableStates . full ( ) ) {
std : : vector < uint64_t > stack ( reachableStates . begin ( ) , reachableStates . end ( ) ) ;
while ( ! stack . empty ( ) ) {
uint64_t stateIndex = stack . back ( ) ;
stack . pop_back ( ) ;
uint64_t modelState = stateIndex / memoryStateCount ;
uint64_t memoryState = stateIndex % memoryStateCount ;
if ( scheduler ) {
auto choices = scheduler - > getChoice ( modelState , memoryState ) . getChoiceAsDistribution ( ) ;
uint64_t groupStart = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] ;
for ( auto const & choice : choices ) {
STORM_LOG_ASSERT ( groupStart + choice . first < model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState + 1 ] , " Invalid choice " < < choice . first < < " at model state " < < modelState < < " . " ) ;
auto const & row = model . getTransitionMatrix ( ) . getRow ( groupStart + choice . first ) ;
for ( auto modelTransitionIt = row . begin ( ) ; modelTransitionIt ! = row . end ( ) ; + + modelTransitionIt ) {
if ( ! storm : : utility : : isZero ( modelTransitionIt - > getValue ( ) ) ) {
uint64_t successorModelState = modelTransitionIt - > getColumn ( ) ;
uint64_t modelTransitionId = modelTransitionIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint64_t successorMemoryState = memorySuccessors [ modelTransitionId * memoryStateCount + memoryState ] ;
uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState ;
if ( ! reachableStates . get ( successorStateIndex ) ) {
reachableStates . set ( successorStateIndex , true ) ;
stack . push_back ( successorStateIndex ) ;
}
}
}
}
} else {
auto const & rowGroup = model . getTransitionMatrix ( ) . getRowGroup ( modelState ) ;
for ( auto modelTransitionIt = rowGroup . begin ( ) ; modelTransitionIt ! = rowGroup . end ( ) ; + + modelTransitionIt ) {
if ( ! storm : : utility : : isZero ( modelTransitionIt - > getValue ( ) ) ) {
uint64_t successorModelState = modelTransitionIt - > getColumn ( ) ;
uint64_t modelTransitionId = modelTransitionIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint64_t successorMemoryState = memorySuccessors [ modelTransitionId * memoryStateCount + memoryState ] ;
uint64_t successorStateIndex = successorModelState * memoryStateCount + successorMemoryState ;
if ( ! reachableStates . get ( successorStateIndex ) ) {
reachableStates . set ( successorStateIndex , true ) ;
stack . push_back ( successorStateIndex ) ;
}
}
}
}
}
}
return reachableStates ;
}
template < typename ValueType >
storm : : storage : : SparseMatrix < ValueType > SparseModelMemoryProduct < ValueType > : : buildDeterministicTransitionMatrix ( storm : : storage : : BitVector const & reachableStates , std : : vector < uint_fast64_t > const & memorySuccessors ) const {
uint_fast64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint_fast64_t numResStates = reachableStates . getNumberOfSetBits ( ) ;
uint_fast64_t numResTransitions = 0 ;
template < typename ValueType , typename RewardModelType >
storm : : storage : : SparseMatrix < ValueType > SparseModelMemoryProduct < ValueType , RewardModelType > : : buildDeterministicTransitionMatrix ( std : : vector < uint64_t > const & memorySuccessors ) const {
uint64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint64_t numResStates = reachableStates . getNumberOfSetBits ( ) ;
uint64_t numResTransitions = 0 ;
for ( auto const & stateIndex : reachableStates ) {
numResTransitions + = model . getTransitionMatrix ( ) . getRow ( stateIndex / memoryStateCount ) . getNumberOfEntries ( ) ;
}
storm : : storage : : SparseMatrixBuilder < ValueType > builder ( numResStates , numResStates , numResTransitions , true ) ;
uint_fast64_t currentRow = 0 ;
uint64_t currentRow = 0 ;
for ( auto const & stateIndex : reachableStates ) {
uint_fast64_t modelState = stateIndex / memoryStateCount ;
uint_fast64_t memoryState = stateIndex % memoryStateCount ;
uint64_t modelState = stateIndex / memoryStateCount ;
uint64_t memoryState = stateIndex % memoryStateCount ;
auto const & modelRow = model . getTransitionMatrix ( ) . getRow ( modelState ) ;
for ( auto entryIt = modelRow . begin ( ) ; entryIt ! = modelRow . end ( ) ; + + entryIt ) {
uint_fast 64_t transitionId = entryIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint_fast 64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
uint64_t transitionId = entryIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
builder . addNextValue ( currentRow , getResultState ( entryIt - > getColumn ( ) , successorMemoryState ) , entryIt - > getValue ( ) ) ;
}
+ + currentRow ;
@ -143,31 +182,31 @@ namespace storm {
return builder . build ( ) ;
}
template < typename ValueType >
storm : : storage : : SparseMatrix < ValueType > SparseModelMemoryProduct < ValueType > : : buildNondeterministicTransitionMatrix ( storm : : storage : : BitVector const & reachableStates , std : : vector < uint_fas t64_t > const & memorySuccessors ) const {
uint_fast 64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint_fast 64_t numResStates = reachableStates . getNumberOfSetBits ( ) ;
uint_fast 64_t numResChoices = 0 ;
uint_fast 64_t numResTransitions = 0 ;
template < typename ValueType , typename RewardModelType >
storm : : storage : : SparseMatrix < ValueType > SparseModelMemoryProduct < ValueType , RewardModelType > : : buildNondeterministicTransitionMatrix ( std : : vector < uint64_t > const & memorySuccessors ) const {
uint64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint64_t numResStates = reachableStates . getNumberOfSetBits ( ) ;
uint64_t numResChoices = 0 ;
uint64_t numResTransitions = 0 ;
for ( auto const & stateIndex : reachableStates ) {
uint_fast 64_t modelState = stateIndex / memoryStateCount ;
for ( uint_fast 64_t modelRow = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] ; modelRow < model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState + 1 ] ; + + modelRow ) {
uint64_t modelState = stateIndex / memoryStateCount ;
for ( uint64_t modelRow = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] ; modelRow < model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState + 1 ] ; + + modelRow ) {
+ + numResChoices ;
numResTransitions + = model . getTransitionMatrix ( ) . getRow ( modelRow ) . getNumberOfEntries ( ) ;
}
}
storm : : storage : : SparseMatrixBuilder < ValueType > builder ( numResChoices , numResStates , numResTransitions , true , true , numResStates ) ;
uint_fast 64_t currentRow = 0 ;
uint64_t currentRow = 0 ;
for ( auto const & stateIndex : reachableStates ) {
uint_fast 64_t modelState = stateIndex / memoryStateCount ;
uint_fast 64_t memoryState = stateIndex % memoryStateCount ;
uint64_t modelState = stateIndex / memoryStateCount ;
uint64_t memoryState = stateIndex % memoryStateCount ;
builder . newRowGroup ( currentRow ) ;
for ( uint_fast 64_t modelRowIndex = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] ; modelRowIndex < model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState + 1 ] ; + + modelRowIndex ) {
for ( uint64_t modelRowIndex = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] ; modelRowIndex < model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState + 1 ] ; + + modelRowIndex ) {
auto const & modelRow = model . getTransitionMatrix ( ) . getRow ( modelRowIndex ) ;
for ( auto entryIt = modelRow . begin ( ) ; entryIt ! = modelRow . end ( ) ; + + entryIt ) {
uint_fast 64_t transitionId = entryIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint_fast 64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
uint64_t transitionId = entryIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
builder . addNextValue ( currentRow , getResultState ( entryIt - > getColumn ( ) , successorMemoryState ) , entryIt - > getValue ( ) ) ;
}
+ + currentRow ;
@ -177,20 +216,115 @@ namespace storm {
return builder . build ( ) ;
}
template < typename ValueType >
storm : : models : : sparse : : StateLabeling SparseModelMemoryProduct < ValueType > : : buildStateLabeling ( storm : : storage : : SparseMatrix < ValueType > const & resultTransitionMatrix ) const {
uint_fast64_t modelStateCount = model . getNumberOfStates ( ) ;
uint_fast64_t memoryStateCount = memory . getNumberOfStates ( ) ;
template < typename ValueType , typename RewardModelType >
storm : : storage : : SparseMatrix < ValueType > SparseModelMemoryProduct < ValueType , RewardModelType > : : buildTransitionMatrixForScheduler ( std : : vector < uint64_t > const & memorySuccessors , storm : : storage : : Scheduler < ValueType > const & scheduler ) const {
uint64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint64_t numResStates = reachableStates . getNumberOfSetBits ( ) ;
uint64_t numResChoices = 0 ;
uint64_t numResTransitions = 0 ;
bool hasTrivialNondeterminism = true ;
for ( auto const & stateIndex : reachableStates ) {
uint64_t modelState = stateIndex / memoryStateCount ;
uint64_t memoryState = stateIndex % memoryStateCount ;
storm : : storage : : SchedulerChoice < ValueType > choice = scheduler . getChoice ( modelState , memoryState ) ;
if ( choice . isDefined ( ) ) {
+ + numResChoices ;
if ( choice . isDeterministic ( ) ) {
uint64_t modelRow = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] + choice . getDeterministicChoice ( ) ;
numResTransitions + = model . getTransitionMatrix ( ) . getRow ( modelRow ) . getNumberOfEntries ( ) ;
} else {
std : : set < uint64_t > successors ;
for ( auto const & choiceIndex : choice . getChoiceAsDistribution ( ) ) {
if ( ! storm : : utility : : isZero ( choiceIndex . second ) ) {
uint64_t modelRow = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] + choiceIndex . first ;
for ( auto const & entry : model . getTransitionMatrix ( ) . getRow ( modelRow ) ) {
successors . insert ( entry . getColumn ( ) ) ;
}
}
}
numResTransitions + = successors . size ( ) ;
}
} else {
uint64_t modelRow = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] ;
uint64_t groupEnd = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState + 1 ] ;
hasTrivialNondeterminism = hasTrivialNondeterminism & & ( groupEnd = = modelRow + 1 ) ;
for ( ; groupEnd ; + + modelRow ) {
+ + numResChoices ;
numResTransitions + = model . getTransitionMatrix ( ) . getRow ( modelRow ) . getNumberOfEntries ( ) ;
}
}
}
storm : : storage : : SparseMatrixBuilder < ValueType > builder ( numResChoices , numResStates , numResTransitions , true , ! hasTrivialNondeterminism , hasTrivialNondeterminism ? 0 : numResStates ) ;
uint64_t currentRow = 0 ;
for ( auto const & stateIndex : reachableStates ) {
uint64_t modelState = stateIndex / memoryStateCount ;
uint64_t memoryState = stateIndex % memoryStateCount ;
if ( ! hasTrivialNondeterminism ) {
builder . newRowGroup ( currentRow ) ;
}
storm : : storage : : SchedulerChoice < ValueType > choice = scheduler . getChoice ( modelState , memoryState ) ;
if ( choice . isDefined ( ) ) {
if ( choice . isDeterministic ( ) ) {
uint64_t modelRowIndex = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] + choice . getDeterministicChoice ( ) ;
auto const & modelRow = model . getTransitionMatrix ( ) . getRow ( modelRowIndex ) ;
for ( auto entryIt = modelRow . begin ( ) ; entryIt ! = modelRow . end ( ) ; + + entryIt ) {
uint64_t transitionId = entryIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
builder . addNextValue ( currentRow , getResultState ( entryIt - > getColumn ( ) , successorMemoryState ) , entryIt - > getValue ( ) ) ;
}
} else {
std : : map < uint64_t , ValueType > transitions ;
for ( auto const & choiceIndex : choice . getChoiceAsDistribution ( ) ) {
if ( ! storm : : utility : : isZero ( choiceIndex . second ) ) {
uint64_t modelRowIndex = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] + choiceIndex . first ;
auto const & modelRow = model . getTransitionMatrix ( ) . getRow ( modelRowIndex ) ;
for ( auto entryIt = modelRow . begin ( ) ; entryIt ! = modelRow . end ( ) ; + + entryIt ) {
uint64_t transitionId = entryIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
ValueType transitionValue = choiceIndex . second * entryIt - > getValue ( ) ;
auto insertionRes = transitions . insert ( std : : make_pair ( getResultState ( entryIt - > getColumn ( ) , successorMemoryState ) , transitionValue ) ) ;
if ( ! insertionRes . second ) {
insertionRes . first - > second + = transitionValue ;
}
}
}
}
for ( auto const & transition : transitions ) {
builder . addNextValue ( currentRow , transition . first , transition . second ) ;
}
}
+ + currentRow ;
} else {
for ( uint64_t modelRowIndex = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] ; modelRowIndex < model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState + 1 ] ; + + modelRowIndex ) {
auto const & modelRow = model . getTransitionMatrix ( ) . getRow ( modelRowIndex ) ;
for ( auto entryIt = modelRow . begin ( ) ; entryIt ! = modelRow . end ( ) ; + + entryIt ) {
uint64_t transitionId = entryIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
builder . addNextValue ( currentRow , getResultState ( entryIt - > getColumn ( ) , successorMemoryState ) , entryIt - > getValue ( ) ) ;
}
+ + currentRow ;
}
}
}
return builder . build ( ) ;
}
template < typename ValueType , typename RewardModelType >
storm : : models : : sparse : : StateLabeling SparseModelMemoryProduct < ValueType , RewardModelType > : : buildStateLabeling ( storm : : storage : : SparseMatrix < ValueType > const & resultTransitionMatrix ) const {
uint64_t modelStateCount = model . getNumberOfStates ( ) ;
uint64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint_fast64_t numResStates = resultTransitionMatrix . getRowGroupCount ( ) ;
uint64_t numResStates = resultTransitionMatrix . getRowGroupCount ( ) ;
storm : : models : : sparse : : StateLabeling resultLabeling ( numResStates ) ;
for ( std : : string modelLabel : model . getStateLabeling ( ) . getLabels ( ) ) {
if ( modelLabel ! = " init " ) {
storm : : storage : : BitVector resLabeledStates ( numResStates , false ) ;
for ( auto const & modelState : model . getStateLabeling ( ) . getStates ( modelLabel ) ) {
for ( uint_fast64_t memoryState = 0 ; memoryState < memoryStateCount ; + + memoryState ) {
uint_fast64_t const & resState = getResultState ( modelState , memoryState ) ;
for ( uint64_t memoryState = 0 ; memoryState < memoryStateCount ; + + memoryState ) {
uint64_t const & resState = getResultState ( modelState , memoryState ) ;
// Check if the state exists in the result (i.e. if it is reachable)
if ( resState < numResStates ) {
resLabeledStates . set ( resState , true ) ;
@ -204,8 +338,8 @@ namespace storm {
STORM_LOG_THROW ( ! resultLabeling . containsLabel ( memoryLabel ) , storm : : exceptions : : InvalidOperationException , " Failed to build the product of model and memory structure: State labelings are not disjoint as both structures contain the label " < < memoryLabel < < " . " ) ;
storm : : storage : : BitVector resLabeledStates ( numResStates , false ) ;
for ( auto const & memoryState : memory . getStateLabeling ( ) . getStates ( memoryLabel ) ) {
for ( uint_fast 64_t modelState = 0 ; modelState < modelStateCount ; + + modelState ) {
uint_fast 64_t const & resState = getResultState ( modelState , memoryState ) ;
for ( uint64_t modelState = 0 ; modelState < modelStateCount ; + + modelState ) {
uint64_t const & resState = getResultState ( modelState , memoryState ) ;
// Check if the state exists in the result (i.e. if it is reachable)
if ( resState < numResStates ) {
resLabeledStates . set ( resState , true ) ;
@ -217,21 +351,24 @@ namespace storm {
return resultLabeling ;
}
template < typename ValueType >
std : : unordered_map < std : : string , storm : : models : : sparse : : StandardRewardModel < ValueType > > SparseModelMemoryProduct < ValueType > : : buildRewardModels ( storm : : storage : : SparseMatrix < ValueType > const & resultTransitionMatrix , std : : vector < uint_fast64_t > const & memorySuccessors ) const {
std : : unordered_map < std : : string , storm : : models : : sparse : : StandardRewardModel < ValueType > > result ;
uint_fast64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint_fast64_t numResStates = resultTransitionMatrix . getRowGroupCount ( ) ;
template < typename ValueType , typename RewardModelType >
std : : unordered_map < std : : string , RewardModelType > SparseModelMemoryProduct < ValueType , RewardModelType > : : buildRewardModels ( storm : : storage : : SparseMatrix < ValueType > const & resultTransitionMatrix , std : : vector < uint64_t > const & memorySuccessors , boost : : optional < storm : : storage : : Scheduler < ValueType > > const & scheduler ) const {
typedef typename RewardModelType : : ValueType RewardValueType ;
std : : unordered_map < std : : string , RewardModelType > result ;
uint64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint64_t numResStates = resultTransitionMatrix . getRowGroupCount ( ) ;
for ( auto const & rewardModel : model . getRewardModels ( ) ) {
boost : : optional < std : : vector < ValueType > > stateRewards ;
boost : : optional < std : : vector < Reward ValueType> > stateRewards ;
if ( rewardModel . second . hasStateRewards ( ) ) {
stateRewards = std : : vector < ValueType > ( numResStates , storm : : utility : : zero < ValueType > ( ) ) ;
uint_fast 64_t modelState = 0 ;
stateRewards = std : : vector < Reward ValueType> ( numResStates , storm : : utility : : zero < Reward ValueType> ( ) ) ;
uint64_t modelState = 0 ;
for ( auto const & modelStateReward : rewardModel . second . getStateRewardVector ( ) ) {
if ( ! storm : : utility : : isZero ( modelStateReward ) ) {
for ( uint_fast 64_t memoryState = 0 ; memoryState < memoryStateCount ; + + memoryState ) {
uint_fast 64_t const & resState = getResultState ( modelState , memoryState ) ;
for ( uint64_t memoryState = 0 ; memoryState < memoryStateCount ; + + memoryState ) {
uint64_t const & resState = getResultState ( modelState , memoryState ) ;
// Check if the state exists in the result (i.e. if it is reachable)
if ( resState < numResStates ) {
stateRewards . get ( ) [ resState ] = modelStateReward ;
@ -241,45 +378,78 @@ namespace storm {
+ + modelState ;
}
}
boost : : optional < std : : vector < ValueType > > stateActionRewards ;
boost : : optional < std : : vector < Reward ValueType> > stateActionRewards ;
if ( rewardModel . second . hasStateActionRewards ( ) ) {
stateActionRewards = std : : vector < ValueType > ( resultTransitionMatrix . getRowCount ( ) , storm : : utility : : zero < ValueType > ( ) ) ;
uint_fast 64_t modelState = 0 ;
uint_fast 64_t modelRow = 0 ;
stateActionRewards = std : : vector < Reward ValueType> ( resultTransitionMatrix . getRowCount ( ) , storm : : utility : : zero < Reward ValueType> ( ) ) ;
uint64_t modelState = 0 ;
uint64_t modelRow = 0 ;
for ( auto const & modelStateActionReward : rewardModel . second . getStateActionRewardVector ( ) ) {
if ( ! storm : : utility : : isZero ( modelStateActionReward ) ) {
while ( modelRow > = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState + 1 ] ) {
+ + modelState ;
}
uint_fast 64_t rowOffset = modelRow - model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] ;
for ( uint_fast 64_t memoryState = 0 ; memoryState < memoryStateCount ; + + memoryState ) {
uint_fast 64_t const & resState = getResultState ( modelState , memoryState ) ;
uint64_t rowOffset = modelRow - model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] ;
for ( uint64_t memoryState = 0 ; memoryState < memoryStateCount ; + + memoryState ) {
uint64_t const & resState = getResultState ( modelState , memoryState ) ;
// Check if the state exists in the result (i.e. if it is reachable)
if ( resState < numResStates ) {
stateActionRewards . get ( ) [ resultTransitionMatrix . getRowGroupIndices ( ) [ resState ] + rowOffset ] = modelStateActionReward ;
if ( scheduler & & scheduler - > getChoice ( modelState , memoryState ) . isDefined ( ) ) {
ValueType factor = scheduler - > getChoice ( modelState , memoryState ) . getChoiceAsDistribution ( ) . getProbability ( rowOffset ) ;
stateActionRewards . get ( ) [ resultTransitionMatrix . getRowGroupIndices ( ) [ resState ] ] = factor * modelStateActionReward ;
} else {
stateActionRewards . get ( ) [ resultTransitionMatrix . getRowGroupIndices ( ) [ resState ] + rowOffset ] = modelStateActionReward ;
}
}
}
}
+ + modelRow ;
}
}
boost : : optional < storm : : storage : : SparseMatrix < ValueType > > transitionRewards ;
boost : : optional < storm : : storage : : SparseMatrix < Reward ValueType> > transitionRewards ;
if ( rewardModel . second . hasTransitionRewards ( ) ) {
storm : : storage : : SparseMatrixBuilder < ValueType > builder ( resultTransitionMatrix . getRowCount ( ) , resultTransitionMatrix . getColumnCount ( ) ) ;
uint_fast 64_t stateIndex = 0 ;
storm : : storage : : SparseMatrixBuilder < Reward ValueType> builder ( resultTransitionMatrix . getRowCount ( ) , resultTransitionMatrix . getColumnCount ( ) ) ;
uint64_t stateIndex = 0 ;
for ( auto const & resState : toResultStateMapping ) {
if ( resState < numResStates ) {
uint_fast64_t modelState = stateIndex / memoryStateCount ;
uint_fast64_t memoryState = stateIndex % memoryStateCount ;
uint_fast64_t rowGroupSize = resultTransitionMatrix . getRowGroupSize ( resState ) ;
for ( uint_fast64_t rowOffset = 0 ; rowOffset < rowGroupSize ; + + rowOffset ) {
uint_fast64_t resRowIndex = resultTransitionMatrix . getRowGroupIndices ( ) [ resState ] + rowOffset ;
uint_fast64_t modelRowIndex = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] + rowOffset ;
auto const & rewardMatrixRow = rewardModel . second . getTransitionRewardMatrix ( ) . getRow ( modelRowIndex ) ;
for ( auto entryIt = rewardMatrixRow . begin ( ) ; entryIt ! = rewardMatrixRow . end ( ) ; + + entryIt ) {
uint_fast64_t transitionId = entryIt - rewardModel . second . getTransitionRewardMatrix ( ) . begin ( ) ;
uint_fast64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
builder . addNextValue ( resRowIndex , getResultState ( entryIt - > getColumn ( ) , successorMemoryState ) , entryIt - > getValue ( ) ) ;
uint64_t modelState = stateIndex / memoryStateCount ;
uint64_t memoryState = stateIndex % memoryStateCount ;
uint64_t rowGroupSize = resultTransitionMatrix . getRowGroupSize ( resState ) ;
if ( scheduler & & scheduler - > getChoice ( modelState , memoryState ) . isDefined ( ) ) {
std : : map < uint64_t , RewardValueType > rewards ;
for ( uint64_t rowOffset = 0 ; rowOffset < rowGroupSize ; + + rowOffset ) {
uint64_t modelRowIndex = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] + rowOffset ;
auto transitionEntryIt = model . getTransitionMatrix ( ) . getRow ( modelRowIndex ) . begin ( ) ;
for ( auto const & rewardEntry : rewardModel . second . getTransitionRewardMatrix ( ) . getRow ( modelRowIndex ) ) {
while ( transitionEntryIt - > getColumn ( ) ! = rewardEntry . getColumn ( ) ) {
STORM_LOG_ASSERT ( transitionEntryIt ! = model . getTransitionMatrix ( ) . getRow ( modelRowIndex ) . end ( ) , " The reward transition matrix is not a submatrix of the model transition matrix. " ) ;
+ + transitionEntryIt ;
}
uint64_t transitionId = transitionEntryIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
auto insertionRes = rewards . insert ( std : : make_pair ( getResultState ( rewardEntry . getColumn ( ) , successorMemoryState ) , rewardEntry . getValue ( ) ) ) ;
if ( ! insertionRes . second ) {
insertionRes . first - > second + = rewardEntry . getValue ( ) ;
}
}
}
uint64_t resRowIndex = resultTransitionMatrix . getRowGroupIndices ( ) [ resState ] ;
for ( auto & reward : rewards ) {
builder . addNextValue ( resRowIndex , reward . first , reward . second ) ;
}
} else {
for ( uint64_t rowOffset = 0 ; rowOffset < rowGroupSize ; + + rowOffset ) {
uint64_t resRowIndex = resultTransitionMatrix . getRowGroupIndices ( ) [ resState ] + rowOffset ;
uint64_t modelRowIndex = model . getTransitionMatrix ( ) . getRowGroupIndices ( ) [ modelState ] + rowOffset ;
auto transitionEntryIt = model . getTransitionMatrix ( ) . getRow ( modelRowIndex ) . begin ( ) ;
for ( auto const & rewardEntry : rewardModel . second . getTransitionRewardMatrix ( ) . getRow ( modelRowIndex ) ) {
while ( transitionEntryIt - > getColumn ( ) ! = rewardEntry . getColumn ( ) ) {
STORM_LOG_ASSERT ( transitionEntryIt ! = model . getTransitionMatrix ( ) . getRow ( modelRowIndex ) . end ( ) , " The reward transition matrix is not a submatrix of the model transition matrix. " ) ;
+ + transitionEntryIt ;
}
uint64_t transitionId = transitionEntryIt - model . getTransitionMatrix ( ) . begin ( ) ;
uint64_t const & successorMemoryState = memorySuccessors [ transitionId * memoryStateCount + memoryState ] ;
builder . addNextValue ( resRowIndex , getResultState ( rewardEntry . getColumn ( ) , successorMemoryState ) , rewardEntry . getValue ( ) ) ;
}
}
}
}
@ -287,32 +457,32 @@ namespace storm {
}
transitionRewards = builder . build ( ) ;
}
result . insert ( std : : make_pair ( rewardModel . first , storm : : models : : sparse : : Standard RewardModel< Value Type> ( std : : move ( stateRewards ) , std : : move ( stateActionRewards ) , std : : move ( transitionRewards ) ) ) ) ;
result . insert ( std : : make_pair ( rewardModel . first , RewardModelType ( std : : move ( stateRewards ) , std : : move ( stateActionRewards ) , std : : move ( transitionRewards ) ) ) ) ;
}
return result ;
}
template < typename ValueType >
std : : shared_ptr < storm : : models : : sparse : : Model < ValueType > > SparseModelMemoryProduct < ValueType > : : buildResult ( storm : : storage : : SparseMatrix < ValueType > & & matrix , storm : : models : : sparse : : StateLabeling & & labeling , std : : unordered_map < std : : string , storm : : models : : sparse : : StandardRewardModel < ValueType > > & & rewardModels ) const {
storm : : storage : : sparse : : ModelComponents < ValueType , storm : : models : : sparse : : Standard RewardModel< Value Type> > components ( std : : move ( matrix ) , std : : move ( labeling ) , std : : move ( rewardModels ) ) ;
template < typename ValueType , typename RewardModelType >
std : : shared_ptr < storm : : models : : sparse : : Model < ValueType , RewardModelType > > SparseModelMemoryProduct < ValueType , RewardModel Type > : : buildResult ( storm : : storage : : SparseMatrix < ValueType > & & matrix , storm : : models : : sparse : : StateLabeling & & labeling , std : : unordered_map < std : : string , RewardModelType > & & rewardModels , boost : : optional < storm : : storage : : Scheduler < ValueType > > const & scheduler ) const {
storm : : storage : : sparse : : ModelComponents < ValueType , RewardModelType > components ( std : : move ( matrix ) , std : : move ( labeling ) , std : : move ( rewardModels ) ) ;
if ( model . isOfType ( storm : : models : : ModelType : : Ctmc ) ) {
components . rateTransitions = true ;
} else if ( model . isOfType ( storm : : models : : ModelType : : MarkovAutomaton ) ) {
// We also need to translate the exit rates and the Markovian states
uint_fast 64_t numResStates = components . transitionMatrix . getRowGroupCount ( ) ;
uint_fast 64_t memoryStateCount = memory . getNumberOfStates ( ) ;
uint64_t numResStates = components . transitionMatrix . getRowGroupCount ( ) ;
uint64_t memoryStateCount = memory . getNumberOfStates ( ) ;
std : : vector < ValueType > resultExitRates ;
resultExitRates . reserve ( components . transitionMatrix . getRowGroupCount ( ) ) ;
storm : : storage : : BitVector resultMarkovianStates ( numResStates , false ) ;
auto const & modelExitRates = dynamic_cast < storm : : models : : sparse : : MarkovAutomaton < ValueType > const & > ( model ) . getExitRates ( ) ;
auto const & modelMarkovianStates = dynamic_cast < storm : : models : : sparse : : MarkovAutomaton < ValueType > const & > ( model ) . getMarkovianStates ( ) ;
auto const & modelExitRates = dynamic_cast < storm : : models : : sparse : : MarkovAutomaton < ValueType , RewardModelType > const & > ( model ) . getExitRates ( ) ;
auto const & modelMarkovianStates = dynamic_cast < storm : : models : : sparse : : MarkovAutomaton < ValueType , RewardModelType > const & > ( model ) . getMarkovianStates ( ) ;
uint_fast 64_t stateIndex = 0 ;
uint64_t stateIndex = 0 ;
for ( auto const & resState : toResultStateMapping ) {
if ( resState < numResStates ) {
assert ( resState = = resultExitRates . size ( ) ) ;
uint_fast 64_t modelState = stateIndex / memoryStateCount ;
uint64_t modelState = stateIndex / memoryStateCount ;
resultExitRates . push_back ( modelExitRates [ modelState ] ) ;
if ( modelMarkovianStates . get ( modelState ) ) {
resultMarkovianStates . set ( resState , true ) ;
@ -324,12 +494,21 @@ namespace storm {
components . exitRates = std : : move ( resultExitRates ) ;
}
return storm : : utility : : builder : : buildModelFromComponents ( model . getType ( ) , std : : move ( components ) ) ;
storm : : models : : ModelType resultType = model . getType ( ) ;
if ( scheduler & & ! scheduler - > isPartialScheduler ( ) ) {
if ( model . isOfType ( storm : : models : : ModelType : : Mdp ) ) {
resultType = storm : : models : : ModelType : : Dtmc ;
}
// Note that converting deterministic MAs to CTMCs via state elimination does not preserve all properties (e.g. step bounded)
}
return storm : : utility : : builder : : buildModelFromComponents ( resultType , std : : move ( components ) ) ;
}
template class SparseModelMemoryProduct < double > ;
template class SparseModelMemoryProduct < storm : : RationalNumber > ;
template class SparseModelMemoryProduct < storm : : RationalFunction > ;
template class SparseModelMemoryProduct < double > ;
template class SparseModelMemoryProduct < double , storm : : models : : sparse : : StandardRewardModel < storm : : Interval > > ;
template class SparseModelMemoryProduct < storm : : RationalNumber > ;
template class SparseModelMemoryProduct < storm : : RationalFunction > ;
}
}