diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h new file mode 100644 index 000000000..1037811d5 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h @@ -0,0 +1,37 @@ +#pragma once + +#include "storm/storage/dd/bisimulation/PartitionRefiner.h" + +namespace storm { + namespace dd { + namespace bisimulation { + + template + class MdpPartitionRefiner : public PartitionRefiner { + public: + MdpPartitionRefiner(storm::models::symbolic::Model const& model, Partition const& initialStatePartition); + + /*! + * Refines the partition. + * + * @param mode The signature mode to use. + * @return False iff the partition is stable and no refinement was actually performed. + */ + bool refine(bisimulation::SignatureMode const& mode = bisimulation::SignatureMode::Eager); + + /*! + * Retrieves the current choice partition in the refinement process. + */ + Partition const& getChoicePartition() const; + + private: + // The choice partition in the refinement process. + Partition choicePartition; + + // The object used to refine the choice partition based on the signatures. + SignatureRefiner choiceSignatureRefiner; + }; + + } + } +}