Stormpy.logic¶

class AtomicExpressionFormula¶

Formula with an atomic expression

get_expression(self: stormpy.logic.logic.AtomicExpressionFormula) → stormpy.storage.storage.Expression¶

class AtomicLabelFormula¶

Formula with an atomic label

property label¶: label in the formula

class BinaryBooleanOperatorType¶

Members:

AND

AND = <BinaryBooleanOperatorType.AND: 0>¶

OR = <BinaryBooleanOperatorType.OR: 1>¶

property name¶

property value¶

class BinaryPathFormula¶

Path formula with two operands

property left_subformula¶

property right_subformula¶

class BinaryStateFormula¶: State formula with two operands

class BooleanBinaryStateFormula¶: Boolean binary state formula

class BooleanLiteralFormula¶: Formula with a boolean literal

class BoundedUntilFormula¶

Until Formula with either a step or a time bound.

property has_lower_bound¶

property is_multidimensional¶: Is the bound multi-dimensional

property left_subformula¶

property right_subformula¶

property upper_bound_expression¶

class ComparisonType¶

Members:

LESS

LEQ

GREATER

GEQ

GEQ = <ComparisonType.GEQ: 3>¶

GREATER = <ComparisonType.GREATER: 2>¶

LEQ = <ComparisonType.LEQ: 1>¶

LESS = <ComparisonType.LESS: 0>¶

property name¶

property value¶

class ConditionalFormula¶: Formula with the right hand side being a condition.

class CumulativeRewardFormula¶: Summed rewards over a the paths

class EventuallyFormula¶: Formula for eventually

class Formula¶

Generic Storm Formula

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

property is_bounded_until_formula¶

property is_eventually_formula¶

property is_multi_objective_formula¶

property is_probability_operator¶: is it a probability operator

property is_reward_operator¶: is it a reward operator

property is_until_formula¶

substitute(self: stormpy.logic.logic.Formula, constants_map: Dict[stormpy.storage.storage.Variable, stormpy.storage.storage.Expression]) → stormpy.logic.logic.Formula¶: Substitute variables

substitute_labels_by_labels(self: stormpy.logic.logic.Formula, replacements: Dict[str, str]) → stormpy.logic.logic.Formula¶: substitute label occurences

class GloballyFormula¶: Formula for globally

class InstantaneousRewardFormula¶: Instantaneous reward

class LongRunAvarageOperator¶: Long run average operator

class LongRunAverageRewardFormula¶: Long run average reward

class MultiObjectiveFormula¶

Multi objective formula

property nr_subformulas¶: Get number of subformulas

property subformulas¶: Get vector of subformulas

class OperatorFormula¶

Operator 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 optimality_type¶: Flag for the optimality type

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

remove_optimality_type(self: stormpy.logic.logic.OperatorFormula) → None¶: remove the optimality type

set_bound(self: stormpy.logic.logic.OperatorFormula, comparison_type: stormpy.logic.logic.ComparisonType, bound: stormpy.storage.storage.Expression) → None¶: Set bound

set_optimality_type(self: stormpy.logic.logic.OperatorFormula, new_optimality_type: stormpy.core.OptimizationDirection) → None¶: set the optimality type (use remove optimiality type for clearing)

property threshold¶: Threshold of bound (currently only applicable to rational expressions)

property threshold_expr¶

class PathFormula¶: Formula about the probability of a set of paths in an automaton

class ProbabilityOperator¶: Probability operator

class RewardOperator¶

Reward operator

has_reward_name(self: stormpy.logic.logic.RewardOperator) → bool¶

property reward_name¶

class StateFormula¶: Formula about a state of an automaton

class TimeOperator¶: The time operator

class UnaryBooleanStateFormula¶: Unary boolean state formula

class UnaryPathFormula¶

Path formula with one operand

property subformula¶: the subformula

class UnaryStateFormula¶

State formula with one operand

property subformula¶: the subformula

class UntilFormula¶: Path Formula for unbounded until