Skip to main content

turnframe_test/explore/
search.rs

1//! The breadth-first search itself.
2
3use std::collections::{BTreeSet, VecDeque};
4
5use turnframe_core::case::CaseRef;
6use turnframe_core::flow::{PhaseOwnership, ViewOf, WorkflowDefinition, check_view};
7use turnframe_core::hash::Digest;
8use turnframe_core::hash::canonical_value;
9use turnframe_core::ids::{CaseId, CaseRevision};
10use turnframe_core::target::{ResolvedAct, ResolvedActKind};
11
12use crate::explore::{
13    ExplorationLimits, ExplorationReport, ExplorationViolation, ExplorationViolationKind,
14    SimulatedTransition, WorkflowModel,
15};
16
17/// Case identifier every explored projection is made against. Exploration never
18/// touches a store, so the identifier only has to be stable.
19pub const EXPLORATION_CASE_ID: &str = "explore";
20
21/// The case revisions exploration projects at, cycled by visit order.
22///
23/// Deliberately **not** derived from the depth. A revision that counted the
24/// commands would be perfectly correlated with the path, so a projector that
25/// reads the revision would produce a different view for every state and never
26/// look wrong; cycling a short, uneven table instead means the same state is
27/// projected at two unrelated revisions and two states at the same depth are
28/// projected at different ones. `0` is in the table because it is the revision
29/// of a case that does not exist yet, which is the value a projector is most
30/// likely to special-case by accident.
31pub const EXPLORATION_REVISIONS: [u64; 4] = [0, 1, 7, 4_096];
32
33/// Explores the states reachable from `model`'s initial states and checks the
34/// projection invariants of spec §8.4 on every one of them.
35///
36/// The search is breadth-first, so the path reported with a violation is the
37/// shortest sequence of commands that reaches the offending state. States are
38/// deduplicated by the canonical JSON of the state, which is why a model must
39/// derive identifiers deterministically.
40///
41/// Checked on every reachable state:
42///
43/// * [`check_view`] passes — one phase, obligation identifiers unique, a
44///   user-owned phase carries a blocking requirement, a terminal phase carries
45///   none and does carry an outcome, no outcome while obligations remain;
46/// * two projections of the same state produce the same obligation identifiers
47///   and the same erased view (I2);
48/// * projecting the same state at another case revision produces the same view
49///   once the case reference itself is set aside, so the map cannot depend on
50///   how often the case was written (see [`EXPLORATION_REVISIONS`]);
51/// * the blocking requirement, when there is one, builds into a card that can
52///   actually be answered ([`InteractionSpec::validate`]), so a user-owned
53///   phase really does derive an interaction (spec §27.3);
54/// * the state is not a dead end: it is terminal, or it offers a candidate
55///   command, or it carries a blocking interaction;
56/// * an *absent* state does not project to a terminal phase or an outcome. A
57///   case's identity outlives its content, so removal is a status and an absent
58///   state means *not yet*, never *no longer*
59///   ([`ExplorationViolationKind::CaseEndsByDisappearing`]).
60///
61/// [`InteractionSpec::validate`]: turnframe_core::interaction::InteractionSpec::validate
62///
63/// Checked on every simulated transition:
64///
65/// * a refused command leaves the state it was given untouched;
66/// * a command [`WorkflowDefinition::validate_command`] refuses is not applied
67///   by the model;
68/// * an applied command does not drop the case it was given
69///   ([`ExplorationViolationKind::TransitionRemovesCase`]), which is the same
70///   rule seen from the model instead of from the projector.
71///
72/// Checked once at the end, and only when the search was **not** truncated:
73/// every outcome [`WorkflowModel::declared_outcomes`] declares was projected
74/// somewhere. A truncated search cannot prove that an outcome is out of reach,
75/// only that it did not get there within the limits, so the check is skipped
76/// rather than reported as a violation.
77#[must_use]
78pub fn explore<W, M>(definition: &W, model: &M, limits: ExplorationLimits) -> ExplorationReport
79where
80    W: WorkflowDefinition,
81    M: WorkflowModel<W> + ?Sized,
82{
83    let mut explorer = Explorer::new(definition, limits);
84    let mut queue: VecDeque<Node<W::State>> = VecDeque::new();
85    for state in model.initial_states() {
86        if let Some(node) = explorer.admit(state, 0, Vec::new()) {
87            queue.push_back(node);
88        }
89    }
90    while let Some(node) = queue.pop_front() {
91        explorer.states_explored += 1;
92        explorer.max_depth_reached = explorer.max_depth_reached.max(node.depth);
93        let facts = explorer.inspect(&node);
94        queue.extend(explorer.expand(model, &node, facts));
95    }
96    explorer.finish(model)
97}
98
99/// One state in the frontier, with the shortest path that reached it.
100struct Node<S> {
101    state: Option<S>,
102    state_json: serde_json::Value,
103    depth: usize,
104    path: Vec<serde_json::Value>,
105}
106
107/// What the projection of a state says about expanding it.
108#[derive(Clone, Copy)]
109struct StateFacts {
110    terminal: bool,
111    has_blocking_interaction: bool,
112}
113
114struct Explorer<'a, W: WorkflowDefinition> {
115    definition: &'a W,
116    limits: ExplorationLimits,
117    seen: BTreeSet<String>,
118    reached_phases: Vec<serde_json::Value>,
119    reached_outcomes: Vec<serde_json::Value>,
120    violations: Vec<ExplorationViolation>,
121    states_explored: usize,
122    transitions_simulated: usize,
123    max_depth_reached: usize,
124    truncated: bool,
125}
126
127impl<'a, W: WorkflowDefinition> Explorer<'a, W> {
128    fn new(definition: &'a W, limits: ExplorationLimits) -> Self {
129        Self {
130            definition,
131            limits,
132            seen: BTreeSet::new(),
133            reached_phases: Vec::new(),
134            reached_outcomes: Vec::new(),
135            violations: Vec::new(),
136            states_explored: 0,
137            transitions_simulated: 0,
138            max_depth_reached: 0,
139            truncated: false,
140        }
141    }
142
143    /// Records a state as visited and turns it into a frontier node, unless it
144    /// was seen before or the state budget is spent.
145    fn admit(
146        &mut self,
147        state: Option<W::State>,
148        depth: usize,
149        path: Vec<serde_json::Value>,
150    ) -> Option<Node<W::State>> {
151        let Ok(state_json) = canonical_value(&state) else {
152            self.violations.push(ExplorationViolation {
153                kind: ExplorationViolationKind::UnserializableState,
154                state: serde_json::Value::Null,
155                depth,
156                path,
157            });
158            return None;
159        };
160        let key = state_json.to_string();
161        if self.seen.contains(&key) {
162            return None;
163        }
164        if self.seen.len() >= self.limits.max_states {
165            self.truncated = true;
166            return None;
167        }
168        self.seen.insert(key);
169        Some(Node {
170            state,
171            state_json,
172            depth,
173            path,
174        })
175    }
176
177    fn violate(&mut self, kind: ExplorationViolationKind, node: &Node<W::State>) {
178        self.violations.push(ExplorationViolation {
179            kind,
180            state: node.state_json.clone(),
181            depth: node.depth,
182            path: node.path.clone(),
183        });
184    }
185
186    /// The case reference an explored projection is made against.
187    fn case_ref_at(&self, revision: u64) -> CaseRef {
188        CaseRef::new(
189            self.definition.key(),
190            CaseId::from(EXPLORATION_CASE_ID),
191            CaseRevision(revision),
192        )
193    }
194
195    /// Projects the state three times — twice at one revision, once at another
196    /// — and checks every per-state rule.
197    fn inspect(&mut self, node: &Node<W::State>) -> StateFacts {
198        let slot = self.states_explored % EXPLORATION_REVISIONS.len();
199        let revision = EXPLORATION_REVISIONS[slot];
200        let other_revision = EXPLORATION_REVISIONS[(slot + 1) % EXPLORATION_REVISIONS.len()];
201        let case_ref = self.case_ref_at(revision);
202        let first = self
203            .definition
204            .project(case_ref.clone(), node.state.as_ref());
205        let second = self.definition.project(case_ref, node.state.as_ref());
206        self.check_revision_independence(node, &first, revision, other_revision);
207        if let Err(violations) = check_view(self.definition, &first) {
208            for violation in violations {
209                self.violate(ExplorationViolationKind::Projection(violation), node);
210            }
211        }
212        let ownership = self.definition.phase_ownership(&first.phase);
213        let facts = StateFacts {
214            terminal: ownership == PhaseOwnership::Terminal || first.outcome.is_some(),
215            has_blocking_interaction: first.blocking_interaction.is_some(),
216        };
217        self.check_absent_state_is_not_terminal(node, &first, facts);
218        self.check_blocking_interaction(node, &first);
219        self.check_catalogued_operations_compile(node, &first);
220        let erased = (
221            first.erase(ownership),
222            second.erase(self.definition.phase_ownership(&second.phase)),
223        );
224        let (Ok(first), Ok(second)) = erased else {
225            self.violate(ExplorationViolationKind::UnserializableState, node);
226            return facts;
227        };
228        let ids = |view: &turnframe_core::flow::ErasedWorkflowView| {
229            view.obligations
230                .iter()
231                .map(|o| o.id.as_str().to_owned())
232                .collect::<Vec<_>>()
233        };
234        let (first_ids, second_ids) = (ids(&first), ids(&second));
235        if first_ids != second_ids {
236            self.violate(
237                ExplorationViolationKind::UnstableObligationIds {
238                    first: first_ids,
239                    second: second_ids,
240                },
241                node,
242            );
243        } else if first != second {
244            self.violate(
245                ExplorationViolationKind::NonDeterministicProjection {
246                    first: canonical_value(&first).unwrap_or(serde_json::Value::Null),
247                    second: canonical_value(&second).unwrap_or(serde_json::Value::Null),
248                },
249                node,
250            );
251        }
252        if !self.reached_phases.contains(&first.phase) {
253            self.reached_phases.push(first.phase.clone());
254        }
255        if let Some(outcome) = first.outcome
256            && !self.reached_outcomes.contains(&outcome)
257        {
258            self.reached_outcomes.push(outcome);
259        }
260        facts
261    }
262
263    /// Asks this state's catalogue whether `compile_act` knows its operations.
264    ///
265    /// The same walk the rest of the explorer already does, and it belongs here
266    /// for the same reason the phase-ownership check does: a catalogue that
267    /// offers what the compiler does not know is a property of a workflow, not
268    /// of a deployment.
269    ///
270    /// Only [`turnframe_core::error::UNKNOWN_OPERATION`] counts. The arguments
271    /// are `null`, which most operations will refuse for an honest reason, so
272    /// any other rejection is left alone — a check that demanded good arguments
273    /// would be testing whether the explorer can invent them.
274    fn check_catalogued_operations_compile(&mut self, node: &Node<W::State>, view: &ViewOf<W>) {
275        for definition in self.definition.operations(view) {
276            let act = ResolvedAct {
277                act: turnframe_core::understanding::ActId::new(
278                    turnframe_core::understanding::UnitId(1),
279                    1,
280                ),
281                kind: ResolvedActKind::ApplyOperation {
282                    operation: definition.key.clone(),
283                },
284                case_ref: view.case_ref.clone(),
285                arguments: serde_json::Value::Null,
286                evidence_digest: Digest::of_bytes(b""),
287            };
288            if let Err(rejection) = self.definition.compile_act(node.state.as_ref(), view, &act)
289                && rejection.code.as_str() == turnframe_core::error::UNKNOWN_OPERATION
290            {
291                self.violate(
292                    ExplorationViolationKind::CatalogedOperationDoesNotCompile {
293                        operation: definition.key.clone(),
294                    },
295                    node,
296                );
297            }
298        }
299    }
300
301    /// Checks that the view does not change when the same state is projected at
302    /// another case revision.
303    ///
304    /// The case reference itself legitimately differs, so it is normalized away
305    /// before the comparison: what must hold is that everything *derived* from
306    /// the state is the same.
307    fn check_revision_independence(
308        &mut self,
309        node: &Node<W::State>,
310        first: &ViewOf<W>,
311        revision: u64,
312        other_revision: u64,
313    ) {
314        let other = self
315            .definition
316            .project(self.case_ref_at(other_revision), node.state.as_ref());
317        let erased = (
318            first.erase(self.definition.phase_ownership(&first.phase)),
319            other.erase(self.definition.phase_ownership(&other.phase)),
320        );
321        let (Ok(first), Ok(mut other)) = erased else {
322            self.violate(ExplorationViolationKind::UnserializableState, node);
323            return;
324        };
325        other.case_ref = first.case_ref.clone();
326        if let Some(detail) = view_difference(&first, &other) {
327            self.violate(
328                ExplorationViolationKind::ProjectionVariesWithRevision {
329                    left: revision,
330                    right: other_revision,
331                    detail: detail.to_owned(),
332                },
333                node,
334            );
335        }
336    }
337
338    /// Checks that an absent state does not project to a terminal phase or an
339    /// outcome.
340    ///
341    /// The executor answers `None` both for a case nobody has created and for a
342    /// case whose row was deleted, so a projector that reads absence as
343    /// completion has one view doing two opposite jobs. The library's position
344    /// is that the second reading is wrong: a case's identity outlives its
345    /// content, removal is a status, and an absent state means *not yet*, never
346    /// *no longer*.
347    fn check_absent_state_is_not_terminal(
348        &mut self,
349        node: &Node<W::State>,
350        view: &ViewOf<W>,
351        facts: StateFacts,
352    ) {
353        if node.state.is_some() || !facts.terminal {
354            return;
355        }
356        let phase = canonical_value(&view.phase).unwrap_or(serde_json::Value::Null);
357        let outcome = view
358            .outcome
359            .as_ref()
360            .map(|outcome| canonical_value(outcome).unwrap_or(serde_json::Value::Null));
361        self.violate(
362            ExplorationViolationKind::CaseEndsByDisappearing { phase, outcome },
363            node,
364        );
365    }
366
367    /// Checks that the blocking requirement of a phase builds into a card the
368    /// user can answer (I6, spec §27.3).
369    fn check_blocking_interaction(&mut self, node: &Node<W::State>, view: &ViewOf<W>) {
370        let Some(requirement) = view.blocking_interaction.as_ref() else {
371            return;
372        };
373        match self
374            .definition
375            .build_interaction(node.state.as_ref(), view, requirement)
376        {
377            Err(rejection) => self.violate(
378                ExplorationViolationKind::BlockingInteractionNotBuildable { rejection },
379                node,
380            ),
381            Ok(spec) => {
382                if let Err(error) = spec.validate() {
383                    self.violate(
384                        ExplorationViolationKind::BlockingInteractionNotAnswerable { error },
385                        node,
386                    );
387                }
388            }
389        }
390    }
391
392    /// Simulates every candidate command and returns the new frontier nodes.
393    fn expand<M>(
394        &mut self,
395        model: &M,
396        node: &Node<W::State>,
397        facts: StateFacts,
398    ) -> Vec<Node<W::State>>
399    where
400        M: WorkflowModel<W> + ?Sized,
401    {
402        let mut commands = model.candidate_commands(node.state.as_ref());
403        if commands.len() > self.limits.max_commands_per_state {
404            commands.truncate(self.limits.max_commands_per_state);
405            self.truncated = true;
406        }
407        if commands.is_empty() && !facts.terminal && !facts.has_blocking_interaction {
408            self.violate(ExplorationViolationKind::DeadEnd, node);
409        }
410        if node.depth >= self.limits.max_depth {
411            self.truncated |= !commands.is_empty();
412            return Vec::new();
413        }
414        let mut frontier = Vec::new();
415        for command in &commands {
416            self.transitions_simulated += 1;
417            if let Some(next) = self.simulate_one(model, node, command) {
418                frontier.push(next);
419            }
420        }
421        frontier
422    }
423
424    fn simulate_one<M>(
425        &mut self,
426        model: &M,
427        node: &Node<W::State>,
428        command: &W::Command,
429    ) -> Option<Node<W::State>>
430    where
431        M: WorkflowModel<W> + ?Sized,
432    {
433        let Ok(command_json) = canonical_value(command) else {
434            self.violate(ExplorationViolationKind::UnserializableCommand, node);
435            return None;
436        };
437        let command_type = command_label(&command_json);
438        let before = canonical_value(&node.state).ok();
439        let validated = self
440            .definition
441            .validate_command(node.state.as_ref(), command);
442        let transition = model.simulate(node.state.as_ref(), command);
443        let mutated = canonical_value(&node.state).ok() != before;
444        match transition {
445            SimulatedTransition::Rejected(_) => {
446                if mutated {
447                    self.violate(
448                        ExplorationViolationKind::RejectedCommandMutatedState {
449                            command: command_json,
450                            command_type,
451                        },
452                        node,
453                    );
454                }
455                None
456            }
457            SimulatedTransition::Applied { state, .. } => {
458                if mutated {
459                    self.violate(
460                        ExplorationViolationKind::AppliedCommandMutatedInputState {
461                            command: command_json.clone(),
462                            command_type: command_type.clone(),
463                        },
464                        node,
465                    );
466                }
467                // The projector half of this rule lives in
468                // `check_absent_state_is_not_terminal`; it cannot see a removal,
469                // because the absent state a removal produces is usually the
470                // initial state and is therefore deduplicated away.
471                if node.state.is_some() && state.is_none() {
472                    self.violate(
473                        ExplorationViolationKind::TransitionRemovesCase {
474                            command: command_json.clone(),
475                            command_type: command_type.clone(),
476                        },
477                        node,
478                    );
479                }
480                if let Err(rejection) = validated {
481                    self.violate(
482                        ExplorationViolationKind::RejectedCommandApplied {
483                            command: command_json.clone(),
484                            command_type,
485                            rejection,
486                        },
487                        node,
488                    );
489                }
490                let mut path = node.path.clone();
491                path.push(command_json);
492                self.admit(state, node.depth + 1, path)
493            }
494        }
495    }
496
497    fn finish<M>(mut self, model: &M) -> ExplorationReport
498    where
499        M: WorkflowModel<W> + ?Sized,
500    {
501        // A truncated search proves nothing about what it did not visit.
502        for outcome in if self.truncated {
503            Vec::new()
504        } else {
505            model.declared_outcomes()
506        } {
507            let kind = match canonical_value(&outcome) {
508                Ok(value) if self.reached_outcomes.contains(&value) => continue,
509                Ok(outcome) => ExplorationViolationKind::UnreachableOutcome { outcome },
510                Err(_) => ExplorationViolationKind::UnserializableState,
511            };
512            self.violations.push(ExplorationViolation {
513                kind,
514                state: serde_json::Value::Null,
515                depth: 0,
516                path: Vec::new(),
517            });
518        }
519        ExplorationReport {
520            workflow: self.definition.key(),
521            workflow_version: self.definition.version(),
522            limits: self.limits,
523            states_explored: self.states_explored,
524            transitions_simulated: self.transitions_simulated,
525            max_depth_reached: self.max_depth_reached,
526            truncated: self.truncated,
527            reached_phases: self.reached_phases,
528            reached_outcomes: self.reached_outcomes,
529            violations: self.violations,
530        }
531    }
532}
533
534/// The first part of two erased views that differs, or `None` when they match.
535///
536/// The labels are field names, never values, so they are safe in a violation
537/// message.
538fn view_difference(
539    left: &turnframe_core::flow::ErasedWorkflowView,
540    right: &turnframe_core::flow::ErasedWorkflowView,
541) -> Option<&'static str> {
542    if left.phase != right.phase {
543        return Some("phase");
544    }
545    if left.phase_ownership != right.phase_ownership {
546        return Some("phase ownership");
547    }
548    if left.obligations.len() != right.obligations.len() {
549        return Some("obligation count");
550    }
551    if left.obligations != right.obligations {
552        return Some("obligations");
553    }
554    if left.blocking_interaction != right.blocking_interaction {
555        return Some("blocking interaction");
556    }
557    if left.notices != right.notices {
558        return Some("notices");
559    }
560    if left.outcome != right.outcome {
561        return Some("outcome");
562    }
563    if left.workflow_version != right.workflow_version {
564        return Some("workflow version");
565    }
566    None
567}
568
569/// Walks the model and returns every reachable state, in visit order.
570///
571/// This is the search without the projection: no definition is consulted and no
572/// invariant is checked, so it is the tool for a domain-specific assertion that
573/// [`ExplorationReport`](crate::explore::ExplorationReport) cannot express —
574/// "some reachable trip really does carry four extras", "the second traveler
575/// is reachable in more than one state". Deduplication and the limits work
576/// exactly as in [`explore`], and the first element is an initial state.
577#[must_use]
578pub fn reachable_states<W, M>(model: &M, limits: ExplorationLimits) -> Vec<Option<W::State>>
579where
580    W: WorkflowDefinition,
581    M: WorkflowModel<W> + ?Sized,
582{
583    let mut seen: BTreeSet<String> = BTreeSet::new();
584    let mut queue: VecDeque<(Option<W::State>, usize)> = VecDeque::new();
585    let mut visited: Vec<Option<W::State>> = Vec::new();
586    let admit = |state: Option<W::State>,
587                 depth: usize,
588                 seen: &mut BTreeSet<String>,
589                 queue: &mut VecDeque<(Option<W::State>, usize)>| {
590        let Ok(key) = canonical_value(&state).map(|value| value.to_string()) else {
591            return;
592        };
593        if seen.contains(&key) || seen.len() >= limits.max_states {
594            return;
595        }
596        seen.insert(key);
597        queue.push_back((state, depth));
598    };
599    for state in model.initial_states() {
600        admit(state, 0, &mut seen, &mut queue);
601    }
602    while let Some((state, depth)) = queue.pop_front() {
603        visited.push(state.clone());
604        if depth >= limits.max_depth {
605            continue;
606        }
607        let mut commands = model.candidate_commands(state.as_ref());
608        commands.truncate(limits.max_commands_per_state);
609        for command in &commands {
610            if let SimulatedTransition::Applied { state: next, .. } =
611                model.simulate(state.as_ref(), command)
612            {
613                admit(next, depth + 1, &mut seen, &mut queue);
614            }
615        }
616    }
617    visited
618}
619
620/// A stable label for a serialized command: the variant name for an externally
621/// tagged enum, the string itself for a unit variant, `"command"` otherwise.
622/// Never carries a value, so it is safe in `Display` output.
623fn command_label(command: &serde_json::Value) -> String {
624    match command {
625        serde_json::Value::String(name) => name.clone(),
626        serde_json::Value::Object(fields) => fields
627            .get("kind")
628            .and_then(serde_json::Value::as_str)
629            .or_else(|| fields.keys().next().map(String::as_str))
630            .unwrap_or("command")
631            .to_owned(),
632        _ => "command".to_owned(),
633    }
634}
635
636#[cfg(test)]
637mod tests {
638    use super::command_label;
639    use serde_json::json;
640
641    #[test]
642    fn command_labels_never_carry_a_value() {
643        assert_eq!(command_label(&json!("submit")), "submit");
644        assert_eq!(
645            command_label(&json!({"set_name": {"value": "x"}})),
646            "set_name"
647        );
648        assert_eq!(
649            command_label(&json!({"kind": "cancel", "reason": "x"})),
650            "cancel"
651        );
652        assert_eq!(command_label(&json!(7)), "command");
653        assert_eq!(command_label(&json!({})), "command");
654    }
655}