tla_eval/lib.rs
1//! Evaluate TLA+ at concrete states.
2//!
3//! The question this crate answers is not "what states can this specification
4//! reach?" but "does this predicate hold *here*?" — where *here* is a state, or
5//! a pair of states for an action. That is enough to decide the obligations a
6//! refinement oracle actually has, and unlike reachability it needs no search.
7//!
8//! ```
9//! use std::collections::BTreeMap;
10//! use tla_eval::{Evaluator, Spec, Value};
11//!
12//! let spec = Spec::parse(
13//! "---- MODULE Counter ----
14//! EXTENDS Naturals
15//! CONSTANT Limit
16//! VARIABLE n
17//! Init == n = 0
18//! Next == n < Limit /\\ n' = n + 1
19//! ========================",
20//! )?;
21//!
22//! let constants = BTreeMap::from([("Limit".to_string(), Value::Int(3))]);
23//! let eval = Evaluator::new(&spec, constants)?;
24//!
25//! let at = |n| BTreeMap::from([("n".to_string(), Value::Int(n))]);
26//! assert!(eval.holds_at("Init", &at(0))?);
27//! assert!(eval.step_allowed("Next", &at(0), &at(1))?);
28//! assert!(!eval.step_allowed("Next", &at(0), &at(2))?);
29//! # Ok::<(), tla_eval::Error>(())
30//! ```
31
32mod builtin;
33mod diagnose;
34mod error;
35mod eval;
36mod spec;
37mod value;
38
39pub use diagnose::Blocked;
40pub use error::{Error, Result};
41pub use eval::{Evaluator, MAX_ELEMENTS, State};
42pub use spec::{Directory, Modules, NoModules, Spec};
43pub use value::{Infinite, Value};