PartitionRefiner.h

Go to the documentation of this file.

#pragma once
 
#include "storm/storage/dd/bisimulation/BisimulationOptions.h"
#include "storm/storage/dd/bisimulation/Partition.h"
#include "storm/storage/dd/bisimulation/Status.h"
 
#include "storm/storage/dd/bisimulation/SignatureComputer.h"
#include "storm/storage/dd/bisimulation/SignatureRefiner.h"
 
namespace storm {
namespace models {
namespace symbolic {
template<storm::dd::DdType DdType, typename ValueType>
class Model;
}
}  // namespace models
 
namespace dd {
namespace bisimulation {
 
template<storm::dd::DdType DdType, typename ValueType>
class PartitionRefiner {
   public:
    PartitionRefiner(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialStatePartition,
                     BisimulationOptions const& bisimulationOptions);
 
    virtual ~PartitionRefiner() = default;

    virtual bool refine(SignatureMode const& mode = SignatureMode::Eager);

    bool refineWrtRewardModel(storm::models::symbolic::StandardRewardModel<DdType, ValueType> const& rewardModel);

    Partition<DdType, ValueType> const& getStatePartition() const;

    Signature<DdType, ValueType> getFullSignature() const;

    Status getStatus() const;
 
    std::chrono::high_resolution_clock::duration getTotalSignatureTime() const;
    std::chrono::high_resolution_clock::duration getTotalRefinementTime() const;
 
   protected:
    Partition<DdType, ValueType> internalRefine(SignatureComputer<DdType, ValueType>& stateSignatureComputer,
                                                SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition,
                                                Partition<DdType, ValueType> const& targetPartition, SignatureMode const& mode = SignatureMode::Eager);
    Partition<DdType, ValueType> internalRefine(Signature<DdType, ValueType> const& signature, SignatureRefiner<DdType, ValueType>& signatureRefiner,
                                                Partition<DdType, ValueType> const& oldPartition);
 
    virtual bool refineWrtStateRewards(storm::dd::Add<DdType, ValueType> const& stateRewards);
    virtual bool refineWrtStateActionRewards(storm::dd::Add<DdType, ValueType> const& stateActionRewards);
 
    // 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<DdType, ValueType> statePartition;
 
    // The object used to compute the signatures.
    SignatureComputer<DdType, ValueType> signatureComputer;
 
    // The object used to refine the state partition based on the signatures.
    SignatureRefiner<DdType, ValueType> signatureRefiner;
 
    // Time measurements.
    std::chrono::high_resolution_clock::duration totalSignatureTime;
    std::chrono::high_resolution_clock::duration totalRefinementTime;
};
 
}  // namespace bisimulation
}  // namespace dd
}  // namespace storm