Browse Source

Cleaner code and checks for GlobalPomdpSelfLoopEliminator

tempestpy_adaptions
Tim Quatmann 5 years ago
parent
commit
2ed1813b39
  1. 13
      src/storm-pomdp-cli/storm-pomdp.cpp
  2. 109
      src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp
  3. 5
      src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h

13
src/storm-pomdp-cli/storm-pomdp.cpp

@ -49,15 +49,15 @@ namespace storm {
auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
bool preprocessingPerformed = false;
if (pomdpSettings.isSelfloopReductionSet()) {
bool apply = formulaInfo.isNonNestedReachabilityProbability() && formulaInfo.maximize();
apply = apply || (formulaInfo.isNonNestedExpectedRewardFormula() && formulaInfo.minimize());
if (apply) {
storm::transformer::GlobalPOMDPSelfLoopEliminator<ValueType> selfLoopEliminator(*pomdp);
if (selfLoopEliminator.preservesFormula(formula)) {
STORM_PRINT_AND_LOG("Eliminating self-loop choices ...");
uint64_t oldChoiceCount = pomdp->getNumberOfChoices();
storm::transformer::GlobalPOMDPSelfLoopEliminator<ValueType> selfLoopEliminator(*pomdp);
pomdp = selfLoopEliminator.transform();
STORM_PRINT_AND_LOG(oldChoiceCount - pomdp->getNumberOfChoices() << " choices eliminated through self-loop elimination." << std::endl);
preprocessingPerformed = true;
} else {
STORM_PRINT_AND_LOG("Not eliminating self-loop choices as it does not preserve the formula." << std::endl);
}
}
if (pomdpSettings.isQualitativeReductionSet() && formulaInfo.isNonNestedReachabilityProbability()) {
@ -65,11 +65,10 @@ namespace storm {
STORM_PRINT_AND_LOG("Computing states with probability 0 ...");
storm::storage::BitVector prob0States = qualitativeAnalysis.analyseProb0(formula.asProbabilityOperatorFormula());
std::cout << prob0States << std::endl;
STORM_PRINT_AND_LOG(" done." << std::endl);
STORM_PRINT_AND_LOG(" done. " << prob0States.getNumberOfSetBits() << " states found." << std::endl);
STORM_PRINT_AND_LOG("Computing states with probability 1 ...");
storm::storage::BitVector prob1States = qualitativeAnalysis.analyseProb1(formula.asProbabilityOperatorFormula());
std::cout << prob1States << std::endl;
STORM_PRINT_AND_LOG(" done." << std::endl);
STORM_PRINT_AND_LOG(" done. " << prob1States.getNumberOfSetBits() << " states found." << std::endl);
storm::pomdp::transformer::KnownProbabilityTransformer<ValueType> kpt = storm::pomdp::transformer::KnownProbabilityTransformer<ValueType>();
pomdp = kpt.transform(*pomdp, prob0States, prob1States);
// Update formulaInfo to changes from Preprocessing

109
src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp

@ -1,5 +1,7 @@
#include "storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h"
#include "storm/storage/BitVector.h"
#include "storm/logic/Formulas.h"
#include "storm/logic/FragmentSpecification.h"
#include <vector>
#include <storm/transformer/ChoiceSelector.h>
@ -7,79 +9,92 @@ namespace storm {
namespace transformer {
template<typename ValueType>
bool GlobalPOMDPSelfLoopEliminator<ValueType>::preservesFormula(storm::logic::Formula const& formula) const {
if (formula.isOperatorFormula() && formula.asOperatorFormula().hasOptimalityType()) {
bool maxProb = formula.isProbabilityOperatorFormula() && storm::solver::maximize(formula.asOperatorFormula().getOptimalityType());
bool minRew = formula.isRewardOperatorFormula() && storm::solver::minimize(formula.asOperatorFormula().getOptimalityType());
auto const& subformula = formula.asOperatorFormula().getSubformula();
if (subformula.isEventuallyFormula()) {
if (subformula.asEventuallyFormula().getSubformula().isInFragment(storm::logic::propositional())) {
return maxProb || minRew;
}
} else if (subformula.isUntilFormula()) {
if (subformula.asUntilFormula().getLeftSubformula().isInFragment(storm::logic::propositional()) && subformula.asUntilFormula().getRightSubformula().isInFragment(storm::logic::propositional()) ) {
return maxProb;
}
}
}
return false;
}
template<typename ValueType>
std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> GlobalPOMDPSelfLoopEliminator<ValueType>::transform() const
{
uint64_t nrStates = pomdp.getNumberOfStates();
std::vector<storm::storage::BitVector> observationSelfLoopMasks;
for (uint64_t obs = 0; obs < pomdp.getNrObservations(); ++obs) {
observationSelfLoopMasks.push_back(storm::storage::BitVector(1, false));
assert(observationSelfLoopMasks.back().size() == 1);
}
assert(pomdp.getNrObservations() >= 1);
assert(observationSelfLoopMasks.size() == pomdp.getNrObservations());
// For each observation, get the choice indices that have a selfloop at every state with that observation
std::vector<storm::storage::BitVector> observationSelfLoopMasks(pomdp.getNrObservations());
for (uint64_t state = 0; state < nrStates; ++state) {
uint32_t observation = pomdp.getObservation(state);
assert(pomdp.getNumberOfChoices(state) != 0);
if (pomdp.getNumberOfChoices(state) == 1) {
continue;
STORM_LOG_ASSERT(observation < observationSelfLoopMasks.size(), "Observation index (" << observation << ") should be less than number of observations (" << observationSelfLoopMasks.size() << "). ");
auto& observationSelfLoopMask = observationSelfLoopMasks[observation];
// If we see this observation for the first time, add the corresponding amount of bits to the observation mask
if (observationSelfLoopMask.size() == 0) {
observationSelfLoopMask.resize(pomdp.getNumberOfChoices(state), true);
}
storm::storage::BitVector actionVector(pomdp.getNumberOfChoices(state), false);
for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) {
STORM_LOG_ASSERT(observationSelfLoopMask.size() == pomdp.getNumberOfChoices(state), "State " << state << " has " << pomdp.getNumberOfChoices(state) << " actions, different from other state(s) with same observation, which have " << observationSelfLoopMask.size() << " actions.");
// Iterate over all set bits in observationSelfLoopMask
// We use `getNextSetIndex` (instead of the more concise `for each`-syntax) to safely unset bits in the BitVector while iterating over it.
for (uint64_t localChoiceIndex = observationSelfLoopMask.getNextSetIndex(0); localChoiceIndex < observationSelfLoopMask.size(); localChoiceIndex = observationSelfLoopMask.getNextSetIndex(localChoiceIndex + 1)) {
// We just look at the first entry.
for (auto const& entry: pomdp.getTransitionMatrix().getRow(state, action)) {
if (storm::utility::isOne(entry.getValue()) && entry.getColumn() == state) {
actionVector.set(action);
}
break;
auto row = pomdp.getTransitionMatrix().getRow(state, localChoiceIndex);
STORM_LOG_ASSERT(row.getNumberOfEntries() > 0, "Unexpected empty row.");
if (row.getNumberOfEntries() > 1 || row.begin()->getColumn() != state) {
observationSelfLoopMask.set(localChoiceIndex, false);
}
}
}
STORM_LOG_ASSERT(observation < observationSelfLoopMasks.size(), "Observation index (" << observation << ") should be less than number of observations (" << observationSelfLoopMasks.size() << "). ");
if (observationSelfLoopMasks[observation].size() == 1) {
observationSelfLoopMasks[observation] = actionVector;
} else {
STORM_LOG_ASSERT(observationSelfLoopMasks[observation].size() == pomdp.getNumberOfChoices(state), "State " + std::to_string(state) + " has " + std::to_string(pomdp.getNumberOfChoices(state)) + " actions, different from other with same observation (" + std::to_string(observationSelfLoopMasks[observation].size()) + ")." );
observationSelfLoopMasks[observation] &= actionVector;
// For each observation, make sure that we keep at least one choice
for (auto & obsMask : observationSelfLoopMasks) {
if (obsMask.size() > 0 && obsMask.full()) {
obsMask.set(0, false);
}
}
storm::storage::BitVector filter(pomdp.getNumberOfChoices(), false);
// Finally create a filter that is 1 for every choice we can keep.
storm::storage::BitVector filter(pomdp.getNumberOfChoices(), true);
uint64_t offset = 0;
for (uint64_t state = 0; state < nrStates; ++state) {
uint32_t observation = pomdp.getObservation(state);
storm::storage::BitVector& vec = observationSelfLoopMasks[observation];
if (vec.full()) {
vec.set(0, false);
}
assert(!vec.full());
// std::cout << "state " << state << " vec " << vec << std::endl;
for (uint64_t action = 0; action < pomdp.getNumberOfChoices(state); ++action) {
if (vec.get(action)) {
filter.set(offset + action);
}
storm::storage::BitVector& observationSelfLoopMask = observationSelfLoopMasks[pomdp.getObservation(state)];
assert(!observationSelfLoopMask.full());
for (auto const& localChoiceIndex : observationSelfLoopMask) {
filter.set(offset + localChoiceIndex, false);
}
offset += pomdp.getNumberOfChoices(state);
}
// std::cout << "filter: " << filter << std::endl;
assert(filter.size() == pomdp.getNumberOfChoices());
// TODO rewards with state-action rewards
filter.complement();
// std::cout << "selection: " << filter << std::endl;
std::cout << "Filter: " << filter << std::endl;
// We do not consider rewards right now, since this reduction only preserves maximizing probabilities and minimizing expected rewards, anyway.
// In both cases, the reward at a selfloop has no effect (assuming not reaching goal means infinite reward)
STORM_LOG_INFO("Selfloop reduction eliminates " << (filter.size() - filter.getNumberOfSetBits()) << " choices.");
ChoiceSelector<ValueType> cs(pomdp);
auto res = cs.transform(filter)->template as<storm::models::sparse::Pomdp<ValueType>>();
res->setIsCanonic();
// The transformation preserves canonicity.
res->setIsCanonic(pomdp.isCanonic());
return res;
}
template class GlobalPOMDPSelfLoopEliminator<storm::RationalNumber>;
template
class GlobalPOMDPSelfLoopEliminator<double>;
template class GlobalPOMDPSelfLoopEliminator<double>;
}
}

5
src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h

@ -3,6 +3,10 @@
#include "storm/models/sparse/Pomdp.h"
namespace storm {
namespace logic {
class Formula;
}
namespace transformer {
template<typename ValueType>
@ -14,6 +18,7 @@ namespace storm {
}
std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> transform() const;
bool preservesFormula(storm::logic::Formula const& formula) const;
storm::models::sparse::Pomdp<ValueType> const& pomdp;
};
}
Loading…
Cancel
Save