diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp index ff97961fe..1b1a5c895 100644 --- a/src/storm-pomdp-cli/storm-pomdp.cpp +++ b/src/storm-pomdp-cli/storm-pomdp.cpp @@ -49,15 +49,15 @@ namespace storm { auto const& pomdpSettings = storm::settings::getModule(); bool preprocessingPerformed = false; if (pomdpSettings.isSelfloopReductionSet()) { - bool apply = formulaInfo.isNonNestedReachabilityProbability() && formulaInfo.maximize(); - apply = apply || (formulaInfo.isNonNestedExpectedRewardFormula() && formulaInfo.minimize()); - if (apply) { + storm::transformer::GlobalPOMDPSelfLoopEliminator selfLoopEliminator(*pomdp); + if (selfLoopEliminator.preservesFormula(formula)) { STORM_PRINT_AND_LOG("Eliminating self-loop choices ..."); uint64_t oldChoiceCount = pomdp->getNumberOfChoices(); - storm::transformer::GlobalPOMDPSelfLoopEliminator 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 kpt = storm::pomdp::transformer::KnownProbabilityTransformer(); pomdp = kpt.transform(*pomdp, prob0States, prob1States); // Update formulaInfo to changes from Preprocessing diff --git a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp index b9e609218..32a4a843b 100644 --- a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.cpp +++ b/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 #include @@ -7,79 +9,92 @@ namespace storm { namespace transformer { + template + bool GlobalPOMDPSelfLoopEliminator::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 std::shared_ptr> GlobalPOMDPSelfLoopEliminator::transform() const { uint64_t nrStates = pomdp.getNumberOfStates(); - std::vector 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 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 cs(pomdp); auto res = cs.transform(filter)->template as>(); - res->setIsCanonic(); + + // The transformation preserves canonicity. + res->setIsCanonic(pomdp.isCanonic()); return res; } template class GlobalPOMDPSelfLoopEliminator; - - template - class GlobalPOMDPSelfLoopEliminator; + template class GlobalPOMDPSelfLoopEliminator; } } diff --git a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h b/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h index 6dec59124..3122a39ce 100644 --- a/src/storm-pomdp/transformer/GlobalPOMDPSelfLoopEliminator.h +++ b/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 @@ -14,6 +18,7 @@ namespace storm { } std::shared_ptr> transform() const; + bool preservesFormula(storm::logic::Formula const& formula) const; storm::models::sparse::Pomdp const& pomdp; }; }