Establish OA/SA prototype baseline and first-release work
This commit is contained in:
@@ -0,0 +1,469 @@
|
||||
//! Structural state-machine rules. Expressions describe intent; they are not executed.
|
||||
use crate::{
|
||||
validation::{Issue, ancestor_of_kind, error, warning},
|
||||
*,
|
||||
};
|
||||
use std::collections::BTreeSet;
|
||||
|
||||
fn ancestors(p: &Project, id: Id) -> Vec<Id> {
|
||||
let mut result = Vec::new();
|
||||
let mut current = p.elements.get(&id).and_then(|e| e.parent);
|
||||
let mut seen = BTreeSet::from([id]);
|
||||
while let Some(id) = current {
|
||||
if !seen.insert(id) {
|
||||
break;
|
||||
}
|
||||
result.push(id);
|
||||
current = p.elements.get(&id).and_then(|e| e.parent);
|
||||
}
|
||||
result
|
||||
}
|
||||
fn within(p: &Project, id: Id, owner: Id) -> bool {
|
||||
ancestors(p, id).contains(&owner)
|
||||
}
|
||||
fn boundary(p: &Project, vertex: &Element) -> Option<Id> {
|
||||
vertex
|
||||
.parent
|
||||
.and_then(|region| p.elements.get(®ion))
|
||||
.and_then(|region| region.parent)
|
||||
}
|
||||
fn first_region(p: &Project, vertex: Id, owner: Id) -> Option<Id> {
|
||||
ancestors(p, vertex).into_iter().find(|id| {
|
||||
p.elements
|
||||
.get(id)
|
||||
.is_some_and(|e| e.kind() == Kind::Region && e.parent == Some(owner))
|
||||
})
|
||||
}
|
||||
fn edges<'a>(
|
||||
p: &'a Project,
|
||||
candidate: Option<&'a Relation>,
|
||||
) -> impl Iterator<Item = &'a Relation> {
|
||||
p.relations
|
||||
.values()
|
||||
.filter(move |r| candidate.is_none_or(|c| c.id != r.id))
|
||||
.chain(candidate)
|
||||
.filter(|r| r.kind() == RelationKind::StateTransition)
|
||||
}
|
||||
fn guard(r: &Relation) -> &str {
|
||||
match &r.body {
|
||||
RelationBody::StateTransition { guard, .. } => guard.trim(),
|
||||
_ => "",
|
||||
}
|
||||
}
|
||||
fn orthogonal(p: &Project, arms: &[Id]) -> bool {
|
||||
let Some(first) = arms.first() else {
|
||||
return true;
|
||||
};
|
||||
if arms.len() < 2 {
|
||||
return true;
|
||||
}
|
||||
let Some(owner) = ancestors(p, *first).into_iter().find(|id| {
|
||||
p.elements
|
||||
.get(id)
|
||||
.is_some_and(|e| e.kind().is_stable_state() || e.kind() == Kind::StateMachine)
|
||||
&& arms.iter().all(|arm| within(p, *arm, *id))
|
||||
}) else {
|
||||
return false;
|
||||
};
|
||||
let regions: Option<BTreeSet<_>> = arms
|
||||
.iter()
|
||||
.map(|arm| first_region(p, *arm, owner))
|
||||
.collect();
|
||||
regions.is_some_and(|regions| regions.len() == arms.len())
|
||||
}
|
||||
|
||||
pub(crate) fn validate_transition(
|
||||
p: &Project,
|
||||
r: &Relation,
|
||||
a: &Element,
|
||||
b: &Element,
|
||||
out: &mut Vec<Issue>,
|
||||
) {
|
||||
let RelationBody::StateTransition {
|
||||
transition_kind,
|
||||
trigger,
|
||||
triggers,
|
||||
guard,
|
||||
..
|
||||
} = &r.body
|
||||
else {
|
||||
return;
|
||||
};
|
||||
let machine = ancestor_of_kind(p, a.id, Kind::StateMachine);
|
||||
if machine.is_none() || machine != ancestor_of_kind(p, b.id, Kind::StateMachine) {
|
||||
error(
|
||||
out,
|
||||
r.id,
|
||||
"transition_machine",
|
||||
"endpoints",
|
||||
"State transition endpoints belong to one state machine.",
|
||||
);
|
||||
}
|
||||
if !a.kind().is_state() || !b.kind().is_state() {
|
||||
return;
|
||||
}
|
||||
if a.id == b.id && !a.kind().is_stable_state() {
|
||||
error(
|
||||
out,
|
||||
r.id,
|
||||
"pseudostate_self",
|
||||
"endpoints",
|
||||
"Only a State or Mode can have a self-transition.",
|
||||
);
|
||||
}
|
||||
let valid_kind = match transition_kind {
|
||||
TransitionKind::Internal => a.kind().is_stable_state() && a.id == b.id,
|
||||
TransitionKind::Local if a.kind() == Kind::EntryPoint => {
|
||||
boundary(p, a).is_some_and(|owner| within(p, b.id, owner))
|
||||
}
|
||||
TransitionKind::Local => {
|
||||
a.kind().is_stable_state()
|
||||
&& p.children(a.id).any(|e| e.kind() == Kind::Region)
|
||||
&& within(p, b.id, a.id)
|
||||
}
|
||||
TransitionKind::External => a.kind() != Kind::EntryPoint,
|
||||
};
|
||||
if !valid_kind {
|
||||
error(
|
||||
out,
|
||||
r.id,
|
||||
"transition_kind",
|
||||
"transition_kind",
|
||||
"Internal requires one stable state; Local goes from a composite or EntryPoint into its boundary; EntryPoint routing must be Local.",
|
||||
);
|
||||
}
|
||||
if matches!(a.kind(), Kind::Final | Kind::Terminate) || b.kind() == Kind::Initial {
|
||||
error(
|
||||
out,
|
||||
r.id,
|
||||
"pseudostate_direction",
|
||||
"endpoints",
|
||||
"Final/Terminate have no outgoing transitions; Initial has no incoming transition.",
|
||||
);
|
||||
}
|
||||
let triggered = !trigger.trim().is_empty() || !triggers.is_empty();
|
||||
if !a.kind().is_stable_state() && triggered {
|
||||
error(
|
||||
out,
|
||||
r.id,
|
||||
if a.kind() == Kind::Initial {
|
||||
"initial_transition"
|
||||
} else {
|
||||
"pseudostate_trigger"
|
||||
},
|
||||
"triggers",
|
||||
"Pseudostate routing cannot wait for an event/work trigger; put the trigger on the incoming stable-state transition.",
|
||||
);
|
||||
}
|
||||
if (matches!(
|
||||
a.kind(),
|
||||
Kind::Initial | Kind::Fork | Kind::ShallowHistory | Kind::DeepHistory
|
||||
) || b.kind() == Kind::Join)
|
||||
&& (!guard.trim().is_empty() || (b.kind() == Kind::Join && triggered))
|
||||
{
|
||||
error(
|
||||
out,
|
||||
r.id,
|
||||
if a.kind() == Kind::Initial {
|
||||
"initial_transition"
|
||||
} else {
|
||||
"pseudostate_segment"
|
||||
},
|
||||
"guard",
|
||||
"Initial/history fallback and Fork output/Join input segments have no guard or trigger.",
|
||||
);
|
||||
}
|
||||
if a.kind() == Kind::Fork && !b.kind().is_stable_state()
|
||||
|| b.kind() == Kind::Join && !a.kind().is_stable_state()
|
||||
{
|
||||
error(
|
||||
out,
|
||||
r.id,
|
||||
"orthogonal_endpoint",
|
||||
"endpoints",
|
||||
"Fork outputs and Join inputs connect stable States/Modes in distinct orthogonal regions.",
|
||||
);
|
||||
}
|
||||
if matches!(a.kind(), Kind::ShallowHistory | Kind::DeepHistory) {
|
||||
let scope = a.parent.is_some_and(|region| {
|
||||
if a.kind() == Kind::ShallowHistory {
|
||||
b.parent == Some(region)
|
||||
} else {
|
||||
within(p, b.id, region)
|
||||
}
|
||||
});
|
||||
if !b.kind().is_stable_state() || !scope {
|
||||
error(
|
||||
out,
|
||||
r.id,
|
||||
"history_scope",
|
||||
"target",
|
||||
"Shallow history falls back to a direct stable child of its region; deep history to a stable descendant within that region.",
|
||||
);
|
||||
}
|
||||
}
|
||||
for (point, other, outgoing) in [(a, b, true), (b, a, false)] {
|
||||
if !matches!(point.kind(), Kind::EntryPoint | Kind::ExitPoint) {
|
||||
continue;
|
||||
}
|
||||
let Some(owner) = boundary(p, point) else {
|
||||
continue;
|
||||
};
|
||||
let needs_inside = (point.kind() == Kind::EntryPoint) == outgoing;
|
||||
if within(p, other.id, owner) != needs_inside || other.id == owner {
|
||||
error(
|
||||
out,
|
||||
r.id,
|
||||
"boundary_transition",
|
||||
"endpoints",
|
||||
"EntryPoint routes from outside to inside its owner boundary; ExitPoint routes from inside to outside it.",
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) fn validate_vertex(
|
||||
p: &Project,
|
||||
e: &Element,
|
||||
candidate: Option<&Relation>,
|
||||
out: &mut Vec<Issue>,
|
||||
) {
|
||||
if !e.kind().is_state() {
|
||||
return;
|
||||
}
|
||||
let incoming: Vec<_> = edges(p, candidate).filter(|r| r.target() == e.id).collect();
|
||||
let outgoing: Vec<_> = edges(p, candidate).filter(|r| r.source() == e.id).collect();
|
||||
let (ins, outs) = (incoming.len(), outgoing.len());
|
||||
let max_in = matches!(e.kind(), Kind::Choice | Kind::Fork).then_some(1);
|
||||
let max_out = matches!(
|
||||
e.kind(),
|
||||
Kind::Initial | Kind::Join | Kind::ShallowHistory | Kind::DeepHistory | Kind::ExitPoint
|
||||
)
|
||||
.then_some(1);
|
||||
if max_in.is_some_and(|max| ins > max) || max_out.is_some_and(|max| outs > max) {
|
||||
error(
|
||||
out,
|
||||
e.id,
|
||||
if e.kind() == Kind::Initial {
|
||||
"initial_transition_count"
|
||||
} else {
|
||||
"pseudostate_cardinality"
|
||||
},
|
||||
"body",
|
||||
format!(
|
||||
"{} has too many {} transitions.",
|
||||
e.kind(),
|
||||
if max_in.is_some_and(|max| ins > max) {
|
||||
"incoming"
|
||||
} else {
|
||||
"outgoing"
|
||||
}
|
||||
),
|
||||
);
|
||||
}
|
||||
let incomplete = match e.kind() {
|
||||
Kind::Initial | Kind::ShallowHistory | Kind::DeepHistory => outs == 0,
|
||||
Kind::Final | Kind::Terminate => ins == 0,
|
||||
Kind::Choice | Kind::Fork => ins == 0 || outs < 2,
|
||||
Kind::Join => ins < 2 || outs == 0,
|
||||
Kind::Junction => ins == 0 || outs == 0,
|
||||
Kind::EntryPoint => outs == 0,
|
||||
Kind::ExitPoint => {
|
||||
ins == 0
|
||||
|| (outs == 0
|
||||
&& boundary(p, e)
|
||||
.and_then(|id| p.elements.get(&id))
|
||||
.is_some_and(|e| e.kind() != Kind::StateMachine))
|
||||
}
|
||||
_ => false,
|
||||
};
|
||||
if incomplete {
|
||||
warning(
|
||||
out,
|
||||
e.id,
|
||||
"incomplete_state_vertex",
|
||||
"body",
|
||||
format!(
|
||||
"Finish the required {} incoming/outgoing routing; incomplete vertices can be saved while wiring.",
|
||||
e.kind()
|
||||
),
|
||||
);
|
||||
}
|
||||
if e.kind() == Kind::Choice {
|
||||
let defaults = outgoing.iter().filter(|r| guard(r) == "else").count();
|
||||
if defaults > 1 {
|
||||
error(
|
||||
out,
|
||||
e.id,
|
||||
"choice_default",
|
||||
"guard",
|
||||
"Choice has at most one literal else branch.",
|
||||
);
|
||||
}
|
||||
if defaults == 0 {
|
||||
warning(
|
||||
out,
|
||||
e.id,
|
||||
"missing_choice_default",
|
||||
"guard",
|
||||
"Add an else branch, or review and document why no alternative may apply.",
|
||||
);
|
||||
}
|
||||
if outgoing.iter().any(|r| guard(r).is_empty()) {
|
||||
warning(
|
||||
out,
|
||||
e.id,
|
||||
"missing_choice_guard",
|
||||
"guard",
|
||||
"Each Choice alternative needs an explicit guard or literal else.",
|
||||
);
|
||||
}
|
||||
}
|
||||
if e.kind() == Kind::Junction && outs > 1 && outgoing.iter().any(|r| guard(r).is_empty()) {
|
||||
warning(
|
||||
out,
|
||||
e.id,
|
||||
"junction_guard",
|
||||
"guard",
|
||||
"Review the unguarded Junction alternatives; guard expressions are not interpreted for disjointness.",
|
||||
);
|
||||
}
|
||||
if matches!(e.kind(), Kind::Fork | Kind::Join) {
|
||||
let arms: Vec<_> = if e.kind() == Kind::Fork {
|
||||
outgoing.iter().map(|r| r.target()).collect()
|
||||
} else {
|
||||
incoming.iter().map(|r| r.source()).collect()
|
||||
};
|
||||
if !orthogonal(p, &arms) {
|
||||
error(
|
||||
out,
|
||||
e.id,
|
||||
"orthogonal_regions",
|
||||
"endpoints",
|
||||
"Each Fork/Join arm must occupy a distinct first region below their nearest common composite or machine; deeper nesting does not create concurrency.",
|
||||
);
|
||||
}
|
||||
}
|
||||
if e.kind() == Kind::EntryPoint
|
||||
&& let Some(owner) = boundary(p, e)
|
||||
{
|
||||
let regions: Vec<_> = outgoing
|
||||
.iter()
|
||||
.filter_map(|r| first_region(p, r.target(), owner))
|
||||
.collect();
|
||||
let distinct: BTreeSet<_> = regions.iter().copied().collect();
|
||||
if distinct.len() != regions.len() {
|
||||
error(
|
||||
out,
|
||||
e.id,
|
||||
"entry_point_cardinality",
|
||||
"target",
|
||||
"EntryPoint has at most one outgoing transition per destination region.",
|
||||
);
|
||||
}
|
||||
if p.children(owner)
|
||||
.filter(|r| r.kind() == Kind::Region)
|
||||
.any(|r| {
|
||||
!distinct.contains(&r.id) && !p.children(r.id).any(|v| v.kind() == Kind::Initial)
|
||||
})
|
||||
{
|
||||
warning(
|
||||
out,
|
||||
e.id,
|
||||
"entry_region_default",
|
||||
"target",
|
||||
"Provide an EntryPoint route or Initial default entry for every concurrent region in this boundary.",
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
pub(crate) fn validate_graph(p: &Project, out: &mut Vec<Issue>) {
|
||||
for e in p.elements.values() {
|
||||
validate_vertex(p, e, None, out);
|
||||
if e.kind() == Kind::Region {
|
||||
for (kind, code) in [
|
||||
(Kind::Initial, "multiple_initial"),
|
||||
(Kind::ShallowHistory, "multiple_shallow_history"),
|
||||
(Kind::DeepHistory, "multiple_deep_history"),
|
||||
] {
|
||||
if p.children(e.id).filter(|c| c.kind() == kind).count() > 1 {
|
||||
error(
|
||||
out,
|
||||
e.id,
|
||||
code,
|
||||
"parent",
|
||||
format!("A region has at most one {kind}."),
|
||||
);
|
||||
}
|
||||
}
|
||||
let explicit_entry =
|
||||
edges(p, None).any(|r| within(p, r.target(), e.id) && !within(p, r.source(), e.id));
|
||||
if !p
|
||||
.children(e.id)
|
||||
.any(|v| matches!(v.kind(), Kind::Initial | Kind::EntryPoint))
|
||||
&& !explicit_entry
|
||||
{
|
||||
warning(
|
||||
out,
|
||||
e.id,
|
||||
"missing_initial",
|
||||
"parent",
|
||||
"Add an Initial default entry or an explicit incoming entry path for this region.",
|
||||
);
|
||||
}
|
||||
}
|
||||
if e.kind() == Kind::StateMachine {
|
||||
validate_reachability(p, e.id, out);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
fn validate_reachability(p: &Project, machine: Id, out: &mut Vec<Issue>) {
|
||||
let mut pending: Vec<_> = p
|
||||
.children(machine)
|
||||
.filter(|e| e.kind() == Kind::Region)
|
||||
.flat_map(|region| p.children(region.id))
|
||||
.filter(|e| matches!(e.kind(), Kind::Initial | Kind::EntryPoint))
|
||||
.map(|e| e.id)
|
||||
.collect();
|
||||
let mut reached = BTreeSet::new();
|
||||
while let Some(id) = pending.pop() {
|
||||
if !reached.insert(id) {
|
||||
continue;
|
||||
}
|
||||
pending.extend(
|
||||
edges(p, None)
|
||||
.filter(|r| r.source() == id)
|
||||
.map(Relation::target),
|
||||
);
|
||||
// Entering a nested vertex activates its composite ancestors. Reaching a
|
||||
// composite also permits each region's default entry; this deliberately
|
||||
// over-approximates guards/history instead of pretending to execute them.
|
||||
pending.extend(ancestors(p, id).into_iter().filter(|id| {
|
||||
p.elements
|
||||
.get(id)
|
||||
.is_some_and(|e| e.kind().is_stable_state())
|
||||
}));
|
||||
pending.extend(
|
||||
p.children(id)
|
||||
.filter(|e| e.kind() == Kind::Region)
|
||||
.flat_map(|region| p.children(region.id))
|
||||
.filter(|e| e.kind() == Kind::Initial)
|
||||
.map(|e| e.id),
|
||||
);
|
||||
}
|
||||
for e in p.elements.values().filter(|e| {
|
||||
e.kind().is_state() && ancestor_of_kind(p, e.id, Kind::StateMachine) == Some(machine)
|
||||
}) {
|
||||
if !reached.contains(&e.id) {
|
||||
warning(
|
||||
out,
|
||||
e.id,
|
||||
"unreachable_state",
|
||||
"body",
|
||||
"No structural path from a machine entry reaches this vertex; review entry, nesting and transitions (guards are not executed).",
|
||||
);
|
||||
}
|
||||
}
|
||||
}
|
||||
Reference in New Issue
Block a user