Storm 1.11.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
FormulaInformation.cpp
Go to the documentation of this file.
9
12
13namespace storm {
14namespace pomdp {
15namespace analysis {
16
18 STORM_LOG_ASSERT(states.empty() == observations.empty(), "Inconsistent StateSet.");
19 return observations.empty();
20}
21
23 // Intentionally left empty
24}
25
26FormulaInformation::FormulaInformation(Type const& type, storm::solver::OptimizationDirection const& dir, std::optional<std::string> const& rewardModelName)
27 : type(type), optimizationDirection(dir), rewardModelName(rewardModelName) {
29 !this->rewardModelName.has_value() || this->type == Type::NonNestedExpectedRewardFormula || this->type == Type::DiscountedTotalRewardFormula,
30 "Got a reward model name for a non-reward formula.");
31}
32
34 return type;
35}
36
40
44
48
50 return type == Type::Unsupported;
51}
52
55 "Target states requested for unexpected formula type.");
56 return targetStates.value();
57}
58
60 STORM_LOG_ASSERT(this->type == Type::NonNestedReachabilityProbability, "Sink states requested for unexpected formula type.");
61 return sinkStates.value();
62}
63
64std::string const& FormulaInformation::getRewardModelName() const {
66 "Reward model requested for unexpected formula type.");
67 return rewardModelName.value();
68}
69
71 return optimizationDirection;
72}
73
75 return storm::solver::minimize(optimizationDirection);
76}
77
79 return storm::solver::maximize(optimizationDirection);
80}
81
82template<typename PomdpType>
85 result.states = std::move(inputStates);
86 for (auto const state : result.states) {
87 result.observations.insert(pomdp.getObservation(state));
88 }
89 // 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
90 result.observationClosed = true;
91 for (uint64_t state = result.states.getNextUnsetIndex(0); state < result.states.size(); state = result.states.getNextUnsetIndex(state + 1)) {
92 if (result.observations.count(pomdp.getObservation(state)) > 0) {
93 result.observationClosed = false;
94 break;
95 }
96 }
97 return result;
98}
99
100template<typename PomdpType>
101void FormulaInformation::updateTargetStates(PomdpType const& pomdp, storm::storage::BitVector&& newTargetStates) {
103 "Target states updated for unexpected formula type.");
104 targetStates = getStateSet(pomdp, std::move(newTargetStates));
105}
106
107template<typename PomdpType>
108void FormulaInformation::updateSinkStates(PomdpType const& pomdp, storm::storage::BitVector&& newSinkStates) {
109 STORM_LOG_ASSERT(this->type == Type::NonNestedReachabilityProbability, "Sink states requested for unexpected formula type.");
110 sinkStates = getStateSet(pomdp, std::move(newSinkStates));
111}
112
113template<typename PomdpType>
114storm::storage::BitVector getStates(storm::logic::Formula const& propositionalFormula, bool formulaInverted, PomdpType const& pomdp) {
116 auto checkResult = mc.check(propositionalFormula);
117 storm::storage::BitVector resultBitVector(checkResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
118 if (formulaInverted) {
119 resultBitVector.complement();
120 }
121 return resultBitVector;
122}
123
124template<typename PomdpType>
126 STORM_LOG_THROW(formula.hasOptimalityType(), storm::exceptions::InvalidPropertyException,
127 "The property does not specify an optimization direction (min/max)");
128 STORM_LOG_WARN_COND(!formula.hasBound(), "The probability threshold for the given property will be ignored.");
129 auto const& subformula = formula.getSubformula();
130 std::shared_ptr<storm::logic::Formula const> targetStatesFormula, constraintsStatesFormula;
131 if (subformula.isEventuallyFormula()) {
132 targetStatesFormula = subformula.asEventuallyFormula().getSubformula().asSharedPointer();
133 constraintsStatesFormula = storm::logic::Formula::getTrueFormula()->asSharedPointer();
134 } else if (subformula.isUntilFormula()) {
135 storm::logic::UntilFormula const& untilFormula = subformula.asUntilFormula();
136 targetStatesFormula = untilFormula.getRightSubformula().asSharedPointer();
137 constraintsStatesFormula = untilFormula.getLeftSubformula().asSharedPointer();
138 }
139 if (targetStatesFormula && targetStatesFormula->isInFragment(storm::logic::propositional()) && constraintsStatesFormula &&
140 constraintsStatesFormula->isInFragment(storm::logic::propositional())) {
142 result.updateTargetStates(pomdp, getStates(*targetStatesFormula, false, pomdp));
143 result.updateSinkStates(pomdp, getStates(*constraintsStatesFormula, true, pomdp));
144 return result;
145 }
146 return FormulaInformation();
147}
148
149template<typename PomdpType>
151 STORM_LOG_THROW(formula.hasOptimalityType(), storm::exceptions::InvalidPropertyException,
152 "The property does not specify an optimization direction (min/max)");
153 STORM_LOG_WARN_COND(!formula.hasBound(), "The reward threshold for the given property will be ignored.");
154 std::string rewardModelName = "";
155 if (formula.hasRewardModelName()) {
156 rewardModelName = formula.getRewardModelName();
157 STORM_LOG_THROW(pomdp.hasRewardModel(rewardModelName), storm::exceptions::InvalidPropertyException,
158 "Selected reward model with name '" << rewardModelName << "' does not exist.");
159 } else {
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();
163 }
164 auto const& subformula = formula.getSubformula();
165 std::shared_ptr<storm::logic::Formula const> targetStatesFormula;
166 if (subformula.isEventuallyFormula()) {
167 targetStatesFormula = subformula.asEventuallyFormula().getSubformula().asSharedPointer();
168 }
169 if (targetStatesFormula && targetStatesFormula->isInFragment(storm::logic::propositional())) {
171 result.updateTargetStates(pomdp, getStates(*targetStatesFormula, false, pomdp));
172 return result;
173 }
174 return FormulaInformation();
175}
176
177template<typename PomdpType>
178FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::Formula const& formula) {
179 if (formula.isProbabilityOperatorFormula()) {
181 } else if (formula.isRewardOperatorFormula()) {
182 return getFormulaInformation(pomdp, formula.asRewardOperatorFormula());
183 }
184 return FormulaInformation();
185}
186
187template void FormulaInformation::updateTargetStates<storm::models::sparse::Pomdp<double>>(storm::models::sparse::Pomdp<double> const& pomdp,
188 storm::storage::BitVector&& newTargetStates);
189template void FormulaInformation::updateSinkStates<storm::models::sparse::Pomdp<double>>(storm::models::sparse::Pomdp<double> const& pomdp,
190 storm::storage::BitVector&& newSinkStates);
191template FormulaInformation getFormulaInformation<storm::models::sparse::Pomdp<double>>(storm::models::sparse::Pomdp<double> const& pomdp,
192 storm::logic::Formula const& formula);
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>>(
199
200} // namespace analysis
201} // namespace pomdp
202} // namespace storm
Formula const & getRightSubformula() const
Formula const & getLeftSubformula() const
RewardOperatorFormula & asRewardOperatorFormula()
Definition Formula.cpp:484
UntilFormula & asUntilFormula()
Definition Formula.cpp:325
static std::shared_ptr< Formula const > getTrueFormula()
Definition Formula.cpp:213
virtual bool isProbabilityOperatorFormula() const
Definition Formula.cpp:180
ProbabilityOperatorFormula & asProbabilityOperatorFormula()
Definition Formula.cpp:476
virtual bool isRewardOperatorFormula() const
Definition Formula.cpp:184
EventuallyFormula & asEventuallyFormula()
Definition Formula.cpp:341
std::shared_ptr< Formula const > asSharedPointer()
Definition Formula.cpp:571
storm::solver::OptimizationDirection const & getOptimalityType() const
std::string const & getRewardModelName() const
Retrieves the name of the reward model this property refers to (if any).
bool hasRewardModelName() const
Retrieves whether the reward model refers to a specific reward model.
Formula const & getSubformula() const
Formula const & getSubformula() const
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.
Definition Pomdp.h:15
void updateSinkStates(PomdpType const &pomdp, storm::storage::BitVector &&newSinkStates)
storm::solver::OptimizationDirection const & getOptimizationDirection() const
Type
Possible supported formula types.
void updateTargetStates(PomdpType const &pomdp, storm::storage::BitVector &&newTargetStates)
A bit vector that is internally represented as a vector of 64-bit values.
Definition BitVector.h:16
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)
Definition macros.h:11
#define STORM_LOG_WARN_COND(cond, message)
Definition macros.h:38
#define STORM_LOG_THROW(cond, exception, message)
Definition macros.h:30
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)
LabParser.cpp.