stormpy.logic

Properties and their formulas, e.g., probability and reward operators of PCTL and CSL.

Functions

parse_properties(properties[, context, ...])	Parse properties given in the Prism property format.
parse_property(property[, context])	Parse a single property given in the Prism property format.

Classes

AtomicExpressionFormula	Formula with an atomic expression
AtomicLabelFormula	Formula with an atomic label
BinaryBooleanOperatorType(*values)	Operator of a binary Boolean state formula
BinaryBooleanStateFormula	Boolean binary state formula
BinaryPathFormula	Path formula with two operands
BinaryStateFormula	State formula with two operands
BooleanLiteralFormula(self, value)	Formula with a boolean literal
BoundedUntilFormula	Until Formula with either a step or a time bound.
ComparisonType(*values)	Comparison of a bound, e.g. < or >=.
ConditionalFormula	Formula with the right hand side being a condition.
CumulativeRewardFormula	Summed rewards over the paths
DiscountedCumulativeRewardFormula	Discounted sum of rewards over the paths
DiscountedTotalRewardFormula	Discounted total reward over the paths
EventuallyFormula	Formula for eventually
Formula	Generic Storm Formula
GameFormula	Game formula
GloballyFormula	Formula for globally
InstantaneousRewardFormula	Instantaneous reward
LongRunAverageOperatorFormula	Long run average operator
LongRunAverageRewardFormula	Long run average reward
MultiObjectiveFormula	Multi objective formula
OperatorFormula	Operator formula
OptimizationDirection(*values)	Direction of optimization
PathFormula	Formula about the probability of a set of paths in an automaton
ProbabilityOperatorFormula(self, subformula)	Probability operator
Property(Property)	Property consisting of a name and a formula
RewardOperatorFormula	Reward operator
StateFormula	Formula about a state of an automaton
TimeOperatorFormula	The time operator
UnaryBooleanStateFormula	Unary boolean state formula
UnaryPathFormula	Path formula with one operand
UnaryStateFormula	State formula with one operand
UntilFormula	Path Formula for unbounded until