storm::logic Namespace Reference

Classes
class	AtomicExpressionFormula
class	AtomicLabelFormula
class	BinaryBooleanPathFormula
class	BinaryBooleanStateFormula
class	BinaryPathFormula
class	BinaryStateFormula
class	BooleanLiteralFormula
struct	Bound
class	BoundedUntilFormula
class	CloneVisitor
class	ConditionalFormula
class	CumulativeRewardFormula
class	EventuallyFormula
class	ExpectedTimeToExpectedRewardVisitor
class	ExpressionSubstitutionVisitor
class	ExtractMaximalStateFormulasVisitor
class	Formula
class	FormulaInformation
class	FormulaInformationVisitor
class	FormulaVisitor
class	FragmentChecker
class	FragmentSpecification
class	GameFormula
class	GloballyFormula
class	HOAPathFormula
class	InheritedInformation
class	InstantaneousRewardFormula
class	LabelSubstitutionVisitor
class	LiftableTransitionRewardsVisitor
class	LongRunAverageOperatorFormula
class	LongRunAverageRewardFormula
class	MultiObjectiveFormula
class	NextFormula
class	OperatorFormula
struct	OperatorInformation
class	PathFormula
class	PlayerCoalition
class	ProbabilityOperatorFormula
class	QuantileFormula
class	RewardAccumulation
class	RewardAccumulationEliminationVisitor
class	RewardModelNameSubstitutionVisitor
class	RewardOperatorFormula
class	StateFormula
class	TimeBound
class	TimeBoundReference
class	TimeOperatorFormula
class	ToExpressionVisitor
class	ToPrefixStringVisitor
class	TotalRewardFormula
class	UnaryBooleanPathFormula
class	UnaryBooleanStateFormula
class	UnaryPathFormula
class	UnaryStateFormula
class	UntilFormula

Enumerations
enum class	BinaryBooleanOperatorType { And , Or }
enum class	ComparisonType { Less , LessEqual , Greater , GreaterEqual }
enum class	FormulaContext {   Undefined , Probability , Reward , LongRunAverage ,   Time }
enum class	TimeBoundType { Steps , Time , Reward }
enum class	UnaryBooleanOperatorType { Not }

Functions
std::ostream &	operator<< (std::ostream &out, Bound const &bound)
std::ostream &	operator<< (std::ostream &out, ComparisonType const &comparisonType)
bool	isStrict (ComparisonType t)
bool	isLowerBound (ComparisonType t)
ComparisonType	invert (ComparisonType t)
ComparisonType	invertPreserveStrictness (ComparisonType t)
template storm::RationalNumber	CumulativeRewardFormula::getBound< storm::RationalNumber > () const
OperatorInformation	substituteOperatorInformation (OperatorInformation const &operatorInformation, std::function< storm::expressions::Expression(storm::expressions::Expression const &)> const &substitutionFunction)
std::ostream &	operator<< (std::ostream &out, Formula const &formula)
std::ostream &	operator<< (std::ostream &out, FormulaContext const &formulaContext)
FragmentSpecification	propositional ()
FragmentSpecification	reachability ()
FragmentSpecification	pctl ()
FragmentSpecification	pctlstar ()
FragmentSpecification	flatPctl ()
FragmentSpecification	rpatl ()
FragmentSpecification	prctl ()
FragmentSpecification	prctlstar ()
FragmentSpecification	csl ()
FragmentSpecification	cslstar ()
FragmentSpecification	csrl ()
FragmentSpecification	csrlstar ()
FragmentSpecification	multiObjective ()
FragmentSpecification	lexObjective ()
FragmentSpecification	quantiles ()
template<typename T0 , typename... Ts>
std::ostream &	operator<< (std::ostream &s, std::variant< T0, Ts... > const &v)
std::ostream &	operator<< (std::ostream &stream, PlayerCoalition const &coalition)
std::ostream &	operator<< (std::ostream &out, RewardAccumulation const &acc)

Enumeration Type Documentation

BinaryBooleanOperatorType

enum class storm::logic::BinaryBooleanOperatorType

strong

Enumerator
And
Or

Definition at line 5 of file BinaryBooleanOperatorType.h.

ComparisonType

enum class storm::logic::ComparisonType

strong

Enumerator
Less
LessEqual
Greater
GreaterEqual

Definition at line 10 of file ComparisonType.h.

FormulaContext

enum class storm::logic::FormulaContext

strong

Enumerator
Undefined
Probability
Reward
LongRunAverage
Time

Definition at line 9 of file FormulaContext.h.

TimeBoundType

enum class storm::logic::TimeBoundType

strong

Enumerator
Steps
Time
Reward

Definition at line 10 of file TimeBoundType.h.

UnaryBooleanOperatorType

enum class storm::logic::UnaryBooleanOperatorType

strong

Enumerator
Not

Definition at line 5 of file UnaryBooleanOperatorType.h.

Function Documentation

csl()

FragmentSpecification storm::logic::csl

(

)

Definition at line 109 of file FragmentSpecification.cpp.

cslstar()

FragmentSpecification storm::logic::cslstar

(

)

Definition at line 117 of file FragmentSpecification.cpp.

csrl()

FragmentSpecification storm::logic::csrl

(

)

Definition at line 129 of file FragmentSpecification.cpp.

csrlstar()

FragmentSpecification storm::logic::csrlstar

(

)

Definition at line 142 of file FragmentSpecification.cpp.

CumulativeRewardFormula::getBound< storm::RationalNumber >()

template storm::RationalNumber storm::logic::CumulativeRewardFormula::getBound< storm::RationalNumber >

(

)

const

flatPctl()

FragmentSpecification storm::logic::flatPctl

(

)

Definition at line 60 of file FragmentSpecification.cpp.

invert()

ComparisonType storm::logic::invert ( ComparisonType  t )

inline

Definition at line 20 of file ComparisonType.h.

invertPreserveStrictness()

ComparisonType storm::logic::invertPreserveStrictness ( ComparisonType  t )

inline

Definition at line 36 of file ComparisonType.h.

isLowerBound()

bool storm::logic::isLowerBound ( ComparisonType  t )

inline

Definition at line 16 of file ComparisonType.h.

isStrict()

bool storm::logic::isStrict ( ComparisonType  t )

inline

Definition at line 12 of file ComparisonType.h.

lexObjective()

FragmentSpecification storm::logic::lexObjective

(

)

Definition at line 179 of file FragmentSpecification.cpp.

multiObjective()

FragmentSpecification storm::logic::multiObjective

(

)

Definition at line 155 of file FragmentSpecification.cpp.

operator<<() [1/7]

std::ostream & storm::logic::operator<< ( std::ostream &  out, Bound const &  bound  )

inline

Definition at line 40 of file Bound.h.

operator<<() [2/7]

std::ostream & storm::logic::operator<<	(	std::ostream &	out,
		ComparisonType const &	comparisonType
	)

Definition at line 7 of file ComparisonType.cpp.

operator<<() [3/7]

std::ostream & storm::logic::operator<<	(	std::ostream &	out,
		Formula const &	formula
	)

Definition at line 578 of file Formula.cpp.

operator<<() [4/7]

std::ostream & storm::logic::operator<<	(	std::ostream &	out,
		FormulaContext const &	formulaContext
	)

Definition at line 6 of file FormulaContext.cpp.

operator<<() [5/7]

std::ostream & storm::logic::operator<<	(	std::ostream &	out,
		RewardAccumulation const &	acc
	)

Definition at line 31 of file RewardAccumulation.cpp.

operator<<() [6/7]

template<typename T0 , typename... Ts>

std::ostream & storm::logic::operator<<	(	std::ostream &	s,
		std::variant< T0, Ts... > const &	v
	)

Definition at line 16 of file PlayerCoalition.cpp.

operator<<() [7/7]

std::ostream & storm::logic::operator<<	(	std::ostream &	stream,
		PlayerCoalition const &	coalition
	)

Definition at line 21 of file PlayerCoalition.cpp.

pctl()

FragmentSpecification storm::logic::pctl

(

)

Definition at line 33 of file FragmentSpecification.cpp.

pctlstar()

FragmentSpecification storm::logic::pctlstar

(

)

Definition at line 48 of file FragmentSpecification.cpp.

prctl()

FragmentSpecification storm::logic::prctl

(

)

Definition at line 81 of file FragmentSpecification.cpp.

prctlstar()

FragmentSpecification storm::logic::prctlstar

(

)

Definition at line 95 of file FragmentSpecification.cpp.

propositional()

FragmentSpecification storm::logic::propositional

(

)

Definition at line 9 of file FragmentSpecification.cpp.

quantiles()

FragmentSpecification storm::logic::quantiles

(

)

Definition at line 221 of file FragmentSpecification.cpp.

reachability()

FragmentSpecification storm::logic::reachability

(

)

Definition at line 21 of file FragmentSpecification.cpp.

rpatl()

FragmentSpecification storm::logic::rpatl

(

)

Definition at line 68 of file FragmentSpecification.cpp.

substituteOperatorInformation()

OperatorInformation storm::logic::substituteOperatorInformation	(	OperatorInformation const &	operatorInformation,
		std::function< storm::expressions::Expression(storm::expressions::Expression const &)> const &	substitutionFunction
	)

Definition at line 15 of file ExpressionSubstitutionVisitor.cpp.