Cord support matrix
The lexer, parser, semantic phase, explorer, and replay implementation define SEK's Cord behavior. Legacy Spec Explorer documentation and successful parsing alone do not prove runtime support.
Status definitions
- Supported — parsed and consumed with tested runtime semantics.
- Conditional — usable only with the stated restrictions and outcome verification.
- Parsed-only — accepted syntax without useful runtime semantics; do not author it.
- Unsupported — rejected or swallowed without usable semantics; do not author it.
Matrix
| Surface | Status | Authoring rule |
|---|---|---|
| Config/machine declarations and inheritance | Supported | Reject unknown or cyclic bases |
using name resolution |
Parsed-only | Keep only for readability |
| Explicit actions | Supported | Preferred; keep scenario short labels unique |
action all |
Conditional | Verify exact rules; no-match can expose all rules |
public/internal/static/abstract modifiers |
Parsed-only | Cosmetic compatibility only |
exclude |
Parsed-only/unsafe | Never author |
Config-level action event |
Conditional | Tagged, but replay is direct invocation |
Config/behavior call and return kinds |
Parsed-only | Do not rely on separate call/return semantics |
Condition.In |
Supported | Use finite domains and inspect emitted values |
Condition.IsTrue |
Conditional | Prefer simple supported expressions; verify rows |
| Interaction/Pairwise/Expand/Isolated/Seeded | Supported/Conditional | Strongest on scalar/struct paths |
Probability.IsTrue + RandomSeed |
Conditional | Both branches are unioned; seed orders, not samples |
| Legacy parenthesized action domains | Parsed-only | Never author |
Config domain / bound clauses |
Unsupported/swallowed | Never author |
;, |, grouping, repetition |
Supported | Parenthesize mixed expressions |
_, ..., ! |
Conditional | Requires a known alphabet; negation is atomic-target only |
-> and binary & |
Supported lowering | Understand context and binary-block semantics |
Root/current ||, |||, |?| |
Conditional | Keep at root; verify same-label interleaving |
| Parallel nested beneath other algebra | Unsupported behavior | Can become empty; never author |
Argument pinning and per-argument _ |
Supported | A non-empty argument list pins |
| Reachable object domains | Conditional | Verify identity and emitted arguments |
new T |
Conditional | Ordinary model action, not intrinsic allocation |
| Parameterized machines | Conditional | Whole-token substitution; verify arity/types |
Bounded let |
Conditional | Prove nonzero concrete assignments |
Top-level model-backed bind |
Conditional | Domain replacement, not intersection |
State preconstraint {. ... .}: |
Conditional | Reflective assignment may fail silently |
: fail in a model slice |
Conditional | Inspect fail metadata; command exit can still succeed |
| Direct model construct | Supported | Preferred core machine |
| Model-backed accepting paths | Supported | Verify a non-empty accepted result |
| Pure-behavior construct targets | Unsupported/unsafe | Explore pure behavior directly |
| Bounded exploration | Conditional | PathDepth is the reliable option |
| Test-case construct | Conditional | Target plus short/long path strategy |
| Point-shoot | Conditional | Simple Boolean goal; verify phases/goals |
| Accept-completion | Conditional | Acceptance pruning; completer semantics incomplete |
| Requirement coverage | Conditional | Aggregate report, not directed generation |
| Model return value in graph | Supported | Reflected model result is recorded |
/ return binding during slicing |
Conditional | Model-time dataflow only |
| Dynamic SUT return binding in generated replay | Unsupported | Use a custom harness |
Collection-size domains, maplets, TypeBinding |
Unsupported | Do not author |
| Hiding, postconstraints, broader legacy grammar | Unsupported | Do not author |
Failure-closed checklist
- Treat semantic warnings as failures.
- Compare the explored action universe with the expected
[Rule]inventory. - Give every scalar parameter a finite domain; do not rely on unconstrained enumeration.
- Verify constraints affect emitted arguments; unknown or unrecognized constraints can be dropped.
- Keep
letfinite/non-empty andbindtop-level; inspect replacement domains. - Keep parallel at the current/root composition.
- Use constructs only around model-backed targets.
- Avoid reflective state slices unless no modeled initialization action works.
- Convert reached
: failstates into an external failing verdict. - Generate model-derived negative conformance from an unsliced machine; slices omit it.
- Do not infer per-input rejection coverage from one action-level negative edge.
- Do not claim asynchronous event conformance from generated
Observe. - Do not claim dynamic SUT-handle threading from
/binding in generated tests. - Reject bounds, empty/suspicious graphs, missing actions, unexpected acceptance/fail states, unmet requirements, and missing negative tests.
- Build current model and SUT binaries; reject stale graphs and generated suites.
- Treat
sek validateas necessary but insufficient for scopes, invocation references, arity, finite domains, constructs, and runtime semantics.