NondeterministicModelPartitionRefiner.h

Go to the documentation of this file.

#pragma once
 
#include "storm/storage/dd/bisimulation/PartitionRefiner.h"
 
namespace storm {
namespace models {
namespace symbolic {
template<storm::dd::DdType DdType, typename ValueType>
class Mdp;
}
}  // namespace models
 
namespace dd {
namespace bisimulation {
 
template<storm::dd::DdType DdType, typename ValueType>
class NondeterministicModelPartitionRefiner : public PartitionRefiner<DdType, ValueType> {
   public:
    NondeterministicModelPartitionRefiner(storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model,
                                          Partition<DdType, ValueType> const& initialStatePartition);

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

    Partition<DdType, ValueType> const& getChoicePartition() const;
 
   private:
    virtual bool refineWrtStateActionRewards(storm::dd::Add<DdType, ValueType> const& stateActionRewards) override;
 
    virtual bool refineWrtStateRewards(storm::dd::Add<DdType, ValueType> const& stateRewards) override;

    storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model;

    Partition<DdType, ValueType> choicePartition;

    SignatureRefiner<DdType, ValueType> stateSignatureRefiner;

    bool statePartitonHasBeenRefinedOnce;
};
 
}  // namespace bisimulation
}  // namespace dd
}  // namespace storm