PrismProgramSimulator.h

Go to the documentation of this file.

#pragma once
 
#include "storm/generator/PrismNextStateGenerator.h"
#include "storm/storage/expressions/SimpleValuation.h"
#include "storm/storage/prism/Program.h"
#include "storm/utility/random.h"
 
namespace storm {
namespace simulator {
 
template<typename ValueType>
class DiscreteTimePrismProgramSimulator {
   public:
    DiscreteTimePrismProgramSimulator(storm::prism::Program const& program, storm::generator::NextStateGeneratorOptions const& options);
    void setSeed(uint64_t);
    std::vector<generator::Choice<ValueType, uint32_t>> const& getChoices() const;
 
    bool isSinkState() const;
 
    bool step(uint64_t actionNumber);
    std::vector<ValueType> const& getLastRewards() const;
    generator::CompressedState const& getCurrentState() const;
    expressions::SimpleValuation getCurrentStateAsValuation() const;
    std::vector<std::string> getCurrentStateLabelling() const;
 
    storm::json<ValueType> getStateAsJson() const;
 
    storm::json<ValueType> getObservationAsJson() const;
 
    std::string getCurrentStateString() const;
    bool resetToInitial();
 
    bool resetToState(generator::CompressedState const& compressedState);
 
    bool resetToState(expressions::SimpleValuation const& valuationState);
 
    std::vector<std::string> getRewardNames() const;
 
   protected:
    bool explore();
    void clearStateCaches();
    uint32_t getOrAddStateIndex(generator::CompressedState const&);
 
    storm::prism::Program const& program;
    generator::CompressedState currentState;
    std::shared_ptr<storm::generator::PrismNextStateGenerator<ValueType, uint32_t>> stateGenerator;
    generator::StateBehavior<ValueType> behavior;
    std::vector<ValueType> zeroRewards;
    std::vector<ValueType> lastActionRewards;
    storm::utility::RandomProbabilityGenerator<ValueType> generator;
    storm::storage::BitVectorHashMap<uint32_t> stateToId;
 
    std::unordered_map<uint32_t, generator::CompressedState> idToState;
 
   private:
    // Create a callback for the next-state generator to enable it to request the index of states.
    std::function<uint32_t(generator::CompressedState const&)> stateToIdCallback =
        std::bind(&DiscreteTimePrismProgramSimulator<ValueType>::getOrAddStateIndex, this, std::placeholders::_1);
};
}  // namespace simulator
}  // namespace storm