Profile contract
state.flat@1
One initial state, explicit terminal states, events and typed guards; safe trace evaluator does not execute actions.
graph projectionFlat lifecycle diagram · Trace validation
Open this profile in the gallery
Primary palette
Relationship roles
Legal endpoints
| Relation | Source roles | Target roles | Self relation |
|---|---|---|---|
state.transition | state.initial, state.state | state.final, state.state | Allowed |
Profile verification
- Exactly one initial marker and at least one final or terminal-tagged state. Initial has no incoming and exactly one unconditional, action-free outgoing transition; terminals have no outgoing.
- Every state is reachable and can reach a terminal; flat states do not contain nested fields/regions.
- Noninitial transitions have an event; typed guard conjunctions use declared finite input domains. Same-state/event alternatives must be provably disjoint within the analysis budget.
- Actions are references reported by the trace evaluator and are never executed; string UML guards/effects are outside this flat evaluator.
Profile defaults
Explicit file settings override eligible CSS, then these profile defaults and the common standard apply. Unspecified semantic facts remain unspecified.
{
"projection.kind": "graph",
"projection.profile": "state.flat@1",
"projection.analysis_budget": 4096
}Projection properties
kind, profile, inputs, analysis_budget, traces, iso, depth
Design operations
- Create states and transitions; edit event/typed guard/action references; declare inputs and supplied traces; inspect reachable paths and trace results.
Bounded analysis
Bounded deterministic trace evaluation: at most 100 traces, 1000 events each; declared-domain checks; exact expected final-state check; actionsExecuted=false.
Outside this profile
- hierarchical/parallel states
- SCXML/UML certification
- timers and executable actions