8namespace bisimulation {
10template<storm::dd::DdType DdType,
typename ValueType>
15 choicePartition(
Partition<
DdType, ValueType>::createTrivialChoicePartition(model, initialStatePartition.getBlockVariables())),
16 stateSignatureRefiner(model.getManager(), this->statePartition.getBlockVariable(), model.getRowVariables(), model.getColumnVariables(), true),
17 statePartitonHasBeenRefinedOnce(false) {
21 auto exitRateVector = this->model.template as<storm::models::symbolic::MarkovAutomaton<DdType, ValueType>>()->getExitRateVector();
26template<storm::dd::DdType DdType,
typename ValueType>
36 this->internalRefine(this->signatureComputer, this->signatureRefiner, this->choicePartition, this->statePartition, mode);
40 if (newChoicePartition.
getNumberOfBlocks() == choicePartition.getNumberOfBlocks() && statePartitonHasBeenRefinedOnce) {
44 this->choicePartition = newChoicePartition;
48 if (this->choicePartition.storedAsBdd()) {
49 choicePartitionAsBdd = this->choicePartition.asBdd();
51 choicePartitionAsBdd = this->choicePartition.asAdd().notZero();
54 auto signatureStart = std::chrono::high_resolution_clock::now();
56 auto signatureEnd = std::chrono::high_resolution_clock::now();
57 this->totalSignatureTime += (signatureEnd - signatureStart);
61 auto refinementStart = std::chrono::high_resolution_clock::now();
62 Partition<DdType, ValueType> newStatePartition = this->internalRefine(stateSignature, this->stateSignatureRefiner, this->statePartition);
63 statePartitonHasBeenRefinedOnce =
true;
64 auto refinementEnd = std::chrono::high_resolution_clock::now();
66 auto signatureTime = std::chrono::duration_cast<std::chrono::milliseconds>(signatureEnd - signatureStart).count();
67 auto refinementTime = std::chrono::duration_cast<std::chrono::milliseconds>(refinementEnd - refinementStart).count();
69 << (signatureTime + refinementTime) <<
"ms (signature: " << signatureTime <<
"ms, refinement: " << refinementTime
72 if (newStatePartition == this->statePartition) {
76 this->statePartition = newStatePartition;
82template<storm::dd::DdType DdType,
typename ValueType>
84 return choicePartition;
87template<storm::dd::DdType DdType,
typename ValueType>
91 if (newStatePartition == this->statePartition) {
94 this->statePartition = newStatePartition;
99template<storm::dd::DdType DdType,
typename ValueType>
102 Partition<DdType, ValueType> newChoicePartition = this->signatureRefiner.refine(this->choicePartition, Signature<DdType, ValueType>(stateActionRewards));
103 if (newChoicePartition == this->choicePartition) {
106 this->choicePartition = newChoicePartition;
111template class NondeterministicModelPartitionRefiner<storm::dd::DdType::CUDD, double>;
113template class NondeterministicModelPartitionRefiner<storm::dd::DdType::Sylvan, double>;
114template class NondeterministicModelPartitionRefiner<storm::dd::DdType::Sylvan, storm::RationalNumber>;
115template class NondeterministicModelPartitionRefiner<storm::dd::DdType::Sylvan, storm::RationalFunction>;
Bdd< LibraryType > existsAbstract(std::set< storm::expressions::Variable > const &metaVariables) const
Existentially abstracts from the given meta variables.
virtual bool refine(bisimulation::SignatureMode const &mode=bisimulation::SignatureMode::Eager) override
Refines the partition.
NondeterministicModelPartitionRefiner(storm::models::symbolic::NondeterministicModel< DdType, ValueType > const &model, Partition< DdType, ValueType > const &initialStatePartition)
Partition< DdType, ValueType > const & getChoicePartition() const
Retrieves the current choice partition in the refinement process.
uint64_t getNumberOfBlocks() const
Partition< DdType, ValueType > statePartition
bool isOfType(storm::models::ModelType const &modelType) const
Checks whether the model is of the given type.
Base class for all nondeterministic symbolic models.
#define STORM_LOG_INFO(message)
#define STORM_LOG_TRACE(message)