Skip to main content

determa_state/
validate.rs

1//! Semantic validation (SPEC §5.5.1 choices, §7 contracts). Structural validation
2//! (unknown fields, required fields) is enforced by serde's `deny_unknown_fields`
3//! during loading; reference resolution happens in [`crate::machine::build`]. This
4//! module adds the checks the JSON schema cannot express.
5
6use crate::loader::LoadError;
7use crate::machine::{Machine, NodeId, StateDef, StateKind};
8use crate::model::{Action, RawMachine};
9use serde::Deserialize;
10use std::collections::{BTreeMap, HashMap, HashSet};
11
12const RESERVED_EVENTS: &[&str] = &["initial", "entry", "exit", "env", "error", "done"];
13const RESERVED_NAMES: &[&str] = &["top", "id", "parent", "event"];
14const IDENT: &str = "^[A-Za-z_][A-Za-z0-9_]*$";
15
16#[derive(Debug, Clone, Default, Deserialize)]
17#[serde(deny_unknown_fields)]
18pub struct Requires {
19    #[serde(default)]
20    pub events: Vec<String>,
21    #[serde(default)]
22    pub states: Vec<String>,
23    #[serde(default)]
24    pub spawns: Vec<String>,
25}
26
27#[derive(Debug, Clone, Deserialize)]
28#[serde(deny_unknown_fields)]
29pub struct Contract {
30    #[serde(default)]
31    pub contract: Option<i64>,
32    pub id: String,
33    #[serde(default)]
34    pub requires: Requires,
35}
36
37/// Fully validate a set of machine definitions (the first is the root). Returns
38/// the list of errors (empty => valid).
39pub fn validate(
40    machines: &[RawMachine],
41    contracts: &[Contract],
42) -> (bool, Vec<LoadError>) {
43    let mut errors: Vec<LoadError> = Vec::new();
44
45    let contract_map: BTreeMap<String, Contract> = contracts
46        .iter()
47        .map(|c| (c.id.clone(), c.clone()))
48        .collect();
49
50    for raw in machines {
51        validate_identifiers(raw, &mut errors);
52    }
53    // inline submachines + build (so semantic checks run on the fully-resolved tree)
54    let registry: HashMap<String, crate::model::StateNode> = machines
55        .iter()
56        .map(|d| (d.id.clone(), d.top.clone()))
57        .collect();
58    for raw in machines {
59        let inlined_top = match crate::model::inline_submachines(
60            &raw.top,
61            &registry,
62            &HashSet::new(),
63        ) {
64            Ok(t) => t,
65            Err(e) => {
66                errors.extend(e);
67                continue;
68            }
69        };
70        let mut inlined = raw.clone();
71        inlined.top = inlined_top;
72        let built = match crate::machine::build(&inlined) {
73            Ok(m) => m,
74            Err(es) => {
75                for e in es {
76                    errors.push(LoadError {
77                        path: format!("machine '{}'", raw.id),
78                        message: e,
79                    });
80                }
81                continue;
82            }
83        };
84        validate_choices(&built, &mut errors);
85        validate_dead_branches(&built, &mut errors);
86        validate_reachability(&built, &mut errors);
87        validate_reserved_events(&built, &mut errors);
88        validate_contracts(&built, &contract_map, &mut errors);
89    }
90
91    (errors.is_empty(), errors)
92}
93
94fn re_ident() -> regex_lite::Regex {
95    regex_lite::new(IDENT)
96}
97
98fn validate_identifiers(raw: &RawMachine, errors: &mut Vec<LoadError>) {
99    let re = re_ident();
100    if !re.is_match(&raw.id) {
101        errors.push(LoadError {
102            path: "machine.id".into(),
103            message: format!("'{}' is not a valid identifier", raw.id),
104        });
105    }
106    if let Some(ev) = &raw.events {
107        for name in ev.keys() {
108            if !re.is_match(name) {
109                errors.push(LoadError {
110                    path: "events".into(),
111                    message: format!("'{name}' is not a valid identifier"),
112                });
113            }
114        }
115    }
116    check_state_identifiers(&raw.top, "top", &re, errors);
117}
118
119fn check_state_identifiers(
120    node: &crate::model::StateNode,
121    path: &str,
122    re: &regex_lite::Regex,
123    errors: &mut Vec<LoadError>,
124) {
125    if let Some(esvs) = &node.esvs {
126        for name in esvs.keys() {
127            check_name(name, &format!("{path}.esvs.{name}"), re, errors);
128        }
129    }
130    if let Some(states) = &node.states {
131        for (name, child) in states {
132            check_name(name, &format!("{path}.states.{name}"), re, errors);
133            check_state_identifiers(child, &format!("{path}.{name}"), re, errors);
134        }
135    }
136    if let Some(regions) = &node.regions {
137        for region in regions {
138            for (name, child) in &region.states {
139                check_name(name, &format!("{path}.states.{name}"), re, errors);
140                check_state_identifiers(child, &format!("{path}.{name}"), re, errors);
141            }
142        }
143    }
144}
145
146/// Reject malformed identifiers and the structural/intrinsic reserved names
147/// `top`, `id`, `parent`, `event` (SPEC §2; reserved event names live in a
148/// different namespace and may be reused as state/esv names).
149fn check_name(name: &str, path: &str, re: &regex_lite::Regex, errors: &mut Vec<LoadError>) {
150    if !re.is_match(name) {
151        errors.push(LoadError {
152            path: path.into(),
153            message: format!("'{name}' is not a valid identifier"),
154        });
155    }
156    if RESERVED_NAMES.contains(&name) {
157        errors.push(LoadError {
158            path: path.into(),
159            message: format!("'{name}' is a reserved name"),
160        });
161    }
162}
163
164
165fn validate_reserved_events(m: &Machine, errors: &mut Vec<LoadError>) {
166    for ev in m.events.keys() {
167        if RESERVED_EVENTS.contains(&ev.as_str()) {
168            errors.push(LoadError {
169                path: "events".into(),
170                message: format!("'{ev}' is a reserved event name"),
171            });
172        }
173    }
174}
175
176// --- choice pseudostates (§5.5.1) -----------------------------------------
177
178fn validate_dead_branches(m: &Machine, errors: &mut Vec<LoadError>) {
179    // In a guarded transition list (§4.5), an unguarded branch is the unconditional
180    // default and MUST be last (first passing guard wins); any branch after it is
181    // dead (SPEC §2).
182    for s in &m.states {
183        for (ev, list) in &s.on_events {
184            if list.len() < 2 {
185                continue;
186            }
187            for (i, t) in list.iter().enumerate() {
188                if i < list.len() - 1 && t.guard.is_none() {
189                    errors.push(LoadError {
190                        path: format!("{}.on_events.{}", s.path, ev),
191                        message:
192                            "an unguarded transition must be last; later branches are dead"
193                                .into(),
194                    });
195                    break;
196                }
197            }
198        }
199    }
200}
201
202// --- reachability (SPEC §2) ------------------------------------------------
203
204/// All `transition_to` / initial targets of a state (resolved NodeIds). Conservative
205/// and guard-agnostic — every target is followed regardless of guards.
206fn state_targets(s: &StateDef) -> Vec<NodeId> {
207    let mut out = Vec::new();
208    if let Some(init) = &s.initial {
209        out.push(init.target);
210    }
211    for r in &s.regions {
212        out.push(r.initial.target);
213    }
214    for list in s.on_events.values() {
215        for t in list {
216            if let Some(tg) = t.target {
217                out.push(tg);
218            }
219        }
220    }
221    for a in &s.after {
222        if let Some(tg) = a.target {
223            out.push(tg);
224        }
225    }
226    if let Some(branches) = &s.choice {
227        for b in branches {
228            out.push(b.target);
229        }
230    }
231    out
232}
233
234fn validate_reachability(m: &Machine, errors: &mut Vec<LoadError>) {
235    use std::collections::HashSet;
236    let mut reachable: HashSet<NodeId> = HashSet::new();
237    let mut stack: Vec<NodeId> = vec![m.top];
238    while let Some(s) = stack.pop() {
239        if reachable.contains(&s) {
240            continue;
241        }
242        reachable.insert(s);
243        // entering a state implies its ancestors; follow their edges too
244        if let Some(par) = m.get(s).parent {
245            if !reachable.contains(&par) {
246                stack.push(par);
247            }
248        }
249        for t in state_targets(m.get(s)) {
250            if !reachable.contains(&t) {
251                stack.push(t);
252            }
253        }
254    }
255    for s in &m.states {
256        if s.path != "top" && !reachable.contains(&m.by_path[&s.path]) {
257            errors.push(LoadError {
258                path: "/".to_string() + &s.path.replace('.', "/"),
259                message: format!("unreachable state '{}'", s.id),
260            });
261        }
262    }
263}
264
265fn validate_choices(m: &Machine, errors: &mut Vec<LoadError>) {
266    for (_idx, s) in m.states.iter().enumerate() {
267        if s.kind != StateKind::Choice {
268            continue;
269        }
270        let branches = match &s.choice {
271            Some(b) => b,
272            None => continue,
273        };
274        // exactly one default (no guard) and it must be last
275        let defaults: Vec<usize> = branches
276            .iter()
277            .enumerate()
278            .filter_map(|(i, b)| if b.guard.is_none() { Some(i) } else { None })
279            .collect();
280        if defaults.is_empty() {
281            errors.push(LoadError {
282                path: s.path.clone(),
283                message: "choice has no default (else) branch".into(),
284            });
285        } else if defaults.len() > 1 {
286            errors.push(LoadError {
287                path: s.path.clone(),
288                message: "choice has more than one default branch".into(),
289            });
290        } else if defaults[0] != branches.len() - 1 {
291            errors.push(LoadError {
292                path: s.path.clone(),
293                message: "the default branch must be last".into(),
294            });
295        }
296    }
297    // acyclicity over the choice -> choice graph
298    let mut visited = HashSet::new();
299    let mut stack = HashSet::new();
300    for (idx, s) in m.states.iter().enumerate() {
301        if s.kind == StateKind::Choice {
302            if has_choice_cycle(m, idx, &mut visited, &mut stack) {
303                errors.push(LoadError {
304                    path: s.path.clone(),
305                    message: "choice graph contains a cycle".into(),
306                });
307            }
308        }
309    }
310}
311
312fn has_choice_cycle(
313    m: &Machine,
314    start: NodeId,
315    visited: &mut HashSet<NodeId>,
316    stack: &mut HashSet<NodeId>,
317) -> bool {
318    if stack.contains(&start) {
319        return true;
320    }
321    if visited.contains(&start) {
322        return false;
323    }
324    visited.insert(start);
325    stack.insert(start);
326    let s = &m.states[start];
327    if let Some(branches) = &s.choice {
328        for b in branches {
329            if m.states[b.target].kind == StateKind::Choice {
330                if has_choice_cycle(m, b.target, visited, stack) {
331                    return true;
332                }
333            }
334        }
335    }
336    stack.remove(&start);
337    false
338}
339
340// --- contracts (§7) --------------------------------------------------------
341
342fn validate_contracts(
343    m: &Machine,
344    contracts: &BTreeMap<String, Contract>,
345    errors: &mut Vec<LoadError>,
346) {
347    // gather all handled event names and spawned def ids
348    let mut handled_events: HashSet<String> = HashSet::new();
349    let mut spawned_defs: HashSet<String> = HashSet::new();
350    let mut all_names: HashSet<String> = HashSet::new();
351    for s in &m.states {
352        all_names.insert(s.id.clone());
353        for ev in s.on_events.keys() {
354            handled_events.insert(ev.clone());
355        }
356        collect_spawns(&s.entry, &mut spawned_defs);
357        collect_spawns(&s.exit, &mut spawned_defs);
358        for ts in s.on_events.values() {
359            for t in ts {
360                collect_spawns(&t.action, &mut spawned_defs);
361            }
362        }
363        if let Some(init) = &s.initial {
364            collect_spawns(&init.action, &mut spawned_defs);
365        }
366        for a in &s.after {
367            collect_spawns(&a.action, &mut spawned_defs);
368        }
369        if let Some(branches) = &s.choice {
370            for b in branches {
371                collect_spawns(&b.action, &mut spawned_defs);
372            }
373        }
374    }
375
376    for cid in &m.contracts {
377        let contract = match contracts.get(cid) {
378            Some(c) => c,
379            None => continue, // cannot verify a contract whose definition is absent
380        };
381        for ev in &contract.requires.events {
382            if !handled_events.contains(ev) {
383                errors.push(LoadError {
384                    path: format!("contract '{}'", cid),
385                    message: format!("required event '{ev}' is not handled anywhere"),
386                });
387            }
388        }
389        for st in &contract.requires.states {
390            if !all_names.contains(st) {
391                errors.push(LoadError {
392                    path: format!("contract '{}'", cid),
393                    message: format!("required state '{st}' is not declared"),
394                });
395            }
396        }
397        for sp in &contract.requires.spawns {
398            if !spawned_defs.contains(sp) {
399                errors.push(LoadError {
400                    path: format!("contract '{}'", cid),
401                    message: format!("required spawn '{sp}' does not appear in any action"),
402                });
403            }
404        }
405    }
406}
407
408fn collect_spawns(actions: &[Action], into: &mut HashSet<String>) {
409    for a in actions {
410        if let Action::Spawn { def, .. } = a {
411            into.insert(def.clone());
412        }
413    }
414}
415
416// ---------------------------------------------------------------------------
417// A tiny regex implementation (no external crate) sufficient for identifier
418// validation: `^[A-Za-z_][A-Za-z0-9_]*$`.
419
420mod regex_lite {
421    pub struct Regex;
422    pub fn new(_pat: &str) -> Regex {
423        Regex
424    }
425    impl Regex {
426        pub fn is_match(&self, s: &str) -> bool {
427            let mut chars = s.chars();
428            match chars.next() {
429                Some(c) if c.is_ascii_alphabetic() || c == '_' => {}
430                _ => return s.is_empty(),
431            }
432            s.chars()
433                .all(|c| c.is_ascii_alphanumeric() || c == '_')
434        }
435    }
436}
437