SparseParametricModelSimplifier.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <memory>
#include <string>
 
#include "storm/logic/Formulas.h"
#include "storm/storage/BitVector.h"
 
namespace storm {
namespace transformer {
 
template<typename SparseModelType>
class SparseParametricModelSimplifier {
   public:
    SparseParametricModelSimplifier(SparseModelType const& model);
    virtual ~SparseParametricModelSimplifier() = default;
 
    /*
     * Invokes the simplification of the model w.r.t. the given formula.
     * Returns true, iff simplification was successful
     */
    bool simplify(storm::logic::Formula const& formula);
 
    /*
     * Retrieves the simplified model.
     * Note that simplify(formula) needs to be called first and has to return true. Otherwise an exception is thrown
     */
    std::shared_ptr<SparseModelType> getSimplifiedModel() const;
 
    /*
     * Retrieves the simplified formula.
     * Note that simplify(formula) needs to be called first and has to return true. Otherwise an exception is thrown
     */
    std::shared_ptr<storm::logic::Formula const> getSimplifiedFormula() const;
 
   protected:
    // Perform the simplification for the corresponding formula type
    virtual bool simplifyForUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula);
    virtual bool simplifyForReachabilityProbabilities(storm::logic::ProbabilityOperatorFormula const& formula);
    virtual bool simplifyForBoundedUntilProbabilities(storm::logic::ProbabilityOperatorFormula const& formula);
    virtual bool simplifyForReachabilityRewards(storm::logic::RewardOperatorFormula const& formula);
    virtual bool simplifyForCumulativeRewards(storm::logic::RewardOperatorFormula const& formula);
 
    static std::shared_ptr<SparseModelType> eliminateConstantDeterministicStates(SparseModelType const& model,
                                                                                 storm::storage::BitVector const& consideredStates,
                                                                                 boost::optional<std::string> const& rewardModelName = boost::none);
 
    SparseModelType const& originalModel;
 
    std::shared_ptr<SparseModelType> simplifiedModel;
    std::shared_ptr<storm::logic::Formula const> simplifiedFormula;
};
}  // namespace transformer
}  // namespace storm