NondeterministicModel.h

Go to the documentation of this file.

#pragma once
 
#include "storm/models/sparse/Model.h"
#include "storm/storage/StateActionPair.h"
 
namespace storm {
 
// Forward declare Scheduler class.
namespace storage {
template<typename ValueType>
class Scheduler;
}
 
namespace models {
namespace sparse {
 
template<class ValueType, typename RewardModelType = StandardRewardModel<ValueType>>
class NondeterministicModel : public Model<ValueType, RewardModelType> {
   public:
    NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType> const& components);
    NondeterministicModel(ModelType modelType, storm::storage::sparse::ModelComponents<ValueType, RewardModelType>&& components);
 
    virtual ~NondeterministicModel() = default;
 
    std::vector<uint_fast64_t> const& getNondeterministicChoiceIndices() const;
 
    using Model<ValueType, RewardModelType>::getNumberOfChoices;
 
    uint_fast64_t getNumberOfChoices(uint_fast64_t state) const;
 
    virtual void reduceToStateBasedRewards() override;
 
    uint_fast64_t getChoiceIndex(storm::storage::StateActionPair const& stateactPair) const;
    std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> applyScheduler(storm::storage::Scheduler<ValueType> const& scheduler,
                                                                                             bool dropUnreachableStates = true,
                                                                                             bool preserveModelType = false) const;
 
    virtual void printModelInformationToStream(std::ostream& out) const override;
 
    virtual void writeDotToStream(std::ostream& outStream, size_t maxWidthLabel = 30, bool includeLabeling = true,
                                  storm::storage::BitVector const* subsystem = nullptr, std::vector<ValueType> const* firstValue = nullptr,
                                  std::vector<ValueType> const* secondValue = nullptr, std::vector<uint_fast64_t> const* stateColoring = nullptr,
                                  std::vector<std::string> const* colors = nullptr, std::vector<uint_fast64_t>* scheduler = nullptr,
                                  bool finalizeOutput = true) const override;
};
 
}  // namespace sparse
}  // namespace models
}  // namespace storm