tla-eval 0.2.0

Evaluate TLA+ predicates and actions at concrete states, with no dependencies
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129

use std::collections::BTreeSet;

use crate::error::{Error, Result, type_error};
use crate::value::{Infinite, Value, count};

/// Operators from the standard modules that specifications `EXTENDS`. They are
/// resolved after the module's own definitions, so a spec may shadow one.
pub fn call(name: &str, args: &[Value]) -> Result<Value> {
    let arity = |n: usize| -> Result<()> {
        if args.len() == n {
            Ok(())
        } else {
            Err(Error::Malformed(format!(
                "{name} takes {n} argument(s), given {}",
                args.len()
            )))
        }
    };
    match name {
        "Cardinality" => {
            arity(1)?;
            match &args[0] {
                Value::Set(s) => Ok(Value::Int(count(s.len()))),
                Value::Infinite(_) => Err(Error::Unbounded(
                    "Cardinality of an infinite set".to_string(),
                )),
                other => type_error(format!("Cardinality expects a set, got {other}")),
            }
        }
        "IsFiniteSet" => {
            arity(1)?;
            Ok(Value::Bool(matches!(args[0], Value::Set(_))))
        }
        "Len" => {
            arity(1)?;
            seq(&args[0], name).map(|s| Value::Int(count(s.len())))
        }
        "Head" => {
            arity(1)?;
            seq(&args[0], name)?
                .first()
                .cloned()
                .ok_or_else(|| Error::Type("Head of an empty sequence".to_string()))
        }
        "Tail" => {
            arity(1)?;
            let s = seq(&args[0], name)?;
            if s.is_empty() {
                return type_error("Tail of an empty sequence");
            }
            Ok(Value::Seq(s[1..].to_vec()))
        }
        "Append" => {
            arity(2)?;
            let mut s = seq(&args[0], name)?.to_vec();
            s.push(args[1].clone());
            Ok(Value::Seq(s))
        }
        "SubSeq" => {
            arity(3)?;
            let s = seq(&args[0], name)?;
            let lo = int(&args[1], name)?.max(1);
            let hi = int(&args[2], name)?.min(count(s.len()));
            if hi < lo {
                return Ok(Value::Seq(Vec::new()));
            }
            let (lo, hi) = index_range(lo, hi);
            Ok(Value::Seq(s[lo..hi].to_vec()))
        }
        "Seq" => {
            arity(1)?;
            Ok(Value::Infinite(Infinite::Sequences(Box::new(
                args[0].clone(),
            ))))
        }
        "Assert" => {
            arity(2)?;
            if args[0] == Value::Bool(true) {
                Ok(Value::Bool(true))
            } else {
                Err(Error::Malformed(format!("assertion failed: {}", args[1])))
            }
        }
        "ToString" => {
            arity(1)?;
            Ok(Value::Str(args[0].to_string()))
        }
        "Print" => {
            arity(2)?;
            Ok(args[1].clone())
        }
        "PrintT" => {
            arity(1)?;
            Ok(Value::Bool(true))
        }
        _ => Err(Error::Undefined(name.to_string())),
    }
}

/// Nullary names the standard modules provide.
pub fn constant(name: &str) -> Option<Value> {
    Some(match name {
        "Nat" => Value::Infinite(Infinite::Nat),
        "Int" => Value::Infinite(Infinite::Int),
        "STRING" => Value::Infinite(Infinite::Strings),
        "BOOLEAN" => Value::Set(BTreeSet::from([Value::Bool(false), Value::Bool(true)])),
        _ => return None,
    })
}

/// A `SubSeq` range, already clamped to `1..=len`, as a Rust slice range.
fn index_range(lo: i64, hi: i64) -> (usize, usize) {
    let to_index = |n: i64| usize::try_from(n).expect("clamped to the sequence's own bounds");
    (to_index(lo) - 1, to_index(hi))
}

fn seq<'a>(v: &'a Value, who: &str) -> Result<&'a [Value]> {
    match v {
        Value::Seq(items) => Ok(items),
        other => type_error(format!("{who} expects a sequence, got {other}")),
    }
}

fn int(v: &Value, who: &str) -> Result<i64> {
    match v {
        Value::Int(n) => Ok(*n),
        other => type_error(format!("{who} expects an integer, got {other}")),
    }
}