Stormpy.logic

class AtomicExpressionFormula

Formula with an atomic expression

class AtomicLabelFormula

Formula with an atomic label

class BinaryPathFormula

Path formula with two operands

left_subformula
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.

class ComparisonType
GEQ = ComparisonType.GEQ
GREATER = ComparisonType.GREATER
LEQ = ComparisonType.LEQ
LESS = ComparisonType.LESS
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()
is_probability_operator

is it a probability operator

is_reward_operator

is it a reward operator

substitute()

Substitute variables

substitute_labels_by_labels()

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 OperatorFormula

Operator formula

comparison_type

Comparison type of bound

has_bound

Flag if formula is bounded

has_optimality_type

Flag if an optimality type is present

optimality_type

Flag for the optimality type

remove_bound()
remove_optimality_type()

remove the optimality type

set_bound()

Set bound

set_optimality_type()

set the optimality type (use remove optimiality type for clearing)

threshold

Threshold of bound (currently only applicable to rational expressions)

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()
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

subformula

the subformula

class UnaryStateFormula

State formula with one operand

subformula

the subformula

class UntilFormula

Path Formula for unbounded until