ConditionalFormula¶

class ConditionalFormula¶

Bases: Formula

Formula with the right hand side being a condition.

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

property conditional_subformula¶: the conditional subformula

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 main_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