EARS-TLA

EARS-TLA is a Scala 3 project that parses EARS-TLA specifications and generates TLA+ modules.

The goal is to make translation from structured requirements to formal models deterministic and mechanical: language constructs are explicit enough that the compiler can map them directly to TLA+ without heuristic interpretation.

---

What this project does

At a high level, the project implements a pipeline:

1. Parse EARS-TLA text into a typed AST
2. (Future) validate and desugar domain extensions
3. Generate TLA+ source from the AST

Current implementation includes:

• Core AST definitions under earstla.ast
• Parser combinators based on cats-parse
• TLA+ renderer/generator
• Sample executable in Main.scala
• Test suite that parses example .earstl files and writes generated .tla output

---

Tech stack

• Scala: 3.7.3
• Build tool: sbt
• Parser library: org.typelevel:cats-parse:1.1.0
• Test framework: org.scalameta:munit:1.1.0

See dependencies in build.sbt.

---

Repository structure

src/main/scala/
  Main.scala                       # Demo entrypoint
  earstla/
    ast/                           # Core ADTs (Specification, Action, Property, etc.)
    parser/EarsTlaParser.scala     # EARS-TLA parser
    codegen/TlaPlusGenerator.scala # TLA+ generator
    ext/DomainExtension.scala      # Domain-extension abstraction (scaffold)

src/test/scala/
  GenerateTlaPlusSuite.scala       # Integration-style generation test

src/test/resources/
  examples/*.earstl                # Input specifications
  generated/*.tla                  # Generated output written by tests

docs/
  earstl.md                        # Language/specification design document

---

Quick start

Prerequisites

• JDK 17+ (recommended for modern Scala toolchains)
• sbt installed

Build and run

sbt compile
sbt test
sbt run

What these commands do:

• sbt compile: compiles parser, AST, and code generator
• sbt test: parses test examples and generates TLA+ into src/test/resources/generated
• sbt run: runs Main, which parses an embedded example spec and prints generated TLA+

---

Language support (current)

The core parser supports the major EARS-TLA blocks, including:

• SYSTEM
• USES
• STATE
• INITIALLY
• ACTION with optional WHEN and PROVIDED
• THEN ... AND ... effect clauses
• Frame clauses:
  • UNCHANGED ...
  • ONLY CHANGES ...
• PROPERTY ... [safety|liveness|invariant]
• FAIRNESS with WEAK and STRONG

Expression support includes:

• Primitive and structured type expressions (boolean, natural, integer ranges, enums, sets, sequences, maps, records, named types)
• Value expressions (identifiers, ints, strings, booleans, arithmetic + / -, size of, empty set/sequence)
• Conditions (is, is not, comparisons, contains, boolean connectives, FOR EACH)
• Event patterns (occurs, is received, is submitted, changes, changes from ... to ...)
• Temporal forms (ALWAYS, NEVER, EVENTUALLY, LEADS TO, bounded leads-to, IF ... THEN EVENTUALLY ...)

---

TLA+ generation behavior

The generator currently emits:

• Module header and standard EXTENDS section
• State variables (VARIABLE lines) and tuple vars
• TypeInvariant
• Init
• One TLA+ action per EARS-TLA ACTION
• Next as disjunction of actions
• Temporal property definitions
• Spec assembled from Init /\ [][Next]_vars plus fairness constraints

Frame handling:

• UNCHANGED x, y maps directly to UNCHANGED <<x, y>>
• ONLY CHANGES x, y computes unchanged variables as complement over declared state variables

---

Running examples

The test suite reads files from:

• src/test/resources/examples/*.earstl

and writes generated modules to:

• src/test/resources/generated/*.tla

To regenerate outputs:

sbt test

Current examples include:

• OrderProcessing.earstl (core language)
• two-phase-commit.earstl (extension-oriented)
• rag-agent.earstl (extension-oriented)
• escrow-payment.earstl (extension-oriented)

Note: extension-oriented examples are useful for future work and may not fully parse until extension parsers/desugarers are implemented.

---

Project status

This project is in active/early development.

Implemented now:

• Core language AST
• Core parser
• Core TLA+ generator
• Basic integration-style generation test

Planned / partial scaffolding:

• Validation pass (e.g., completeness checks)
• Domain extensions (DistributedSystems, AgentWorkflows, FinancialTransactions)
• Full compile pipeline with extension resolution and desugaring

See docs/earstl.md for the complete language design and roadmap context.

---

How to contribute

1. Read docs/earstl.md for language intent and mapping rules.
2. Keep parser and generator changes aligned with deterministic translation principles.
3. Add/adjust .earstl examples and corresponding generated expectations when introducing features.
4. Add tests for both success and failure cases, especially around grammar edge conditions.

---

License

No license file is currently present in this repository. Add one if you plan to publish or distribute the project.