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
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
//! The front end assembled: a checked [`Problem`], and [`load`] to read one from disk.
use crate::ast::Init;
use crate::lower_formula::{lower_formula, Bindings};
use crate::{
build_declarative, build_explicit, ground_actions, parse_file, Constants, Ctx, Diagnostics,
GroundAction, Sig,
};
use delhi_mb::State;
use delhi_syntax::{FormulaId, Store};
/// A fully checked problem: signature, initial state, goal, and ground actions.
///
/// `Debug` is derived because `Problem::parse` returns it in a `Result`, and
/// `Result::unwrap_err` requires the success type to be printable.
#[derive(Debug)]
pub struct Problem {
/// Formula arena shared by everything below.
pub store: Store,
/// The checked signature.
pub sig: Sig,
/// The constant table, kept so later queries lower against the same one.
pub consts: Constants,
/// The definition table, kept for the same reason: a name that works in the file
/// must work at the prompt, and a query is lowered after the file has been checked.
pub defs: crate::Defs,
/// The initial state.
pub state: State,
/// The declared goal, if the file had one.
pub goal: Option<FormulaId>,
/// Declared invariants, each with the source text that wrote it.
///
/// The text is kept so a violation can name the constraint as the author wrote it
/// rather than as a formula id or a re-rendering.
pub invariants: Vec<(FormulaId, String)>,
/// Every ground action whose precondition is satisfiable.
pub actions: Vec<GroundAction>,
}
impl Problem {
/// Parses and checks a source file.
///
/// On failure returns every diagnostic rendered against the source, so one call
/// reports all the problems rather than only the first. A construction that
/// produced a state but also raised a diagnostic is a failure too: the state is
/// only as trustworthy as the checks that passed alongside it.
pub fn parse(src: &str) -> Result<Problem, String> {
match Problem::check(src) {
(Some(p), diags) if diags.is_empty() => Ok(p),
(_, diags) => Err(diags.render(src)),
}
}
/// Parses and checks, returning the diagnostics rather than a rendering of them.
///
/// A caller that wants to *act* on a fault — jump a cursor to it, underline it —
/// needs the spans, which `parse`'s rendered string has already thrown away. The
/// problem comes back even when diagnostics were raised, so a UI can report the
/// errors and still show whatever was successfully built.
pub fn check(src: &str) -> (Option<Problem>, Diagnostics) {
let mut diags = Diagnostics::default();
let mut ast = parse_file(src, &mut diags);
// Definitions are expanded away before anything else looks at the tree, so the
// signature, the constants, the initial state and the actions never see a name
// that is not a real proposition.
let defs = crate::Defs::build(&ast, &mut diags);
crate::expand_ast(&mut ast, &defs, &mut diags);
let sig = Sig::build(&ast, &mut diags);
let mut consts = Constants::build(&ast, &sig, &mut diags);
// Horn rules saturate into the constant table, so a derived predicate is an
// ordinary constant by the time anything is lowered.
crate::rules::saturate(&ast, &sig, &mut consts, &mut diags);
let mut store = Store::default();
let state = {
let ctx = Ctx { sig: &sig, consts: &consts };
match &ast.init {
// The block's own span goes through: it is what whole-block failures
// are reported against, and reconstructing one from the entries would
// blame an arbitrary entry (or, for an empty block, byte zero).
Some(Init::Declarative(items, block)) => {
build_declarative(items, *block, &ctx, &mut store, &mut diags)
}
Some(Init::Explicit { worlds, edges, span }) => {
build_explicit(worlds, edges, *span, &ctx, &mut store, &mut diags)
}
None => None,
}
};
let goal = ast
.goal
.as_ref()
.map(|g| lower_formula(g, &sig, &consts, &Bindings::default(), &mut store, &mut diags));
let invariants: Vec<(FormulaId, String)> = ast
.invariants
.iter()
.map(|(e, sp)| {
let f =
lower_formula(e, &sig, &consts, &Bindings::default(), &mut store, &mut diags);
(f, src[sp.start.min(src.len())..sp.end.min(src.len())].trim().to_string())
})
.collect();
let actions = ground_actions(&ast.actions, &sig, &consts, &mut store, &mut diags);
let problem = state.map(|state| Problem {
store,
sig,
consts,
defs,
state,
goal,
invariants,
actions,
});
(problem, diags)
}
/// A ground action by its display name, e.g. `move(alice,hall,study)`. A
/// zero-parameter action keeps its empty argument list, so `peek_c` is `peek_c()`.
pub fn action(&self, name: &str) -> Option<&GroundAction> {
self.actions.iter().find(|a| a.name == name)
}
/// Whether the initial state models `f`.
///
/// Precondition: `f` was produced by this problem's [`Problem::store`].
pub fn entails(&self, f: FormulaId) -> bool {
debug_assert!(
(f as usize) < self.store.len(),
"formula must come from this problem's store"
);
self.state.entails(&self.store, f)
}
/// The declared invariants that `state` violates, as the author wrote them.
///
/// Takes the state rather than using `self.state`, because the point of an invariant
/// is that it is checked *after every action* — a version that could only inspect the
/// initial state would be a slower way of writing an `initially` entry.
pub fn violated(&self, state: &State) -> Vec<&str> {
self.invariants
.iter()
.filter(|(f, _)| !state.entails(&self.store, *f))
.map(|(_, text)| text.as_str())
.collect()
}
}
/// Reads and parses a file from disk. Read errors are reported with the path, so a
/// missing file reads the same way as a malformed one.
pub fn load(path: &str) -> Result<Problem, String> {
let src = std::fs::read_to_string(path).map_err(|e| format!("{path}: {e}"))?;
Problem::parse(&src)
}
#[cfg(test)]
mod tests {
use super::*;
const SRC: &str = r#"
types{ Actor - Object } objects{ a, b - Actor } agents{ a, b } props{ p }
initially { p, ?[a] p, B[a] p }
invariants {
!((B[a] p & B[b] !p) | (B[a] !p & B[b] p))
K[b] p
}
actions { lie() { actor b, announces !p, a observes, b observes } }
"#;
#[test]
fn an_invariant_holding_initially_can_still_be_broken_by_an_action() {
// The whole point of an invariant over an `initially` assertion: it is checked
// against states the file never mentions.
let mut p = Problem::parse(SRC).unwrap_or_else(|e| panic!("{e}"));
assert!(p.violated(&p.state).is_empty(), "clean at the start");
let n = p.sig.n_agents();
let def = p.action("lie()").expect("action").def.clone();
let am = delhi_mb::build(&def, &mut p.store, n);
let after = p.state.clone().apply(&p.store, &am).expect("applicable");
let bad = p.violated(&after);
assert_eq!(bad.len(), 1, "exactly the disagreement one: {bad:?}");
assert!(bad[0].starts_with("!(("), "got {:?}", bad[0]);
}
#[test]
fn a_violation_quotes_the_constraint_exactly_as_written() {
// Guards a real bug: `Expr::span()` of a parenthesised expression covers only its
// contents, so slicing by it truncated `!(a | b)` to `!(a | b`. The span is taken
// from the parser's token positions instead.
let p = Problem::parse(SRC).unwrap_or_else(|e| panic!("{e}"));
let texts: Vec<&str> = p.invariants.iter().map(|(_, t)| t.as_str()).collect();
assert_eq!(texts[0], "!((B[a] p & B[b] !p) | (B[a] !p & B[b] p))");
assert_eq!(texts[1], "K[b] p");
for t in &texts {
assert_eq!(
t.matches('(').count(),
t.matches(')').count(),
"parens must balance in the quoted text: {t}"
);
}
}
#[test]
fn a_file_with_no_invariants_section_has_none_and_violates_nothing() {
let p = Problem::parse(r#"types{} objects{} agents{} props{ p } initially{ p } actions{}"#)
.unwrap_or_else(|e| panic!("{e}"));
assert!(p.invariants.is_empty());
assert!(p.violated(&p.state).is_empty());
}
}