27 : type(type), optimizationDirection(dir), rewardModelName(rewardModelName) {
30 "Got a reward model name for a non-reward formula.");
55 "Target states requested for unexpected formula type.");
56 return targetStates.value();
61 return sinkStates.value();
66 "Reward model requested for unexpected formula type.");
67 return rewardModelName.value();
71 return optimizationDirection;
82template<
typename PomdpType>
85 result.
states = std::move(inputStates);
86 for (
auto const state : result.
states) {
92 if (result.
observations.count(pomdp.getObservation(state)) > 0) {
100template<
typename PomdpType>
103 "Target states updated for unexpected formula type.");
104 targetStates =
getStateSet(pomdp, std::move(newTargetStates));
107template<
typename PomdpType>
110 sinkStates =
getStateSet(pomdp, std::move(newSinkStates));
113template<
typename PomdpType>
116 auto checkResult = mc.
check(propositionalFormula);
118 if (formulaInverted) {
121 return resultBitVector;
124template<
typename PomdpType>
127 "The property does not specify an optimization direction (min/max)");
130 std::shared_ptr<storm::logic::Formula const> targetStatesFormula, constraintsStatesFormula;
131 if (subformula.isEventuallyFormula()) {
134 }
else if (subformula.isUntilFormula()) {
149template<
typename PomdpType>
152 "The property does not specify an optimization direction (min/max)");
154 std::string rewardModelName =
"";
157 STORM_LOG_THROW(pomdp.hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException,
158 "Selected reward model with name '" << rewardModelName <<
"' does not exist.");
160 STORM_LOG_THROW(pomdp.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException,
161 "Reward operator formula does not specify a reward model and the reward model is not unique.");
162 rewardModelName = pomdp.getUniqueRewardModelName();
165 std::shared_ptr<storm::logic::Formula const> targetStatesFormula;
166 if (subformula.isEventuallyFormula()) {
177template<
typename PomdpType>
193template void FormulaInformation::updateTargetStates<storm::models::sparse::Pomdp<storm::RationalNumber>>(
195template void FormulaInformation::updateSinkStates<storm::models::sparse::Pomdp<storm::RationalNumber>>(
197template FormulaInformation getFormulaInformation<storm::models::sparse::Pomdp<storm::RationalNumber>>(
virtual std::unique_ptr< CheckResult > check(Environment const &env, CheckTask< storm::logic::Formula, SolutionType > const &checkTask)
Checks the provided formula.
This class represents a partially observable Markov decision process.
A bit vector that is internally represented as a vector of 64-bit values.
void complement()
Negates all bits in the bit vector.
bool empty() const
Retrieves whether no bits are set to true in this bit vector.
uint64_t getNextUnsetIndex(uint64_t startingIndex) const
Retrieves the index of the bit that is the next bit set to false in the bit vector.
size_t size() const
Retrieves the number of bits this bit vector can store.
#define STORM_LOG_ASSERT(cond, message)
#define STORM_LOG_WARN_COND(cond, message)
#define STORM_LOG_THROW(cond, exception, message)
FragmentSpecification propositional()
storm::storage::BitVector getStates(storm::logic::Formula const &propositionalFormula, bool formulaInverted, PomdpType const &pomdp)
FormulaInformation::StateSet getStateSet(PomdpType const &pomdp, storm::storage::BitVector &&inputStates)
FormulaInformation getFormulaInformation(PomdpType const &pomdp, storm::logic::ProbabilityOperatorFormula const &formula)
bool constexpr maximize(OptimizationDirection d)
bool constexpr minimize(OptimizationDirection d)