Scheduler.h

Go to the documentation of this file.

#pragma once
 
#include <cstdint>
#include "storm/storage/BitVector.h"
#include "storm/storage/SchedulerChoice.h"
#include "storm/storage/memorystructure/MemoryStructure.h"
 
namespace storm {
 
namespace storage {

template<typename ValueType>
class Scheduler {
   public:
    Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure> const& memoryStructure = boost::none);
    Scheduler(uint_fast64_t numberOfModelStates, boost::optional<storm::storage::MemoryStructure>&& memoryStructure);

    void setChoice(SchedulerChoice<ValueType> const& choice, uint_fast64_t modelState, uint_fast64_t memoryState = 0);

    bool isChoiceSelected(BitVector const& selectedStates, uint64_t memoryState = 0) const;

    bool isChoiceSelected(uint64_t modelState, uint64_t memoryState = 0) const;

    void clearChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0);

    SchedulerChoice<ValueType> const& getChoice(uint_fast64_t modelState, uint_fast64_t memoryState = 0) const;

    void setDontCare(uint_fast64_t modelState, uint_fast64_t memoryState = 0, bool setArbitraryChoice = true);

    void unSetDontCare(uint_fast64_t modelState, uint_fast64_t memoryState = 0);

    bool isDontCare(uint_fast64_t modelState, uint64_t memoryState = 0) const;

    storm::storage::BitVector computeActionSupport(std::vector<uint64_t> const& nondeterministicChoiceIndicies) const;

    bool isPartialScheduler() const;

    bool isDeterministicScheduler() const;

    bool isMemorylessScheduler() const;

    uint_fast64_t getNumberOfMemoryStates() const;
    uint_fast64_t getNumberOfModelStates() const;

    boost::optional<storm::storage::MemoryStructure> const& getMemoryStructure() const;

    Scheduler<ValueType> getMemorylessSchedulerForMemoryState(uint64_t memoryState = 0) const;

    template<typename NewValueType>
    Scheduler<NewValueType> toValueType() const {
        uint_fast64_t numModelStates = schedulerChoices.front().size();
        Scheduler<NewValueType> newScheduler(numModelStates, memoryStructure);
        for (uint_fast64_t memState = 0; memState < this->getNumberOfMemoryStates(); ++memState) {
            for (uint_fast64_t modelState = 0; modelState < numModelStates; ++modelState) {
                newScheduler.setChoice(getChoice(modelState, memState).template toValueType<NewValueType>(), modelState, memState);
            }
        }
        return newScheduler;
    }

    void printToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false,
                       bool skipDontCareStates = false) const;

    void printJsonToStream(std::ostream& out, std::shared_ptr<storm::models::sparse::Model<ValueType>> model = nullptr, bool skipUniqueChoices = false,
                           bool skipDontCareStates = false) const;
 
   private:
    boost::optional<storm::storage::MemoryStructure> memoryStructure;
    std::vector<std::vector<SchedulerChoice<ValueType>>> schedulerChoices;
    std::vector<storm::storage::BitVector> dontCareStates;
    uint_fast64_t numOfUndefinedChoices;
    uint_fast64_t numOfDeterministicChoices;
    uint_fast64_t numOfDontCareStates;
};
}  // namespace storage
}  // namespace storm