Storm
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 Unsupported // The formula type is unsupported
32 };
33
34 FormulaInformation(); // Unsupported
35 FormulaInformation(Type const& type, storm::solver::OptimizationDirection const& dir, std::optional<std::string> const& rewardModelName = std::nullopt);
36
37 Type const& getType() const;
40 bool isUnsupported() const;
41 StateSet const& getTargetStates() const;
42 StateSet const& getSinkStates() const; // Shall not be called for reward formulas
43 std::string const& getRewardModelName() const; // Shall not be called for probability formulas
45 bool minimize() const;
46 bool maximize() const;
47
48 template<typename PomdpType>
49 void updateTargetStates(PomdpType const& pomdp, storm::storage::BitVector&& newTargetStates);
50
51 template<typename PomdpType>
52 void updateSinkStates(PomdpType const& pomdp, storm::storage::BitVector&& newSinkStates);
53
54 private:
55 Type type;
56 storm::solver::OptimizationDirection optimizationDirection;
57 std::optional<StateSet> targetStates;
58 std::optional<StateSet> sinkStates;
59 std::optional<std::string> rewardModelName;
60};
61
62template<typename PomdpType>
63FormulaInformation getFormulaInformation(PomdpType const& pomdp, storm::logic::Formula const& formula);
64
65} // namespace analysis
66} // namespace pomdp
67} // 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:18
FormulaInformation getFormulaInformation(PomdpType const &pomdp, storm::logic::ProbabilityOperatorFormula const &formula)
LabParser.cpp.
Definition cli.cpp:18