README.md

metadata

title: Operon Coalgebra
emoji: ⚙️
colorFrom: indigo
colorTo: blue
sdk: gradio
sdk_version: 6.5.1
app_file: app.py
pinned: false
license: mit
short_description: Composable state machines with bounded equivalence checks

⚙️ Coalgebra -- State Machine Explorer

Build, compose, and compare coalgebraic state machines -- the formal backbone of agent state management in Operon.

What to Try

1. Open the Step-by-Step tab, pick a machine type (e.g. "Counter" or "Modular mod 10"), enter a comma-separated input sequence like 1,2,3,4,5, and click Run Sequence to see the full transition trace.
2. Switch to the Composition tab, select two different machine types and a mode (Parallel or Sequential), then run inputs to watch both machines evolve together.
3. In the Finite-Trace Equivalence tab, pick two machines, enter an input sequence, and click Check Equivalence to see if they produce identical outputs or find the divergence witness.

How It Works

A coalgebra defines a state machine with observation (readout) and transition (update) functions. Machines can be composed in parallel (shared input) or sequentially (output feeds input), and check_bisimulation() compares whether two machines are observationally equivalent over a supplied input sequence. In other words, this demo shows a bounded finite-trace equivalence check rather than an all-input proof.

Learn More

GitHub | PyPI | Paper