diff --git a/src/storm-pomdp/analysis/QualitativeAnalysis.cpp b/src/storm-pomdp/analysis/QualitativeAnalysis.cpp new file mode 100644 index 000000000..09e2cf496 --- /dev/null +++ b/src/storm-pomdp/analysis/QualitativeAnalysis.cpp @@ -0,0 +1,165 @@ +#include "storm-pomdp/analysis/QualitativeAnalysis.h" + +#include "storm/utility/macros.h" +#include "storm/utility/graph.h" +#include "storm/models/sparse/Pomdp.h" +#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" +#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" + +#include "storm/exceptions/InvalidPropertyException.h" +#include "storm/exceptions/NotImplementedException.h" + +namespace storm { + namespace analysis { + + template + QualitativeAnalysis::QualitativeAnalysis(storm::models::sparse::Pomdp const& pomdp) : pomdp(pomdp) { + // Intentionally left empty + } + + template + storm::storage::BitVector QualitativeAnalysis::analyseProb0(storm::logic::ProbabilityOperatorFormula const& formula) const { + return analyseProb0or1(formula, true); + } + + template + storm::storage::BitVector QualitativeAnalysis::analyseProb1(storm::logic::ProbabilityOperatorFormula const& formula) const { + return analyseProb0or1(formula, false); + } + + template + storm::storage::BitVector QualitativeAnalysis::analyseProb0or1(storm::logic::ProbabilityOperatorFormula const& formula, bool prob0) const { + // check whether the property is minimizing or maximizing + STORM_LOG_THROW(formula.hasOptimalityType() || formula.hasBound(), storm::exceptions::InvalidPropertyException, "The formula " << formula << " does not specify whether to minimize or maximize."); + bool minimizes = (formula.hasOptimalityType() && storm::solver::minimize(formula.getOptimalityType())) || (formula.hasBound() && storm::logic::isLowerBound(formula.getBound().comparisonType)); + + std::shared_ptr subformula = formula.getSubformula().asSharedPointer(); + // If necessary, convert the subformula to a more general case + if (subformula->isEventuallyFormula()) { + subformula = std::make_shared(storm::logic::Formula::getTrueFormula(), subformula->asEventuallyFormula().getSubformula().asSharedPointer()); + } + + if (subformula->isUntilFormula()) { + if (minimizes && prob0) { + return analyseProb0Min(subformula->asUntilFormula()); + } else if (minimizes && !prob0){ + return analyseProb1Min(subformula->asUntilFormula()); + } else if (!minimizes && prob0){ + return analyseProb0Max(subformula->asUntilFormula()); + } else if (!minimizes && !prob0){ + return analyseProb1Max(subformula->asUntilFormula()); + } + } + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Prob0or1 analysis is not supported for the property " << formula); + } + + + template + storm::storage::BitVector QualitativeAnalysis::analyseProb0Max(storm::logic::UntilFormula const& formula) const { + return storm::utility::graph::performProb0A(pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula())); + } + + template + storm::storage::BitVector QualitativeAnalysis::analyseProb0Min(storm::logic::UntilFormula const& formula) const { + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Prob0 analysis is currently not implemented for minimizing properties."); + } + + template + storm::storage::BitVector QualitativeAnalysis::analyseProb1Max(storm::logic::UntilFormula const& formula) const { + // We consider the states that satisfy the formula with prob.1 under arbitrary schedulers as goal states. + storm::storage::BitVector goalStates = storm::utility::graph::performProb1A(pomdp.getTransitionMatrix(), pomdp.getTransitionMatrix().getRowGroupIndices(), pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula())); + + // Now find a set of observations such that there is a memoryless scheduler inducing prob. 1 for each state whose observation is in the set. + storm::storage::BitVector candidateStates = goalStates | checkPropositionalFormula(formula.getLeftSubformula()); + storm::storage::BitVector candidateActions = pomdp.getTransitionMatrix().getRowFilter(candidateStates); + storm::storage::BitVector candidateObservations(pomdp.getNrObservations(), true); + + + bool converged = false; + while (!converged) { + converged = true; + + // Get the candidate states that can reach the goal with prob1 via candidate actions + storm::storage::BitVector newCandidates; + if (candidateActions.full()) { + newCandidates = storm::utility::graph::performProb1E(pomdp.getTransitionMatrix(), pomdp.getTransitionMatrix().getRowGroupIndices(), pomdp.getBackwardTransitions(), candidateStates, goalStates); + } else { + storm::storage::SparseMatrix filteredTransitions(pomdp.getTransitionMatrix().filterEntries(candidateActions)); + newCandidates = storm::utility::graph::performProb1E(filteredTransitions, filteredTransitions.getRowGroupIndices(), filteredTransitions.transpose(true), candidateStates, goalStates); + } + if (candidateStates != newCandidates) { + converged = false; + candidateStates = std::move(newCandidates); + } + + // Unselect all observations that have a non-candidate state + for (uint64_t state = candidateStates.getNextUnsetIndex(0); state < candidateStates.size(); state = candidateStates.getNextUnsetIndex(state + 1)) { + candidateObservations.set(pomdp.getObservation(state), false); + } + + // update the candidate actions to the set of actions that stay inside the candidate state set + std::vector candidateActionsPerObservation(pomdp.getNrObservations()); + for (auto const& state : candidateStates) { + auto& candidateActionsAtState = candidateActionsPerObservation[pomdp.getObservation(state)]; + if (candidateActionsAtState.size() == 0) { + candidateActionsAtState.resize(pomdp.getNumberOfChoices(state), true); + } + STORM_LOG_ASSERT(candidateActionsAtState.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(candidateActionsAtState.size()) + ")." ); + for (auto const& action : candidateActionsAtState) { + for (auto const& entry : pomdp.getTransitionMatrix().getRow(state, action)) { + if (!candidateStates.get(entry.getColumn())) { + candidateActionsAtState.set(action, false); + break; + } + } + } + } + + // Unselect all observations without such an action + for (auto const& o : candidateObservations) { + if (candidateActionsPerObservation[o].empty()) { + candidateObservations.set(o, false); + } + } + + // only keep the candidate states with a candidateObservation + for (auto const& state : candidateStates) { + if (!candidateObservations.get(pomdp.getObservation(state)) && !goalStates.get(state)) { + candidateStates.set(state, false); + converged = false; + } + } + + // Only keep the candidate actions originating from a candidateState. Also transform the representation of candidate actions + candidateActions.clear(); + for (auto const& state : candidateStates) { + uint64_t offset = pomdp.getTransitionMatrix().getRowGroupIndices()[state]; + for (auto const& action : candidateActionsPerObservation[pomdp.getObservation(state)]) { + candidateActions.set(offset + action); + } + } + } + + assert(goalStates.isSubsetOf(candidateStates)); + + return candidateStates; + + } + + template + storm::storage::BitVector QualitativeAnalysis::analyseProb1Min(storm::logic::UntilFormula const& formula) const { + return storm::utility::graph::performProb1A(pomdp.getTransitionMatrix(), pomdp.getTransitionMatrix().getRowGroupIndices(), pomdp.getBackwardTransitions(), checkPropositionalFormula(formula.getLeftSubformula()), checkPropositionalFormula(formula.getRightSubformula())); + } + + template + storm::storage::BitVector QualitativeAnalysis::checkPropositionalFormula(storm::logic::Formula const& propositionalFormula) const { + storm::modelchecker::SparsePropositionalModelChecker> mc(pomdp); + STORM_LOG_THROW(mc.canHandle(propositionalFormula), storm::exceptions::InvalidPropertyException, "Propositional model checker can not handle formula " << propositionalFormula); + return mc.check(propositionalFormula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); + } + + + template class QualitativeAnalysis; + + } +} \ No newline at end of file diff --git a/src/storm-pomdp/analysis/QualitativeAnalysis.h b/src/storm-pomdp/analysis/QualitativeAnalysis.h new file mode 100644 index 000000000..ac692e866 --- /dev/null +++ b/src/storm-pomdp/analysis/QualitativeAnalysis.h @@ -0,0 +1,27 @@ +#include "storm/models/sparse/Pomdp.h" +#include "storm/storage/BitVector.h" +#include "storm/logic/Formulas.h" +namespace storm { + namespace analysis { + template + class QualitativeAnalysis { + public: + + QualitativeAnalysis(storm::models::sparse::Pomdp const& pomdp); + storm::storage::BitVector analyseProb0(storm::logic::ProbabilityOperatorFormula const& formula) const; + storm::storage::BitVector analyseProb1(storm::logic::ProbabilityOperatorFormula const& formula) const; + + private: + storm::storage::BitVector analyseProb0or1(storm::logic::ProbabilityOperatorFormula const& formula, bool prob0) const; + storm::storage::BitVector analyseProb0Max(storm::logic::UntilFormula const& formula) const; + storm::storage::BitVector analyseProb0Min(storm::logic::UntilFormula const& formula) const; + storm::storage::BitVector analyseProb1Max(storm::logic::UntilFormula const& formula) const; + storm::storage::BitVector analyseProb1Min(storm::logic::UntilFormula const& formula) const; + + storm::storage::BitVector checkPropositionalFormula(storm::logic::Formula const& propositionalFormula) const; + + storm::models::sparse::Pomdp const& pomdp; + }; + } +} +