MarkovAutomaton.h

Go to the documentation of this file.

#pragma once
 
#include "storm/adapters/IntervalForward.h"
#include "storm/adapters/RationalFunctionForward.h"
#include "storm/adapters/RationalNumberForward.h"
#include "storm/models/sparse/Ctmc.h"
#include "storm/models/sparse/NondeterministicModel.h"
 
namespace storm {
namespace models {
namespace sparse {

template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
class MarkovAutomaton : public NondeterministicModel<ValueType, RewardModelType> {
   public:
    MarkovAutomaton(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
                    storm::storage::BitVector const& markovianStates,
                    std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());

    MarkovAutomaton(storm::storage::SparseMatrix<ValueType>&& transitionMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
                    storm::storage::BitVector&& markovianStates,
                    std::unordered_map<std::string, RewardModelType>&& rewardModels = std::unordered_map<std::string, RewardModelType>());

    MarkovAutomaton(storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components);
    MarkovAutomaton(storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components);
 
    MarkovAutomaton(MarkovAutomaton<ValueType, RewardModelType> const& other) = default;
    MarkovAutomaton& operator=(MarkovAutomaton<ValueType, RewardModelType> const& other) = default;
 
    MarkovAutomaton(MarkovAutomaton<ValueType, RewardModelType>&& other) = default;
    MarkovAutomaton& operator=(MarkovAutomaton<ValueType, RewardModelType>&& other) = default;

    bool isClosed() const;

    bool containsZenoCycle() const;

    bool isHybridState(storm::storage::sparse::state_type state) const;

    bool isMarkovianState(storm::storage::sparse::state_type state) const;

    bool isProbabilisticState(storm::storage::sparse::state_type state) const;

    std::vector<ValueType> const& getExitRates() const;

    std::vector<ValueType>& getExitRates();

    ValueType const& getExitRate(storm::storage::sparse::state_type state) const;

    ValueType getMaximalExitRate() const;

    storm::storage::BitVector const& getMarkovianStates() const;

    void close();

    bool isConvertibleToCtmc() const;
 
    bool hasOnlyTrivialNondeterminism() const;

    std::shared_ptr<storm::models::sparse::Ctmc<ValueType, RewardModelType>> convertToCtmc() const;
 
    virtual void printModelInformationToStream(std::ostream& out) const override;
 
   private:
    void turnRatesToProbabilities();

    bool checkIsClosed() const;

    bool checkContainsZenoCycle() const;
 
    // A bit vector representing the set of Markovian states.
    storm::storage::BitVector markovianStates;
 
    // A vector storing the exit rates of all states of the model.
    std::vector<ValueType> exitRates;
 
    // A flag indicating whether the Markov automaton has been closed, which is typically a prerequisite for model checking.
    bool closed;
 
    // A flag indicating whether the Markov automaton contains Zeno cycles.
    mutable boost::optional<bool> hasZenoCycle;
};
 
// Instantiated in MarkovAutomaton.cpp; prevents hidden consumers from duplicating the vtable/RTTI.
extern template class MarkovAutomaton<double>;
extern template class MarkovAutomaton<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
extern template class MarkovAutomaton<storm::RationalNumber>;
extern template class MarkovAutomaton<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>;
extern template class MarkovAutomaton<storm::Interval>;
extern template class MarkovAutomaton<storm::RationalInterval>;
extern template class MarkovAutomaton<storm::RationalFunction>;
 
}  // namespace sparse
}  // namespace models
}  // namespace storm