LongRunAverageOperatorFormula

class LongRunAverageOperatorFormula

Bases: OperatorFormula

Long run average operator

clone(self: stormpy.logic.Formula) → stormpy.logic.Formula

property comparison_type

Comparison type of bound

property has_bound

Flag if formula is bounded

property has_optimality_type

Flag if an optimality type is present

property is_bounded_until_formula

property is_discounted_cumulative_reward_formula

is it a discounted cumulative reward formula

property is_discounted_total_reward_formula

is it a discounted total reward formula

property is_eventually_formula

property is_multi_objective_formula

property is_probability_operator_formula

Whether it is a probability operator

property is_reward_operator_formula

Whether it is a reward operator

property is_until_formula

property optimality_type

Flag for the optimality type

remove_bound(self: stormpy.logic.OperatorFormula) → None

remove_optimality_type(self: stormpy.logic.OperatorFormula) → None

remove the optimality type

set_bound(

self: stormpy.logic.OperatorFormula,

comparison_type: stormpy.logic.ComparisonType,

bound: stormpy.expressions.Expression,

) → None

Set bound

set_optimality_type(

self: stormpy.logic.OperatorFormula,

new_optimality_type,

) → None

set the optimality type (use remove optimiality type for clearing)

property subformula

the subformula

substitute(

self: stormpy.logic.Formula,

constants_map: collections.abc.Mapping[stormpy.expressions.Variable, stormpy.expressions.Expression],

) → stormpy.logic.Formula

Substitute variables

substitute_labels_by_labels(

self: stormpy.logic.Formula,

replacements: collections.abc.Mapping[str, str],

) → stormpy.logic.Formula

substitute label occurences

property threshold

Threshold of bound (currently only applicable to rational expressions)

property threshold_expr