Crate tla_eval 

Evaluate TLA+ at concrete states.

The question this crate answers is not “what states can this specification reach?” but “does this predicate hold here?” — where here is a state, or a pair of states for an action. That is enough to decide the obligations a refinement oracle actually has, and unlike reachability it needs no search.

use std::collections::BTreeMap;
use tla_eval::{Evaluator, Spec, Value};

let spec = Spec::parse(
    "---- MODULE Counter ----
     EXTENDS Naturals
     CONSTANT Limit
     VARIABLE n
     Init == n = 0
     Next == n < Limit /\\ n' = n + 1
     ========================",
)?;

let constants = BTreeMap::from([("Limit".to_string(), Value::Int(3))]);
let eval = Evaluator::new(&spec, constants)?;

let at = |n| BTreeMap::from([("n".to_string(), Value::Int(n))]);
assert!(eval.holds_at("Init", &at(0))?);
assert!(eval.step_allowed("Next", &at(0), &at(1))?);
assert!(!eval.step_allowed("Next", &at(0), &at(2))?);

Structs

Blocked

How close one action came to permitting the step.

Directory

Modules as <directory>/<Name>.tla, which is how TLA+ tools find them.

Evaluator

NoModules

No modules beyond the one given and whatever it declares inside itself.

Spec

A specification: a root module together with every module it reaches.

Enums

Error

Infinite

Value

A TLA+ value.

Constants

MAX_ELEMENTS

Nothing enumerable is materialized beyond this many elements. The bound exists so a SUBSET or [S -> T] over an unexpectedly large set reports a limit instead of exhausting memory.

Traits

Modules

Where the source of a module named in EXTENDS or INSTANCE comes from.

Type Aliases

Result

State

A binding of every variable the specification declares.