Temporal Logic Trees

Previous Next

Reference

Temporal Logic Trees (TLTs).

This module wires tuple-encoded temporal logic formulas (see pyspect.logics) to implementation-agnostic set builders (see pyspect.set_builder) and provides a small runtime for constructing, combining, and realizing TLTs against a concrete implementation Impl[R] (see pyspect.impls.*).

Key ideas
  • A TLT wraps:
    • _formula: a TLExpr made of tuples and proposition names
    • _builder: a SetBuilder[R] describing the set semantics
    • _approx: an APPROXDIR flag describing the approximation direction
    • _setmap: a mapping from proposition names to SetBuilder bindings
  • Primitives are registered on the class via TLT.select(...) and used by new_from_formula when building trees.
  • Realization checks requirements (operations and bound props) and then calls the builder with the selected Impl.

APPROXDIR

Bases: Enum

Approximation direction tag for a TLT node.

Values
  • INVALID: semantics cannot be guaranteed (construction error)
  • UNDER: under-approximation (subset of the exact set)
  • EXACT: exact semantics
  • OVER: over-approximation (superset of the exact set)

The enum supports + and * with either another APPROXDIR or an int with the conventional meaning used by the primitive combination rules.

__add__(other)

Combine approximation directions additively, propagating INVALID.

__mul__(other)

Combine approximation directions multiplicatively, propagating INVALID.

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

Impl

Marker base class for concrete implementation backends.

ImplClient

Client-side mixin for declaring and checking required operations.

Clients refer to objects that use an implementation backend. ImplClient ensures to list the names of operations they need the implementation to provide via the class attribute require. This mixin offers methods to: - report which operations are missing on a given Impl - test if an implementation satisfies all requirements - extend or inherit requirement sets dynamically

add_requirements(funcnames)

Add function names to the set of required operations.

inherit_requirements(*others)

Merge requirement sets from other ImplClient-like classes.

is_supported(impl) classmethod

Return True if impl provides all operations listed in require.

missing_ops(impl) classmethod

Return the names of required operations not found on impl.

ImplClientMeta

Bases: type

Metaclass that aggregates required operation names across inheritance.

Classes using this metaclass can declare a tuple[str, ...] in require. During class creation, this metaclass unions all require tuples found in the base classes (that also use ImplClientMeta) with the one declared on the subclass, storing the result back into require.

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.

TLT

Bases: ImplClient[R]

Temporal Logic Tree node parameterized by a concrete set type R.

A TLT encapsulates a tuple-based logic formula, an implementation-agnostic set builder realizing its semantics, an approximation direction, and a mapping from free proposition names to bound SetBuilders.

Construction
  • TLT.select(primitives) must be called to choose available operators.
  • TLT(arg, **where) dispatches based on the type of arg: str -> proposition SetBuilder -> constant set, assigned a unique proposition name tuple(TLExpr)-> formula; recursively constructs children via primitives TLT -> existing tree, optionally updated with new bindings
Realization
  • Call .realize(impl) to obtain an R from an implementation.
  • .assert_realizable() checks missing props/ops and approximation validity.

__new__(arg, **kwds)

Construct a TLT by dispatching on the kind of arg.

__new_from_builder__(sb, **kwds) classmethod

Create a TLT from a constant SetBuilder, assigning it a unique name.

__new_from_formula__(formula, **kwds) classmethod

Create a TLT from a TLExpr by invoking registered primitives.

__new_from_prop__(prop, **kwds) classmethod

Create a TLT from a proposition name, optionally binding it from kwds.

__new_from_tlt__(tlt, **kwds) classmethod

Rebuild a TLT from an existing one, optionally rebinding free props.

__new_init__(formula=..., builder=..., approx=..., setmap=..., times=...) classmethod

Initialize a bare TLT instance with the provided internal fields.

assert_realizable(impl=None)

Validate that this TLT can be realized, optionally against impl.

construct(arg, **kwds) classmethod

Explicit constructor alias to apply usual dispatch rules.

is_realizable(impl=None)

Return True if assert_realizable would succeed.

iter_free()

Iterate names of free (unbound) propositions in this TLT.

iter_frml(formula=None, **kwds)

Yield sub-formulas in post-order; optionally only terminals.

Parameters:

Name Type Description Default
- formula

root to traverse (defaults to self._formula)

 required
- only_terminals

if True, yield only terminal sub-formulas

 required

realize(impl, memoize=False)

Realize this TLT into a concrete set R using impl.

Raises if
  • some proposition is unbound
  • required Impl operations are missing
  • approximation is INVALID

memoize=True is reserved for a future optimization where realized sets may be cached on the node.

select(primitives) classmethod

Select the set of primitive operator implementations for this class.

TLTDebugger

Internal helper to add lightweight debugging and tracing to TLT building.

Use TLT.debug(print=True, indent=2) to enable, and TLT.nodebug() to reset. Arbitrary keyword args starting with '__debug' are collected and forwarded.

debug(**kwds) classmethod

Set debug options.

Supported options (with prefix '__debug_' accepted on wrapper): - print: bool, enable/disable printing - indent: int, indentation level increment per nested step

Pass Ellipsis to unset a debug option.

nodebug() classmethod

Reset debug options to defaults for subsequent constructions.

wrap(msg) classmethod

Decorator to print debug information for TLT construction.

  • Enable with TLT.debug(print=True).
  • Choose indentation size with TLT.debug(indent=...).

Compl(*args)

Return complement of a builder via Impl.complement.

Identity(arg)

Identity helper that constructs a TLT from any TLTLike input.

Inter(*args)

Return intersection of builders via Impl.intersect.

Union(*args)

Return union of builders via Impl.union.

collect_keys(d, *keys, default=...)

Collect a subset of keys from d.

Behavior: - If default is Ellipsis (the default), include only keys that exist in d. - Otherwise, include all requested keys, filling missing ones with default.

Returns: - New dict containing the selected keys.

collect_prefix(d, prefix, remove=False)

Extract and remove items whose keys start with prefix.

Side effect: - Matching items are popped from d.

Parameters: - d: source dictionary (mutated) - prefix: string to match at the start of each key - remove: if True, strip prefix from keys in the returned dict; if False, keep original keys

Returns: - New dict of the extracted items.

flatten(nested, *, sep='_', inplace=False)

Flatten nested mappings into a single level by joining keys with sep.

Example: - {"a": {"b": 1}, "c": 2} -> {"a_b": 1, "c": 2} (sep="_")

Parameters: - nested: mapping to flatten; nested values that are mappings are expanded - sep: string inserted between joined key parts - inplace: if True and nested is mutable, mutate it in place; otherwise return a new dict

Returns: - A flat dict (or the mutated input when inplace=True).

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

iterwin(seq, winlen=1)

Yield fixed-size windows from an indexable sequence by striding.

Equivalent to: zip((seq[i::winlen] for i in range(winlen))). For generic iterables, prefer: zip([iter(seq)] * winlen).

Parameters: - seq: indexable sequence (supports slicing) - winlen: positive window/stride length

Yields: - Tuples of length winlen with elements at positions i mod winlen

prefix_keys(d, prefix)

Return a new dict with prefix added to every key in d.

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.

setdefaults(d, *args, **kwds)

Set default key/value pairs on dict d without overwriting existing keys.

Calling conventions: - Keyword form: setdefaults(d, a=1, b=2) - Dict form: setdefaults(d, {'a': 1, 'b': 2}) - Variadic kv: setdefaults(d, 'a', 1, 'b', 2) # even number of args

Raises: - TypeError/ValueError if the calling convention is invalid.

Logic Fragments TLT Primitives