class AtomicExpressionFormula

Formula with an atomic expression

class AtomicLabelFormula

Formula with an atomic label

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.

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

property is_probability_operator

is it a probability operator

property is_reward_operator

is it a reward operator


Substitute variables


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

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 the optimality type


Set bound


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

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