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

OR

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 GameFormula

Game formula

property is_game_formula

is it a game formula

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