SparseParametricMdpSimplifier.h

Go to the documentation of this file.

#pragma once
 
#include "storm-pars/transformer/SparseParametricModelSimplifier.h"
 
namespace storm {
namespace transformer {
 
template<typename SparseModelType>
class SparseParametricMdpSimplifier : public SparseParametricModelSimplifier<SparseModelType> {
   public:
    SparseParametricMdpSimplifier(SparseModelType const& model);
 
   protected:
    // Perform the simplification for the corresponding formula type
    virtual bool simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override;
    virtual bool simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula) override;
    virtual bool simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula) override;
    virtual bool simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula) override;
 
    static std::shared_ptr<SparseModelType> eliminateNeutralEndComponents(SparseModelType const& model, storm::storage::BitVector const& ignoredStates,
                                                                          boost::optional<std::string> const& rewardModelName = boost::none);
};
}  // namespace transformer
}  // namespace storm