SparseParametricDtmcSimplifier.h

Go to the documentation of this file.

#pragma once
 
#include "storm-pars/transformer/SparseParametricModelSimplifier.h"
 
namespace storm {
namespace transformer {
 
template<typename SparseModelType>
class SparseParametricDtmcSimplifier : public SparseParametricModelSimplifier<SparseModelType> {
   public:
    SparseParametricDtmcSimplifier(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;
};
}  // namespace transformer
}  // namespace storm