expectation_graph/
conflict.rs

1//! Conflicts: two expectations that can both apply but promise things that can't both be true.
2//!
3//! - **Outcome**: the same action, Givens that overlap, Thens that contradict. In a state
4//!   where both Givens hold, the system can't do both.
5//! - **Invariant**: an expectation leaves the system in a state where an invariant's Given
6//!   holds but its Then can't.
7//!
8//! An `Overrides:` between the two (directly or through a chain) settles a conflict: the
9//! winner is an exception to the loser. Settled conflicts are kept, since docs show them.
10
11use crate::precedence::Precedence;
12use expectation_model::{Condition, Diagnostic, ExpId, Expectation, Shift, Suite, Trigger, VarId};
13
14#[derive(Clone, Copy, Debug, PartialEq, Eq)]
15pub enum Kind {
16    Outcome,
17    Invariant,
18}
19
20#[derive(Clone, Debug)]
21pub struct Conflict {
22    pub kind: Kind,
23    /// For [`Kind::Invariant`], `a` breaks the invariant `b`.
24    pub a: ExpId,
25    pub b: ExpId,
26    /// The states they disagree about.
27    pub vars: Vec<VarId>,
28    /// States where both apply (for an invariant conflict: the states `a` leaves behind).
29    pub situation: Condition,
30    /// The action that sets both off (outcome conflicts).
31    pub trigger: Trigger,
32    /// The exception that settles it.
33    pub winner: Option<ExpId>,
34}
35
36impl Conflict {
37    pub fn involves(&self, x: ExpId, y: ExpId) -> bool {
38        (self.a == x && self.b == y) || (self.a == y && self.b == x)
39    }
40
41    pub fn loser(&self) -> Option<ExpId> {
42        self.winner.map(|w| if w == self.a { self.b } else { self.a })
43    }
44}
45
46pub fn detect(suite: &Suite, prec: &Precedence) -> Vec<Conflict> {
47    let mut out = vec![];
48    let winner = |a: ExpId, b: ExpId| {
49        if prec.beats(a, b) {
50            Some(a)
51        } else if prec.beats(b, a) {
52            Some(b)
53        } else {
54            None
55        }
56    };
57
58    let transitions: Vec<&Expectation> = suite.transitions().collect();
59    for (i, a) in transitions.iter().enumerate() {
60        for b in &transitions[i + 1..] {
61            if !a.trigger.compatible(&b.trigger) {
62                continue;
63            }
64            let situation = a.given.and(&b.given);
65            if !situation.is_satisfiable() {
66                continue;
67            }
68            let trigger = Trigger { event: a.trigger.event, changes: a.trigger.changes.and(&b.trigger.changes) };
69            let before = situation.overlay(&trigger.changes);
70            let vars = disagree(suite, a, b, &before);
71            if vars.is_empty() {
72                continue;
73            }
74            out.push(Conflict {
75                kind: Kind::Outcome,
76                a: a.id,
77                b: b.id,
78                vars,
79                situation,
80                trigger,
81                winner: winner(a.id, b.id),
82            });
83        }
84    }
85
86    for x in &suite.expectations {
87        let after = x.outcome(&suite.vocabulary);
88        for inv in suite.invariants() {
89            if inv.id == x.id || out.iter().any(|c| c.kind == Kind::Invariant && c.involves(x.id, inv.id)) {
90                continue;
91            }
92            let scope = after.and(&inv.given);
93            if !scope.is_satisfiable() || scope.and(&inv.then).is_satisfiable() {
94                continue;
95            }
96            // Only if `x` is what breaks it: something it changes is in the invariant's Given
97            // or is what the invariant gets wrong. Otherwise the clash was in its Given already,
98            // a state the invariant itself rules out.
99            let vars = scope.contradictions(&inv.then);
100            let changed: Vec<VarId> = x.sets().chain(x.trigger.changes.vars()).collect();
101            if !changed.iter().any(|v| inv.given.get(*v).is_some() || vars.contains(v)) {
102                continue;
103            }
104            out.push(Conflict {
105                kind: Kind::Invariant,
106                a: x.id,
107                b: inv.id,
108                vars,
109                situation: scope,
110                trigger: x.trigger.clone(),
111                winner: winner(x.id, inv.id),
112            });
113        }
114    }
115    out
116}
117
118/// The states two expectations' Thens disagree about, starting from `before`. Absolute Thens
119/// disagree if they can't both hold. Two different relative Thens always disagree. A relative
120/// Then and an absolute one disagree unless `before` pins down the one value where they meet.
121fn disagree(suite: &Suite, a: &Expectation, b: &Expectation, before: &Condition) -> Vec<VarId> {
122    let v = &suite.vocabulary;
123    let (ea, eb) = (a.effect(v, before), b.effect(v, before));
124    let mut vars = ea.contradictions(&eb);
125    let shift = |e: &Expectation, x: VarId| {
126        e.shifts.iter().find(|(w, _)| *w == x).map(|(_, s)| match s {
127            Shift::Same => 0.0,
128            Shift::By(d) => *d,
129        })
130    };
131    for x in a.sets().filter(|x| b.sets().any(|y| y == *x)) {
132        let differ = match (shift(a, x), shift(b, x)) {
133            (Some(p), Some(q)) => p != q,
134            (Some(_), None) | (None, Some(_)) => ea.get(x) != eb.get(x),
135            (None, None) => false,
136        };
137        if differ && !vars.contains(&x) {
138            vars.push(x);
139        }
140    }
141    vars
142}
143
144/// Errors for unsettled conflicts, warnings for overrides that settle nothing, and errors
145/// for a Background that breaks an invariant.
146pub fn diagnose(suite: &Suite, prec: &Precedence, conflicts: &[Conflict]) -> Vec<Diagnostic> {
147    let v = &suite.vocabulary;
148    let mut diags = vec![];
149    for c in conflicts.iter().filter(|c| c.winner.is_none()) {
150        let (a, b) = (suite.exp(c.a), suite.exp(c.b));
151        let subjects: Vec<String> = c.vars.iter().map(|&x| v.var(x).subject.clone()).collect();
152        let before = c.situation.overlay(&c.trigger.changes);
153        let on = |e: &Expectation| v.describe(&e.effect(v, &before).restrict(c.vars.iter().copied()));
154        let d = match c.kind {
155            Kind::Outcome => {
156                let mut when = v.describe(&c.situation);
157                if !c.trigger.is_none() {
158                    when = format!("{when}, and {}", suite.describe_trigger(&c.trigger));
159                }
160                Diagnostic::error(
161                    "conflict",
162                    format!(
163                        "«{}» and «{}» disagree about {}",
164                        a.name,
165                        b.name,
166                        expectation_model::text::join_and(&subjects)
167                    ),
168                )
169                .at(&a.span, format!("«{}» says {}", a.name, on(a)))
170                .at(&b.span, format!("«{}» says {}", b.name, on(b)))
171                .note_that(format!("both apply when {when}"))
172                .help(exception_help(a, b))
173            }
174            Kind::Invariant => Diagnostic::error("conflict", format!("«{}» breaks «{}»", a.name, b.name))
175                .at(&a.span, format!("afterwards {}", v.describe(&c.situation.restrict(c.vars.iter().copied()))))
176                .at(&b.span, format!("but whenever {}, {}", v.describe(&b.given), on(b)))
177                .help(format!(
178                    "narrow one of the Givens, or if «{}» is a deliberate exception, add `Overrides: {}` to it",
179                    a.name, b.name
180                )),
181        };
182        diags.push(d);
183    }
184
185    for &(w, l) in &prec.declared {
186        if !conflicts.iter().any(|c| c.involves(w, l)) {
187            let (w, l) = (suite.exp(w), suite.exp(l));
188            diags.push(
189                Diagnostic::warning(
190                    "unneeded-override",
191                    format!("«{}» overrides «{}», but they never disagree", w.name, l.name),
192                )
193                .at(&w.span, "")
194                .help("either they can't apply at the same time or they agree; remove the Overrides line"),
195            );
196        }
197    }
198
199    for section in &suite.sections {
200        for inv in suite.invariants() {
201            let scope = section.start.and(&inv.given);
202            if scope.is_satisfiable() && !scope.and(&inv.then).is_satisfiable() {
203                let mut d = Diagnostic::error(
204                    "conflict",
205                    format!("the Background of «{}» breaks «{}»", section.name, inv.name),
206                )
207                .at(&inv.span, format!("whenever {}, {}", v.describe(&inv.given), v.describe(&inv.then)));
208                if let Some(s) = section.setup_steps.first() {
209                    d = d.at(&s.span, format!("but «{}» starts with {}", section.name, v.describe(&section.start)));
210                }
211                diags.push(d);
212            }
213        }
214    }
215    diags
216}
217
218fn exception_help(a: &Expectation, b: &Expectation) -> String {
219    // The more specific one is the likely exception.
220    let (special, general) = if a.given.implies(&b.given) && !b.given.implies(&a.given) { (a, b) } else { (b, a) };
221    let specific = special.given.implies(&general.given) && !general.given.implies(&special.given);
222    if specific {
223        format!(
224            "«{}» is the more specific; if it's an exception, add `Overrides: {}` to it. Otherwise narrow a Given so they can't both apply",
225            special.name, general.name
226        )
227    } else {
228        "if one is an exception to the other, add `Overrides: <the other>` to it; otherwise narrow a Given so they can't both apply".into()
229    }
230}
expectation_graph/conflict.rs

expectation_graph/
conflict.rs
