TLT Primitives

Previous Next

Reference

Primitives for temporal logic trees (TLTs).

This module defines: - primitive: a decorator class to register TLT primitives tied to tuple-form formulas - Derived connectives built from equivalences (e.g., Minus, Implies, Eventually) - Different sets of primitive TLTs for propositional and temporal operators

Concepts
  • A primitive is specified by a TLExpr (operator head and argument names). Decorating a factory function with @primitive(("OP", "x", "y")) binds the function to that operator and returns a single-element set of a primitive TLT. Union of such sets forms the underlying grammar/logic fragment.
  • A decorated factory should return (SetBuilder[R], APPROXDIR) which specify how to realize the set semantics and the approximation direction the primitive contributes. The decorator constructs a TLT by:
    • Substituting child formulas into the operator head
    • Composing the children's set maps
    • Propagating requirements/constraints

AppliedSet

Bases: SetBuilder[R]

Defer a call to a function f where args are realized builders.

The function is specified by name funcname and looked up on the Impl at realization, i.e. Impl.<funcname>(*args), or a direct lambda if func is a callable.

  • Accumulates required Impl methods from children and adds funcname.
  • Propagates and de-duplicates children's free variables.
  • On realization, calls child builders first, then invokes the Impl method.
  • Wraps child exceptions to pinpoint which argument failed.

HalfSpaceSet

Bases: SetBuilder[R]

Half-space described by the normal and offset of a hyperplane.

Note: The set is in the direction of the normal.

Parameters:

Name Type Description Default
normal list[float]

coefficients along each axis

 required
offset list[float]

offsets along each axis

 required
axes list[Axis]

axis indices (or str if using AxesImpl) in the Impl's coordinate system

 required
kwds Any

forwarded to Impl.halfspace

 {}
Requires
  • Impl.halfspace(normal, offset, axes, ...) -> R

ReferredSet

Bases: SetBuilder[R]

Reference a named free variable resolved from the realization mapping.

ReferredSet('X')(impl, X=some_builder) realizes to some_builder(impl, ...). This is useful in two ways: 1. We can be lazy when constructing the call tree, i.e. we allow users to define which builder to use at a later stage. 2. This essentially allow variables to exist within the call tree which avoids having to reconstruct an entire tree in some cases.

Set

Bases: SetBuilder[R]

Wrap a concrete set value R and return it unchanged on realization.

SetBuilder

Bases: ImplClient[R]

Abstract base for all set builders.

Responsibilities
  • Be callable with an implementation Impl[R] to produce a concrete set R.
  • Track required Impl operations through ImplClient.
  • Track free variable names (see ReferredSet).

Subclasses should implement __call__, which is called to realize the sets.

uid property

Stable hexadecimal id derived from the object hash.

__repr__()

Return a compact identifier for the builder instance.

primitive

Decorator class for declaring TLT primitives.

Usage: - Specify the operator form and argument names: @primitive(AND('_1', '_2')) def And(_1: TLTLike[R], _2: TLTLike[R]) -> tuple[SetBuilder[R], APPROXDIR]: ... The decorator registers a callable under the operator head ("AND") that, when invoked with TLTLike arguments, returns a constructed TLT[R]. The arguments to the decorated function are mapped by name from the provided operands by order as they appear in the formula. The formula must consist of only a single connective.

Notes: - The decorated function receives named arguments matching the formula's parameter names (strings in the TLExpr tail) and should return the pair (SetBuilder[R], APPROXDIR) describing the primitive's semantics and its approximation contribution.

__call__(func)

Decorator entry: wrap func to build a TLT node for this primitive.

The wrapped function: - Validates/assembles the operator formula with the child formulas - Calls func with named arguments mapped from the provided children - Constructs a TLT using the returned (SetBuilder, APPROXDIR) - Merges children's set maps and inherits requirements

Returns:

Type Description
idict[str, PrimitiveFunc]

idict mapping {connective: function}

__init__(formula)

Bind this primitive to a formula shape.

Parameters:

Name Type Description Default
formula TLExpr

a TLExpr operator tuple whose head is the operator name and whose tail elements are unique proposition names (str)

 required

define_as(equiv)

Define this operator via a pure logical equivalence.

This produces a thin wrapper that expands calls to this operator into the provided equivalent TLExpr, without supplying a new SetBuilder.

Constraints: - equiv must be well-formed - equiv must reference exactly the same set of proposition names as the original operator formula

Returns:

Type Description
idict[str, Callable[..., TLT]]

idict mapping {connective: expansion_function}

And(_1, _2)

Conjunction (intersection).

Compl(*args)

Return complement of a builder via Impl.complement.

Falsify()

Bottom/falsehood (∅).

Inter(*args)

Return intersection of builders via Impl.intersect.

Next(_1)

Next/predecessor set.

Not(_1)

Logical negation (complement).

Or(_1, _2)

Disjunction (union).

Union(*args)

Return union of builders via Impl.union.

Until(_1, _2)

Until (reachability): hold _1 until _2 is reached.

get_malformed(formula)

Return the first malformed subexpression, or None if well-formed.

Parameters:

Name Type Description Default
- formula

TLExpr to check

 required

Returns:

Type Description
Optional[TLExpr]
  • None if the expression is well-formed; otherwise the first offending subexpression
Well-formedness rules
  • Propositions: non-empty str, or any SetBuilder instance
  • Operator tuples: length 1..3, head must be str, and all arguments recursively valid

get_props(formula)

Collect proposition names appearing in a formula.

  • String terminals are treated as proposition names and included.
  • SetBuilder terminals are constants and contribute no proposition names.
  • Operator tuples are traversed recursively.

Parameters: - formula: TLExpr to inspect

Returns: - Set of unique proposition names found in formula

replace_prop(formula, prop, expr)

Replace all occurrences of proposition prop with expr.

Parameters:

Name Type Description Default
- formula

operator tuple (TLOpNullary/Unary/Binary)

 required
- prop

proposition name to replace

 required
- expr

replacement sub-expression

 required

Returns:

Type Description
TLExpr
  • New TLExpr with replacements applied
Notes
  • This function expects formula to be an operator tuple (not a raw str or SetBuilder). It descends recursively and replaces terminals that match prop.
  • For nullary or terminal positions, if the terminal equals prop, it is replaced by expr.
Temporal Logic Trees hj_reachability