NonMarkovianChainTransformer.h

Go to the documentation of this file.

#pragma once
 
#include "storm/logic/Formula.h"
#include "storm/models/sparse/MarkovAutomaton.h"
 
namespace storm {
namespace transformer {
 
enum EliminationLabelBehavior { KeepLabels, ExtendLabels, MergeLabels, DeleteLabels };
 
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
class NonMarkovianChainTransformer {
   public:
    static std::shared_ptr<models::sparse::Model<ValueType, RewardModelType>> eliminateNonmarkovianStates(
        std::shared_ptr<models::sparse::MarkovAutomaton<ValueType, RewardModelType>> ma,
        EliminationLabelBehavior labelBehavior = EliminationLabelBehavior::KeepLabels);
 
    static bool preservesFormula(storm::logic::Formula const& formula);
 
    static std::vector<std::shared_ptr<storm::logic::Formula const>> checkAndTransformFormulas(
        std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
};
}  // namespace transformer
}  // namespace storm