Formula¶

class Formula¶

Bases: pybind11_object

Generic Storm Formula

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

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¶

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