SparseParametricModelSimplifier.h

Go to the documentation of this file.

#pragma once
 
#include <boost/optional.hpp>
#include <memory>
#include <optional>
#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);
 
    /*
     * 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;

    void setPreserveParametricTransitions(bool preserveParametricTransitions);

    bool isPreserveParametricTransitionsSet() const;
 
   private:
    SparseModelType const& originalModel;
 
    std::shared_ptr<SparseModelType> simplifiedModel;
    std::shared_ptr<storm::logic::Formula const> simplifiedFormula;
    bool preserveParametricTransitions = false;
};
}  // namespace transformer
}  // namespace storm