Metadata-Version: 2.4
Name: tlakit
Version: 0.0.1
Summary: A Python and notebook client for the TLA+ toolchain
Project-URL: Homepage, https://github.com/LUC-AI4FM/tlakit
Project-URL: Repository, https://github.com/LUC-AI4FM/tlakit
Project-URL: Issues, https://github.com/LUC-AI4FM/tlakit/issues
Project-URL: Try it in a browser, https://tlakit.pages.dev
Author: Eric Spencer
License: MIT
Keywords: formal-methods,jupyter,model-checking,tla+,tlaplus,tlc
Classifier: Development Status :: 3 - Alpha
Classifier: Framework :: Jupyter
Classifier: Intended Audience :: Developers
Classifier: Intended Audience :: Education
Classifier: Intended Audience :: Science/Research
Classifier: License :: OSI Approved :: MIT License
Classifier: Programming Language :: Python :: 3
Classifier: Programming Language :: Python :: 3.10
Classifier: Programming Language :: Python :: 3.11
Classifier: Programming Language :: Python :: 3.12
Classifier: Programming Language :: Python :: 3.13
Classifier: Topic :: Scientific/Engineering
Classifier: Topic :: Software Development :: Testing
Classifier: Typing :: Typed
Requires-Python: >=3.10
Requires-Dist: platformdirs>=4.0
Provides-Extra: dev
Requires-Dist: fastapi>=0.110; extra == 'dev'
Requires-Dist: httpx>=0.27; extra == 'dev'
Requires-Dist: ipykernel>=6.0; extra == 'dev'
Requires-Dist: jupyter-client>=7.0; extra == 'dev'
Requires-Dist: nbclient>=0.9; extra == 'dev'
Requires-Dist: nbmake>=1.5; extra == 'dev'
Requires-Dist: pytest-timeout>=2.0; extra == 'dev'
Requires-Dist: pytest>=8.0; extra == 'dev'
Requires-Dist: uvicorn>=0.27; extra == 'dev'
Provides-Extra: kernel
Requires-Dist: ipykernel>=6.0; extra == 'kernel'
Requires-Dist: jupyter-client>=7.0; extra == 'kernel'
Provides-Extra: notebook
Requires-Dist: ipython>=8.0; extra == 'notebook'
Provides-Extra: serve
Requires-Dist: fastapi>=0.110; extra == 'serve'
Requires-Dist: pydantic>=2.0; extra == 'serve'
Requires-Dist: uvicorn>=0.27; extra == 'serve'
Description-Content-Type: text/markdown

# tlakit

[![CI](https://github.com/LUC-AI4FM/tlakit/actions/workflows/ci.yml/badge.svg)](https://github.com/LUC-AI4FM/tlakit/actions/workflows/ci.yml)

A Python and notebook client for the TLA+ toolchain.

TLA+ has good tools — TLC, SANY, the TLA+ Debugger, the animation modules. None
of them are reachable from Python, and none of them compose with a notebook.
tlakit is the missing client. It does not reimplement any of them.

```python
import tlakit

spec = tlakit.load("Microwave.tla")
result = spec.check(invariants=["Safety"])

if not result.ok:
    print(result.outcome)                       # Outcome.INVARIANT_VIOLATION
    print(result.trace.delta(3))                # frozenset({'radiation'})
    result.trace.to_dataframe(flatten=True)     # nested records as columns
```

Sweep a constant and get the smallest configuration that breaks:

```python
sweep = spec.sweep({"Servers": [3, 4, 5]}, invariants=["Inv"],
                   workers=3, heap="2G")
sweep.first_failure().constants     # {'Servers': 4}
sweep.to_dataframe()                # one row per configuration
```

## As a Jupyter kernel

```bash
pip install "tlakit[kernel]"
python -m tlakit.kernel.install
```

Then pick **TLA⁺ (tlakit)** from Jupyter's kernel list and write TLA+ directly —
no magics, no Python wrapper:

```tla
---- MODULE Microwave ----
EXTENDS Naturals
VARIABLES door, radiation
...
====
```

```
SPECIFICATION Spec
INVARIANT Safety
```

Python still works in the same notebook, which is the point of building on
IPython rather than replacing it:

```python
result.trace.to_dataframe()
```

## Or as magics in an ordinary Python kernel

```
%load_ext tlakit
```

```
%%tla Microwave
---- MODULE Microwave ----
...
====
```

```
%%tlc Microwave
SPECIFICATION Spec
INVARIANT Safety
```

## Status

M1 is complete: `CliRunner`, normalized results, `%%tla` / `%%tlc` magics,
and static HTML rendering of counterexamples and diagnostics. See
`docs/superpowers/specs/` for the design and `docs/superpowers/plans/` for the
implementation plan.

## Requirements

- Python 3.10+
- Java
- TLA+ tools **v1.8.0 or newer** — tlakit runs TLC with `-dumpTrace json`;
  v1.7.4 (TLC 2.19) does not have that option

Fetch the pinned, checksummed tools:

```bash
python -m tlakit.install
```

Or point tlakit at jars you already have with
`TLAKIT_TLA2TOOLS=/path/to/tla2tools.jar`.
`TLAKIT_COMMUNITY_MODULES` optionally locates `CommunityModules-deps.jar`, which
`SVG.tla` and `Json.tla` need.

## License

MIT
