Storm
1.14.0.1
A Modern Probabilistic Model Checker
Loading...
Searching...
No Matches
PropertyInformation.h
Go to the documentation of this file.
1
#pragma once
2
3
#include <optional>
4
#include <set>
5
#include <string>
6
#include <vector>
7
8
#include "
storm-pomdp/beliefs/utility/types.h
"
9
#include "
storm/logic/TimeBound.h
"
10
#include "
storm/solver/OptimizationDirection.h
"
11
12
namespace
storm::pomdp::beliefs
{
14
struct
RewardBound
{
15
std::string
rewardModelName
;
16
std::optional<storm::logic::TimeBound>
lowerBound
;
17
std::optional<storm::logic::TimeBound>
upperBound
;
18
};
19
26
struct
PropertyInformation
{
27
enum class
Kind
{
ReachabilityProbability
,
ExpectedTotalReachabilityReward
,
RewardBoundedReachabilityProbability
};
28
Kind
kind
;
29
std::set<BeliefObservationType>
targetObservations
;
30
std::optional<std::string>
rewardModelName
;
31
storm::OptimizationDirection
dir
;
32
std::vector<RewardBound>
rewardBounds
;
33
};
34
}
// namespace storm::pomdp::beliefs
OptimizationDirection.h
TimeBound.h
storm::pomdp::beliefs
Definition
ClippingBeliefAbstraction.cpp:15
storm::OptimizationDirection
solver::OptimizationDirection OptimizationDirection
Definition
OptimizationDirection.h:29
storm::pomdp::beliefs::PropertyInformation
Property data consumed by the belief MDP construction.
Definition
PropertyInformation.h:26
storm::pomdp::beliefs::PropertyInformation::Kind
Kind
Definition
PropertyInformation.h:27
storm::pomdp::beliefs::PropertyInformation::Kind::ReachabilityProbability
@ ReachabilityProbability
Definition
PropertyInformation.h:27
storm::pomdp::beliefs::PropertyInformation::Kind::ExpectedTotalReachabilityReward
@ ExpectedTotalReachabilityReward
Definition
PropertyInformation.h:27
storm::pomdp::beliefs::PropertyInformation::Kind::RewardBoundedReachabilityProbability
@ RewardBoundedReachabilityProbability
Definition
PropertyInformation.h:27
storm::pomdp::beliefs::PropertyInformation::rewardModelName
std::optional< std::string > rewardModelName
Definition
PropertyInformation.h:30
storm::pomdp::beliefs::PropertyInformation::kind
Kind kind
Definition
PropertyInformation.h:28
storm::pomdp::beliefs::PropertyInformation::dir
storm::OptimizationDirection dir
Definition
PropertyInformation.h:31
storm::pomdp::beliefs::PropertyInformation::targetObservations
std::set< BeliefObservationType > targetObservations
Definition
PropertyInformation.h:29
storm::pomdp::beliefs::PropertyInformation::rewardBounds
std::vector< RewardBound > rewardBounds
Definition
PropertyInformation.h:32
storm::pomdp::beliefs::RewardBound
One reward dimension of a reward-bounded reachability property.
Definition
PropertyInformation.h:14
storm::pomdp::beliefs::RewardBound::rewardModelName
std::string rewardModelName
Definition
PropertyInformation.h:15
storm::pomdp::beliefs::RewardBound::lowerBound
std::optional< storm::logic::TimeBound > lowerBound
Definition
PropertyInformation.h:16
storm::pomdp::beliefs::RewardBound::upperBound
std::optional< storm::logic::TimeBound > upperBound
Definition
PropertyInformation.h:17
types.h
src
storm-pomdp
beliefs
verification
PropertyInformation.h
Generated by
1.15.0