---
name: reference-spot-omega-automaton-install-2026-07-03
description: Spot 2.15.1 (LRDE/EPITA ω-automaton library) install protocol on WSL Ubuntu-24.04 + Rei-project 統合 pattern (Windows Python subprocess 経由 CLI 呼び出し)
metadata: 
  node_type: memory
  type: reference
  originSessionId: aee9a4d4-1e0c-46fc-a09d-0f70575aaf8f
---

# Spot ω-automaton install protocol (Rei-project reference, 2026-07-03 established)

## Spot 概要

- **Spot** (LRDE/EPITA) = ω-automaton library、 LTL formula → Büchi automaton 変換 (`ltl2tgba`)、 automaton operations (`autfilt`: product / complement / emptiness / universality) 等。 C++ + Python bindings。
- 数学問題への application: **限定的** ([[project-step1251-1252-collatz-buchi-mod25-spot-2026-07-03]] per):
  - (a) 数学 formalization infrastructure — 中程度 (Coq/Lean coinductive types 系)
  - (b) algorithmic sub-decidability — 有効 (Presburger, LTL model checking)
  - (c) 検証済範囲拡張 — 有効
  - (d) 具体的 conjecture 決着 — 不十分
- Rei-project では **STEP 1178 automata route wall の precise map 化 tool** として位置付け、 「Collatz 解ける」 期待ではない

## Install path (Rei-project WSL setup 実測 record)

### 前提
- Rei-project Windows 11 host
- WSL2 Ubuntu-22.04 (memory 上 STEP 1052 で LMFDB fetch 等で活用済) と Ubuntu-24.04 の 2 distro install 済 (Docker Desktop も並存)
- Both distro に **LRDE 公式 repo (`http://www.lrde.epita.fr/repo/debian stable/`)** が既に登録済 (前 session で追加されたと思われる)

### 選択 distro: Ubuntu-24.04 (noble)
Ubuntu 22.04 (jammy) では libc 2.35 / libstdc++ 12.3 / Python 3.10 が Spot 2.15 依存 (libc ≥ 2.38 / libstdc++ ≥ 14 / Python ≥ 3.13) と mismatch → Ubuntu-24.04 (libc 2.39 / libstdc++ 14 / Python 3.12) に switch。

### 初回 setup (Ubuntu-24.04)
```powershell
wsl -d Ubuntu-24.04
```
初回起動時 UNIX user 名 (小文字英数字) + password prompt。 Ubuntu-22.04 と別 user でも同 user でも可。

### Install command
```bash
sudo apt update

# ★ python3-spot は Python 3.13 要求で Ubuntu 24.04 (Python 3.12) 上不可、 CLI のみ install
sudo apt install -y spot

# Verify
ltl2tgba --version
```

**Expected output**: `ltl2tgba (spot) 2.15.1`

## Rei fact-check 実測 evidence (2026-07-03 時点)

### Ubuntu default repo での spot availability

| Distro | main | universe | LRDE repo (追加時) |
|---|---|---|---|
| Ubuntu 22.04 (jammy) | ✗ | ✗ | 2.15 系 (libc mismatch) |
| Ubuntu 24.04 (noble) | ✗ | ✗ | 2.15 系 (Python bindings のみ mismatch) |
| Ubuntu 24.10+ / Debian trixie | ? | (要確認) | 2.15 (fully compatible) |

★ **Ubuntu 22.04 / 24.04 default repo に spot package 不存在** = 実測 evidence (私 Claude Code の hallucination 「spot 2.10 or 2.11 available」 を 藤本さん実測で修正した pattern)

### LRDE repo が提供する version 依存 pattern

| Spot version | libc 要求 | libstdc++ 要求 | Python 要求 |
|---|---|---|---|
| 2.11.6 | ≥ 2.14 | ≥ 9 | 3.9 only |
| 2.13.0 | ≥ 2.32 | ≥ 11 | 3.11 only |
| 2.14.0 | ≥ 2.32 | ≥ 11 | 3.11 only |
| 2.14.3.16+ | ≥ 2.32 | ≥ 13.1 | 3.13 only |
| 2.15.1 | ≥ 2.38 | ≥ 14 | 3.13 only |

★ **Python 3.12 対応 python3-spot version は LRDE repo 内に空白**。 python3-spot install はいずれか version でも Ubuntu 24.04 (Python 3.12) では不可。 **spot CLI 単独なら 2.14.0+ が Ubuntu 24.04 で clean install 可能**。

## Rei-project 統合 pattern (subprocess CLI 呼び出し)

**Python bindings SKIPPED** (Python 3.13 不足)、 Spot CLI を subprocess で呼ぶ pattern:

```python
import subprocess
WSL_DISTRO = "Ubuntu-24.04"

def run_spot(cmd: list[str], stdin_data: str | None = None, timeout_s: int = 30) -> tuple[int, str, str]:
    full = ["wsl.exe", "-d", WSL_DISTRO, "--"] + cmd
    proc = subprocess.run(
        full, input=stdin_data, text=True, capture_output=True,
        timeout=timeout_s, encoding="utf-8",
    )
    return proc.returncode, proc.stdout, proc.stderr

# Example: LTL → Büchi
rc, hoa, err = run_spot(["ltl2tgba", "--hoaf", "GF acc"])

# Example: HOA emptiness check
rc, out, err = run_spot(["autfilt", "--is-empty"], stdin_data=hoa_str)
```

### HOA (Hanoi Omega-Automata) v1 format 例
```
HOA: v1
name: "my-automaton"
States: N
Start: initial_state
AP: 1 "acc"
Acceptance: 1 Inf(0)
acc-name: Buchi
properties: trans-labels explicit-labels state-acc
--BODY--
State: 0 {0}  /* {0} = accepting */
  [t] 1       /* [t] = true (unconditional transition) */
  [t] 2
State: 1
  [t] 0
--END--
```

## Disk cost
- spot (CLI) 2.15.1 + graphviz + libs = **23.5 MB installed**
- Rei-project 依存の他 tool と比較して **negligible** (Mathlib cache ~7 GB / CollatzRei build ~2 GB / Rust toolchain ~2 GB)

## Uninstall (念のため)
```bash
sudo apt remove --purge -y spot && sudo apt autoremove -y
```

## Common Spot CLI use cases (Rei-project scope)

| Command | 用途 |
|---|---|
| `ltl2tgba 'GF a'` | LTL formula → Büchi automaton (HOA output with `--hoaf`) |
| `autfilt --stats='%s,%e,%a,%d'` | state count / edge count / acc-set count / deterministic (0 or 1) |
| `autfilt --is-empty` | ω-language emptiness check (exit 0=empty, 1=non-empty) |
| `autfilt --is-universal` | universal language check |
| `autfilt --intersect=<lang.hoa>` | product with another automaton |
| `autfilt --complement` | Büchi complementation |
| `autfilt --dot` | GraphViz DOT output for visualization |

## Rei-project usage record
- STEP 1252 で initial integration + STEP 1178 automata wall precise articulation Spot side confirmation ([[project-step1251-1252-collatz-buchi-mod25-spot-2026-07-03]])
- Future ω-language operations (product / complement / emptiness) は同 pattern で拡張可能
- 「大 tool 導入 = problem 解決」 SF-inflation 回避、 「壁の地図の精密化」 用途に留める

## Related memory
- [[project-step1251-1252-collatz-buchi-mod25-spot-2026-07-03]]
- [[feedback-evaluation-symmetry-principle]] (私 3 連続 fact-check 不足 origin session)
- STEP 930 (Büchi-25 × Q33 coset-level 95% formalization、 全 orbit ではない)
- STEP 1178 (Collatz frontier 7 routes wall audit、 route 5 automata world-open)