Metadata-Version: 2.4
Name: pyspect
Version: 1.1
Summary: Python Specification and Control with Temporal Logic Trees
Project-URL: Homepage, https://kth-sml.github.io/pyspect
Project-URL: Repository, https://github.com/kth-sml/pyspect.git
Project-URL: Issues, https://github.com/kth-sml/pyspect/issues
Author-email: Kaj Munhoz Arfvidsson <kajarf@kth.se>
License: MIT License
        
        Copyright (c) 2024 KTH Smart Mobility Lab
        
        Permission is hereby granted, free of charge, to any person obtaining a copy
        of this software and associated documentation files (the "Software"), to deal
        in the Software without restriction, including without limitation the rights
        to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
        copies of the Software, and to permit persons to whom the Software is
        furnished to do so, subject to the following conditions:
        
        The above copyright notice and this permission notice shall be included in all
        copies or substantial portions of the Software.
        
        THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
        IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
        FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
        AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
        LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
        OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
        SOFTWARE.
License-File: LICENSE
Keywords: control,reachability,temporal logic
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3 :: Only
Requires-Python: >=3.12
Requires-Dist: plotly
Provides-Extra: docs
Requires-Dist: mkdocs-shadcn==0.9.5; extra == 'docs'
Requires-Dist: mkdocs==1.6.1; extra == 'docs'
Requires-Dist: mkdocstrings-python==1.18.2; extra == 'docs'
Requires-Dist: pymdown-extensions==10.16.1; extra == 'docs'
Provides-Extra: hj-reachability
Requires-Dist: hj-reachability<0.8,>=0.7; extra == 'hj-reachability'
Provides-Extra: zonoopt
Requires-Dist: zonoopt; extra == 'zonoopt'
Description-Content-Type: text/markdown

# pyspect

**Compile temporal-logic specs into reachability programs.**

pyspect lets you write specifications once, then realize them against interchangeable backends (e.g., Hamilton–Jacobi level sets or Hybrid Zonotopes) via **Temporal Logic Trees (TLTs)**. The toolbox performs interface + approximation checks so your output set remains sound.

> **TL;DR**: You express *what* to verify in logic; implementations decide *how* to compute the sets. pyspect bridges the two with TLTs and small, pluggable operator primitives. See paper *"pyspect: An Extensible Toolbox for Automatic Construction of Temporal Logic Trees via Reachability Analysis."*

## Why pyspect

- **Decouple** logic, set semantics, and numerics: write specs once, compare multiple reachability methods side-by-side.
- **Method-agnostic** and easily extensible: currently supports HJ (level sets) and HZ-based (hybrid zonotopes) reachability within the same interface.
- **Correct by construction**: static checks for **approximation direction** (over/under) and backend capability before any heavy computation, avoiding invalid evaluation of the spec.

## Getting started

[Read our docs here!](https://kth-sml.github.io/pyspect)

### Installation

```bash
pip install pyspect

# Example to install with implementation-specific dependencies (Optional)
pip install pyspect[hj_reachability]

# From source
python -m venv .venv && source .venv/bin/activate
pip install -e ".[hj_reachability]"
```

### Program

```python
from pyspect.logics import *
from pyspect.tlt import TLT, ContLTL
from pyspect.impls.hj_reachability import TVHJImpl

# 1) Pick primitives/fragment
TLT.select(ContLTL) # Continuous-time LTL

# 2) Write the spec once
phi = UNTIL(AND(NOT('D'), 'corridor'), 'goal')   # task: avoid D, stay in corridor, then reach goal

# 3) Bind propositions later via set builders
tlt = TLT(phi, where={
    'D': Union(BoundedSet(...), BoundedSet(...)),
    'corridor': BoundedSet(...),
    'goal': HalfSpaceSet(...),
})

# 4) Realize on a backend
impl = TVHJImpl(...)    # Each implementation can have their own settings
Phi = tlt.realize(impl) # The satisfaction set in the backend’s representation
```

## Cite

If you use pyspect in academic work, please cite:
```
@inproceedings{11311974,
	title = {pyspect: An Extensible Toolbox for Automatic Construction of Temporal Logic Trees via Reachability Analysis},
	issn = {2576-2370},
	url = {https://ieeexplore.ieee.org/abstract/document/11311974},
	doi = {10.1109/CDC57313.2025.11311974},
	shorttitle = {pyspect},
	pages = {6911--6918},
	booktitle = {2025 {IEEE} 64th Conference on Decision and Control ({CDC})},
	author = {Arfvidsson, Kaj Munhoz and Hadjiloizou, Loizos and Jiang, Frank J. and Johansson, Karl H. and Mårtensson, Jonas},
	date = {2025-12},
}
```

## Paper Examples

For paper examples, checkout branches:

- [`cdc24`](https://github.com/KTH-SML/pyspect/tree/cdc24/examples): Intersection & Parking
- [`cdc25`](https://github.com/KTH-SML/pyspect/tree/cdc25/examples): Double Integrator with HJ & HZ


<!--

## Core ideas

### I. Logic as a tiny AST
1. Write formulas (e.g. LTL) as lightweight, typed tuples: 
   `('AND', a, b)`, `('NOT', a)`, `('UNTIL', phi, psi)`, etc.
2. Symbols (propositions) are bound later via a mapping `M: AP -> SetBuilder`.

### II. Temporal Logic Trees (TLTs)
> A **TLT** mirrors formula structure with set/reachability nodes, verifying temporal logic using reachability.

1. `TLT.select(Q)` chooses a set of primitives `Q` matching the temporal logic fragment. **Key:** the primitives operationalize the fragment (how we evaluate).
2. `TLT(spec).realize(impl)` constructs and executes a reachability program verifying `spec`.

### III. Implementations

...

### IV. Set builders (lazy, backend-agnostic)
1. **SetBuilder** objects (`B: Impl -> R`) describe sets *implicitly* and are evaluated only when realized by an implementation (“dependency injection”).
2. pyspect provides common combinators: `Union`, `Inter`, `Compl`, plus constructors like `BoundedSet(…)`. (Backends/Implementations supply the actual set operations.)

-->
