Skip to content
Open
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
13 commits
Select commit Hold shift + click to select a range
b136561
fix(runtime): observe change-trigger conditions at every feature write
devin-ai-integration[bot] Oct 2, 2026
d045c9d
feat(lower,runtime): run effects and pseudostate routes of transition…
devin-ai-integration[bot] Oct 2, 2026
7e1a828
test(runtime): admit both composite-entry interleavings
devin-ai-integration[bot] Oct 2, 2026
b938fe8
docs(states): derive entry-transition effects and write-granular chan…
devin-ai-integration[bot] Oct 2, 2026
68fea83
fix(check): keep the accepter-source diagnostic for a triggered trans…
devin-ai-integration[bot] Oct 2, 2026
82a9904
docs(states): name the accepter rule for a triggered transition out o…
devin-ai-integration[bot] Oct 2, 2026
1a94509
fix(runtime): read entry-route junctions before the entry effect, kee…
devin-ai-integration[bot] Oct 3, 2026
1f83547
refactor(runtime): drop the dead choice branch from defaultEntryRoute…
devin-ai-integration[bot] Oct 3, 2026
3d70265
Merge remote-tracking branch 'origin/develop' into fix/state-machine-…
devin-ai-integration[bot] Oct 3, 2026
9c9a7ff
fix(runtime): read a nested default entry's junction when its entry t…
devin-ai-integration[bot] Oct 3, 2026
174a894
test(runtime): make the outer-effect entry junction fixture discrimin…
devin-ai-integration[bot] Oct 3, 2026
208fd8c
docs(states): state the outer-effect entry junction fixture without r…
devin-ai-integration[bot] Oct 3, 2026
579c4f1
Merge remote-tracking branch 'origin/develop' into fix/state-machine-…
devin-ai-integration[bot] Oct 3, 2026
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions changes/unreleased/entry-transition-effects.added.md
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
- **Transitions out of a named entry action run effects and routes.** `entry action boot; transition boot do { … } then s;` runs its effect after the entry action and before `s` is entered, and may target a junction or choice of the same body, whose route is resolved after the entry action; availability checks only the incoming transition's own route, and a dead nested default-entry junction fails with a typed run error when its separate entry transition is taken. In a region of a parallel state the effect, like a compound transition's segment effect inside the region it enters, interleaves with the sibling regions' entries, and `-schedule explore` reaches every order. A trigger on such a transition, or an effect on the shorthand `entry; then s;`, is still rejected.
1 change: 1 addition & 0 deletions changes/unreleased/state-change-trigger-writes.fixed.md
Original file line number Diff line number Diff line change
@@ -0,0 +1 @@
- **Change triggers observe every completed write.** A state machine's `accept when <condition>` is re-evaluated after each completed feature write that touches a feature the condition reads, and every false-to-true rise queues one change signal, so a condition that becomes true and false again within one run-to-completion step still fires; a value one assignment writes and replaces before it completes raises no rise. Snapshots, held images, replay and `-schedule explore` carry the observed and pending rises.
159 changes: 95 additions & 64 deletions docs/internals/design/precise-semantics-alignment.md

Large diffs are not rendered by default.

25 changes: 16 additions & 9 deletions docs/internals/design/pseudostates.md
Original file line number Diff line number Diff line change
Expand Up @@ -24,7 +24,10 @@ Pseudostates are transient vertices in state machines that enable complex contro
- Used to merge multiple incoming transitions or split paths
- Several enabled branches are a transition choice point (`ChoiceTaken` at the junction,
enumerated by `explore`); an unguarded branch is the else branch
- No enabled branch disables the compound transition (PSSM *Junction 002*)
- No enabled branch on the transition's own route disables it; a junction on a composite's
nested default entry belongs to a separate transition out of `entry`, is read after the outer
effect and composite entry, and fails at run time with a typed no-way-through error if no
branch is enabled (SM46; PSSM *Junction 002* differs by design)

### Semantics

Expand Down Expand Up @@ -134,11 +137,14 @@ choice point at the junction the schedule policy draws and records only as the t
candidate another region's reaction disarms draws nothing; the unguarded segments are the
default when no guard holds — and goes on until the route reaches a state or a choice. The
guards read the data as it stands before the incoming transition's effect. If no static
branch is available, only `errNoWayThrough` leaves the compound transition unenabled before
selection; the occurrence remains available to another enabled transition, deferral, or unmatched
discard. A completion with no path is dropped. A history default route is checked this way only
when the source is outside the history owner, because leaving the owner may record the history
before its default route is read (see the precise-semantics alignment note, SM29 and SM32).
branch is available on the transition's own route, only `errNoWayThrough` leaves that transition
unenabled before selection; the occurrence remains available to another enabled transition,
deferral, or unmatched discard. A completion with no path is dropped. A junction on a composite's
nested default entry is read when its separate entry transition is taken, after the outer effect
and composite entry; if no branch is enabled, the run fails with a typed no-way-through error
(SM46). A history default route is checked this way only when the source is outside the history
owner, because leaving the owner may record the history before its default route is read (see the
precise-semantics alignment note, SM29, SM32 and SM46).

**Choice evaluation** is dynamic. `followOut` leaves the route open at a choice. Firing
(`travel`) then exits the states every branch of the open choice leaves — the source's ancestors
Expand Down Expand Up @@ -256,9 +262,10 @@ package JunctionTest {
2. **Junction:**
- Guards read before the incoming transition fires, in definition order; several holding is a
recorded choice point, as at a choice
- No way through leaves the compound transition unenabled before selection, so the occurrence
is handled as unmatched: another enabled transition may take it, it may be deferred, or it
may be discarded; a completion with no way through is dropped
- No way through on the transition's own route leaves it unenabled before selection, so the
occurrence is handled as unmatched: another enabled transition may take it, it may be
deferred, or it may be discarded; a completion with no way through is dropped. A dead
junction on a nested default entry instead fails when that entry transition is taken (SM46)
- Only `errNoWayThrough` disables; route cycles, unevaluable guards and binding failures remain
run errors, and static route checking stops at the first choice

Expand Down
8 changes: 8 additions & 0 deletions docs/internals/design/region-order-scheduling.md
Original file line number Diff line number Diff line change
Expand Up @@ -655,6 +655,14 @@ an empty `StatePerformance` and a completion like any other) and PSSM contradict
event is dispatched after the step whatever the source performs). That is a special case of the
translation's shape, not a semantics.

*Since resolved for these three.* The spelling argument above holds for the shorthand
`EntryTransitionMember` only. A transition out of a named entry action is a `TransitionUsage`
whose source is an action, a `NonStateTransitionPerformance` (`TransitionPerformances.kerml`):
it follows the entry action within the entry and runs its effect before the target's entry,
which is the entry-unit row exactly. The emitter now writes the initial transition that way, the
effect is a unit of its region's queue on the entry front, and *Entering 010*, *Entering 011* and
*Junction 005* pass with no runtime rule about completions.

**The first halves of the History tests are about the pool's order.** Both regions enter a
silent state whose completion is enabled at once. PSSM's pool holds the two completion events in
the order they were generated — §8.5.9, "a new `CompletionEventOccurrence` is placed into the
Expand Down
30 changes: 30 additions & 0 deletions docs/project/behavior-semantic-oracle.md
Original file line number Diff line number Diff line change
Expand Up @@ -1730,6 +1730,36 @@ which is drawn against the branches' remaining target entries, six outcomes.
`state_do_step_machine_before_top_entries` is the same shape at the machine, whose do behavior
begins before its top regions are entered: six outcomes.

### Effects on the way into the regions of a parallel state: each precedes its own target's entry, the regions interleave

Fixtures: `state_entry_transition_effect_regions` (golden, explored, checked),
`state_junction_inside_orthogonal_region` (golden, explored, checked).

A transition out of a named entry action, `entry action boot; transition boot do { … } then s;`,
is a `TransitionUsage` whose source is an action rather than a state, so its performance is a
`NonStateTransitionPerformance` (`TransitionPerformances.kerml`; `Actions.sysml`
`DecisionTransitionAction`, `Action::decisionTransitions`): `transitionLinkSource then effect`
and `effect then transitionLink.laterOccurrence` place the effect after the entry action and
before the target's `StatePerformance` begins, and `succession transitionLinkSource then
Performance::self` makes the transition part of the entry, not a step dispatched after it. It
has no trigger: an accepter needs a state source (the pilot's
`validateTransitionUsageTriggerActions`). The shorthand `entry; then s;` (§7.18.3
`EntryTransitionMember`, a `GuardedTargetSuccession`) still carries a guard at most. A segment
of a compound transition that continues inside a region of the parallel state it enters is the
same shape one level down: its effect is a `TransitionPerformance` step between the
pseudostate's predecessor and its target's entry.

The regions of a parallel state are `middle` steps of its `StatePerformance`
(`StatePerformances.kerml` `succession entry then middle`), concurrent with each other, and
nothing in either library orders one region's transition performance against another
region's. So the parallel state's own entry comes first, each region's effect precedes its own
target's entry, and the regions' chains interleave in every way: for a region whose chain is an
effect then an entry beside one whose chain is a single entry, three orders. PSSM's *Entering
010*, *Entering 011* and *Junction 005* admit exactly these linearizations. The executor
offers each effect as a unit of its region's queue on the entry front
(`state_unit_front.go` `entryTransitionEffectHead`, `state_region_entry.go` `enterRegion`), so
`-schedule explore` reaches each order.

### A succession outside a behavior body orders the performances it relates, wherever they run

Fixtures: `namespace_succession_chain_ends` (golden), `type_succession_performed_actions`
Expand Down
78 changes: 33 additions & 45 deletions docs/project/pssm-referee-baseline.json
Original file line number Diff line number Diff line change
Expand Up @@ -6,14 +6,14 @@
"url": "https://www.omg.org/spec/PSSM/20181101/PSSM_TestSuite.xmi",
"suiteDigest": "c355b249c356774377a46b60345019d827af1ce417bde88e533aa5f39206ae07",
"tests": 103,
"recorded": "2026-10-01",
"develop": "deca2b0389f796b02fa1c30a387617d0613a034c"
"recorded": "2026-10-03",
"develop": "3d45ca6fb200339461594cd086004e461633e6d1"
},
"buckets": {
"differs-by-design": 5,
"fail": 11,
"differs-by-design": 7,
"fail": 6,
"not-expressible": 34,
"pass": 53
"pass": 56
},
"tests": [
{
Expand Down Expand Up @@ -630,32 +630,24 @@
"name": "Entering 010",
"area": "Entering",
"class": "standard",
"bucket": "fail",
"reasons": [
"admitted trace not reached: S1(entry)::T2.1(effect)::S1.1(entry)::S2.1(entry)",
"admitted trace not reached: S1(entry)::T2.1(effect)::S2.1(entry)::S1.1(entry)"
],
"bucket": "pass",
"expected": [
"S1(entry)::S1.1(entry)::T2.1(effect)::S2.1(entry)",
"S1(entry)::T2.1(effect)::S1.1(entry)::S2.1(entry)",
"S1(entry)::T2.1(effect)::S2.1(entry)::S1.1(entry)"
],
"reached": [
"S1(entry)::S1.1(entry)::T2.1(effect)::S2.1(entry)"
"S1(entry)::S1.1(entry)::T2.1(effect)::S2.1(entry)",
"S1(entry)::T2.1(effect)::S1.1(entry)::S2.1(entry)",
"S1(entry)::T2.1(effect)::S2.1(entry)::S1.1(entry)"
],
"runs": 4
"runs": 20
},
{
"name": "Entering 011",
"area": "Entering",
"class": "standard",
"bucket": "fail",
"reasons": [
"admitted trace not reached: S1(entry)::T1.1(effect)::T2.1(effect)::S1.1(entry)::S1.2(entry)",
"admitted trace not reached: S1(entry)::T1.1(effect)::T2.1(effect)::S1.2(entry)::S1.1(entry)",
"admitted trace not reached: S1(entry)::T2.1(effect)::T1.1(effect)::S1.1(entry)::S1.2(entry)",
"admitted trace not reached: S1(entry)::T2.1(effect)::T1.1(effect)::S1.2(entry)::S1.1(entry)"
],
"bucket": "pass",
"expected": [
"S1(entry)::T1.1(effect)::S1.1(entry)::T2.1(effect)::S1.2(entry)",
"S1(entry)::T1.1(effect)::T2.1(effect)::S1.1(entry)::S1.2(entry)",
Expand All @@ -666,9 +658,13 @@
],
"reached": [
"S1(entry)::T1.1(effect)::S1.1(entry)::T2.1(effect)::S1.2(entry)",
"S1(entry)::T2.1(effect)::S1.2(entry)::T1.1(effect)::S1.1(entry)"
"S1(entry)::T1.1(effect)::T2.1(effect)::S1.1(entry)::S1.2(entry)",
"S1(entry)::T1.1(effect)::T2.1(effect)::S1.2(entry)::S1.1(entry)",
"S1(entry)::T2.1(effect)::S1.2(entry)::T1.1(effect)::S1.1(entry)",
"S1(entry)::T2.1(effect)::T1.1(effect)::S1.1(entry)::S1.2(entry)",
"S1(entry)::T2.1(effect)::T1.1(effect)::S1.2(entry)::S1.1(entry)"
],
"runs": 4
"runs": 40
},
{
"name": "Exiting 001",
Expand Down Expand Up @@ -1438,20 +1434,17 @@
"name": "Junction 002",
"area": "Junction",
"class": "extension",
"row": "SM32",
"rowKind": "agrees",
"bucket": "fail",
"row": "SM46",
"rowKind": "differs because v2 differs",
"bucket": "differs-by-design",
"reasons": [
"reached a trace the suite does not admit: S1(entry)",
"run error: process event: fire transition out of wait: entry transition through junction S1_Junction1: no way through: junction S1_Junction1: no guard evaluated to true",
"admitted trace not reached: T3(effect)",
"reports on SM32 (Junction or join with no path through): agrees"
"reports on SM46 (Junction on a nested default entry): differs because v2 differs"
],
"expected": [
"T3(effect)"
],
"reached": [
"S1(entry)"
],
"runs": 1
},
{
Expand All @@ -1473,40 +1466,35 @@
"name": "Junction 004",
"area": "Junction",
"class": "extension",
"row": "SM32",
"rowKind": "agrees",
"bucket": "fail",
"row": "SM46",
"rowKind": "differs because v2 differs",
"bucket": "differs-by-design",
"reasons": [
"reached a trace the suite does not admit: S1(entry)::T1.3(effect)::S1.2(exit)",
"run error: process event: fire transition out of wait: enter state: enter starting state in region S1/Region2: entry transition through junction S1_Junction1_2: no way through: junction S1_Junction1_2: no guard evaluated to true",
"admitted trace not reached: T3(effect)",
"reports on SM32 (Junction or join with no path through): agrees"
"reports on SM46 (Junction on a nested default entry): differs because v2 differs"
],
"expected": [
"T3(effect)"
],
"reached": [
"S1(entry)::T1.3(effect)::S1.2(exit)"
],
"runs": 2
"runs": 6
},
{
"name": "Junction 005",
"area": "Junction",
"class": "extension",
"bucket": "fail",
"reasons": [
"admitted trace not reached: S1(entry)::T2.1(effect)::S2.1(entry)::T1.3(effect)::S1.2(exit)::S1(exit)",
"admitted trace not reached: S1(entry)::T2.1(effect)::T1.3(effect)::S2.1(entry)::S1.2(exit)::S1(exit)"
],
"bucket": "pass",
"expected": [
"S1(entry)::T1.3(effect)::T2.1(effect)::S2.1(entry)::S1.2(exit)::S1(exit)",
"S1(entry)::T2.1(effect)::S2.1(entry)::T1.3(effect)::S1.2(exit)::S1(exit)",
"S1(entry)::T2.1(effect)::T1.3(effect)::S2.1(entry)::S1.2(exit)::S1(exit)"
],
"reached": [
"S1(entry)::T1.3(effect)::T2.1(effect)::S2.1(entry)::S1.2(exit)::S1(exit)"
"S1(entry)::T1.3(effect)::T2.1(effect)::S2.1(entry)::S1.2(exit)::S1(exit)",
"S1(entry)::T2.1(effect)::S2.1(entry)::T1.3(effect)::S1.2(exit)::S1(exit)",
"S1(entry)::T2.1(effect)::T1.3(effect)::S2.1(entry)::S1.2(exit)::S1(exit)"
],
"runs": 4
"runs": 20
},
{
"name": "Junction 006",
Expand Down
Loading
Loading