expectation_graph/
semantics.rs

1//! What happens when the system is in some state and something happens to it. States here are
2//! [`Condition`]s, sets of concrete states, so one step answers for all of them at once.
3//! Story planning and the flow graph both step through a suite with [`perform`].
4
5use crate::precedence::Precedence;
6use expectation_model::{Condition, ExpId, Expectation, Suite, Trigger, VarId};
7use std::collections::BTreeSet;
8
9#[derive(Debug, Default)]
10pub struct Outcome {
11    /// Expectations that certainly fire.
12    pub fired: Vec<ExpId>,
13    /// Expectations that might fire: the state or the action doesn't pin down whether their
14    /// Given or trigger holds.
15    pub uncertain: Vec<ExpId>,
16    /// (loser, winner): would have fired, but an exception that also fires wins.
17    pub overridden: Vec<(ExpId, ExpId)>,
18    /// Fired expectations whose Thens can't both hold, and the state they disagree on.
19    pub clashes: Vec<(ExpId, ExpId, VarId)>,
20    /// Invariants in force afterwards.
21    pub invariants: Vec<ExpId>,
22    /// The state afterwards.
23    pub after: Condition,
24}
25
26/// Perform `action` in `state`.
27///
28/// An expectation fires if the state implies its Given and the action implies its trigger.
29/// The rest of a compound action happens first: in "When the dial is 0 % and the user
30/// presses reset", an expectation about reset sees the dial at 0. The new state is the old
31/// one with the action's changes and every fired Then written over it (anything nobody
32/// mentions keeps its value), and then the invariants applied.
33pub fn perform(suite: &Suite, prec: &Precedence, state: &Condition, action: &Trigger) -> Outcome {
34    perform_among(suite, prec, state, action, suite.transitions())
35}
36
37/// [`perform`], looking only at `candidates`: every transition the action might set off must
38/// be among them. Searches that perform the same actions over and over work these out once.
39pub fn perform_among<'a>(
40    suite: &Suite,
41    prec: &Precedence,
42    state: &Condition,
43    action: &Trigger,
44    candidates: impl IntoIterator<Item = &'a Expectation>,
45) -> Outcome {
46    let mut fired = vec![];
47    let mut uncertain = vec![];
48    for e in candidates {
49        if !action.may_fire(&e.trigger) {
50            continue;
51        }
52        let seen = seen_by(state, action, &e.trigger);
53        if !seen.overlaps(&e.given) {
54            continue;
55        }
56        if action.fires(&e.trigger) && seen.implies(&e.given) {
57            fired.push(e.id);
58        } else {
59            uncertain.push(e.id);
60        }
61    }
62
63    // Exceptions win. A winner that only might fire leaves its loser uncertain too.
64    let mut overridden = vec![];
65    let all = fired.clone();
66    fired.retain(|&l| match all.iter().find(|&&w| prec.beats(w, l)) {
67        Some(&w) => {
68            overridden.push((l, w));
69            false
70        }
71        None => true,
72    });
73    uncertain.retain(|&l| !all.iter().any(|&w| prec.beats(w, l)));
74    let (fired, maybe_beaten): (Vec<_>, Vec<_>) =
75        fired.into_iter().partition(|&l| !uncertain.iter().any(|&w| prec.beats(w, l)));
76    uncertain.extend(maybe_beaten);
77
78    // What each Then makes of the state the action leaves, relative Thens included.
79    let before = state.overlay(&action.changes);
80    let effects: Vec<Condition> = fired.iter().map(|&e| suite.exp(e).effect(&suite.vocabulary, &before)).collect();
81    let mut then = Condition::new();
82    let mut clashes = vec![];
83    for (i, &a) in fired.iter().enumerate() {
84        for (j, &b) in fired[..i].iter().enumerate() {
85            for v in effects[j].contradictions(&effects[i]) {
86                clashes.push((b, a, v));
87            }
88        }
89        then = then.and(&effects[i]);
90    }
91    let (after, invariants) = settle(suite, prec, &before.overlay(&then), &fired);
92    Outcome { fired, uncertain, overridden, clashes, invariants, after }
93}
94
95/// The state an expectation with `trigger` checks its Given against when `action` happens in
96/// `state`: the action's other changes already made.
97pub fn seen_by(state: &Condition, action: &Trigger, trigger: &Trigger) -> Condition {
98    let others = action.changes.vars().filter(|v| trigger.changes.get(*v).is_none());
99    state.overlay(&action.changes.restrict(others))
100}
101
102/// Apply every invariant whose Given certainly holds, until nothing changes. Invariants that
103/// one of `exempt_by` overrides are skipped.
104pub fn settle(suite: &Suite, prec: &Precedence, state: &Condition, exempt_by: &[ExpId]) -> (Condition, Vec<ExpId>) {
105    let mut s = state.clone();
106    let mut in_force = BTreeSet::new();
107    for _ in 0..8 {
108        let mut changed = false;
109        for inv in suite.invariants() {
110            if !s.is_satisfiable() || exempt_by.iter().any(|&w| prec.beats(w, inv.id)) || !s.implies(&inv.given) {
111                continue;
112            }
113            in_force.insert(inv.id);
114            let next = s.and(&inv.then);
115            if next != s {
116                s = next;
117                changed = true;
118            }
119        }
120        if !changed {
121            break;
122        }
123    }
124    (s, in_force.into_iter().collect())
125}
expectation_graph/semantics.rs

expectation_graph/
semantics.rs
