Properties

In case you create expressions using Python code you probably want to use the convenience function prop() instead of working with the classes provided here directly. Note that this function is still provisional, however, it provides a much more concise way of defining expressions. In any case, instead of constructing objects directly it is recommended to use the constructor functions documented bellow.

Constructor Functions

momba.model.properties.aggregate(function, values, states=StateSelector(predicate=<StatePredicate.INITIAL: 'initial'>))

Creates an Aggregate property.

momba.model.properties.min_prob(formula)

Constructs a \(P_\mathit{min}\) property.

momba.model.properties.max_prob(formula)

Constructs a \(P_\mathit{max}\) property.

momba.model.properties.forall_paths(formula)

CTL \(\forall\) path operator.

momba.model.properties.exists_path(formula)

CTL \(\exists\) exists operator.

momba.model.properties.min_expected_reward(reward, *, accumulate=None, reachability=None, step_instant=None, time_instant=None, reward_instants=None)

Constructs a \(E_\mathit{min}\) property.

momba.model.properties.max_expected_reward(reward, *, accumulate=None, reachability=None, step_instant=None, time_instant=None, reward_instants=None)

Constructs a \(E_\mathit{max}\) property.

momba.model.properties.min_steady_state(formula, *, accumulate=None)

Constructs a \(S_\mathit{min}\) property.

momba.model.properties.max_steady_state(formula, *, accumulate=None)

Constructs a \(S_\mathit{max}\) property.

momba.model.properties.until(left, right, *, step_bounds=None, time_bounds=None, reward_bounds=None)

Constructs a temporal until property.

momba.model.properties.weak_until(left, right, *, step_bounds=None, time_bounds=None, reward_bounds=None)

Constructs a temporal weak-until property.

momba.model.properties.release(left, right, *, step_bounds=None, time_bounds=None, reward_bounds=None)

Constructs a temporal release property.

momba.model.properties.eventually(formula, *, step_bounds=None, time_bounds=None, reward_bounds=None)

Constructs a temporal evenutally property.

momba.model.properties.globally(formula, *, step_bounds=None, time_bounds=None, reward_bounds=None)

Constructs a temporal globally property.

Class Reference

class momba.model.properties.Aggregate(function, values, predicate)

Applies an aggregation function over a set of states.

function

The aggregation function to apply.

values

The values to aggregate over.

predcate

The predicate used to identify the states to aggregate over.

property children

The direct children of the expression.

class momba.model.properties.StatePredicate(value)

An enum of state predicates to be used with Aggregate.

INITIAL = 'initial'

The state is an initial state.

DEADLOCK = 'deadlock'

The state is a deadlock state.

TIMELOCK = 'timelock'

The state is a timelock state.

class momba.model.properties.StateSelector(predicate)

State selector expression using StatePredicate.

predicate

A StatePredicate.

property children

The direct children of the expression.

properties.INITIAL_STATES = StateSelector(predicate=<StatePredicate.INITIAL: 'initial'>)

properties.DEADLOCK_STATES = StateSelector(predicate=<StatePredicate.DEADLOCK: 'deadlock'>)

properties.TIMELOCK_STATES = StateSelector(predicate=<StatePredicate.TIMELOCK: 'timelock'>)

class momba.model.properties.Probability(operator, formula)

Probability property.

operator

Min or max probability (MinMax).

formula

Boolean expression to compute the probability for.

property children

The direct children of the expression.

class momba.model.properties.PathQuantifier(quantifier, formula)

A temporal path quantifier property.

quantifier

The quantifier (Quantifier).

formula

The inner formula.

property children

The direct children of the expression.

class momba.model.properties.AccumulationInstant(value)

En enumeration of reward accumulation instants.

STEPS = 'steps'

Accumulate at each step.

TIME = 'time'

Accumulate with the progression of time.

EXIT = 'exit'

Accumulate after exiting a state.

class momba.model.properties.ExpectedReward(operator, reward, accumulate=None, reachability=None, step_instant=None, time_instant=None, reward_instants=None)

Expected reward property.

operator

Min or max probability (MinMax).

reward

Expression to compute the reward.

accumulate

A set of accumulation instants.

reachability

step_instant

time_instant

reward_instants

property children

The direct children of the expression.

class momba.model.properties.RewardInstant(expression, accumulate, instant)

A reward instant.

expression

accumulate

instant

class momba.model.properties.SteadyState(operator, formula, accumulate=None)

A steady-state property.

operator

formula

accumulate

property children

The direct children of the expression.

class momba.model.properties.BinaryPathFormula(operator, left, right, step_bounds=None, time_bounds=None, reward_bounds=None)

A temporal binary path formula.

operator

left

right

step_bounds

time_bounds

reward_bounds

property children

The direct children of the expression.

class momba.model.properties.UnaryPathFormula(operator, formula, step_bounds=None, time_bounds=None, reward_bounds=None)

A temporal unary path formula.

operator

formula

step_bounds

time_bounds

reward_bounds

property children

The direct children of the expression.

class momba.model.properties.Interval(lower=None, upper=None, lower_exclusive=None, upper_exclusive=None)

An interval.

lower

The lower bound of the interval or None.

upper

The upper bound of the interval or None.

lower_exclusive

Whether the lower bound is exclusive.

upper_exclusive

Whether the upper bound is exclusive.

class momba.model.properties.RewardBound(expression, accumulate, bounds)

A reward bound.

expression

accumulate

bounds