tla_eval/
spec.rs

1use std::collections::{BTreeMap, BTreeSet};
2
3use tla_syntax::{Def, Expr, Module, Unit, parse_module};
4
5use crate::error::{Error, Result};
6
7/// Where the source of a module named in `EXTENDS` or `INSTANCE` comes from.
8///
9/// The standard modules are not looked up here: their operators are built in,
10/// so `EXTENDS Naturals` needs nothing loaded.
11pub trait Modules {
12    fn source(&self, name: &str) -> Option<String>;
13}
14
15/// No modules beyond the one given and whatever it declares inside itself.
16pub struct NoModules;
17
18impl Modules for NoModules {
19    fn source(&self, _name: &str) -> Option<String> {
20        None
21    }
22}
23
24/// Modules as `<directory>/<Name>.tla`, which is how TLA+ tools find them.
25pub struct Directory(pub std::path::PathBuf);
26
27impl Modules for Directory {
28    fn source(&self, name: &str) -> Option<String> {
29        std::fs::read_to_string(self.0.join(format!("{name}.tla"))).ok()
30    }
31}
32
33/// The standard modules, whose operators this crate implements directly.
34const BUILT_IN: &[&str] = &[
35    "Naturals",
36    "Integers",
37    "Reals",
38    "Sequences",
39    "FiniteSets",
40    "TLC",
41    "Bags",
42    "RealTime",
43    "Randomization",
44    "Toolbox",
45];
46
47/// A specification: a root module together with every module it reaches.
48#[derive(Debug)]
49pub struct Spec {
50    modules: Vec<Module>,
51    facts: Vec<Facts>,
52    root: usize,
53}
54
55/// What was worked out about one module once all of them were loaded.
56#[derive(Debug, Default)]
57struct Facts {
58    /// Declared here or in anything this module extends.
59    variables: BTreeSet<String>,
60    constants: BTreeSet<String>,
61    extends: Vec<usize>,
62    instances: Vec<Instance>,
63}
64
65#[derive(Debug)]
66pub(crate) struct Instance {
67    pub(crate) name: Option<String>,
68    pub(crate) target: usize,
69    /// Every name the target declares, paired with what replaces it. Names the
70    /// `WITH` clause leaves out are replaced by the same name here, which is
71    /// what TLA+ says an omitted substitution means.
72    pub(crate) subs: Vec<(String, Expr)>,
73}
74
75impl Spec {
76    /// Parse a self-contained specification. `EXTENDS` of a standard module is
77    /// honoured; anything else it names is reported as missing.
78    pub fn parse(src: &str) -> Result<Self> {
79        Self::load(src, &NoModules)
80    }
81
82    /// Read a specification from a `.tla` file, resolving whatever it extends
83    /// or instantiates from the directory the file is in — which is where TLA+
84    /// tools look, and what makes a path enough to work from.
85    pub fn from_file(path: impl AsRef<std::path::Path>) -> Result<Self> {
86        let path = path.as_ref();
87        let src = std::fs::read_to_string(path)
88            .map_err(|e| Error::Malformed(format!("reading {}: {e}", path.display())))?;
89        let directory = path.parent().unwrap_or(std::path::Path::new("."));
90        Self::load(&src, &Directory(directory.to_path_buf()))
91    }
92
93    pub fn load(src: &str, modules: &impl Modules) -> Result<Self> {
94        let root = parse_module(src)?;
95        let mut builder = Builder {
96            modules: Vec::new(),
97            index: BTreeMap::new(),
98            source: modules,
99        };
100        let root = builder.add(root)?;
101        let modules = builder.modules;
102        let facts = resolve(&modules, &builder.index)?;
103        Ok(Self {
104            modules,
105            facts,
106            root,
107        })
108    }
109
110    pub fn name(&self) -> &str {
111        &self.modules[self.root].name
112    }
113
114    /// The variables of the root module, including any it inherits.
115    pub fn variables(&self) -> impl Iterator<Item = &str> {
116        self.facts[self.root].variables.iter().map(String::as_str)
117    }
118
119    pub fn constants(&self) -> impl Iterator<Item = &str> {
120        self.facts[self.root].constants.iter().map(String::as_str)
121    }
122
123    pub fn defines(&self, name: &str) -> bool {
124        self.definition(self.root, name).is_some()
125    }
126
127    pub(crate) fn root(&self) -> usize {
128        self.root
129    }
130
131    pub(crate) fn declares_variable(&self, module: usize, name: &str) -> bool {
132        self.facts[module].variables.contains(name)
133    }
134
135    pub(crate) fn declares_constant(&self, module: usize, name: &str) -> bool {
136        self.facts[module].constants.contains(name)
137    }
138
139    /// Find a definition, following `EXTENDS`. The module it was found in
140    /// comes back with it, because that is the scope its body must be read in.
141    pub(crate) fn definition(&self, module: usize, name: &str) -> Option<(usize, &Def)> {
142        let mut seen = BTreeSet::new();
143        self.search(module, name, &mut seen)
144    }
145
146    fn search(
147        &self,
148        module: usize,
149        name: &str,
150        seen: &mut BTreeSet<usize>,
151    ) -> Option<(usize, &Def)> {
152        if !seen.insert(module) {
153            return None;
154        }
155        if let Some(def) = self.modules[module].definition(name) {
156            return Some((module, def));
157        }
158        self.facts[module]
159            .extends
160            .iter()
161            .find_map(|&parent| self.search(parent, name, seen))
162    }
163
164    /// Find an instance by the name it was given, following `EXTENDS`.
165    pub(crate) fn instance(&self, module: usize, name: &str) -> Option<&Instance> {
166        let mut seen = BTreeSet::new();
167        self.find_instance(module, name, &mut seen)
168    }
169
170    fn find_instance(
171        &self,
172        module: usize,
173        name: &str,
174        seen: &mut BTreeSet<usize>,
175    ) -> Option<&Instance> {
176        if !seen.insert(module) {
177            return None;
178        }
179        let here = self.facts[module]
180            .instances
181            .iter()
182            .find(|i| i.name.as_deref() == Some(name));
183        if here.is_some() {
184            return here;
185        }
186        self.facts[module]
187            .extends
188            .iter()
189            .find_map(|&parent| self.find_instance(parent, name, seen))
190    }
191}
192
193struct Builder<'a, M: Modules> {
194    modules: Vec<Module>,
195    index: BTreeMap<String, usize>,
196    source: &'a M,
197}
198
199impl<M: Modules> Builder<'_, M> {
200    /// Register a module and everything it names, depth first.
201    fn add(&mut self, module: Module) -> Result<usize> {
202        let name = module.name.clone();
203        if let Some(&existing) = self.index.get(&name) {
204            return Ok(existing);
205        }
206        let position = self.modules.len();
207        self.index.insert(name, position);
208        self.modules.push(module);
209
210        // Inner modules are visible to their parent, and are registered before
211        // anything is loaded from outside so they take precedence.
212        let inner: Vec<Module> = self.modules[position]
213            .units
214            .iter()
215            .filter_map(|u| match u {
216                Unit::Inner(m) => Some((**m).clone()),
217                _ => None,
218            })
219            .collect();
220        for module in inner {
221            self.add(module)?;
222        }
223
224        let mut wanted: Vec<String> = self.modules[position].extends.clone();
225        wanted.extend(self.modules[position].units.iter().filter_map(|u| match u {
226            Unit::Instance { module, .. } => Some(module.clone()),
227            _ => None,
228        }));
229        for name in wanted {
230            if BUILT_IN.contains(&name.as_str()) || self.index.contains_key(&name) {
231                continue;
232            }
233            let Some(src) = self.source.source(&name) else {
234                return Err(Error::Undefined(format!(
235                    "module `{name}` is neither a standard module nor one that could be found"
236                )));
237            };
238            let parsed = parse_module(&src)?;
239            self.add(parsed)?;
240        }
241        Ok(position)
242    }
243}
244
245fn resolve(modules: &[Module], index: &BTreeMap<String, usize>) -> Result<Vec<Facts>> {
246    let mut facts: Vec<Facts> = modules.iter().map(|_| Facts::default()).collect();
247
248    for (position, module) in modules.iter().enumerate() {
249        facts[position].extends = module
250            .extends
251            .iter()
252            .filter_map(|name| index.get(name).copied())
253            .collect();
254        facts[position].variables = module.variables().cloned().collect();
255        facts[position].constants = module.constants().map(|d| d.name.clone()).collect();
256    }
257
258    // A module declares whatever it extends declares.
259    for position in 0..modules.len() {
260        let mut seen = BTreeSet::new();
261        let mut inherited = (BTreeSet::new(), BTreeSet::new());
262        collect(position, &facts, &mut seen, &mut inherited);
263        facts[position].variables.extend(inherited.0);
264        facts[position].constants.extend(inherited.1);
265    }
266
267    for (position, module) in modules.iter().enumerate() {
268        facts[position].instances = module
269            .units
270            .iter()
271            .filter_map(|u| match u {
272                Unit::Instance { name, module, subs } => Some((name, module, subs)),
273                _ => None,
274            })
275            .map(|(name, target, subs)| {
276                let target = *index.get(target).ok_or_else(|| {
277                    Error::Undefined(format!("INSTANCE of unknown module `{target}`"))
278                })?;
279                Ok(Instance {
280                    name: name.clone(),
281                    target,
282                    subs: complete(&facts[target], subs),
283                })
284            })
285            .collect::<Result<Vec<_>>>()?;
286    }
287    Ok(facts)
288}
289
290fn collect(
291    position: usize,
292    facts: &[Facts],
293    seen: &mut BTreeSet<usize>,
294    out: &mut (BTreeSet<String>, BTreeSet<String>),
295) {
296    for &parent in &facts[position].extends {
297        if !seen.insert(parent) {
298            continue;
299        }
300        out.0.extend(facts[parent].variables.iter().cloned());
301        out.1.extend(facts[parent].constants.iter().cloned());
302        collect(parent, facts, seen, out);
303    }
304}
305
306/// A `WITH` clause need not mention every declared name; the ones it leaves
307/// out keep their names, and so refer to whatever bears that name where the
308/// instance was written.
309fn complete(target: &Facts, given: &[(String, Expr)]) -> Vec<(String, Expr)> {
310    let mut subs = given.to_vec();
311    let declared = target.constants.iter().chain(target.variables.iter());
312    for name in declared {
313        if !subs.iter().any(|(given, _)| given == name) {
314            subs.push((name.clone(), Expr::Ident(name.clone())));
315        }
316    }
317    subs
318}
tla_eval/spec.rs

tla_eval/
spec.rs
