sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

rewardBounded/RewardUnfolding: Allowed the case that not all dimensions have a bound a priori.

tempestpy_adaptions
TimQu 6 years ago
parent
4ac23d630f
commit
1d5f2410b5
5 changed files with 53 additions and 19 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 9
      src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.cpp
  2. 3
      src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h
  3. 29
      src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
  4. 11
      src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h
  5. 20
      src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp

9
src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.cpp
View File

@ -186,6 +186,15 @@ namespace storm {
epoch |= (value << (dimension * bitsPerDimension));
}
void EpochManager::setDimensionOfEpochClass(EpochClass& epochClass, uint64_t const& dimension, bool const& setToBottom) const {
STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
if (setToBottom) {
epochClass |= (1 << dimension);
} else {
epochClass &= ~(1 << dimension);
}
}
bool EpochManager::isBottomDimension(Epoch const& epoch, uint64_t const& dimension) const {
STORM_LOG_ASSERT(dimensionCount > 0, "Invoked EpochManager with zero dimension count.");
return (epoch | (dimensionBitMask << (dimension * bitsPerDimension))) == epoch;

3
src/storm/modelchecker/prctl/helper/rewardbounded/EpochManager.h
View File

@ -13,7 +13,7 @@ namespace storm {
public:
typedef uint64_t Epoch; // The number of reward steps that are "left" for each dimension
typedef uint64_t EpochClass; // The number of reward steps that are "left" for each dimension
typedef uint64_t EpochClass; // Encodes the dimensions of an epoch that are bottom. Two epoch models within the same class have the same graph structure.
EpochManager();
EpochManager(uint64_t dimensionCount);
@ -40,6 +40,7 @@ namespace storm {
void setBottomDimension(Epoch& epoch, uint64_t const& dimension) const;
void setDimensionOfEpoch(Epoch& epoch, uint64_t const& dimension, uint64_t const& value) const; // assumes that the value is valid, i.e., small enough
void setDimensionOfEpochClass(EpochClass& epochClass, uint64_t const& dimension, bool const& setToBottom) const;
bool isBottomDimension(Epoch const& epoch, uint64_t const& dimension) const;
bool isBottomDimensionEpochClass(EpochClass const& epochClass, uint64_t const& dimension) const;

29
src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp
View File

@ -31,7 +31,7 @@ namespace storm {
}
template<typename ValueType, bool SingleObjectiveMode>
MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MultiDimensionalRewardUnfolding(storm::models::sparse::Model<ValueType> const& model, std::shared_ptr<storm::logic::OperatorFormula const> objectiveFormula) : model(model) {
MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MultiDimensionalRewardUnfolding(storm::models::sparse::Model<ValueType> const& model, std::shared_ptr<storm::logic::OperatorFormula const> objectiveFormula, std::function<void(std::vector<Epoch>&, EpochManager const&)> const& epochStepsCallback) : model(model) {
if (objectiveFormula->isProbabilityOperatorFormula()) {
if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) {
@ -53,18 +53,28 @@ namespace storm {
objective.considersComplementaryEvent = false;
objectives.push_back(std::move(objective));
initialize();
initialize(epochStepsCallback);
}
template<typename ValueType, bool SingleObjectiveMode>
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initialize() {
void MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::initialize(std::function<void(std::vector<Epoch>&, EpochManager const&)> const& epochStepsCallback) {
maxSolutionsStored = 0;
STORM_LOG_ASSERT(!SingleObjectiveMode || (this->objectives.size() == 1), "Enabled single objective mode but there are multiple objectives.");
std::vector<Epoch> epochSteps;
initializeObjectives(epochSteps);
if (epochStepsCallback) {
epochStepsCallback(epochSteps, epochManager);
}
// collect which epoch steps are possible
possibleEpochSteps.clear();
for (auto const& step : epochSteps) {
possibleEpochSteps.insert(step);
}
initializeMemoryProduct(epochSteps);
}
@ -186,12 +196,6 @@ namespace storm {
epochSteps.push_back(step);
}
// collect which epoch steps are possible
possibleEpochSteps.clear();
for (auto const& step : epochSteps) {
possibleEpochSteps.insert(step);
}
// Set the maximal values we need to consider for each dimension
computeMaxDimensionValues();
@ -247,13 +251,13 @@ namespace storm {
}
template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStartEpoch() {
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::Epoch MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getStartEpoch(bool setUnknownDimsToBottom) {
Epoch startEpoch = epochManager.getZeroEpoch();
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
if (dimensions[dim].isBounded) {
STORM_LOG_ASSERT(dimensions[dim].maxValue, "No max-value for dimension " << dim << " was given.");
if (dimensions[dim].isBounded && dimensions[dim].maxValue) {
epochManager.setDimensionOfEpoch(startEpoch, dim, dimensions[dim].maxValue.get());
} else {
STORM_LOG_THROW(setUnknownDimsToBottom || !dimensions[dim].isBounded, storm::exceptions::UnexpectedException, "Tried to obtain the start epoch although not all dimensions are known.");
epochManager.setBottomDimension(startEpoch, dim);
}
}
@ -799,7 +803,6 @@ namespace storm {
template<typename ValueType, bool SingleObjectiveMode>
typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::SolutionType const& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::getInitialStateResult(Epoch const& epoch, uint64_t initialStateIndex) {
STORM_LOG_ASSERT(model.getInitialStates().get(initialStateIndex), "The given model state is not an initial state.");
STORM_LOG_ASSERT(!epochManager.hasBottomDimension(epoch), "Tried to get the initial state result in an epoch that still contains at least one bottom dimension.");
return getStateSolution(epoch, productModel->getInitialProductState(initialStateIndex, model.getInitialStates()));
}

11
src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.h
View File

@ -36,11 +36,16 @@ namespace storm {
*
*/
MultiDimensionalRewardUnfolding(storm::models::sparse::Model<ValueType> const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives);
MultiDimensionalRewardUnfolding(storm::models::sparse::Model<ValueType> const& model, std::shared_ptr<storm::logic::OperatorFormula const> objectiveFormula);
MultiDimensionalRewardUnfolding(storm::models::sparse::Model<ValueType> const& model, std::shared_ptr<storm::logic::OperatorFormula const> objectiveFormula, std::function<void(std::vector<Epoch>&, EpochManager const&)> const& epochStepsCallback = nullptr);
~MultiDimensionalRewardUnfolding() = default;
Epoch getStartEpoch();
/*!
* Retrieves the desired epoch that needs to be analyzed to compute the reward bounded values.
* @param setUnknownDimsToBottom if true, dimensions for which no maxValue is known are set to the bottom dimension. If false, an exception is thrown if there are unknown maxValues.
*/
Epoch getStartEpoch(bool setUnknownDimsToBottom = false);
std::vector<Epoch> getEpochComputationOrder(Epoch const& startEpoch);
EpochModel<ValueType, SingleObjectiveMode>& setCurrentEpoch(Epoch const& epoch);
@ -68,7 +73,7 @@ namespace storm {
private:
void setCurrentEpochClass(Epoch const& epoch);
void initialize();
void initialize(std::function<void(std::vector<Epoch>&, EpochManager const&)> const& epochStepsCallback = nullptr);
void initializeObjectives(std::vector<Epoch>& epochSteps);
void computeMaxDimensionValues();

20
src/storm/modelchecker/prctl/helper/rewardbounded/ProductModel.cpp
View File

@ -458,10 +458,11 @@ namespace storm {
template<typename ValueType>
void ProductModel<ValueType>::collectReachableEpochClasses(std::set<EpochClass, std::function<bool(EpochClass const&, EpochClass const&)>>& reachableEpochClasses, std::set<Epoch> const& possibleSteps) const {
// Get the start epoch according to the given bounds.
// For dimensions for which no bound (aka. maxValue) is known, we will later overapproximate the set of reachable classes.
Epoch startEpoch = epochManager.getZeroEpoch();
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
if (dimensions[dim].isBounded) {
STORM_LOG_ASSERT(dimensions[dim].maxValue, "No max-value for dimension " << dim << " was given.");
if (dimensions[dim].maxValue) {
epochManager.setDimensionOfEpoch(startEpoch, dim, dimensions[dim].maxValue.get());
} else {
epochManager.setBottomDimension(startEpoch, dim);
@ -485,6 +486,21 @@ namespace storm {
}
}
}
// Also treat dimensions without a priori bound
for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
if (!dimensions[dim].maxValue) {
std::vector<EpochClass> newClasses;
for (auto const& c : reachableEpochClasses) {
auto newClass = c;
epochManager.setDimensionOfEpochClass(newClass, dim, false);
newClasses.push_back(newClass);
}
for (auto const& c: newClasses) {
reachableEpochClasses.insert(c);
}
}
}
}
template<typename ValueType>

Write Preview
Loading…
Cancel
Save