tempest/src/storm-pomdp/analysis/FormulaInformation.cpp

#include "storm-pomdp/analysis/FormulaInformation.h"
#include "storm/logic/Formulas.h"
#include "storm/logic/FragmentSpecification.h"
#include "storm/models/sparse/Pomdp.h"
#include "storm/models/sparse/StandardRewardModel.h"
#include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"

#include "storm/utility/macros.h"
#include "storm/exceptions/InvalidPropertyException.h"

namespace storm {
    namespace pomdp {
        namespace analysis {
            
            bool FormulaInformation::StateSet::empty() const {
                STORM_LOG_ASSERT(states.empty() == observations.empty(), "Inconsistent StateSet.");
                return observations.empty();
            }
            
            FormulaInformation::FormulaInformation() : type(Type::Unsupported) {
                // Intentionally left empty
            }
            
            FormulaInformation::FormulaInformation(Type const& type, storm::solver::OptimizationDirection const& dir, boost::optional<std::string> const& rewardModelName) : type(type), optimizationDirection(dir), rewardModelName(rewardModelName) {
                STORM_LOG_ASSERT(!this->rewardModelName.is_initialized() || this->type == Type::NonNestedExpectedRewardFormula, "Got a reward model name for a non-reward formula.");

            }
             
            FormulaInformation::Type const&  FormulaInformation::getType() const {
                return type;
            }
            
            bool  FormulaInformation::isNonNestedReachabilityProbability() const {
                return type == Type::NonNestedReachabilityProbability;
            }
            
            bool  FormulaInformation::isNonNestedExpectedRewardFormula() const {
                return type == Type::NonNestedExpectedRewardFormula;
            }
            
            bool  FormulaInformation::isUnsupported() const {
                return type == Type::Unsupported;
            }
            
            typename FormulaInformation::StateSet const& FormulaInformation::getTargetStates() const {
                STORM_LOG_ASSERT(this->type == Type::NonNestedExpectedRewardFormula || this->type == Type::NonNestedReachabilityProbability, "Target states requested for unexpected formula type.");
                return targetStates.get();
            }
             
            typename FormulaInformation::StateSet const& FormulaInformation::getSinkStates() const {
                STORM_LOG_ASSERT(this->type == Type::NonNestedReachabilityProbability, "Sink states requested for unexpected formula type.");
               return sinkStates.get();
            }
             
            std::string const& FormulaInformation::getRewardModelName() const {
                STORM_LOG_ASSERT(this->type == Type::NonNestedExpectedRewardFormula, "Reward model requested for unexpected formula type.");
                return rewardModelName.get();
            }
            
            storm::solver::OptimizationDirection const& FormulaInformation::getOptimizationDirection() const {
                return optimizationDirection;
            }
            
            bool FormulaInformation::minimize() const {
                return storm::solver::minimize(optimizationDirection);
            }
            
            bool FormulaInformation::maximize() const {
                return storm::solver::maximize(optimizationDirection);
            }
          
            template <typename PomdpType>
            FormulaInformation::StateSet getStateSet(PomdpType const& pomdp, storm::storage::BitVector&& inputStates) {
                FormulaInformation::StateSet result;
                result.states = std::move(inputStates);
                for (auto const& state : result.states) {
                    result.observations.insert(pomdp.getObservation(state));
                }
                // check if this set is observation-closed, i.e., whether there is a state outside of this set with one of the observations collected above
                result.observationClosed = true;
                for (uint64_t state = result.states.getNextUnsetIndex(0); state < result.states.size(); state = result.states.getNextUnsetIndex(state + 1)) {
                    if (result.observations.count(pomdp.getObservation(state)) > 0) {
                        result.observationClosed = false;
                        break;
                    }
                }
                return result;
            }
            
            template <typename PomdpType>
            void FormulaInformation::updateTargetStates(PomdpType const& pomdp, storm::storage::BitVector&& newTargetStates) {
                STORM_LOG_ASSERT(this->type == Type::NonNestedExpectedRewardFormula || this->type == Type::NonNestedReachabilityProbability, "Target states updated for unexpected formula type.");
                targetStates = getStateSet(pomdp, std::move(newTargetStates));
            }
            
            template <typename PomdpType>
            void FormulaInformation::updateSinkStates(PomdpType const& pomdp, storm::storage::BitVector&& newSinkStates) {
                STORM_LOG_ASSERT(this->type == Type::NonNestedReachabilityProbability, "Sink states requested for unexpected formula type.");
                sinkStates = getStateSet(pomdp, std::move(newSinkStates));
            }
            
            template <typename PomdpType>
            storm::storage::BitVector getStates(storm::logic::Formula const& propositionalFormula, bool formulaInverted, PomdpType const& pomdp) {
                storm::modelchecker::SparsePropositionalModelChecker<PomdpType> mc(pomdp);
                auto checkResult = mc.check(propositionalFormula);
                storm::storage::BitVector resultBitVector(checkResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
                if (formulaInverted) {
                    resultBitVector.complement();
                }
                return resultBitVector;
            }
            
            template <typename PomdpType>
            FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::ProbabilityOperatorFormula const& formula) {
                STORM_LOG_THROW(formula.hasOptimalityType(), storm::exceptions::InvalidPropertyException, "The property does not specify an optimization direction (min/max)");
                STORM_LOG_WARN_COND(!formula.hasBound(), "The probability threshold for the given property will be ignored.");
                auto const& subformula = formula.getSubformula();
                std::shared_ptr<storm::logic::Formula const> targetStatesFormula, constraintsStatesFormula;
                if (subformula.isEventuallyFormula()) {
                    targetStatesFormula = subformula.asEventuallyFormula().getSubformula().asSharedPointer();
                    constraintsStatesFormula = storm::logic::Formula::getTrueFormula()->asSharedPointer();
                } else if (subformula.isUntilFormula()) {
                    storm::logic::UntilFormula const &untilFormula = subformula.asUntilFormula();
                    targetStatesFormula = untilFormula.getRightSubformula().asSharedPointer();
                    constraintsStatesFormula = untilFormula.getLeftSubformula().asSharedPointer();
                }
                if (targetStatesFormula && targetStatesFormula->isInFragment(storm::logic::propositional()) && constraintsStatesFormula && constraintsStatesFormula->isInFragment(storm::logic::propositional())) {
                    FormulaInformation result(FormulaInformation::Type::NonNestedReachabilityProbability, formula.getOptimalityType());
                    result.updateTargetStates(pomdp, getStates(*targetStatesFormula, false, pomdp));
                    result.updateSinkStates(pomdp, getStates(*constraintsStatesFormula, true, pomdp));
                    return result;
                }
                return FormulaInformation();
            }
            
            template <typename PomdpType>
            FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::RewardOperatorFormula const& formula) {
                STORM_LOG_THROW(formula.hasOptimalityType(), storm::exceptions::InvalidPropertyException, "The property does not specify an optimization direction (min/max)");
                STORM_LOG_WARN_COND(formula.hasBound(), "The reward threshold for the given property will be ignored.");
                std::string rewardModelName = "";
                if (formula.hasRewardModelName()) {
                    rewardModelName = formula.getRewardModelName();
                    STORM_LOG_THROW(pomdp.hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException, "Selected reward model with name '" << rewardModelName << "' does not exist.");
                } else {
                    STORM_LOG_THROW(pomdp.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "Reward operator formula does not specify a reward model and the reward model is not unique.");
                    rewardModelName = pomdp.getUniqueRewardModelName();
                }
                auto const& subformula = formula.getSubformula();
                std::shared_ptr<storm::logic::Formula const> targetStatesFormula;
                if (subformula.isEventuallyFormula()) {
                    targetStatesFormula = subformula.asEventuallyFormula().getSubformula().asSharedPointer();
                }
                if (targetStatesFormula && targetStatesFormula->isInFragment(storm::logic::propositional())) {
                    FormulaInformation result(FormulaInformation::Type::NonNestedReachabilityProbability, formula.getOptimalityType(), rewardModelName);
                    result.updateTargetStates(pomdp, getStates(*targetStatesFormula, false, pomdp));
                    return result;
                }
                return FormulaInformation();
            }
            
            template <typename PomdpType>
            FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::Formula const& formula) {
                if (formula.isProbabilityOperatorFormula()) {
                    return getFormulaInformation(pomdp, formula.asProbabilityOperatorFormula());
                } else if (formula.isRewardOperatorFormula()) {
                    return getFormulaInformation(pomdp, formula.asRewardOperatorFormula());
                }
                return FormulaInformation();
            }
            
            template FormulaInformation getFormulaInformation<storm::models::sparse::Pomdp<double>>(storm::models::sparse::Pomdp<double> const& pomdp, storm::logic::Formula const& formula);
            template FormulaInformation getFormulaInformation<storm::models::sparse::Pomdp<storm::RationalNumber>>(storm::models::sparse::Pomdp<storm::RationalNumber> const& pomdp, storm::logic::Formula const& formula);
            
        }
    }
}