|
|
@ -51,19 +51,21 @@ namespace storm { |
|
|
|
|
|
|
|
template<typename ValueType, typename RewardModelType> |
|
|
|
std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> NondeterministicModel<ValueType, RewardModelType>::applyScheduler(storm::storage::Scheduler<ValueType> const& scheduler, bool dropUnreachableStates) { |
|
|
|
boost::optional<storm::storage::SparseModelMemoryProduct<ValueType>> memoryProduct; |
|
|
|
if (scheduler.isMemorylessScheduler()) { |
|
|
|
storm::storage::MemoryStructure memStruct = storm::storage::MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(*this); |
|
|
|
memoryProduct = memStruct.product(*this); |
|
|
|
auto memoryProduct = storm::storage::MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(*this).product(*this); |
|
|
|
if (!dropUnreachableStates) { |
|
|
|
memoryProduct.setBuildFullProduct(); |
|
|
|
} |
|
|
|
return memoryProduct.build(scheduler); |
|
|
|
} else { |
|
|
|
boost::optional<storm::storage::MemoryStructure> const& memStruct = scheduler.getMemoryStructure(); |
|
|
|
STORM_LOG_ASSERT(memStruct, "Memoryless scheduler without memory structure."); |
|
|
|
memoryProduct = memStruct->product(*this); |
|
|
|
} |
|
|
|
if (!dropUnreachableStates) { |
|
|
|
memoryProduct->setBuildFullProduct(); |
|
|
|
auto memoryProduct = memStruct->product(*this); |
|
|
|
if (!dropUnreachableStates) { |
|
|
|
memoryProduct.setBuildFullProduct(); |
|
|
|
} |
|
|
|
return memoryProduct.build(scheduler); |
|
|
|
} |
|
|
|
return memoryProduct->build(scheduler); |
|
|
|
} |
|
|
|
|
|
|
|
template<typename ValueType, typename RewardModelType> |
|
|
|