ProbabilityOperatorFormula¶

class ProbabilityOperatorFormula( self: stormpy.logic.ProbabilityOperatorFormula, subformula: stormpy.logic.Formula, )¶

Bases: OperatorFormula

Probability operator

construct probability operator formula

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¶