Reticulate

A Python tool for lattice analysis of session type state spaces.

Given a session type definition, Reticulate constructs the state-space labeled transition system, computes its SCC quotient, checks whether the quotient forms a bounded lattice, and optionally generates a Hasse diagram. Part of the Session Types as Algebraic Reticulates research project.

Requirements

• Python 3.11+
• Optional: graphviz Python package + system binary (for Hasse diagram rendering)

Installation

# Install from source
pip install .

# With visualisation support
pip install .[viz]

# Development (editable + pytest)
pip install -e .[dev]

This installs the session2lattice command (plus aliases s2l, sess2lat, lattice-check, bica).

Usage

Command Line

# Basic lattice check
session2lattice "rec X.&{a:X, b:end}"

# Show version
session2lattice --version

# Generate DOT output for Hasse diagram
session2lattice --dot "rec X.&{a:X, b:end}"

# Render Hasse diagram to file
session2lattice --hasse output "&{m: end, n: end}"

# Check distributivity (Birkhoff classification)
session2lattice --distributive "(&{a: end} || &{b: end})"

# Pretty-print lattice tables (states, transitions, meet/join)
session2lattice --lattice "&{a: end, b: end}"

# Generate JUnit test source
session2lattice --test-gen --class-name FileHandle "&{open: &{read: end, close: end}}"

# All options
session2lattice --help

As a Library

from reticulatep import parse, build_statespace, check_lattice

# Parse a session type
st = parse("rec X.&{a:X, b:end}")

# Build state space
ss = build_statespace(st)

# Check lattice property
result = check_lattice(ss)
print(f"Is lattice: {result.is_lattice}")
print(f"States: {len(ss.states)}, SCCs: {len(set(result.scc_map.values()))}")

Session Type Grammar

S  ::=  &{ m1 : S1 , ... , mn : Sn }    -- branch (external choice)
     |  +{ l1 : S1 , ... , ln : Sn }    -- selection (internal choice)
     |  ( S1 || S2 )                     -- parallel composition
     |  rec X . S                        -- recursion
     |  X                                -- variable
     |  end                              -- terminated

Unicode alternatives: ⊕ for +, ∥ for ||, μ for rec.

Modules

Core

Analysis

Multiparty

Output

Tests

# Run all tests (2,481 tests)
python -m pytest tests/ -v

# Run specific test module
python -m pytest tests/test_lattice.py -v

# Run benchmarks only
python -m pytest tests/benchmarks/ -v

Benchmarks

79 binary and 24 multiparty real-world protocol benchmarks are included in tests/benchmarks/, spanning networking (SMTP, HTTP, DNS, TLS, MQTT), databases (JDBC, Redis), distributed systems (Raft, 2PC, Saga), security (OAuth 2.0), AI agents (MCP, A2A), and more. All form bounded lattices.

Reference

This tool accompanies the paper:

A. Z. Caldeira and V. T. Vasconcelos. "Session Type State Spaces Form Lattices." ICE 2026.

License

MIT License. See LICENSE.