Storm 1.11.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
FormulaInformation.h
Go to the documentation of this file.
1#pragma once
2
3#include <optional>
4#include <set>
5#include <string>
8
9namespace storm {
10
11namespace logic {
12class Formula;
13}
14
15namespace pomdp {
16namespace analysis {
18 public:
20 struct StateSet {
21 storm::storage::BitVector states; // The set of states
22 std::set<uint32_t> observations; // The set of the observations that are assigned to at least one state of the set
23 bool observationClosed; // True iff this state set can be uniquely characterized by the observations
24 bool empty() const;
25 };
26
28 enum class Type {
29 NonNestedReachabilityProbability, // e.g. 'Pmax=? [F "target"]' or 'Pmin=? [!"sink" U "target"]'
30 NonNestedExpectedRewardFormula, // e.g. 'Rmin=? [F x>0 ]'
31 DiscountedTotalRewardFormula, // e.g. 'Rmax=? [Cdiscount=9/10}]'
32 Unsupported // The formula type is unsupported
33 };
34
35 FormulaInformation(); // Unsupported
36 FormulaInformation(Type const& type, storm::solver::OptimizationDirection const& dir, std::optional<std::string> const& rewardModelName = std::nullopt);
37
38 Type const& getType() const;
42 bool isUnsupported() const;
43 StateSet const& getTargetStates() const;
44 StateSet const& getSinkStates() const; // Shall not be called for reward formulas
45 std::string const& getRewardModelName() const; // Shall not be called for probability formulas
47 bool minimize() const;
48 bool maximize() const;
49
50 template<typename PomdpType>
51 void updateTargetStates(PomdpType const& pomdp, storm::storage::BitVector&& newTargetStates);
52
53 template<typename PomdpType>
54 void updateSinkStates(PomdpType const& pomdp, storm::storage::BitVector&& newSinkStates);
55
56 private:
57 Type type;
58 storm::solver::OptimizationDirection optimizationDirection;
59 std::optional<StateSet> targetStates;
60 std::optional<StateSet> sinkStates;
61 std::optional<std::string> rewardModelName;
62};
63
64template<typename PomdpType>
65FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::Formula const& formula);
66
67} // namespace analysis
68} // namespace pomdp
69} // namespace storm
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
FormulaInformation getFormulaInformation(PomdpType const &pomdp, storm::logic::ProbabilityOperatorFormula const &formula)
LabParser.cpp.