Polyweave
Repositories
1
 Projects Packages

@polyweave/tla-runner (1.0.6)

Published 2026-07-11 15:33:49 +00:00 by Dvorak

Installation

@polyweave:registry=https://hub.kl1.tenere.ai/api/packages/Polyweave/npm/
npm install @polyweave/tla-runner@1.0.6
"@polyweave/tla-runner": "1.0.6"

About this package

@polyweave/tla-runner

Deterministic Node.js wrappers around the TLA+ toolchain — SANY syntax checking, TLC model checking, TLAPS theorem proving, and Apalache symbolic model checking. Factory pattern, frame-compatible results.

Synopsis

import {
  createSanyRunner,
  createTlcRunner,
  createTlapsRunner,
  createApalacheRunner,
  createTlaRunner,
  runCommand
} from '@polyweave/tla-runner';

const tla = createTlaRunner({
  tlaToolsJar: '/opt/tla/tla2tools.jar'
});

const sanyResult = await tla.validateSyntax('/workspace/spec/MySpec.tla');
const tlcResult  = await tla.runTlc('MySpec', '/workspace/spec/MySpec.cfg');

Install

npm install @polyweave/tla-runner

Why

Each TLA+ tool (SANY, TLC, TLAPS, Apalache) has a different CLI interface and error format. This package normalizes child-process execution with consistent { ok, stdout, stderr, error } result objects. It handles tool-not-installed detection (producing skipped: true instead of crashing) and exposes both per-tool factories and a unified createTlaRunner composite. The low-level runCommand export lets callers shell out to any TLA+ tool.

API

createSanyRunner(options)

Creates a runner for the SANY syntax checker. SANY is run via java -cp <tlaToolsJar> tla2sany.SANY <modulePath>.

Parameter Type Required Default Description
options.javaBin string No 'java' Path to the Java binary
options.tlaToolsJar string Yes — Path to tla2tools.jar
options.defaultTimeoutMs number No 30000 Command timeout in milliseconds

Returns { check(modulePath[, extraArgs[, cwd]]) }.

check(modulePath, extraArgs = [], cwd = undefined):

  • Returns Promise<{ ok: boolean, stdout: string, stderr: string, error?: string }>
  • ok: true for successful syntax check (exit code 0)
  • ok: false for process failure, with error set to the error message

Throws: Error('createSanyRunner requires tlaToolsJar path') if tlaToolsJar is not provided.

Error conditions: If the Java process exits non-zero, ok is false and error contains error.message. Timeouts are surfaced as process errors.

createTlcRunner(options)

Creates a runner for the TLC model checker. TLC is run via java -cp <tlaToolsJar> tlc2.TLC -config <cfgPath> <moduleName>.

Parameter Type Required Default Description
options.javaBin string No 'java' Path to the Java binary
options.tlaToolsJar string Yes — Path to tla2tools.jar
options.defaultTimeoutMs number No 60000 Command timeout in milliseconds

Returns { check(moduleName, cfgPath[, extraArgs[, cwd]]) }.

check(moduleName, cfgPath, extraArgs = [], cwd = undefined):

  • Returns Promise<{ ok: boolean, stdout: string, stderr: string, error?: string }>

Throws: Error('createTlcRunner requires tlaToolsJar path') if tlaToolsJar is not provided.

createTlapsRunner(options)

Creates a runner for the TLAPS theorem prover (TLAPM). TLAPS is run via <bin> --check <modulePath>.

Parameter Type Required Default Description
options.bin string No process.env.TLAPM_BIN || 'tlapm' Path to the tlapm binary
options.timeoutMs number No 180000 Command timeout in milliseconds

Returns { prove({ modulePath, cwd }) }.

prove({ modulePath, cwd }):

  • Returns Promise<{ ok: boolean, stdout: string, stderr: string, skipped: boolean, reason?: string, error?: string }>
  • ok: true for successful proof
  • ok: false, skipped: true when TLAPM is not installed (ENOENT / "not found" in output); reason is 'tlaps_not_installed'
  • ok: false, skipped: false for proof failures; error contains the failure reason

Error conditions: TLAPM binary not found produces { ok: false, skipped: true, reason: 'tlaps_not_installed' } rather than throwing. Process timeouts and non-zero exits produce { ok: false, skipped: false, error }.

createApalacheRunner(options)

Creates a runner for the Apalache symbolic model checker. Apalache is run via <bin> check --inv=TypeOK <moduleName>.

Parameter Type Required Default Description
options.bin string No process.env.APALACHE_BIN || 'apalache-mc' Path to the apalache-mc binary
options.timeoutMs number No 120000 Command timeout in milliseconds

Returns { check({ moduleName, modulePath, cwd }) }.

check({ moduleName, modulePath, cwd }):

  • Returns Promise<{ ok: boolean, stdout: string, stderr: string, skipped: boolean, reason?: string, error?: string }>
  • ok: true for successful check
  • ok: false, skipped: true when Apalache is not installed; reason is 'apalache_not_installed'
  • ok: false, skipped: false for check failures

Error conditions: Apalache binary not found produces { ok: false, skipped: true, reason: 'apalache_not_installed' }. The missing-binary detection checks stdout, stderr, and failed.error.message for not found, No such file, ENOENT, and spawn ... ENOENT patterns.

createTlaRunner(options = {})

Composite factory that creates all four runners at once. Accepts the same options as individual factories plus optional override instances.

Parameter Type Required Default Description
options.sany object No createSanyRunner(options) Pre-constructed SANY runner
options.tlc object No createTlcRunner(options) Pre-constructed TLC runner
options.tlaps object No createTlapsRunner(options) Pre-constructed TLAPS runner
options.apalache object No createApalacheRunner(options) Pre-constructed Apalache runner
(all runner options) No — Passed through to each runner factory

Returns:

{
  sany,            // the SANY runner
  tlc,             // the TLC runner
  tlaps,           // the TLAPS runner
  apalache,        // the Apalache runner
  validateSyntax,  // alias for sany.check
  runTlc,          // alias for tlc.check
  proveTheorem,    // alias for tlaps.prove
  apalacheCheck    // alias for apalache.check
}

runCommand(command, args, timeoutMs, cwd)

Low-level child-process execution via execFile. Used internally by all runners; exported for direct use.

Parameter Type Required Description
command string Yes Executable to run
args string[] Yes Arguments to pass
timeoutMs number Yes Timeout (passed to execFile timeout option)
cwd string No Working directory
  • Returns Promise<{ stdout: string, stderr: string }> on success (exit code 0)
  • Rejects with { error, stdout, stderr } on non-zero exit, timeout, or spawn failure

Frame Protocol

tla-runner does not produce frames. All results are plain objects returned from async functions. The { ok, stdout, stderr, error, skipped } shape matches Polyweave frame-compatibility conventions but results are direct values, not pipeline frames.

Tests

npm test

Runs via node --test test/*.test.js. Covers runner creation (including missing tlaToolsJar throws), command execution, result normalization, timeout handling, and skip detection for missing tool binaries.

Requirements

  • Node.js >= 22.0.0
  • ESM only
  • @polyweave/core (peer)

Dependencies

Development Dependencies

ID Version
@rigor/core *

Keywords

polyweave tla-plus tlaplus tlc sany tlaps apalache formal-verification
Details
npm
2026-07-11 15:33:49 +00:00
29
John Dvorak
SEE LICENSE IN LICENSE
latest
4.6 KiB
Assets (1)
tla-runner-1.0.6.tgz 4.6 KiB
Versions (5) View all
1.0.6 2026-07-11
1.0.5 2026-07-11
1.0.3 2026-07-11
1.0.2 2026-07-11
1.0.1 2026-07-10