API Reference

This page contains the documentation for the FeSTL Python interface.

Core Functions

`festl_python.festl_python.parse_formula(formula_str)`

Parse an STL formula from a string using the same DSL syntax as Rust's stl! macro.

This allows you to write formulas using the same syntax as Rust, making it easy to port formulas between Python and Rust code.

Syntax:

Predicates:

signal > value - Signal greater than value
signal < value - Signal less than value
signal >= value - Signal greater than or equal
signal <= value - Signal less than or equal

Variable Predicates (for runtime-updateable thresholds):

signal > $variable - Signal greater than variable
signal < $variable - Signal less than variable
signal >= $variable - Signal greater than or equal to variable
signal <= $variable - Signal less than or equal to variable

Boolean Constants:

true - Always true
false - Always false

Unary Operators:

!(sub) or not(sub) - Negation
G[start, end](sub) or globally[start, end](sub) - Globally (always)
F[start, end](sub) or eventually[start, end](sub) - Eventually (finally)

Binary Operators:

left && right or left and right - Conjunction
left || right or left or right - Disjunction
left -> right or left implies right - Implication
left U[start, end] right or left until[start, end] right - Until

Parameters:

Name	Type	Description	Default
`formula_str`	`str`	A string containing an STL formula	required

Returns:

Type	Description
`Formula`	The parsed Formula object

Raises:

Type	Description
`ValueError`	If the formula string cannot be parsed

Examples:

>>> # Simple predicate
>>> f = parse_formula("x > 5")
>>> # Globally operator
>>> f = parse_formula("G[0, 10](x > 5)")
>>> # Complex formula
>>> f = parse_formula("G[0, 10](x > 5) && F[0, 5](y < 3)")
>>> # Using keyword syntax
>>> f = parse_formula("globally[0, 10](x > 5) and eventually[0, 5](y < 3)")
>>> # Using variables for runtime-updateable thresholds
>>> f = parse_formula("G[0, 10](x > $threshold)")
>>> f = parse_formula("x > $min && x < $max")

Core Classes

`festl_python.festl_python.Monitor`

Online STL monitor.

Monitors signal traces against an STL formula and produces verdicts. Supports multiple semantics (DelayedQualitative, EagerQualitative, DelayedQuantitative, Rosi), algorithms (Incremental, Naive), and synchronization strategies (ZeroOrderHold, Linear, None).

The monitor processes signals incrementally and produces verdicts when sufficient information is available.

Examples:

>>> phi = Formula.always(0, 5, Formula.gt('x', 0.5))
>>> monitor = Monitor(phi, semantics='Rosi')
>>> for t in range(10):
...     result = monitor.update('x', 0.8, float(t))
...     print(result)

`update(signal, value, timestamp)`

Update the monitor with a new signal value.

Processes the new data point and produces verdicts when sufficient information is available. Each update may trigger multiple evaluations, one for each synchronized step (which may include interpolated values).

Parameters:

Name	Type	Description	Default
`signal`	`str`	Name of the signal being updated	required
`value`	`float`	Signal value at this timestamp	required
`timestamp`	`float`	Timestamp in seconds (must be monotonically increasing)	required

Returns:

Type	Description
`MonitorOutput`	MonitorOutput object containing:
`MonitorOutput`	Display/Debug formatting via `__str__()` and `__repr__()`
`MonitorOutput`	Properties: input_signal, input_timestamp, input_value
`MonitorOutput`	Methods: has_verdicts(), total_raw_outputs(), is_pending(), verdicts()
`MonitorOutput`	Structured data access via `to_dict()`

Note

Evaluations list may be empty if data is being buffered
For multi-signal formulas, the synchronizer may produce interpolated steps
Each evaluation corresponds to a specific synchronized step
Multiple outputs may be produced for each synchronized step

Examples:

>>> output = monitor.update('x', 0.8, 1.0)
>>> # Use Rust-style Display formatting
>>> print(output)
>>> # Access properties
>>> print(f"Input: {output.input_signal} at t={output.input_timestamp}")
>>> # Get verdicts
>>> for ts, val in output.verdicts():
...     print(f"Verdict at {ts}: {val}")
>>> # Access as dictionary
>>> d = output.to_dict()
>>> for eval in d['evaluations']:
...     for out in eval['outputs']:
...         print(f"  t={out['timestamp']}: {out['value']}")

`get_signal_identifiers()`

Get the set of signal identifiers used in the monitor's formula.

Returns:

Type	Description
`set[str]`	Set[str]: A set of signal names (identifiers) used in the formula.

Examples:

>>> phi = parse_formula("G[0,5](x > 5) && F[0,3](y < 10)")
>>> monitor = Monitor(phi)
>>> signals = monitor.get_signal_identifiers()
>>> print(signals)  # {'x', 'y'}

`get_variables()`

Get the Variables object associated with this monitor.

This allows you to update variable values at runtime, which will affect future evaluations of the formula.

Returns:

Type	Description
`Variables`	The Variables object containing runtime variable values.

Examples:

>>> vars = Variables()
>>> vars.set("threshold", 5.0)
>>> monitor = Monitor(formula, variables=vars)
>>> # Update a variable at runtime
>>> monitor.get_variables().set("threshold", 10.0)

`get_specification()`

Get the STL specification as a string representation.

Returns:

Type	Description
`str`	String representation of the STL formula being monitored.

Examples:

>>> phi = parse_formula("G[0,5](x > 5)")
>>> monitor = Monitor(phi)
>>> print(monitor.get_specification())  # "G[0s,5s](x > 5)"

`get_algorithm()`

Get the algorithm used by this monitor.

Returns:

Type	Description
`str`	"Incremental" or "Naive"

Examples:

>>> monitor = Monitor(phi, algorithm="Incremental")
>>> print(monitor.get_algorithm())  # "Incremental"

`get_semantics()`

Get the semantics used by this monitor.

Returns:

Type	Description
`str`	One of: "DelayedQualitative", "EagerQualitative", "DelayedQuantitative", or "Rosi"

Examples:

>>> monitor = Monitor(phi, semantics="DelayedQuantitative")
>>> print(monitor.get_semantics())  # "DelayedQuantitative"

`get_synchronization_strategy()`

Get the synchronization strategy used by this monitor.

Returns:

Type	Description
`str`	One of: "ZeroOrderHold", "Linear", or "None"

Examples:

>>> monitor = Monitor(phi, synchronization="Linear")
>>> print(monitor.get_synchronization_strategy())  # "Linear"

`get_temporal_depth()`

Get the maximum lookahead required by the formula (temporal depth).

This corresponds to the maximum time interval in any temporal operator.

Returns:

Type	Description
`float`	The temporal depth in seconds.

Examples:

>>> phi = parse_formula("G[0,5](x > 5) && F[0,3](y < 10)")
>>> monitor = Monitor(phi)
>>> print(monitor.get_temporal_depth())  # 5.0

`update_batch(steps)`

Update the monitor with multiple signal values in batch.

This method processes multiple data points at once. Steps are automatically sorted by timestamp in chronological order before processing, which is optimal for the Incremental algorithm.

Parameters:

Name	Type	Description	Default
`steps`	`dict[str, List[Tuple[float, float]]]`	A dictionary mapping signal names to lists of (value, timestamp) tuples. Examples: `{"x": [(1.0, 0.0), (2.0, 1.0)], "y": [(5.0, 0.5)]}`	required

Returns:

Type	Description
`MonitorOutput`	A single MonitorOutput containing all evaluation results from processing
`MonitorOutput`	the batch. The input metadata reflects the last step processed.

Raises:

Type	Description
`ValueError`	If the steps dictionary is empty or contains no steps.

Note

Steps are processed in chronological order (sorted by timestamp) regardless of the order in which signals appear in the dictionary. If you need a specific processing order, use update() directly.

Examples:

>>> steps = {
...     "temperature": [(25.0, 1.0), (26.0, 2.0)],
...     "pressure": [(101.3, 1.5)]
... }
>>> output = monitor.update_batch(steps)
>>> print(output)  # Display all finalized verdicts

`festl_python.festl_python.Variables`

Container for runtime variable values.

Variables allow you to define STL formulas with dynamic thresholds that can be updated at runtime. Use the $variable syntax in formulas to reference variables.

Examples:

>>> # Create variables and set initial values
>>> vars = Variables()
>>> vars.set("threshold", 5.0)
>>> vars.set("limit", 10.0)
>>>
>>> # Parse a formula using variables
>>> formula = parse_formula("x > $threshold && y < $limit")
>>>
>>> # Create a monitor with variables
>>> monitor = Monitor(formula, variables=vars)
>>>
>>> # Update a variable value at runtime
>>> vars.set("threshold", 7.0)  # Affects future evaluations

Note

Variable predicates require the Incremental algorithm. Using variables with the Naive algorithm will raise an error.

`clear()`

Remove all variables.

Examples:

>>> vars = Variables()
>>> vars.set("x", 5.0)
>>> vars.clear()
>>> vars.names()  # []

`contains(name)`

Check if a variable exists.

Parameters:

Name	Type	Description	Default
`name`	`str`	The variable name (without $ prefix)	required

Returns:

Type	Description
`bool`	True if the variable exists, False otherwise.

Examples:

>>> vars = Variables()
>>> vars.set("x", 5.0)
>>> vars.contains("x")  # True
>>> vars.contains("y")  # False

`get(name)`

Get a variable's value.

Parameters:

Name	Type	Description	Default
`name`	`str`	The variable name (without $ prefix)	required

Returns:

Type	Description
`Union[float, None]`	The variable's value, or None if not set.

Examples:

>>> vars = Variables()
>>> vars.set("x", 5.0)
>>> print(vars.get("x"))  # prints 5.0
>>> print(vars.get("y"))  # prints None

`names()`

Get a list of all variable names.

Returns:

Type	Description
`List[str]`	A list of variable names.

Examples:

>>> vars = Variables()
>>> vars.set("a", 1.0)
>>> vars.set("b", 2.0)
>>> vars.names()  # ['a', 'b']

`remove(name)`

Remove a variable.

Parameters:

Name	Type	Description	Default
`name`	`str`	The variable name to remove (without $ prefix)	required

Returns:

Type	Description
`Union[float, None]`	The variable's previous value, or None if it didn't exist.

Examples:

>>> vars = Variables()
>>> vars.set("x", 5.0)
>>> vars.remove("x")  # returns 5.0
>>> vars.remove("x")  # returns None

`set(name, value)`

Set a variable to a value.

Parameters:

Name	Type	Description	Default
`name`	`str`	The variable name (without $ prefix)	required
`value`	`float`	The variable value	required

Examples:

>>> vars = Variables()
>>> vars.set("threshold", 5.0)

`festl_python.festl_python.Formula`

Signal Temporal Logic (STL) formula.

Use static methods to construct formulas. Formulas can be composed using boolean and temporal operators.

Examples:

>>> # G[0,5](x > 0.5)
>>> phi = Formula.always(0, 5, Formula.gt('x', 0.5))
>>> # (x > 0.3) AND F[0,3](y < 0.8)
>>> phi2 = Formula.and_(
...     Formula.gt('x', 0.3),
...     Formula.eventually(0, 3, Formula.lt('y', 0.8))
... )
>>> # Using variables for dynamic thresholds
>>> phi3 = Formula.gt_var('x', 'threshold')

`always(start, end, child)` `staticmethod`

Create a globally (always) temporal formula.

The formula must hold at all time points in the interval [start, end] relative to the current time.

Parameters:

Name	Type	Description	Default
`start`	`float`	Start of time interval (seconds)	required
`end`	`float`	End of time interval (seconds)	required
`child`	`Formula`	Formula that must hold throughout the interval	required

Returns:

Type	Description
`Formula`	Formula representing: `G[start,end](child)`

Examples:

>>> # For the next 5 seconds, x must be > 0.5
>>> Formula.always(0, 5, Formula.gt('x', 0.5))

`and_(left, right)` `staticmethod`

Create a conjunction (AND) of two formulas.

Parameters:

Name	Type	Description	Default
`left`	`Formula`	First formula	required
`right`	`Formula`	Second formula	required

Returns:

Type	Description
`Formula`	Formula representing: `left ∧ right`

Examples:

>>> Formula.and_(Formula.gt('x', 0.5), Formula.lt('x', 1.0))

`eventually(start, end, child)` `staticmethod`

Create an eventually (finally) temporal formula.

The formula must hold at some time point in the interval [start, end] relative to the current time.

Parameters:

Name	Type	Description	Default
`start`	`float`	Start of time interval (seconds)	required
`end`	`float`	End of time interval (seconds)	required
`child`	`Formula`	Formula that must hold at some point in the interval	required

Returns:

Type	Description
`Formula`	Formula representing: `F[start,end](child)`

Examples:

>>> # Within 3 seconds, y must drop below 0.8
>>> Formula.eventually(0, 3, Formula.lt('y', 0.8))

`false_()` `staticmethod`

Create a constant false formula.

Returns:

Type	Description
`Formula`	Formula that is never satisfied (⊥)

Examples:

>>> Formula.false_()

`gt(signal, value)` `staticmethod`

Create a greater-than atomic predicate.

Parameters:

Name	Type	Description	Default
`signal`	`str`	Name of the signal to compare	required
`value`	`float`	Threshold value to compare against	required

Returns:

Type	Description
`Formula`	Formula representing: `signal > value`

Examples:

>>> Formula.gt('x', 0.5)  # x > 0.5

`gt_var(signal, variable)` `staticmethod`

Create a greater-than atomic predicate with a variable threshold.

The variable value is looked up at runtime from a Variables object, allowing dynamic thresholds that can be updated on-the-fly.

Parameters:

Name	Type	Description	Default
`signal`	`str`	Name of the signal to compare	required
`variable`	`str`	Name of the variable (without $ prefix)	required

Returns:

Type	Description
`Formula`	Formula representing: `signal > $variable`

Note

Requires Incremental algorithm. The Naive algorithm does not support variables.

Examples:

>>> Formula.gt_var('x', 'threshold')  # x > $threshold

`implies(left, right)` `staticmethod`

Create an implication between two formulas.

Parameters:

Name	Type	Description	Default
`left`	`Formula`	Antecedent (condition)	required
`right`	`Formula`	Consequent (result)	required

Returns:

Type	Description
`Formula`	Formula representing: `left → right` (if left then right)

Examples:

>>> # If x > 2.0, then y < 1.0
>>> Formula.implies(Formula.gt('x', 2.0), Formula.lt('y', 1.0))

`lt(signal, value)` `staticmethod`

Create a less-than atomic predicate.

Parameters:

Name	Type	Description	Default
`signal`	`str`	Name of the signal to compare	required
`value`	`float`	Threshold value to compare against	required

Returns:

Type	Description
`Formula`	Formula representing: `signal < value`

Examples:

>>> Formula.lt('x', 0.5)  # x < 0.5

`lt_var(signal, variable)` `staticmethod`

Create a less-than atomic predicate with a variable threshold.

The variable value is looked up at runtime from a Variables object, allowing dynamic thresholds that can be updated on-the-fly.

Parameters:

Name	Type	Description	Default
`signal`	`str`	Name of the signal to compare	required
`variable`	`str`	Name of the variable (without $ prefix)	required

Returns:

Type	Description
`Formula`	Formula representing: `signal < $variable`

Note

Requires Incremental algorithm. The Naive algorithm does not support variables.

Examples:

>>> Formula.lt_var('y', 'limit')  # y < $limit

`not_(child)` `staticmethod`

Create a negation (NOT) of a formula.

Parameters:

Name	Type	Description	Default
`child`	`Formula`	Formula to negate	required

Returns:

Type	Description
`Formula`	Formula representing: `¬child`

Examples:

>>> Formula.not_(Formula.gt('x', 0.5))  # x <= 0.5

`or_(left, right)` `staticmethod`

Create a disjunction (OR) of two formulas.

Parameters:

Name	Type	Description	Default
`left`	`Formula`	First formula	required
`right`	`Formula`	Second formula	required

Returns:

Type	Description
`Formula`	Formula representing: `left ∨ right`

Examples:

>>> Formula.or_(Formula.gt('x', 1.0), Formula.lt('x', 0.0))

`true_()` `staticmethod`

Create a constant true formula.

Returns:

Type	Description
`Formula`	Formula that is always satisfied (⊤)

Examples:

>>> Formula.true_()

`until(start, end, left, right)` `staticmethod`

Create an until temporal formula.

The left formula must hold until the right formula becomes true, and the right formula must become true within the interval [start, end].

Parameters:

Name	Type	Description	Default
`start`	`float`	Start of time interval (seconds)	required
`end`	`float`	End of time interval (seconds)	required
`left`	`Formula`	Formula that must hold until right becomes true	required
`right`	`Formula`	Formula that must eventually become true	required

Returns:

Type	Description
`Formula`	Formula representing: `left U[start,end] right`

Examples:

>>> # x > 0 must hold until y < 0.5 (within 5 seconds)
>>> Formula.until(0, 5, Formula.gt('x', 0), Formula.lt('y', 0.5))

Data Structures

`festl_python.festl_python.MonitorOutputDict`

Bases: TypedDict

Output from a monitor update operation.

`evaluations` `instance-attribute`

List of evaluations, one for each synchronized step. May be empty if data is buffered.

`input_signal` `instance-attribute`

The signal name that was updated.

`input_timestamp` `instance-attribute`

The timestamp of the input that triggered this update.

`festl_python.festl_python.EvaluationDict`

Bases: TypedDict

Result of evaluating a synchronized step.

`outputs` `instance-attribute`

List of output verdicts produced by evaluating this sync step.

`sync_step_signal` `instance-attribute`

Signal name of the synchronized step (may be interpolated).

`sync_step_timestamp` `instance-attribute`

Timestamp of the synchronized step.

`sync_step_value` `instance-attribute`

Value of the synchronized step.

API Reference

Core Functions

festl_python.festl_python.parse_formula(formula_str)

Core Classes

festl_python.festl_python.Monitor

update(signal, value, timestamp)

get_signal_identifiers()

get_variables()

get_specification()

get_algorithm()

get_semantics()

get_synchronization_strategy()

get_temporal_depth()

update_batch(steps)

festl_python.festl_python.Variables

clear()

contains(name)

get(name)

names()

remove(name)

set(name, value)

festl_python.festl_python.Formula

always(start, end, child) staticmethod

and_(left, right) staticmethod

eventually(start, end, child) staticmethod

false_() staticmethod

gt(signal, value) staticmethod

gt_var(signal, variable) staticmethod

implies(left, right) staticmethod

lt(signal, value) staticmethod

lt_var(signal, variable) staticmethod

not_(child) staticmethod

or_(left, right) staticmethod

true_() staticmethod

until(start, end, left, right) staticmethod

Data Structures

festl_python.festl_python.MonitorOutputDict

evaluations instance-attribute

input_signal instance-attribute

input_timestamp instance-attribute

festl_python.festl_python.EvaluationDict

outputs instance-attribute

sync_step_signal instance-attribute

sync_step_timestamp instance-attribute

sync_step_value instance-attribute

`festl_python.festl_python.parse_formula(formula_str)`

`festl_python.festl_python.Monitor`

`update(signal, value, timestamp)`

`get_signal_identifiers()`

`get_variables()`

`get_specification()`

`get_algorithm()`

`get_semantics()`

`get_synchronization_strategy()`

`get_temporal_depth()`

`update_batch(steps)`

`festl_python.festl_python.Variables`

`clear()`

`contains(name)`

`get(name)`

`names()`

`remove(name)`

`set(name, value)`

`festl_python.festl_python.Formula`

`always(start, end, child)` `staticmethod`

`and_(left, right)` `staticmethod`

`eventually(start, end, child)` `staticmethod`

`false_()` `staticmethod`

`gt(signal, value)` `staticmethod`

`gt_var(signal, variable)` `staticmethod`

`implies(left, right)` `staticmethod`

`lt(signal, value)` `staticmethod`

`lt_var(signal, variable)` `staticmethod`

`not_(child)` `staticmethod`

`or_(left, right)` `staticmethod`

`true_()` `staticmethod`

`until(start, end, left, right)` `staticmethod`

`festl_python.festl_python.MonitorOutputDict`

`evaluations` `instance-attribute`

`input_signal` `instance-attribute`

`input_timestamp` `instance-attribute`

`festl_python.festl_python.EvaluationDict`

`outputs` `instance-attribute`

`sync_step_signal` `instance-attribute`

`sync_step_timestamp` `instance-attribute`

`sync_step_value` `instance-attribute`