diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h new file mode 100644 index 000000000..413889300 --- /dev/null +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -0,0 +1,66 @@ +#pragma once + +#include "storm/storage/dd/bisimulation/Status.h" +#include "storm/storage/dd/bisimulation/Partition.h" + +#include "storm/storage/dd/bisimulation/SignatureComputer.h" +#include "storm/storage/dd/bisimulation/SignatureRefiner.h" + +namespace storm { + namespace models { + namespace symbolic { + template + class Model; + } + } + + namespace dd { + namespace bisimulation { + + template + class PartitionRefiner { + public: + PartitionRefiner(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 state partition in the refinement process. + */ + Partition const& getStatePartition() const; + + /*! + * Retrieves the status of the refinement process. + */ + Status getStatus() const; + + private: + // The current status. + Status status; + + // The number of refinements that were made. + uint64_t refinements; + + // The state partition in the refinement process. Initially set to the initial partition. + Partition statePartition; + + // The object used to compute the signatures. + SignatureComputer signatureComputer; + + // The object used to refine the partition(s) based on the signatures. + SignatureRefiner signatureRefiner; + + // Time measurements. + std::chrono::high_resolution_clock::duration totalSignatureTime; + std::chrono::high_resolution_clock::duration totalRefinementTime; + }; + + } + } +}