Browse Source

backbone for a simulator on top of explicit state models

tempestpy_adaptions
Sebastian Junges 5 years ago
parent
commit
1ef92dee9e
  1. 50
      src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp
  2. 30
      src/storm/simulator/DiscreteTimeSparseModelSimulator.h
  3. 24
      src/storm/utility/random.cpp
  4. 29
      src/storm/utility/random.h

50
src/storm/simulator/DiscreteTimeSparseModelSimulator.cpp

@ -0,0 +1,50 @@
#include "storm/simulator/DiscreteTimeSparseModelSimulator.h"
#include "storm/models/sparse/Model.h"
namespace storm {
namespace simulator {
template<typename ValueType, typename RewardModelType>
DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::DiscreteTimeSparseModelSimulator(storm::models::sparse::Model<ValueType, RewardModelType> const& model) : model(model), currentState(*model.getInitialStates().begin()) {
STORM_LOG_WARN_COND(model.getInitialStates().getNumberOfSetBits()==1, "The model has multiple initial states. This simulator assumes it starts from the initial state with the lowest index.");
}
template<typename ValueType, typename RewardModelType>
void DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::setSeed(uint64_t seed) {
generator = storm::utility::RandomProbabilityGenerator<double>(seed);
}
template<typename ValueType, typename RewardModelType>
bool DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::step(uint64_t action) {
// TODO lots of optimization potential.
// E.g., do not sample random numbers if there is only a single transition
ValueType probability = generator.random();
STORM_LOG_ASSERT(action < model.getTransitionMatrix().getRowGroupSize(currentState), "Action index higher than number of actions");
uint64_t row = model.getTransitionMatrix().getRowGroupIndices()[currentState] + action;
ValueType sum = storm::utility::zero<ValueType>();
for (auto const& entry : model.getTransitionMatrix().getRow(row)) {
sum += entry.getValue();
if (sum >= probability) {
currentState = entry.getColumn();
return true;
}
}
return false;
STORM_LOG_ASSERT(false, "This position should never be reached");
}
template<typename ValueType, typename RewardModelType>
uint64_t DiscreteTimeSparseModelSimulator<ValueType, RewardModelType>::getCurrentState() const {
return currentState;
}
template<typename ValueType, typename RewardModelType>
bool DiscreteTimeSparseModelSimulator<ValueType,RewardModelType>::resetToInitial() {
currentState = *model.getInitialStates().begin();
return true;
}
template class DiscreteTimeSparseModelSimulator<double>;
}
}

30
src/storm/simulator/DiscreteTimeSparseModelSimulator.h

@ -0,0 +1,30 @@
#include <cstdint>
#include "storm/models/sparse/Model.h"
#include "storm/utility/random.h"
namespace storm {
namespace simulator {
/**
* This class is a low-level interface to quickly sample from Discrete-Time Models
* stored explicitly as a SparseModel.
* Additional information about state, actions, should be obtained via the model itself.
*
* TODO: It may be nice to write a CPP wrapper that does not require to actually obtain such informations yourself.
* @tparam ModelType
*/
template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
class DiscreteTimeSparseModelSimulator {
public:
DiscreteTimeSparseModelSimulator(storm::models::sparse::Model<ValueType, RewardModelType> const& model);
void setSeed(uint64_t);
bool step(uint64_t action);
uint64_t getCurrentState() const;
bool resetToInitial();
protected:
uint64_t currentState;
storm::models::sparse::Model<ValueType, RewardModelType> const& model;
storm::utility::RandomProbabilityGenerator<ValueType> generator;
};
}
}

24
src/storm/utility/random.cpp

@ -0,0 +1,24 @@
#include "storm/utility/random.h"
namespace storm {
namespace utility {
RandomProbabilityGenerator<double>::RandomProbabilityGenerator()
: distribution(0.0, 1.0)
{
std::random_device rd;
engine = std::mt19937(rd());
}
RandomProbabilityGenerator<double>::RandomProbabilityGenerator(uint64_t seed)
: engine(seed), distribution(0.0, 1.0)
{
}
double RandomProbabilityGenerator<double>::random() {
return distribution(engine);
}
}
}

29
src/storm/utility/random.h

@ -0,0 +1,29 @@
#include <random>
namespace storm {
namespace utility {
template<typename ValueType>
class RandomProbabilityGenerator {
public:
RandomProbabilityGenerator();
RandomProbabilityGenerator(uint64_t seed);
ValueType random() const;
};
template<>
class RandomProbabilityGenerator<double> {
public:
RandomProbabilityGenerator();
RandomProbabilityGenerator(uint64_t seed);
double random();
private:
std::uniform_real_distribution<double> distribution;
std::mt19937 engine;
};
}
}
Loading…
Cancel
Save