From b136561df9dd498ad041e40109315fa4d744477b Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Fri, 2 Oct 2026 22:09:13 +0000 Subject: [PATCH 01/17] fix(runtime): observe change-trigger conditions at every feature write Co-Authored-By: jason.han --- internal/exec/runtime/binding.go | 9 +- internal/exec/runtime/check_state.go | 15 +++ internal/exec/runtime/classifier_behavior.go | 2 + internal/exec/runtime/context.go | 13 ++ internal/exec/runtime/dependents.go | 16 +++ internal/exec/runtime/feature_write_watch.go | 106 ++++++++++++++++ internal/exec/runtime/held_image_behavior.go | 8 ++ internal/exec/runtime/instance.go | 2 + .../robustness_change_trigger_writes_test.go | 119 ++++++++++++++++++ internal/exec/runtime/snapshot.go | 25 ++-- internal/exec/runtime/state_change_trigger.go | 93 +++++++++++++- .../exec/runtime/state_change_trigger_test.go | 33 +++++ internal/exec/runtime/state_executor.go | 21 +++- internal/exec/runtime/state_statements.go | 2 + ..._change_trigger_atomic_write.expected.json | 17 +++ .../state_change_trigger_atomic_write.sysml | 26 ++++ ...e_change_trigger_atomic_write.trace.golden | 29 +++++ ...hange_trigger_transient_rise.expected.json | 10 ++ .../state_change_trigger_transient_rise.sysml | 22 ++++ ...change_trigger_transient_rise.trace.golden | 18 +++ ...state_change_trigger_transient_rise.golden | 38 ++++++ .../state_change_trigger_transient_rise.sysml | 22 ++++ 22 files changed, 635 insertions(+), 11 deletions(-) create mode 100644 internal/exec/runtime/feature_write_watch.go create mode 100644 internal/exec/runtime/robustness_change_trigger_writes_test.go create mode 100644 internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.trace.golden create mode 100644 tests/parser/testdata/parse/state_change_trigger_transient_rise.golden create mode 100644 tests/parser/testdata/parse/state_change_trigger_transient_rise.sysml diff --git a/internal/exec/runtime/binding.go b/internal/exec/runtime/binding.go index 3092ae130c..3b3807ce2d 100644 --- a/internal/exec/runtime/binding.go +++ b/internal/exec/runtime/binding.go @@ -188,11 +188,12 @@ func (ctx *Context) resolveBindingValue(inst *Instance, name string) (Value, boo if ctx.resolvingBindings[key] { return Value{}, false, &BindingCycleError{Features: []string{bindingLocationText(bindingLocation{instance: inst, name: name})}} } - if !target.BindingDerived || ctx.CompositeTypeOf(target.Feature) != nil { + if !target.BindingDerived || target.Written || ctx.CompositeTypeOf(target.Feature) != nil { return ctx.resolveBindings(inst, target, name, key) } // A value a binding gave is resolved afresh: clearing it and binding it again is one write. before := ctx.beforeWrite(target) + ctx.noteFeatureWrite(target) ctx.noteProbeWrite(target) target.Value = Value{} target.Values = Value{} @@ -870,7 +871,8 @@ func (ctx *Context) unmaterializedObjectEnd(endpoint bindingEndpoint) bool { // bindingEndpointDerived reports a feature end whose every value was assigned by a binding. func bindingEndpointDerived(endpoint bindingEndpoint) bool { for _, loc := range endpoint.locations { - if !loc.instance.FeatureValues[loc.name].BindingDerived { + fv := loc.instance.FeatureValues[loc.name] + if !fv.BindingDerived || fv.Written { return false } } @@ -889,6 +891,8 @@ func (ctx *Context) assignBindingEndpoint(endpoint bindingEndpoint, val Value, b } loc := endpoint.locations[0] fv := loc.instance.FeatureValues[loc.name] + endWrite := ctx.beginFeatureWrite(fv) + defer endWrite() before := ctx.beforeWrite(fv) err := ctx.assignBindingValue(loc.instance, fv, loc.name, val) ctx.afterWrite(fv, before) @@ -904,6 +908,7 @@ func (ctx *Context) assignBindingValue(inst *Instance, fv *FeatureValue, name st return err } ctx.noteProbeWrite(fv) + ctx.noteFeatureWrite(fv) if fv.Feature.Scalar() { fv.Value = val fv.Values = Value{} diff --git a/internal/exec/runtime/check_state.go b/internal/exec/runtime/check_state.go index d61a532b65..2161522136 100644 --- a/internal/exec/runtime/check_state.go +++ b/internal/exec/runtime/check_state.go @@ -306,6 +306,12 @@ func (s *stateSpeller) machine(e *StateExecutor) { for _, trans := range sortedTransitions(e.changeFired) { fmt.Fprintf(&s.out, " latched{%s}", s.transition(e, trans)) } + for _, trans := range sortedTransitions(e.changePending) { + fmt.Fprintf(&s.out, " pending{%s}", s.transition(e, trans)) + } + for _, trans := range sortedTransitionKeys(e.changeObserved) { + fmt.Fprintf(&s.out, " observed{%s=%t}", s.transition(e, trans), e.changeObserved[trans]) + } for _, act := range e.doActions { fmt.Fprintf(&s.out, " do{%s: %d pending", e.statePath(act.state), len(act.pending)) if act.run != nil { @@ -362,6 +368,15 @@ func sortedTransitions(m map[*lower.Transition]bool) []*lower.Transition { return transitions } +func sortedTransitionKeys(m map[*lower.Transition]bool) []*lower.Transition { + transitions := make([]*lower.Transition, 0, len(m)) + for trans := range m { + transitions = append(transitions, trans) + } + sort.Slice(transitions, func(i, j int) bool { return transitionKey(transitions[i]) < transitionKey(transitions[j]) }) + return transitions +} + // transitionKey identifies a transition by its source, target and where it was written. func transitionKey(trans *lower.Transition) string { key := nodeKey(trans.Source) + "->" + nodeKey(trans.Target) diff --git a/internal/exec/runtime/classifier_behavior.go b/internal/exec/runtime/classifier_behavior.go index 774e92ce3c..56f42cf196 100644 --- a/internal/exec/runtime/classifier_behavior.go +++ b/internal/exec/runtime/classifier_behavior.go @@ -1154,10 +1154,12 @@ func (ctx *Context) performanceOccurrence( sentinel, name, inst.ID, err) } ctx.noteProbeWrite(fv) + endWrite := ctx.beginFeatureWrite(fv) before := ctx.beforeWrite(fv) fv.Value = Value{Kind: ValInstance, Instance: occurrence.ID} fv.Materialized = true ctx.afterWrite(fv, before) + endWrite() return occurrence, nil } id, ok := fv.HeldValue().Object() diff --git a/internal/exec/runtime/context.go b/internal/exec/runtime/context.go index 91920fa77f..b9d6d2b8e1 100644 --- a/internal/exec/runtime/context.go +++ b/internal/exec/runtime/context.go @@ -126,6 +126,19 @@ type Context struct { // behaviorRunDepth is the number of classifier-behavior starts under way. behaviorRunDepth int + // stateExecutors are the live state machines this context can notify of a + // completed feature write, in creation order. + stateExecutors []*StateExecutor + + // featureWriteDepth coalesces nested stores into one completed write. + featureWriteDepth int + featureWriteState bool + featureWriteBefore map[*FeatureValue]featureWriteValue + featureWriteOrder []*FeatureValue + + // readRecorders collect feature values read by an observed change condition. + readRecorders [][]*FeatureValue + // declarative makes the context read declared values only: no classifier // behavior starts when an object is materialized (see DeclaredReader). declarative bool diff --git a/internal/exec/runtime/dependents.go b/internal/exec/runtime/dependents.go index 8718cfd6ba..095e820e56 100644 --- a/internal/exec/runtime/dependents.go +++ b/internal/exec/runtime/dependents.go @@ -113,6 +113,19 @@ func (ctx *Context) deriveOnce(inst *Instance, fv *FeatureValue, name string) (v // noteRead lists the value being derived, if any, as a dependent of the fv just read, // held by inst, and fv among what it reads; a derivation being observed sees the read. func (ctx *Context) noteRead(inst *Instance, fv *FeatureValue) { + if len(ctx.readRecorders) != 0 { + reads := ctx.readRecorders[len(ctx.readRecorders)-1] + found := false + for _, read := range reads { + if read == fv { + found = true + break + } + } + if !found { + ctx.readRecorders[len(ctx.readRecorders)-1] = append(reads, fv) + } + } if len(ctx.tracing) != 0 { ctx.observeRead(inst, fv) } @@ -296,6 +309,8 @@ func (ctx *Context) invalidateDependents(fv *FeatureValue) { // invalidate unmaterializes the dependents, transitively, returning those being // derived right now: each stays listed, its derivation stale as its source changed under it. func (ctx *Context) invalidate(dependents []*FeatureValue) (deriving []*FeatureValue) { + endWrite := ctx.beginFeatureWrite(nil) + defer endWrite() for _, dep := range dependents { switch { case ctx.markStale(dep): @@ -306,6 +321,7 @@ func (ctx *Context) invalidate(dependents []*FeatureValue) (deriving []*FeatureV ctx.invalidateDependents(dep) default: ctx.noteProbeWrite(dep) + ctx.noteFeatureWrite(dep) dep.Value, dep.Values, dep.Materialized, dep.intrinsic = Value{}, Value{}, false, false ctx.invalidateDependents(dep) } diff --git a/internal/exec/runtime/feature_write_watch.go b/internal/exec/runtime/feature_write_watch.go new file mode 100644 index 0000000000..0af8c1b811 --- /dev/null +++ b/internal/exec/runtime/feature_write_watch.go @@ -0,0 +1,106 @@ +package runtime + +import "slices" + +type featureWriteValue struct { + value Value + materialized bool +} + +func (ctx *Context) beginFeatureWrite(fv *FeatureValue) func() { + if ctx.probes > 0 || len(ctx.stateExecutors) == 0 { + return func() {} + } + if ctx.featureWriteDepth == 0 { + ctx.featureWriteBefore = make(map[*FeatureValue]featureWriteValue) + ctx.featureWriteOrder = nil + ctx.featureWriteState = false + } + ctx.featureWriteDepth++ + ctx.noteFeatureWrite(fv) + return func() { + ctx.endFeatureWrite() + } +} + +func (ctx *Context) noteFeatureWrite(fv *FeatureValue) { + if ctx.probes > 0 || ctx.featureWriteDepth == 0 || fv == nil { + return + } + if _, seen := ctx.featureWriteBefore[fv]; seen { + return + } + ctx.featureWriteBefore[fv] = featureWriteValue{value: fv.HeldValue(), materialized: fv.Materialized} + ctx.featureWriteOrder = append(ctx.featureWriteOrder, fv) +} + +func (ctx *Context) endFeatureWrite() { + if ctx.featureWriteDepth == 0 { + return + } + ctx.featureWriteDepth-- + if ctx.featureWriteDepth != 0 { + return + } + before, order := ctx.featureWriteBefore, ctx.featureWriteOrder + stateChanged := ctx.featureWriteState + ctx.featureWriteBefore, ctx.featureWriteOrder = nil, nil + ctx.featureWriteState = false + executors := slices.Clone(ctx.stateExecutors) + for _, fv := range order { + prior := before[fv] + if prior.materialized == fv.Materialized && (!fv.Materialized || heldSame(prior.value, fv.HeldValue())) { + continue + } + for _, exec := range executors { + exec.observeFeatureWrite(fv) + } + } + if stateChanged { + for _, exec := range executors { + exec.observeStateDataWrite() + } + } +} + +func (ctx *Context) noteStateDataWrite() { + if ctx.probes > 0 || len(ctx.stateExecutors) == 0 { + return + } + if ctx.featureWriteDepth > 0 { + ctx.featureWriteState = true + return + } + for _, exec := range slices.Clone(ctx.stateExecutors) { + exec.observeStateDataWrite() + } +} + +func (ctx *Context) beginChangeRead() func() []*FeatureValue { + reads := make([]*FeatureValue, 0) + ctx.readRecorders = append(ctx.readRecorders, reads) + return func() []*FeatureValue { + last := len(ctx.readRecorders) - 1 + reads = ctx.readRecorders[last] + ctx.readRecorders = ctx.readRecorders[:last] + return reads + } +} + +func (ctx *Context) registerStateExecutor(exec *StateExecutor) { + for _, registered := range ctx.stateExecutors { + if registered == exec { + return + } + } + ctx.stateExecutors = append(ctx.stateExecutors, exec) +} + +func (ctx *Context) unregisterStateExecutor(exec *StateExecutor) { + for i, registered := range ctx.stateExecutors { + if registered == exec { + ctx.stateExecutors = append(ctx.stateExecutors[:i], ctx.stateExecutors[i+1:]...) + return + } + } +} diff --git a/internal/exec/runtime/held_image_behavior.go b/internal/exec/runtime/held_image_behavior.go index f2e66595b2..bd8263ef64 100644 --- a/internal/exec/runtime/held_image_behavior.go +++ b/internal/exec/runtime/held_image_behavior.go @@ -122,6 +122,8 @@ type imagedState struct { timerScheduled map[*lower.Transition]bool timeTriggerVerdict map[*lower.Transition]error changeFired map[*lower.Transition]bool + changeObserved map[*lower.Transition]bool + changePending map[*lower.Transition]bool firingChange *lower.Transition firingNotes []RunNote changeRearmed map[*lower.Transition]bool @@ -371,6 +373,8 @@ func (t *imaging) stateExecutor(e *StateExecutor) (*imagedState, error) { timerScheduled: maps.Clone(e.timerScheduled), timeTriggerVerdict: maps.Clone(e.timeTriggerVerdict), changeFired: maps.Clone(e.changeFired), + changeObserved: maps.Clone(e.changeObserved), + changePending: maps.Clone(e.changePending), firingChange: e.firingChange, firingNotes: slices.Clone(e.firingNotes), changeRearmed: maps.Clone(e.changeRearmed), @@ -482,6 +486,7 @@ func (m *materializing) behavior(b imagedBehavior) error { if err := m.stateExecutor(exec, b.state); err != nil { return err } + dst.registerStateExecutor(exec) if b.onClock { dst.clock.attach(exec) } @@ -759,6 +764,9 @@ func (m *materializing) stateExecutor(e *StateExecutor, img *imagedState) error e.timerScheduled = maps.Clone(img.timerScheduled) e.timeTriggerVerdict = maps.Clone(img.timeTriggerVerdict) e.changeFired = maps.Clone(img.changeFired) + e.changeObserved = maps.Clone(img.changeObserved) + e.changePending = maps.Clone(img.changePending) + e.changeReads = make(map[*lower.Transition][]*FeatureValue) e.firingChange, e.firingNotes = img.firingChange, slices.Clone(img.firingNotes) e.changeRearmed = maps.Clone(img.changeRearmed) e.changeWaits = slices.Clone(img.changeWaits) diff --git a/internal/exec/runtime/instance.go b/internal/exec/runtime/instance.go index a409c16a29..bb6fd06d34 100644 --- a/internal/exec/runtime/instance.go +++ b/internal/exec/runtime/instance.go @@ -787,6 +787,8 @@ func (inst *Instance) storeFeatureValue(ctx *Context, fv *FeatureValue, name str if err != nil { return err } + endWrite := ctx.beginFeatureWrite(fv) + defer endWrite() return ctx.storedBeforeStarting(func() error { if err := ctx.holdWritten(inst, fv, value); err != nil { return fmt.Errorf("feature %s.%s: %w", inst.Type.Name, name, err) diff --git a/internal/exec/runtime/robustness_change_trigger_writes_test.go b/internal/exec/runtime/robustness_change_trigger_writes_test.go new file mode 100644 index 0000000000..d3e81d24e7 --- /dev/null +++ b/internal/exec/runtime/robustness_change_trigger_writes_test.go @@ -0,0 +1,119 @@ +package runtime + +import ( + "errors" + "testing" +) + +func TestRuntimeRobustnessChangeTriggerWrites(t *testing.T) { + t.Run("write-time condition error is deferred to poll", func(t *testing.T) { + exec := stateExecutorForSource(t, "Machine", `package test { + state Machine { + attribute divisor : Integer = 1; + entry; then changing; + state changing { + do action poison { + assign divisor := 0; + } + } + accept when divisor == 0 and 1 / divisor > 0 then done; + state done; + } + }`) + if err := exec.RunToCompletion(); !errors.Is(err, ErrDivisionByZero) { + t.Fatalf("RunToCompletion() = %v, want ErrDivisionByZero", err) + } + }) + + t.Run("many writes remain step bounded", func(t *testing.T) { + exec := stateExecutorForSource(t, "Machine", `package test { + state Machine { + attribute ready : Boolean = false; + attribute armed : Boolean = false; + entry; then start; + state start; + state spinning { + do action spin { + while true { + assign ready := not ready; + } + } + } + accept when ready and armed then done; + state done; + succession first start then spinning; + } + }`) + exec.ctx.maxSteps = 40 + if err := exec.RunToCompletion(); !errors.Is(err, ErrStepLimitExceeded) { + t.Fatalf("RunToCompletion() = %v, want ErrStepLimitExceeded", err) + } + }) + + t.Run("snapshot restores a pending rise", func(t *testing.T) { + ctx, holder, exec := changeTriggerWriteHolder(t) + if err := exec.RunToCompletion(); err != nil { + t.Fatalf("initial run: %v", err) + } + if err := holder.SetFeatureValue(ctx, "ready", boolValue(true)); err != nil { + t.Fatalf("raise ready: %v", err) + } + if err := holder.SetFeatureValue(ctx, "ready", boolValue(false)); err != nil { + t.Fatalf("lower ready: %v", err) + } + snapshot, err := exec.Snapshot() + if err != nil { + t.Fatalf("Snapshot: %v", err) + } + defer snapshot.Release() + + if err := exec.RunToCompletion(); err != nil { + t.Fatalf("run with pending rise: %v", err) + } + assertCurrentState(t, exec, "done") + snapshot.Restore() + if err := exec.RunToCompletion(); err != nil { + t.Fatalf("run after restore: %v", err) + } + assertCurrentState(t, exec, "done") + }) + + t.Run("check state distinguishes a pending rise", func(t *testing.T) { + ctx, holder, exec := changeTriggerWriteHolder(t) + if err := exec.RunToCompletion(); err != nil { + t.Fatalf("initial run: %v", err) + } + before := (&Invocation{States: []*StateExecutor{exec}}).canonicalState(nil).text + if err := holder.SetFeatureValue(ctx, "ready", boolValue(true)); err != nil { + t.Fatalf("raise ready: %v", err) + } + if err := holder.SetFeatureValue(ctx, "ready", boolValue(false)); err != nil { + t.Fatalf("lower ready: %v", err) + } + after := (&Invocation{States: []*StateExecutor{exec}}).canonicalState(nil).text + if before == after { + t.Fatalf("canonical state did not change after the rise:\n%s", before) + } + }) +} + +func changeTriggerWriteHolder(t *testing.T) (*Context, *Instance, *StateExecutor) { + t.Helper() + idx, _, ctx := buildRuntimeWithLibraries(t, "", parseAndBuild(t, ` + part def Holder { + attribute ready : Boolean = false; + exhibit state main { + entry; then waiting; + state waiting; + accept when ready then done; + state done; + } + } + part holder : Holder; + `)) + holder, err := ctx.occurrenceOf(resolveSymbol(t, idx.DocumentRoot(""), "holder")) + if err != nil { + t.Fatalf("occurrenceOf(holder): %v", err) + } + return ctx, holder, holder.ExhibitedStates()[0].State +} diff --git a/internal/exec/runtime/snapshot.go b/internal/exec/runtime/snapshot.go index 2b37f08ba8..0ff7d88616 100644 --- a/internal/exec/runtime/snapshot.go +++ b/internal/exec/runtime/snapshot.go @@ -69,6 +69,7 @@ type runCapture struct { heldBehaviors mapState[*ObjectBehavior, bool] holdingDriven bool clockRun *runState + stateExecutors []*StateExecutor } // traceCapture is a recorder's state at the mark. Records are only appended to, cut @@ -353,6 +354,7 @@ func (ctx *Context) captureRun() runCapture { heldBehaviors: captureMap(ctx.heldBehaviors), holdingDriven: ctx.holdingDriven, clockRun: ctx.clockRun.state, + stateExecutors: slices.Clone(ctx.stateExecutors), } return c } @@ -374,6 +376,7 @@ func (c runCapture) restore(ctx *Context) { ctx.heldBehaviors = c.heldBehaviors.restore() ctx.holdingDriven = c.holdingDriven ctx.clockRun.state = c.clockRun + ctx.stateExecutors = slices.Clone(c.stateExecutors) ctx.workChanged() } @@ -669,6 +672,8 @@ type stateCapture struct { timerScheduled mapState[*lower.Transition, bool] timeTriggerVerdict mapState[*lower.Transition, error] changeFired mapState[*lower.Transition, bool] + changeObserved mapState[*lower.Transition, bool] + changePending mapState[*lower.Transition, bool] firingChange *lower.Transition firingNotes []RunNote changeRearmed mapState[*lower.Transition, bool] @@ -726,6 +731,8 @@ func (e *StateExecutor) capture() stateCapture { timerScheduled: captureMap(e.timerScheduled), timeTriggerVerdict: captureMap(e.timeTriggerVerdict), changeFired: captureMap(e.changeFired), + changeObserved: captureMap(e.changeObserved), + changePending: captureMap(e.changePending), firingChange: e.firingChange, firingNotes: slices.Clone(e.firingNotes), changeRearmed: captureMap(e.changeRearmed), @@ -788,6 +795,9 @@ func (c stateCapture) restore() { e.timerScheduled = c.timerScheduled.restore() e.timeTriggerVerdict = c.timeTriggerVerdict.restore() e.changeFired = c.changeFired.restore() + e.changeObserved = c.changeObserved.restore() + e.changePending = c.changePending.restore() + e.changeReads = make(map[*lower.Transition][]*FeatureValue) e.firingChange, e.firingNotes = c.firingChange, slices.Clone(c.firingNotes) e.changeRearmed = c.changeRearmed.restore() e.changeWaits = slices.Clone(c.changeWaits) @@ -808,13 +818,14 @@ func cloneHeldEntries(entries []heldEntry) []heldEntry { cloned := make([]heldEntry, len(entries)) for i, entry := range entries { cloned[i] = heldEntry{ - owner: entry.owner, - regions: slices.Clone(entry.regions), - branches: maps.Clone(entry.branches), - chain: slices.Clone(entry.chain), - scopes: slices.Clone(entry.scopes), - machine: entry.machine, - firing: entry.firing.snapshot(), + owner: entry.owner, + regions: slices.Clone(entry.regions), + branches: maps.Clone(entry.branches), + chain: slices.Clone(entry.chain), + scopes: slices.Clone(entry.scopes), + machine: entry.machine, + firing: entry.firing.snapshot(), + routeEffects: cloneRouteEntryEffects(entry.routeEffects), } } return cloned diff --git a/internal/exec/runtime/state_change_trigger.go b/internal/exec/runtime/state_change_trigger.go index f5851da8da..c85c1ad7b1 100644 --- a/internal/exec/runtime/state_change_trigger.go +++ b/internal/exec/runtime/state_change_trigger.go @@ -133,6 +133,10 @@ func (e *StateExecutor) risenChanges() ([]*lower.Transition, bool) { defer e.ctx.beginProbe()() fired := maps.Clone(e.changeFired) defer func() { e.changeFired = fired }() + observed, pending, reads := maps.Clone(e.changeObserved), maps.Clone(e.changePending), maps.Clone(e.changeReads) + defer func() { + e.changeObserved, e.changePending, e.changeReads = observed, pending, reads + }() poll := newChangePoll() e.changeRearmed = make(map[*lower.Transition]bool) defer func() { e.changeRearmed = nil }() @@ -204,10 +208,15 @@ func (e *StateExecutor) observeChangeConditions(poll *changePoll) error { if err != nil { return fmt.Errorf("state %s: %w", source.Name, err) } - poll.condition[trans] = holds + pending := e.changePending[trans] + delete(e.changePending, trans) + poll.condition[trans] = holds || pending poll.observed = append(poll.observed, trans) + e.changeObserved[trans] = holds if !holds { delete(e.changeFired, trans) + } + if !poll.condition[trans] { poll.wait(trans, source.Name, "condition is false") continue } @@ -252,16 +261,98 @@ func (e *StateExecutor) probeChangeGuard(poll *changePoll, state *ast.StateNode, // changeConditionHolds evaluates one change condition in the scope the // transition was written in, the machine's data shadowing it. func (e *StateExecutor) changeConditionHolds(changeEvent *ast.ChangeEvent, trans *lower.Transition) (bool, error) { + if e.changeEvaluating { + return false, fmt.Errorf("change condition evaluation is reentrant") + } + e.changeEvaluating = true + defer func() { e.changeEvaluating = false }() + endRead := e.ctx.beginChangeRead() condVal, err := e.evalStepOf(trans.Source, changeEvent.Condition, trans.Scope) if err != nil { + endRead() return false, fmt.Errorf("eval change condition: %w", err) } if condVal.Kind != ValConst || condVal.Const.Kind != semantics.ValBool { + endRead() return false, fmt.Errorf("change condition must be boolean, got %v", condVal.Kind) } + e.changeReads[trans] = endRead() return condVal.Const.Bool, nil } +func (e *StateExecutor) observeFeatureWrite(fv *FeatureValue) { + if fv == nil || e.ctx.probes > 0 || e.changeEvaluating { + return + } + e.observeChangedValue(func(reads []*FeatureValue) bool { + return reads == nil || containsFeatureValue(reads, fv) + }) +} + +func (e *StateExecutor) observeStateDataWrite() { + if e.ctx.probes > 0 || e.changeEvaluating { + return + } + e.observeChangedValue(func([]*FeatureValue) bool { return true }) +} + +func (e *StateExecutor) observeChangedValue(relevant func([]*FeatureValue) bool) { + seen := make(map[*lower.Transition]bool) + observe := func(source *ast.StateNode, previouslyWatched bool) { + for _, trans := range e.graph.Transitions[source] { + changeEvent, ok := trans.Trigger.(*ast.ChangeEvent) + if !ok || seen[trans] { + continue + } + seen[trans] = true + if previouslyWatched { + if _, watched := e.changeObserved[trans]; !watched { + continue + } + } + if !relevant(e.changeReads[trans]) { + continue + } + var holds bool + var err error + e.preview(func() { holds, err = e.changeConditionHolds(changeEvent, trans) }) + if err != nil { + continue + } + observed := e.changeObserved[trans] + if !holds { + e.changeObserved[trans] = false + delete(e.changeFired, trans) + continue + } + if !observed && !e.changeFired[trans] { + e.changePending[trans] = true + } + e.changeObserved[trans] = true + } + } + for _, leaf := range e.activeLeaves() { + for _, source := range e.getParentChain(leaf) { + observe(source, false) + } + } + // A transition effect runs after the source exits but before the target + // enters. Enclosing states remain active throughout that interval. + observe(e.graph.Machine, true) + for _, source := range e.graph.States { + observe(source, true) + } +} + +func containsFeatureValue(values []*FeatureValue, target *FeatureValue) bool { + for _, value := range values { + if value == target { + return true + } + } + return false +} + // risenChangeTransitions returns the positions of the state's change-triggered // transitions whose condition has risen, whose guard holds and whose route has a // static way through, several enabled at once being a choice point. diff --git a/internal/exec/runtime/state_change_trigger_test.go b/internal/exec/runtime/state_change_trigger_test.go index 830cafaca4..5d12ec015f 100644 --- a/internal/exec/runtime/state_change_trigger_test.go +++ b/internal/exec/runtime/state_change_trigger_test.go @@ -61,6 +61,39 @@ func TestChangeTriggerFiresOnRiseFromDoBehavior(t *testing.T) { } } +func TestChangeTriggerKeepsOutsideWriteRiseUntilPoll(t *testing.T) { + idx, _, ctx := buildRuntimeWithLibraries(t, "", parseAndBuild(t, ` + part def Holder { + attribute ready : Boolean = false; + exhibit state main { + entry; then waiting; + state waiting; + accept when ready then done; + state done; + } + } + part holder : Holder; + `)) + holder, err := ctx.occurrenceOf(resolveSymbol(t, idx.DocumentRoot(""), "holder")) + if err != nil { + t.Fatalf("occurrenceOf(holder): %v", err) + } + exec := holder.ExhibitedStates()[0].State + if err := exec.RunToCompletion(); err != nil { + t.Fatalf("initial run: %v", err) + } + if err := holder.SetFeatureValue(ctx, "ready", boolValue(true)); err != nil { + t.Fatalf("raise ready: %v", err) + } + if err := holder.SetFeatureValue(ctx, "ready", boolValue(false)); err != nil { + t.Fatalf("lower ready: %v", err) + } + if err := exec.RunToCompletion(); err != nil { + t.Fatalf("run after external writes: %v", err) + } + assertCurrentState(t, exec, "done") +} + // A false change condition is not quiescence: the machine suspends, and says // which condition it is waiting on rather than reporting silent completion. func TestChangeTriggerFalseConditionIsReported(t *testing.T) { diff --git a/internal/exec/runtime/state_executor.go b/internal/exec/runtime/state_executor.go index 30c28efb84..ce6fec0551 100644 --- a/internal/exec/runtime/state_executor.go +++ b/internal/exec/runtime/state_executor.go @@ -124,7 +124,11 @@ type StateExecutor struct { // changeFired holds the change-triggered transitions already taken on a // condition that has stayed true, so an unchanged one does not re-fire. - changeFired map[*lower.Transition]bool + changeFired map[*lower.Transition]bool + changeObserved map[*lower.Transition]bool + changePending map[*lower.Transition]bool + changeReads map[*lower.Transition][]*FeatureValue + changeEvaluating bool // firingChange is the change-triggered transition being taken, whose latch the // state entries it causes must leave alone. @@ -252,6 +256,7 @@ func newStateExecutorForOccurrence( return nil, err } ctx.clock.attach(exec) + ctx.registerStateExecutor(exec) return exec, nil } @@ -282,6 +287,9 @@ func newStateExecutorOn( timerScheduled: make(map[*lower.Transition]bool), timeTriggerVerdict: make(map[*lower.Transition]error), changeFired: make(map[*lower.Transition]bool), + changeObserved: make(map[*lower.Transition]bool), + changePending: make(map[*lower.Transition]bool), + changeReads: make(map[*lower.Transition][]*FeatureValue), breakpointNodes: make(map[ast.Node]bool), dispatchMark: -1, activeConfig: &StateConfiguration{ @@ -512,6 +520,8 @@ func (e *StateExecutor) mirrorOccurrence(name string, value Value) (Value, error } func (e *StateExecutor) assignAttribute(name string, value Value) error { + endWrite := e.ctx.beginFeatureWrite(nil) + defer endWrite() if e.occurrence != nil { if err := e.occurrence.SetFeatureValue(e.ctx, name, value); err != nil { return fmt.Errorf("%w: write %s of object #%d: %w", @@ -535,6 +545,7 @@ func (e *StateExecutor) assignAttribute(name string, value Value) error { } } e.stateData[name] = value + e.ctx.noteStateDataWrite() return nil } @@ -5183,6 +5194,9 @@ func (e *StateExecutor) performEntry(state *ast.StateNode) error { e.changeRearmed[trans] = true } } + delete(e.changeObserved, trans) + delete(e.changePending, trans) + delete(e.changeReads, trans) } if e.breakpointNodes[state] && e.breakpointHit == nil { @@ -5231,6 +5245,9 @@ func (e *StateExecutor) exitState(state *ast.StateNode) error { timed := make(map[*lower.Transition]bool) for _, trans := range e.graph.Transitions[state] { delete(e.timerScheduled, trans) + delete(e.changeObserved, trans) + delete(e.changePending, trans) + delete(e.changeReads, trans) if _, isTime := trans.Trigger.(*ast.TimeEvent); isTime { timed[trans] = true } @@ -5357,6 +5374,7 @@ func (e *StateExecutor) writeStateValue(name string, value Value) error { return e.assignAttribute(name, value) } e.stateData[name] = value + e.ctx.noteStateDataWrite() return nil } @@ -5585,6 +5603,7 @@ func (e *StateExecutor) Release() { } } e.ctx.clock.detach(e) + e.ctx.unregisterStateExecutor(e) } // Resume returns a machine suspended at quiescence to running, so a driver that diff --git a/internal/exec/runtime/state_statements.go b/internal/exec/runtime/state_statements.go index 1c79a19269..6a68301793 100644 --- a/internal/exec/runtime/state_statements.go +++ b/internal/exec/runtime/state_statements.go @@ -399,6 +399,7 @@ func (h *stateStmtHost) assignStateAttribute(name string, value Value) (bool, er return true, err } data[name] = value + h.exec.ctx.noteStateDataWrite() return true, nil } @@ -516,6 +517,7 @@ func (h *stateStmtHost) assignAround(name string, value Value) (bool, error) { } if _, ok := h.exec.stateData[name]; ok { h.exec.stateData[name] = value + h.exec.ctx.noteStateDataWrite() return true, nil } return assignPerformerFeature(h.exec.ctx, h.exec.self, h.behavior.Scope, name, value) diff --git a/internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.expected.json b/internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.expected.json new file mode 100644 index 0000000000..c19f76a6ca --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.expected.json @@ -0,0 +1,17 @@ +{ + "type": "instance", + "libraries": true, + "trace": true, + "instantiate": "test::P", + "objects": [ + { + "events": [{"signal": "Go"}], + "finalState": "waiting", + "stateVisits": ["outer", "waiting", "writing", "waiting"], + "slots": { + "a": {"type": "Integer", "value": 1}, + "b": {"type": "Integer", "value": 1} + } + } + ] +} diff --git a/internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.sysml b/internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.sysml new file mode 100644 index 0000000000..700cd29314 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.sysml @@ -0,0 +1,26 @@ +package test { + private import ScalarValues::*; + attribute def Go; + + part def P { + attribute a : Integer = 0; + attribute b : Integer; + bind b = a; + + exhibit state machine { + entry; then outer; + state outer { + entry; then waiting; + state waiting; + state writing { + entry action update { assign a := 1; } + } + transition first waiting accept Go then writing; + transition first writing then waiting; + } + state done; + + transition first outer accept when a != b then done; + } + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.trace.golden b/internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.trace.golden new file mode 100644 index 0000000000..fcef9cd64b --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_change_trigger_atomic_write.trace.golden @@ -0,0 +1,29 @@ +materialize: P #1 +start: exhibited state machine machine of #1 +materialize: machine #2 +enter: outer +enter: waiting +run: exhibited state machine machine of #1 + eval feature a -> 0 + eval literal 0 -> 0 + eval feature b -> 0 +eval operator != -> false + eval feature a -> 0 + eval literal 0 -> 0 + eval feature b -> 0 +eval operator != -> false +exit: waiting +enter: writing (entry action) +stmt action body + stmt assign a + eval literal 1 -> 1 +transition: waiting -> writing (event: accept Go) + eval feature a -> 1 + eval feature b -> 1 +eval operator != -> false +exit: writing +enter: waiting +transition: writing -> waiting + eval feature a -> 1 + eval feature b -> 1 +eval operator != -> false diff --git a/internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.expected.json b/internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.expected.json new file mode 100644 index 0000000000..24437d3054 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.expected.json @@ -0,0 +1,10 @@ +{ + "type": "state", + "trace": true, + "finalState": "done", + "events": [{"signal": "Go"}], + "stateVisits": ["outer", "waiting", "pulsing", "done"], + "outputs": { + "log": {"type": "Integer", "value": 1} + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.sysml b/internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.sysml new file mode 100644 index 0000000000..6d3e354f65 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.sysml @@ -0,0 +1,22 @@ +package test { + attribute def Go; + + state Machine { + attribute ready : Boolean = false; + attribute log : Integer = 0; + + entry; then outer; + state outer { + entry; then waiting; + state waiting; + state pulsing; + transition first waiting accept Go do action pulse { + assign ready := true; + assign ready := false; + } then pulsing; + } + state done; + + transition first outer accept when ready do assign log := log + 1 then done; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.trace.golden b/internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.trace.golden new file mode 100644 index 0000000000..2374883bcb --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_change_trigger_transient_rise.trace.golden @@ -0,0 +1,18 @@ +eval feature ready -> false +exit: waiting +stmt action body + stmt assign ready + eval literal true -> true + stmt assign ready + eval literal false -> false +enter: pulsing +transition: waiting -> pulsing (event: accept Go) +eval feature ready -> false +exit: pulsing +exit: outer +stmt assign log + eval feature log -> 0 + eval literal 1 -> 1 + eval operator + -> 1 +enter: done +transition: pulsing -> done (event: change) diff --git a/tests/parser/testdata/parse/state_change_trigger_transient_rise.golden b/tests/parser/testdata/parse/state_change_trigger_transient_rise.golden new file mode 100644 index 0000000000..a547216d23 --- /dev/null +++ b/tests/parser/testdata/parse/state_change_trigger_transient_rise.golden @@ -0,0 +1,38 @@ +(RootNamespace + (Membership visibility="default" + (Package name="test" library=false standard=false + (Membership visibility="default" + (Definition kind="attribute" abstract=false variation=false name="Go")) + (Membership visibility="default" + (Usage kind="state" name="Machine" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (Membership visibility="default" + (Usage kind="attribute" name="ready" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Boolean + (*ast.QualifiedName)) + (LiteralBool value=false))) + (Membership visibility="default" + (Usage kind="attribute" name="log" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Integer + (*ast.QualifiedName)) + (LiteralInteger value="0"))) + (EntryMember) + (SuccessionEdge source="@entry" target="outer") + (Membership visibility="default" + (Usage kind="state" name="outer" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (EntryMember) + (SuccessionEdge source="@entry" target="waiting") + (SubstateMember name="waiting") + (SubstateMember name="pulsing") + (TransitionMember source="waiting" target="pulsing" + (Usage kind="attribute" name="" ref=true direction="out" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Go + (*ast.QualifiedName))) + (Membership visibility="default" + (Usage kind="action" name="pulse" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (*ast.AssignmentActionNode) + (*ast.AssignmentActionNode)))))) + (SubstateMember name="done") + (TransitionMember source="outer" target="done" + (ChangeEvent + (FeatureReference name="ready")) + (*ast.AssignmentActionNode))))))) \ No newline at end of file diff --git a/tests/parser/testdata/parse/state_change_trigger_transient_rise.sysml b/tests/parser/testdata/parse/state_change_trigger_transient_rise.sysml new file mode 100644 index 0000000000..6d3e354f65 --- /dev/null +++ b/tests/parser/testdata/parse/state_change_trigger_transient_rise.sysml @@ -0,0 +1,22 @@ +package test { + attribute def Go; + + state Machine { + attribute ready : Boolean = false; + attribute log : Integer = 0; + + entry; then outer; + state outer { + entry; then waiting; + state waiting; + state pulsing; + transition first waiting accept Go do action pulse { + assign ready := true; + assign ready := false; + } then pulsing; + } + state done; + + transition first outer accept when ready do assign log := log + 1 then done; + } +} From d045c9dcece5fe4b96b3c39cb984216fb8aaf701 Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Fri, 2 Oct 2026 22:09:30 +0000 Subject: [PATCH 02/17] feat(lower,runtime): run effects and pseudostate routes of transitions out of the entry action Co-Authored-By: jason.han --- docs/project/behavior-semantic-oracle.md | 4 + .../check/passes/behavior/state_transition.go | 88 ++++++++-- .../passes/behavior/state_transition_test.go | 67 ++++++-- .../check/passes/behavior/w12d_rules_test.go | 14 +- .../exec/analysis/modelform/graphs_state.go | 81 +++++++-- ...robustness_entry_transition_effect_test.go | 103 ++++++++++++ internal/exec/runtime/robustness_test.go | 10 +- internal/exec/runtime/state_executor.go | 145 +++++++++++++++- internal/exec/runtime/state_region_entry.go | 18 +- internal/exec/runtime/state_route.go | 155 +++++++++++++++++- .../exec/runtime/state_run_to_completion.go | 8 +- internal/exec/runtime/state_unit_front.go | 10 ++ .../runtime/testdata/conformance/README.md | 6 +- ...tate_entry_transition_choice.expected.json | 6 + .../state_entry_transition_choice.sysml | 16 ++ ...state_entry_transition_choice.trace.golden | 6 + ...tate_entry_transition_effect.expected.json | 9 + .../state_entry_transition_effect.sysml | 20 +++ ...state_entry_transition_effect.trace.golden | 25 +++ ...nsition_effect_regions.check.expected.json | 13 ++ ...ition_effect_regions.declared.trace.golden | 30 ++++ ...ry_transition_effect_regions.expected.json | 32 ++++ ...nsition_effect_regions.seed-1.trace.golden | 31 ++++ ...tate_entry_transition_effect_regions.sysml | 32 ++++ ...try_transition_effect_regions.trace.golden | 30 ++++ ...ry_transition_explicit_inner.expected.json | 6 + ...tate_entry_transition_explicit_inner.sysml | 17 ++ ...try_transition_explicit_inner.trace.golden | 4 + ...ion_guarded_effect_not_taken.expected.json | 9 + ..._transition_guarded_effect_not_taken.sysml | 19 +++ ...tion_guarded_effect_not_taken.trace.golden | 6 + ...y_transition_history_restore.expected.json | 9 + ...ate_entry_transition_history_restore.sysml | 22 +++ ...ry_transition_history_restore.trace.golden | 44 +++++ ...te_entry_transition_junction.expected.json | 9 + .../state_entry_transition_junction.sysml | 22 +++ ...ate_entry_transition_junction.trace.golden | 22 +++ ...ion_junction_no_way_disables.expected.json | 6 + ..._transition_junction_no_way_disables.sysml | 20 +++ ...tion_junction_no_way_disables.trace.golden | 3 + ...side_orthogonal_region.check.expected.json | 10 ++ ...de_orthogonal_region.declared.trace.golden | 46 ++++++ ...ion_inside_orthogonal_region.expected.json | 31 +++- ...side_orthogonal_region.seed-1.trace.golden | 45 +++++ ...te_junction_inside_orthogonal_region.sysml | 6 +- ...tion_inside_orthogonal_region.trace.golden | 1 + ...de_orthogonal_region_metadata.trace.golden | 1 + internal/ir/lower/entry_transition.go | 119 +++++++++----- internal/ir/lower/fork_plan.go | 5 +- internal/ir/lower/state_graph.go | 80 +++++++-- internal/ir/lower/transition_source_test.go | 67 +++++++- internal/ir/view/behavior.go | 19 ++- .../state_entry_transition_effect.golden | 16 ++ .../parse/state_entry_transition_effect.sysml | 9 + tools/referee/pssm/emit.go | 116 +++++++------ tools/referee/pssm/emit_test.go | 49 +++--- 56 files changed, 1569 insertions(+), 228 deletions(-) create mode 100644 internal/exec/runtime/robustness_entry_transition_effect_test.go create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_choice.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_choice.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_choice.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_effect.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_effect.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_effect.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.check.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.declared.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.seed-1.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_junction.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_junction.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_junction.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.sysml create mode 100644 internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.check.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.declared.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.seed-1.trace.golden create mode 100644 tests/parser/testdata/parse/state_entry_transition_effect.golden create mode 100644 tests/parser/testdata/parse/state_entry_transition_effect.sysml diff --git a/docs/project/behavior-semantic-oracle.md b/docs/project/behavior-semantic-oracle.md index 56c9d06979..86393b8274 100644 --- a/docs/project/behavior-semantic-oracle.md +++ b/docs/project/behavior-semantic-oracle.md @@ -1730,6 +1730,10 @@ 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. +### Entry transitions in the regions of a parallel state: each effect precedes its own target's entry, the regions interleave + +Derivation pending. + ## What the executor gets wrong Nothing, at present: every derivation above is met and carries a golden. The table this section diff --git a/internal/check/passes/behavior/state_transition.go b/internal/check/passes/behavior/state_transition.go index be24cf5c14..3fa94e1086 100644 --- a/internal/check/passes/behavior/state_transition.go +++ b/internal/check/passes/behavior/state_transition.go @@ -85,10 +85,11 @@ type transitionChecker struct { // machine holds what checking one state machine needs: the vertices it owns, // those its transitions leave, and its routing pseudostates in source order. type machine struct { - vertices map[ast.Node]bool - sources map[ast.Node]bool - unresolved map[string]bool - routing []routingDecl + vertices map[ast.Node]bool + sources map[ast.Node]bool + unresolved map[string]bool + invalidEntryTargets map[ast.Node]bool + routing []routingDecl } // routingDecl is a routing pseudostate as declared: a PseudostateNode of the @@ -139,14 +140,15 @@ func (c *transitionChecker) checkMachine(decl ast.Node, scope *symbols.Scope) { return } m := &machine{ - vertices: vertices, - sources: map[ast.Node]bool{}, - unresolved: map[string]bool{}, + vertices: vertices, + sources: map[ast.Node]bool{}, + unresolved: map[string]bool{}, + invalidEntryTargets: map[ast.Node]bool{}, } c.walkBody(m, scope, ast.DeclMembers(decl), decl) for _, ps := range m.routing { - if m.sources[ps.decl] || m.unresolved[ps.name] { + if m.sources[ps.decl] || m.unresolved[ps.name] || m.invalidEntryTargets[ps.decl] { continue } c.report(ps.decl.Span(), CodeNoOutgoingTransition, fmt.Sprintf( @@ -317,11 +319,16 @@ func (c *transitionChecker) walkBody(m *machine, scope *symbols.Scope, members [ c.checkEndpoint(m, scope, n.Target, true, nil) continue } + if c.entryActionSource(scope, n.Source, starts) { + c.checkNamedEntryTransition(m, scope, n) + c.checkEndpoint(m, scope, n.Target, true, nil) + continue + } if c.checkAccepterSource(scope, n) { c.checkEndpoint(m, scope, n.Target, true, nil) continue } - bare := n.Trigger == nil && len(n.Effect) == 0 + bare := n.Trigger == nil m.markLeft(c.checkEndpoint(m, scope, n.Source, false, c.startsOf(m, scope, n.Target, bare, starts)), n.Source) c.checkEndpoint(m, scope, n.Target, true, nil) case *ast.SuccessionEdge: @@ -400,15 +407,58 @@ func (c *transitionChecker) checkEntryTransition(m *machine, scope *symbols.Scop c.report(n.Span(), CodeEntryTransitionShape, (&lower.EntryTransitionShapeError{Transition: n}).Error()) return } - if n.Target == nil { + c.checkEntryTransitionTarget(m, scope, n.Target) +} + +func (c *transitionChecker) checkNamedEntryTransition(m *machine, scope *symbols.Scope, n *ast.TransitionMember) { + if n.Trigger != nil { + c.report(n.Span(), CodeEntryTransitionShape, (&lower.EntryTransitionShapeError{Transition: n}).Error()) + return + } + c.checkEntryTransitionTarget(m, scope, n.Target) +} + +func (c *transitionChecker) checkEntryTransitionTarget(m *machine, scope *symbols.Scope, target ast.Node) { + if target == nil { + return + } + sym, ok := c.resolver.EndpointSymbol(scope, target) + if !ok || !m.vertices[sym.Decl] { + return + } + if lower.IsStateSourceDecl(c.resolver, scope, sym.Decl) { return } - sym, ok := c.resolver.EndpointSymbol(scope, n.Target) - if ok && m.vertices[sym.Decl] && !lower.IsStateSourceDecl(c.resolver, scope, sym.Decl) { - c.report(n.Target.Span(), CodeEntryTransitionTarget, (&lower.EntryTransitionTargetError{Target: sym.Decl}).Error()) + if _, routing := entryRoutingKind(c.resolver, scope, sym.Decl); routing && sym.OwnerScope == scope { + return + } + if _, pseudo := sym.Decl.(*ast.PseudostateNode); pseudo { + m.invalidEntryTargets[sym.Decl] = true + } else if usage, usageDecl := sym.Decl.(*ast.Usage); usageDecl { + if _, annotated := lower.PseudostateMetadata(c.resolver, scope, usage); annotated { + m.invalidEntryTargets[sym.Decl] = true + } + } + c.report(target.Span(), CodeEntryTransitionTarget, (&lower.EntryTransitionTargetError{Target: sym.Decl}).Error()) +} + +func entryRoutingKind(resolver *resolve.Resolver, scope *symbols.Scope, decl ast.Node) (ast.PseudostateKind, bool) { + switch node := decl.(type) { + case *ast.PseudostateNode: + return node.Kind, node.Kind == ast.PseudostateJunction || node.Kind == ast.PseudostateChoice + case *ast.Usage: + kind, ok := lower.PseudostateMetadata(resolver, scope, node) + return kind, ok && (kind == ast.PseudostateJunction || kind == ast.PseudostateChoice) + default: + return -1, false } } +func (c *transitionChecker) entryActionSource(scope *symbols.Scope, source ast.Node, starts map[ast.Node]bool) bool { + sym, ok := c.resolver.EndpointSymbol(scope, source) + return ok && starts[sym.Decl] +} + // startsOf returns the entry actions a transition of this shape may leave: only a // bare completion transition into a state names the state the machine starts in, // which is the shape lowering reads (SysML 7.19.3). @@ -430,12 +480,16 @@ func (c *transitionChecker) startsOf( if !m.vertices[decl] { return nil } - if _, pseudostate := decl.(*ast.PseudostateNode); pseudostate { - return nil + if pseudostate, ok := decl.(*ast.PseudostateNode); ok { + if pseudostate.Kind != ast.PseudostateJunction && pseudostate.Kind != ast.PseudostateChoice { + return nil + } } if usage, ok := decl.(*ast.Usage); ok { - if _, annotated := lower.PseudostateMetadata(c.resolver, scope, usage); annotated { - return nil + if kind, annotated := lower.PseudostateMetadata(c.resolver, scope, usage); annotated { + if kind != ast.PseudostateJunction && kind != ast.PseudostateChoice { + return nil + } } } return starts diff --git a/internal/check/passes/behavior/state_transition_test.go b/internal/check/passes/behavior/state_transition_test.go index 9228c697e8..44b78d23be 100644 --- a/internal/check/passes/behavior/state_transition_test.go +++ b/internal/check/passes/behavior/state_transition_test.go @@ -350,9 +350,7 @@ func TestGuardedEntryTransitionIsLegal(t *testing.T) { }`) } -// An entry transition chooses the starting state by its guard alone (SysML v2 -// §7.18.3): a trigger or an effect on it, or a target that is no state, is -// reported where the endpoint diagnostics report. +// An entry transition accepts a guard alone unless it has an explicit source. func TestEntryTransitionShapeIsReported(t *testing.T) { wantOneError(t, `package test { state def M { @@ -360,7 +358,7 @@ func TestEntryTransitionShapeIsReported(t *testing.T) { accept go then active; state active; } -}`, behavior.CodeEntryTransitionShape, "carries a trigger") +}`, behavior.CodeEntryTransitionShape, "A transition with an accepter must have a state as its source") wantOneError(t, `package test { state def M { entry; then init; @@ -368,23 +366,49 @@ func TestEntryTransitionShapeIsReported(t *testing.T) { state init; state active; } -}`, behavior.CodeEntryTransitionShape, "carries a trigger") +}`, behavior.CodeEntryTransitionShape, "A transition with an accepter must have a state as its source") wantOneError(t, `package test { state def M { entry; if true do action mark then active; state active; } -}`, behavior.CodeEntryTransitionShape, "carries an effect") +}`, behavior.CodeEntryTransitionShape, "a shorthand transition out of an entry action may carry a guard at most") wantOneError(t, `package test { state def M { entry; if true then pick; + fork pick; + state active; + } +}`, behavior.CodeEntryTransitionTarget, "reaches the fork pick") + wantOneError(t, `package test { + state def M { + entry action boot { } + transition boot accept go then active; + state active; + } +}`, behavior.CodeEntryTransitionShape, "A transition with an accepter must have a state as its source") + wantClean(t, `package test { + action def mark; + state def M { + entry action boot { } + transition boot do action mark then active; + state active; + } +}`) +} + +func TestEntryActionTransitionIntoChoiceIsClean(t *testing.T) { + wantClean(t, `package test { + state def M { + entry action boot { } + transition boot then pick; choice pick; transition first pick then active; state active; } -}`, behavior.CodeEntryTransitionTarget, "reaches the choice pick") +}`) } // The member before the shorthand is an entry action or an attribute rather than @@ -643,14 +667,14 @@ func TestTransitionOutOfEntryActionIsLegal(t *testing.T) { // guarded or not: a triggered transition is an edge between two vertices, and // an entry action is none. A trigger names the accepter rule, which is the // specific reading of the same rejection. -func TestTriggeredTransitionOutOfEntryActionIsNotAVertex(t *testing.T) { +func TestTriggeredTransitionOutOfEntryActionIsRejected(t *testing.T) { wantOneError(t, `package test { state def M { entry action begin { } transition begin accept Warning then busy; state busy; } -}`, behavior.CodeAccepterSourceNotState, "must have a state as its source") +}`, behavior.CodeEntryTransitionShape, "A transition with an accepter must have a state as its source") wantClean(t, `package test { state def M { in attribute c : Boolean; @@ -687,18 +711,31 @@ func TestTransitionOutOfAnotherStatesEntryActionIsNotAVertex(t *testing.T) { }`, behavior.CodeEndpointNotOfMachine, "begin") } -// A start designation names the state the machine starts in, so a transition out -// of an entry action into a pseudostate is not one. -func TestEntryActionTransitionIntoPseudostateIsNotAVertex(t *testing.T) { - wantOneError(t, `package test { +// A transition out of an entry action may target a junction or choice route. +func TestEntryActionTransitionIntoJunctionIsClean(t *testing.T) { + wantClean(t, `package test { state def M { entry action begin { } transition begin then j; junction j; state b; - transition j then b; + transition first j then b; } -}`, behavior.CodeEndpointNotOfMachine, "begin") +}`) +} + +func TestEntryActionTransitionIntoJunctionInAnotherBodyIsReported(t *testing.T) { + wantOneError(t, `package test { + state def M { + entry action begin { } + transition begin then inner::route; + state inner { + junction route; + state active; + transition route then active; + } + } +}`, behavior.CodeEntryTransitionTarget, "not a state or junction/choice route the body can start in") } // TestImplicitSourcePseudostateBothSpellings: a sourceless transition hangs diff --git a/internal/check/passes/behavior/w12d_rules_test.go b/internal/check/passes/behavior/w12d_rules_test.go index 47a2fb50bc..f705e1dc3d 100644 --- a/internal/check/passes/behavior/w12d_rules_test.go +++ b/internal/check/passes/behavior/w12d_rules_test.go @@ -73,17 +73,13 @@ func TestW12DAccepterSourceMustBeAState(t *testing.T) { transition init accept A then S2_1; state S2_1; } -}` + }` got := transitionDiags(t, src) - if len(got) != 1 || got[0].Code != behavior.CodeAccepterSourceNotState { - t.Fatalf("got %+v, want one %s", got, behavior.CodeAccepterSourceNotState) + if len(got) != 1 || got[0].Code != behavior.CodeEntryTransitionShape { + t.Fatalf("got %+v, want one %s", got, behavior.CodeEntryTransitionShape) } - if got[0].Message != behavior.MsgAccepterSourceNotState { - t.Errorf("message = %q, want %q", got[0].Message, behavior.MsgAccepterSourceNotState) - } - at := src[got[0].Span.Offset : got[0].Span.Offset+got[0].Span.Len] - if !strings.Contains(at, "A") || strings.Contains(at, "then") { - t.Errorf("reported at %q, want the trigger", at) + if !strings.Contains(got[0].Message, behavior.MsgAccepterSourceNotState) { + t.Errorf("message = %q, want it to cite %q", got[0].Message, behavior.MsgAccepterSourceNotState) } } diff --git a/internal/exec/analysis/modelform/graphs_state.go b/internal/exec/analysis/modelform/graphs_state.go index 30204bf634..2a834bcb10 100644 --- a/internal/exec/analysis/modelform/graphs_state.go +++ b/internal/exec/analysis/modelform/graphs_state.go @@ -96,11 +96,13 @@ type TransitionForm struct { type EntryTransitionForm struct { // Body is the state or region the transition is written in; absent for the // machine's own body. - Body *int `json:"body,omitempty"` - Guard *ExprForm `json:"guard,omitempty"` - Target int `json:"target"` - Scope string `json:"scope,omitempty"` - Decl SpanForm `json:"decl"` + Body *int `json:"body,omitempty"` + Guard *ExprForm `json:"guard,omitempty"` + Target *int `json:"target,omitempty"` + Via *int `json:"via,omitempty"` + Effect []BehaviorForm `json:"effect,omitempty"` + Scope string `json:"scope,omitempty"` + Decl SpanForm `json:"decl"` } // BehaviorForm is an entry, do, exit or effect behavior. @@ -223,15 +225,39 @@ func (x *graphsExporter) stateForm(sym *symbols.Symbol, graph *lower.StateGraph) } } for _, et := range graph.EntryTransitions[node] { - ids.add(et.Target) + if et.Target != nil { + ids.add(et.Target) + } + if et.Via != nil { + ids.add(et.Via) + } + for _, behavior := range et.Effect { + ids.add(behavior.Owner) + } } } for _, et := range graph.EntryTransitions[nil] { - ids.add(et.Target) + if et.Target != nil { + ids.add(et.Target) + } + if et.Via != nil { + ids.add(et.Via) + } + for _, behavior := range et.Effect { + ids.add(behavior.Owner) + } } for _, r := range regions.order { for _, et := range graph.EntryTransitions[r] { - ids.add(et.Target) + if et.Target != nil { + ids.add(et.Target) + } + if et.Via != nil { + ids.add(et.Via) + } + for _, behavior := range et.Effect { + ids.add(behavior.Owner) + } } } vertices := len(ids.order) @@ -309,7 +335,9 @@ func (x *graphsExporter) stateForm(sym *symbols.Symbol, graph *lower.StateGraph) } form.Regions = append(form.Regions, rf) } - x.entryTransitions(form, graph, ids, regions) + if err := x.entryTransitions(form, graph, ids, regions); err != nil { + return nil, err + } if len(ids.order) != vertices { return nil, fmt.Errorf("%w: %s: a vertex is reached only while it is written", ErrGraphsOrder, symbols.FQNOf(sym)) } @@ -319,32 +347,55 @@ func (x *graphsExporter) stateForm(sym *symbols.Symbol, graph *lower.StateGraph) // entryTransitions writes the entry transitions body by body: the machine's own // first, then those of each state vertex, then those of each region. -func (x *graphsExporter) entryTransitions(form *StateForm, graph *lower.StateGraph, ids, regions *vertexIDs) { - write := func(body *int, list []*lower.EntryTransition) { +func (x *graphsExporter) entryTransitions(form *StateForm, graph *lower.StateGraph, ids, regions *vertexIDs) error { + write := func(body *int, list []*lower.EntryTransition) error { for _, et := range list { scope := orScope(et.Scope, graph.Scope) + effect, err := x.behaviors(ids, scope, et.Effect) + if err != nil { + return err + } + var target, via *int + if et.Target != nil { + id := ids.add(et.Target) + target = &id + } + if et.Via != nil { + id := ids.add(et.Via) + via = &id + } form.EntryTransitions = append(form.EntryTransitions, EntryTransitionForm{ Body: body, Guard: x.expr(scope, et.Guard), - Target: ids.add(et.Target), + Target: target, + Via: via, + Effect: effect, Scope: scopeName(et.Scope), Decl: x.span(scope, et.Decl), }) } + return nil + } + if err := write(nil, graph.EntryTransitions[nil]); err != nil { + return err } - write(nil, graph.EntryTransitions[nil]) for id, node := range ids.order { if list, ok := graph.EntryTransitions[node]; ok { body := id - write(&body, list) + if err := write(&body, list); err != nil { + return err + } } } for id, node := range regions.order { if list, ok := graph.EntryTransitions[node]; ok { body := id - write(&body, list) + if err := write(&body, list); err != nil { + return err + } } } + return nil } // behaviors writes the lowered behaviors of one kind in order. diff --git a/internal/exec/runtime/robustness_entry_transition_effect_test.go b/internal/exec/runtime/robustness_entry_transition_effect_test.go new file mode 100644 index 0000000000..3443b6773a --- /dev/null +++ b/internal/exec/runtime/robustness_entry_transition_effect_test.go @@ -0,0 +1,103 @@ +package runtime + +import ( + "errors" + "testing" + + "github.com/Open-MBEE/OpenSysML/internal/ir/lower" +) + +func TestRuntimeRobustnessEntryTransitionEffect(t *testing.T) { + t.Run("effect error is returned", func(t *testing.T) { + _, _, err := executeStateSource(t, "Machine", `package test { + state Machine { + attribute zero : Integer = 0; + entry action boot { } + transition boot do action { + assign zero := 1 / zero; + } then active; + state active; + } + }`) + if !errors.Is(err, ErrDivisionByZero) { + t.Fatalf("execution error = %v, want ErrDivisionByZero", err) + } + }) + + t.Run("junction is resolved after the entry action", func(t *testing.T) { + _, _, err := executeStateSource(t, "Machine", `package test { + state Machine { + attribute ready : Boolean = true; + entry action boot { assign ready := false; } + transition boot then route; + junction route; + transition route if ready then active; + state active; + } + }`) + if !errors.Is(err, errNoWayThrough) { + t.Fatalf("execution error = %v, want errNoWayThrough", err) + } + }) + + t.Run("choice without an enabled branch disables entry", func(t *testing.T) { + exec := stateExecutorForSource(t, "Machine", `package test { + attribute def Go; + attribute def Later; + state Machine { + attribute ready : Boolean = false; + entry; then start; + state start; + state target { + entry action boot { } + transition boot then pick; + choice pick; + transition pick if ready then nested; + state nested; + } + state fallback; + transition first start accept Go then target; + transition first start accept Later then fallback; + } + }`) + exec.SendSignal("Go", nil) + if err := exec.ProcessNextEvent(); err != nil { + t.Fatalf("ProcessNextEvent(Go) = %v, want disabled transition", err) + } + assertCurrentState(t, exec, "start") + exec.SendSignal("Later", nil) + if err := exec.ProcessNextEvent(); err != nil { + t.Fatalf("ProcessNextEvent(Later): %v", err) + } + assertCurrentState(t, exec, "fallback") + }) + + t.Run("fork target remains unsupported", func(t *testing.T) { + err := stateExecutorError(t, `package test { + state Machine { + entry; then split; + fork split; + state active; + } + }`, "Machine") + var targetErr *lower.EntryTransitionTargetError + if !errors.As(err, &targetErr) { + t.Fatalf("executor error = %v, want EntryTransitionTargetError", err) + } + }) + + t.Run("trigger remains unsupported", func(t *testing.T) { + err := stateExecutorError(t, `package test { + attribute def Go; + state Machine { + entry action boot { } + transition boot accept Go then active; + state active; + } + }`, "Machine") + var shapeErr *lower.EntryTransitionShapeError + if !errors.As(err, &shapeErr) { + t.Fatalf("executor error = %v, want EntryTransitionShapeError", err) + } + }) +} diff --git a/internal/exec/runtime/robustness_test.go b/internal/exec/runtime/robustness_test.go index a81394359d..84c38243b7 100644 --- a/internal/exec/runtime/robustness_test.go +++ b/internal/exec/runtime/robustness_test.go @@ -7955,15 +7955,13 @@ func testNoEntryTransitionGuardHolds(t *testing.T) { } } -// testEntryTransitionTargetIsNotAState: an entry transition starts its body in -// a state; reaching a pseudostate instead is a typed lowering error. +// testEntryTransitionTargetIsNotAState: a fork remains an unsupported entry target. func testEntryTransitionTargetIsNotAState(t *testing.T) { err := stateExecutorError(t, ` package test { state Machine { entry; then pick; - choice pick; - transition first pick then idle; + fork pick; state idle; } } @@ -7972,7 +7970,7 @@ func testEntryTransitionTargetIsNotAState(t *testing.T) { if !errors.As(err, &targetErr) { t.Fatalf("expected EntryTransitionTargetError, got %v", err) } - want := "create state executor: lower state machine: " + fmt.Sprintf(lower.EntryTransitionTargetFormat, "the choice pick") + want := "create state executor: lower state machine: " + fmt.Sprintf(lower.EntryTransitionTargetFormat, "the fork pick") if err.Error() != want { t.Fatalf("message:\n got %q\nwant %q", err.Error(), want) } @@ -7993,7 +7991,7 @@ func testEntryTransitionCarriesATrigger(t *testing.T) { if !errors.As(err, &shapeErr) { t.Fatalf("expected EntryTransitionShapeError, got %v", err) } - want := "create state executor: lower state machine: " + fmt.Sprintf(lower.EntryTransitionShapeFormat, "a trigger") + want := "create state executor: lower state machine: " + shapeErr.Error() if err.Error() != want { t.Fatalf("message:\n got %q\nwant %q", err.Error(), want) } diff --git a/internal/exec/runtime/state_executor.go b/internal/exec/runtime/state_executor.go index ce6fec0551..7cf8d9eb81 100644 --- a/internal/exec/runtime/state_executor.go +++ b/internal/exec/runtime/state_executor.go @@ -157,7 +157,8 @@ type StateExecutor struct { moving *moveMark // front is the site under way whose regions' units are drawn one at a time; // it lives within one move, so no snapshot sees it. - front *unitFront + front *unitFront + pendingRouteEntryEffects map[*ast.StateRegion][]routeEffect // began are the do behaviors the move under way started, whose due steps its entry sites // draw against the entries left; path is the draw along an entry path no front orders. began []*doAction @@ -2304,13 +2305,23 @@ func (e *StateExecutor) moveTo(trans *lower.Transition, currentState *ast.StateN fromName = currentState.Name } lca := e.moveBoundary(currentState, trans, targetState) + immediate, entryEffects := e.routeEntryFrontEffects(effects, e.descendantChain(lca, targetState), targetState) + previousEffects := e.pendingRouteEntryEffects + e.pendingRouteEntryEffects = cloneRouteEntryEffects(previousEffects) + if e.pendingRouteEntryEffects == nil && len(entryEffects) > 0 { + e.pendingRouteEntryEffects = make(map[*ast.StateRegion][]routeEffect) + } + for region, routeEffects := range entryEffects { + e.pendingRouteEntryEffects[region] = append(e.pendingRouteEntryEffects[region], routeEffects...) + } + defer func() { e.pendingRouteEntryEffects = previousEffects }() // Exit states (deepest to shallowest) if err := e.exitStates(e.exitPath(currentState, lca, nil)); err != nil { return err } - if err := e.runEffects(effects, e.descendantChain(lca, targetState)); err != nil { + if err := e.runEffects(immediate, e.descendantChain(lca, targetState)); err != nil { return err } if lca == targetState { @@ -2319,6 +2330,35 @@ func (e *StateExecutor) moveTo(trans *lower.Transition, currentState *ast.StateN return e.enterBelow(trans, fromName, lca, targetState, branches) } +func (e *StateExecutor) routeEntryFrontEffects( + effects []routeEffect, + chain []*ast.StateNode, + target *ast.StateNode, +) ([]routeEffect, map[*ast.StateRegion][]routeEffect) { + entering := make(map[*ast.StateNode]bool, len(chain)) + for _, state := range chain { + entering[state] = true + } + var immediate []routeEffect + byRegion := make(map[*ast.StateRegion][]routeEffect) + for _, effect := range effects { + source, ok := effect.segment.Source.(*ast.PseudostateNode) + if !ok { + immediate = append(immediate, effect) + continue + } + region := e.graph.PseudostateRegion[source] + owner := e.graph.RegionOwner[region] + if region == nil || owner == nil || !entering[owner] || + e.regionUnder(owner, target) != region { + immediate = append(immediate, effect) + continue + } + byRegion[region] = append(byRegion[region], effect) + } + return immediate, byRegion +} + // enterBelow finishes a move whose exits and effects are done: it enters the // states below lca down to targetState, then the target's own start. func (e *StateExecutor) enterBelow(trans *lower.Transition, fromName string, lca, targetState *ast.StateNode, branches map[*ast.StateRegion]*ast.StateNode) error { @@ -4950,9 +4990,7 @@ func (e *StateExecutor) enterMachineRegions() error { return nil } -// startIn chooses the state owner's body starts in: the target of the first -// transition out of its entry action whose guard holds, in declaration order. -// It is nil when the body declares none; when none holds, that is an error. +// startIn chooses where the owner's body starts and performs its entry route. func (e *StateExecutor) startIn(owner ast.Node) (*ast.StateNode, error) { transitions := e.graph.StartOf(owner) for _, entry := range transitions { @@ -4961,10 +4999,21 @@ func (e *StateExecutor) startIn(owner ast.Node) (*ast.StateNode, error) { return nil, err } if holds { + if err := e.runEntryEffect(owner, entry); err != nil { + return nil, err + } + target := entry.Target + if entry.Via != nil { + var err error + target, err = e.followEntryRoute(owner, entry.Via) + if err != nil { + return nil, err + } + } if entry.Decl != nil { - e.fired = append(e.fired, FiredTransition{Decl: entry.Decl, Target: entry.Target, Owner: e.graph.EntryOwner(owner)}) + e.fired = append(e.fired, FiredTransition{Decl: entry.Decl, Target: entryTarget(entry), Owner: e.graph.EntryOwner(owner)}) } - return entry.Target, nil + return target, nil } } if len(transitions) > 0 { @@ -4974,6 +5023,84 @@ func (e *StateExecutor) startIn(owner ast.Node) (*ast.StateNode, error) { return nil, nil } +func entryTarget(entry *lower.EntryTransition) ast.Node { + if entry.Via != nil { + return entry.Via + } + return entry.Target +} + +func (e *StateExecutor) runEntryEffect(owner ast.Node, entry *lower.EntryTransition) error { + if len(entry.Effect) == 0 { + return nil + } + if _, err := e.unit(ChoiceEntryOrder, e.entryTransitionEffectHead(owner, entry)); err != nil { + return err + } + if err := e.executeBehaviors(entry.Effect); err != nil { + return fmt.Errorf("entry transition effect: %w", err) + } + return nil +} + +func (e *StateExecutor) followEntryRoute(owner ast.Node, via *ast.PseudostateNode) (*ast.StateNode, error) { + route, err := e.followOut(via, route{}) + if err != nil { + return nil, fmt.Errorf("entry transition through %s %s: %w", via.Kind, via.Name, err) + } + for { + if route.draw != nil { + route, err = e.settleDraws(route) + e.noteAll(route.notes) + route.notes = nil + if err != nil { + return nil, fmt.Errorf("entry transition through %s %s: %w", via.Kind, via.Name, err) + } + } + if err := e.runEntryRouteEffects(route.effects(e.graph)); err != nil { + return nil, err + } + e.noteFired(route.segments...) + e.noteAll(route.notes) + route.notes = nil + if route.choice == nil { + if route.target == nil { + return nil, fmt.Errorf("entry transition through %s %s has no state target", via.Kind, via.Name) + } + return route.target, nil + } + route, err = e.resolveChoice(route) + if err != nil { + if errors.Is(err, ErrChoiceWithoutBranch) { + err = fmt.Errorf("%w: %w", errNoWayThrough, err) + } + return nil, fmt.Errorf("entry transition through choice %s: %w", via.Name, err) + } + } +} + +func (e *StateExecutor) runEntryRouteEffects(effects []routeEffect) error { + var ended []ast.Node + for i, effect := range effects { + if e.endedBefore(ended, effect.behavior) { + continue + } + if i == 0 || effects[i-1].segment != effect.segment { + if _, err := e.unit(ChoiceEntryOrder, unitHead{label: e.effectLabel(effect.segment), at: effect.segment.Decl}); err != nil { + return err + } + } + terminated, err := e.executeBehavior(effect.behavior) + if err != nil { + return fmt.Errorf("entry route transition effect: %w", err) + } + if terminated { + ended = append(ended, effect.behavior.Block) + } + } + return nil +} + // entryGuardHolds evaluates an entry transition's guard in the body it is // written in, reading the attributes of the state that owns that body. func (e *StateExecutor) entryGuardHolds(owner ast.Node, entry *lower.EntryTransition) (bool, error) { @@ -4982,10 +5109,10 @@ func (e *StateExecutor) entryGuardHolds(owner ast.Node, entry *lower.EntryTransi } val, err := e.evalStepOf(e.bodyState(owner), entry.Guard, entry.Scope) if err != nil { - return false, fmt.Errorf("eval guard of the entry transition into %s: %w", entry.Target.Name, err) + return false, fmt.Errorf("eval guard of the entry transition into %s: %w", StateVertexName(entryTarget(entry)), err) } if val.Kind != ValConst || val.Const.Kind != semantics.ValBool { - return false, fmt.Errorf("guard of the entry transition into %s must be boolean, got %v", entry.Target.Name, val.Kind) + return false, fmt.Errorf("guard of the entry transition into %s must be boolean, got %v", StateVertexName(entryTarget(entry)), val.Kind) } return val.Const.Bool, nil } diff --git a/internal/exec/runtime/state_region_entry.go b/internal/exec/runtime/state_region_entry.go index db92959c7a..a7b88167ff 100644 --- a/internal/exec/runtime/state_region_entry.go +++ b/internal/exec/runtime/state_region_entry.go @@ -2,6 +2,7 @@ package runtime import ( "fmt" + "slices" "github.com/Open-MBEE/OpenSysML/internal/ir/lower" "github.com/Open-MBEE/OpenSysML/internal/syntax/ast" @@ -13,6 +14,7 @@ type regionEntry struct { container *ast.StateNode branches map[*ast.StateRegion]*ast.StateNode target *ast.StateNode // where the region starts instead of its own start, if anywhere + effects []routeEffect } // lazyEntry is the chain of states a fork's branches still have to enter down to @@ -40,7 +42,12 @@ func (e *StateExecutor) forkEntry(boundary, owner *ast.StateNode) *lazyEntry { func (e *StateExecutor) enterRegionsInto(container *ast.StateNode, regions []*ast.StateRegion, branches map[*ast.StateRegion]*ast.StateNode) error { entries := make([]*regionEntry, 0, len(regions)) for _, region := range regions { - entries = append(entries, ®ionEntry{region: region, container: container, branches: branches, target: branches[region]}) + entry := ®ionEntry{region: region, container: container, branches: branches, target: branches[region]} + if effects := e.pendingRouteEntryEffects[region]; len(effects) > 0 { + entry.effects = slices.Clone(effects) + delete(e.pendingRouteEntryEffects, region) + } + entries = append(entries, entry) } return e.enterRegions(container, entries, true) } @@ -128,6 +135,9 @@ func (e *StateExecutor) runBranchEffect(branch *lower.Transition) error { // enterRegion enters one region down to the state it starts in, as a transition does; a start // its guards decide is drawn before they are read, so they read what earlier units wrote. func (e *StateExecutor) enterRegion(w *regionEntry) error { + if err := e.runEntryRouteEffects(w.effects); err != nil { + return err + } if w.target == nil && e.graph.RegionState[w.region] == nil && len(e.graph.StartOf(w.region)) > 0 { if err := e.unitAhead(ChoiceEntryOrder, e.startHead(w.region, w.container)); err != nil { return err @@ -155,6 +165,12 @@ func (e *StateExecutor) enterRegion(w *regionEntry) error { func (e *StateExecutor) startHead(body ast.Node, above *ast.StateNode) unitHead { starts := e.graph.StartOf(body) if len(starts) > 0 && starts[0].Guard == nil { + if len(starts[0].Effect) > 0 { + return e.entryTransitionEffectHead(body, starts[0]) + } + if starts[0].Via != nil { + return unitHead{label: "start of " + e.describeBody(body), at: body, site: e.bodySite(body)} + } target := starts[0].Target for _, state := range e.descendantChain(above, target) { if e.entryIsUnit(state) { diff --git a/internal/exec/runtime/state_route.go b/internal/exec/runtime/state_route.go index c857c15d62..0a74744959 100644 --- a/internal/exec/runtime/state_route.go +++ b/internal/exec/runtime/state_route.go @@ -75,6 +75,17 @@ type routeEffect struct { segment *lower.Transition } +func cloneRouteEntryEffects(effects map[*ast.StateRegion][]routeEffect) map[*ast.StateRegion][]routeEffect { + if effects == nil { + return nil + } + cloned := make(map[*ast.StateRegion][]routeEffect, len(effects)) + for region, routeEffects := range effects { + cloned[region] = slices.Clone(routeEffects) + } + return cloned +} + // effects are the behaviors the route's segments perform, in path order, each // with the state enclosing it. func (r route) effects(g *lower.StateGraph) []routeEffect { @@ -195,12 +206,14 @@ func (e *StateExecutor) routeAvailable(trans *lower.Transition, event *Event) bo } defer unbind() - _, routeErr = e.resolveRoute(trans, event) + resolved, err := e.resolveRoute(trans, event) + routeErr = err if routeErr != nil { return } hist, ok := trans.Target.(*ast.PseudostateNode) if !ok || hist.Kind != ast.PseudostateShallowHistory && hist.Kind != ast.PseudostateDeepHistory { + routeErr = e.defaultEntryRoutesAvailable(trans, resolved) return } owner, err := e.historyOwner(hist) @@ -211,11 +224,149 @@ func (e *StateExecutor) routeAvailable(trans *lower.Transition, event *Event) bo if ok && (source == owner || e.nestedIn(source, owner)) { return } - _, routeErr = e.followOut(hist, route{}) + fallback, err := e.followOut(hist, route{}) + routeErr = err + if routeErr == nil { + routeErr = e.defaultEntryRoutesAvailable(trans, fallback) + } }) return !errors.Is(routeErr, errNoWayThrough) } +func (e *StateExecutor) defaultEntryRoutesAvailable(trans *lower.Transition, route route) error { + targets, stops, err := e.reachable(route) + if err != nil || len(stops) > 0 { + return err + } + current := e.moveOrigin() + for _, target := range targets { + available := true + seenBodies := make(map[ast.Node]bool) + seenStates := make(map[*ast.StateNode]bool) + for _, entered := range e.enteredByMove(current, trans, target) { + if entered == target { + available = e.defaultEntryBodyAvailable(entered, seenBodies, seenStates) + if !available { + break + } + continue + } + regions, composite := e.graph.CompositeStates[entered] + if !composite { + continue + } + explicitRegion := e.regionUnder(entered, target) + for _, region := range regions { + if region == explicitRegion { + continue + } + if !e.defaultEntryBodyAvailable(region, seenBodies, seenStates) { + available = false + break + } + } + if !available { + break + } + } + if available { + return nil + } + } + if len(targets) == 0 { + return nil + } + return errNoWayThrough +} + +func (e *StateExecutor) defaultEntryBodyAvailable( + owner ast.Node, + seenBodies map[ast.Node]bool, + seenStates map[*ast.StateNode]bool, +) bool { + if seenBodies[owner] { + return true + } + seenBodies[owner] = true + entries := e.graph.StartOf(owner) + if len(entries) == 0 || entries[0].Guard != nil { + return true + } + entry := entries[0] + var targets []*ast.StateNode + if entry.Via != nil { + var resolved route + var routeErr error + e.preview(func() { + resolved, routeErr = e.followOut(entry.Via, route{}) + }) + if errors.Is(routeErr, errNoWayThrough) { + return false + } + if routeErr != nil { + return true + } + if !e.defaultEntryRouteAvailable(resolved) { + return false + } + var stops []*ast.Usage + targets, stops, routeErr = e.reachable(resolved) + if routeErr != nil || len(stops) > 0 { + return true + } + } else if entry.Target != nil { + targets = append(targets, entry.Target) + } + for _, target := range targets { + if seenStates[target] { + continue + } + seenStates[target] = true + regions, composite := e.graph.CompositeStates[target] + if !composite { + if !e.defaultEntryBodyAvailable(target, seenBodies, seenStates) { + return false + } + continue + } + for _, region := range regions { + if !e.defaultEntryBodyAvailable(region, seenBodies, seenStates) { + return false + } + } + } + return true +} + +func (e *StateExecutor) defaultEntryRouteAvailable(current route) bool { + if current.draw != nil { + for _, branch := range current.draw.beyond { + if e.defaultEntryRouteAvailable(branch.route) { + return true + } + } + return false + } + if current.choice == nil { + return true + } + outgoing := e.graph.Transitions[current.choice] + enabled, _, err := e.enabledBranches(current.choice, outgoing) + if err != nil { + return true + } + for _, index := range enabled { + beyond, err := e.follow(current.choice, outgoing[index], route{crossed: current.crossed}) + if errors.Is(err, errNoWayThrough) { + continue + } + if err != nil || e.defaultEntryRouteAvailable(beyond) { + return true + } + } + return false +} + // settleDraws makes the draws the route is open at, in turn, once the transition // is committed to fire and nothing has moved yet: the policy draws among the // enabled branches, as a choice point among the route's notes, and the route goes diff --git a/internal/exec/runtime/state_run_to_completion.go b/internal/exec/runtime/state_run_to_completion.go index 9c20ade189..65654a8758 100644 --- a/internal/exec/runtime/state_run_to_completion.go +++ b/internal/exec/runtime/state_run_to_completion.go @@ -31,7 +31,8 @@ type heldEntry struct { machine bool // firing is the transition whose entry the cascade is, with the payload it // bound; the entries and do behaviors performed on resumption read it. - firing *firing + firing *firing + routeEffects map[*ast.StateRegion][]routeEffect } // RunToCompletionValueError reports an unevaluable or non-Boolean RTC value. @@ -116,7 +117,7 @@ func (e *StateExecutor) holdEntry(owner *ast.StateNode, regions []*ast.StateRegi e.held = append(e.held, heldEntry{ owner: owner, regions: regions, branches: branches, chain: chain, scopes: scopes, machine: machine, - firing: e.currentFiring(), + firing: e.currentFiring(), routeEffects: cloneRouteEntryEffects(e.pendingRouteEntryEffects), }) return true, nil } @@ -133,6 +134,9 @@ func (e *StateExecutor) heldOwner(state *ast.StateNode) *heldEntry { // performHeld resumes one held entry cascade within the firing that began it. func (e *StateExecutor) performHeld(item heldEntry) (err error) { defer e.resumeFiring(item.firing)() + previousEffects := e.pendingRouteEntryEffects + e.pendingRouteEntryEffects = cloneRouteEntryEffects(item.routeEffects) + defer func() { e.pendingRouteEntryEffects = previousEffects }() clear(e.entering) for _, state := range item.chain { e.entering[state] = true diff --git a/internal/exec/runtime/state_unit_front.go b/internal/exec/runtime/state_unit_front.go index 63cd57ef79..07a8b4c054 100644 --- a/internal/exec/runtime/state_unit_front.go +++ b/internal/exec/runtime/state_unit_front.go @@ -35,6 +35,16 @@ func (e *StateExecutor) effectLabel(trans *lower.Transition) string { return e.transitionLabel(trans) + "(effect)" } +func (e *StateExecutor) entryTransitionEffectHead(owner ast.Node, entry *lower.EntryTransition) unitHead { + label := e.describeBody(owner) + "(effect)" + if transition, ok := entry.Decl.(*ast.TransitionMember); ok { + if source := lower.EndpointText(transition.Source); source != "" { + label = source + "->" + StateVertexName(entryTarget(entry)) + "(effect)" + } + } + return unitHead{label: label, at: entry.Decl, site: e.bodySite(owner)} +} + // stateName is the state's name, qualified by its region where another region's state shares it. func (e *StateExecutor) stateName(state *ast.StateNode) string { if region := e.graph.RegionOf[state]; region != nil && region.Name != "" && e.nameShared(state) { diff --git a/internal/exec/runtime/testdata/conformance/README.md b/internal/exec/runtime/testdata/conformance/README.md index 370a3d5b47..670ed522e5 100644 --- a/internal/exec/runtime/testdata/conformance/README.md +++ b/internal/exec/runtime/testdata/conformance/README.md @@ -267,9 +267,9 @@ regenerates them beside the default golden. ### Checking Every Schedule (`.check.expected.json`) -An action case with an admissible set also owns a `.check.expected.json`: -what the explicit-state checker (`runtime.CheckAction`, the `check` engine) -finds when it searches every schedule of the action, derived from the library +A case with an admissible set also owns a `.check.expected.json`: what the +explicit-state checker (`runtime.Check`, the `check` engine) finds when it +searches every schedule of the action or state machine, derived from the library text as the admissible set was: ```json diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_choice.expected.json b/internal/exec/runtime/testdata/conformance/state_entry_transition_choice.expected.json new file mode 100644 index 0000000000..01d15ee7cb --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_choice.expected.json @@ -0,0 +1,6 @@ +{ + "type": "state", + "trace": true, + "events": [{"signal": "Go"}], + "finalState": "active" +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_choice.sysml b/internal/exec/runtime/testdata/conformance/state_entry_transition_choice.sysml new file mode 100644 index 0000000000..f2af86f7a1 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_choice.sysml @@ -0,0 +1,16 @@ +package Test { + attribute def Go; + + state Machine { + entry; then idle; + state idle; + state working { + entry action boot { } + transition boot then route; + choice route; + transition route if true then active; + state active; + } + transition first idle accept Go then working; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_choice.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_choice.trace.golden new file mode 100644 index 0000000000..c3def5e7e7 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_choice.trace.golden @@ -0,0 +1,6 @@ +exit: idle +enter: working (entry action) +stmt action body +eval literal true -> true +enter: active +transition: idle -> working (event: accept Go) diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_effect.expected.json b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect.expected.json new file mode 100644 index 0000000000..d03e5fe493 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect.expected.json @@ -0,0 +1,9 @@ +{ + "type": "state", + "trace": true, + "finalState": "active", + "events": [{"signal": "Go"}], + "outputs": { + "log": {"type": "Integer", "value": 123} + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_effect.sysml b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect.sysml new file mode 100644 index 0000000000..60f0d69761 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect.sysml @@ -0,0 +1,20 @@ +package Test { + attribute def Go; + + state Machine { + attribute log : Integer = 0; + + entry; then idle; + state idle; + state working { + entry action boot { assign log := log * 10 + 1; } + transition boot do action { + assign log := log * 10 + 2; + } then active; + state active { + entry action { assign log := log * 10 + 3; } + } + } + transition first idle accept Go then working; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_effect.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect.trace.golden new file mode 100644 index 0000000000..60206057db --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect.trace.golden @@ -0,0 +1,25 @@ +exit: idle +enter: working (entry action) +stmt action body + stmt assign log + eval feature log -> 0 + eval literal 10 -> 10 + eval operator * -> 0 + eval literal 1 -> 1 + eval operator + -> 1 +stmt action body + stmt assign log + eval feature log -> 1 + eval literal 10 -> 10 + eval operator * -> 10 + eval literal 2 -> 2 + eval operator + -> 12 +enter: active (entry action) +stmt action body + stmt assign log + eval feature log -> 12 + eval literal 10 -> 10 + eval operator * -> 120 + eval literal 3 -> 3 + eval operator + -> 123 +transition: idle -> working (event: accept Go) diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.check.expected.json b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.check.expected.json new file mode 100644 index 0000000000..3b41ae7de6 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.check.expected.json @@ -0,0 +1,13 @@ +{ + "verdict": "divergent", + "divergent": { + "log": [ + "\"a-effect a-entry b-effect b-entry \"", + "\"a-effect b-effect a-entry b-entry \"", + "\"a-effect b-effect b-entry a-entry \"", + "\"b-effect a-effect a-entry b-entry \"", + "\"b-effect a-effect b-entry a-entry \"", + "\"b-effect b-entry a-effect a-entry \"" + ] + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.declared.trace.golden new file mode 100644 index 0000000000..34ea612dff --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.declared.trace.golden @@ -0,0 +1,30 @@ +exit: idle +enter: working +choice entering working: next left(entry), right(entry) (unordered; took left(entry) first) +stmt action body +choice entering working: next boot->active(effect), right(entry) (unordered; took boot->active(effect) first) +stmt action body + stmt assign log + eval feature log -> "" + eval literal "a-effect " -> "a-effect " + eval operator + -> "a-effect " +choice entering working: next left.active(entry), right(entry) (unordered; took left.active(entry) first) +enter: active (entry action) +stmt action body + stmt assign log + eval feature log -> "a-effect " + eval literal "a-entry " -> "a-entry " + eval operator + -> "a-effect a-entry " +stmt action body +stmt action body + stmt assign log + eval feature log -> "a-effect a-entry " + eval literal "b-effect " -> "b-effect " + eval operator + -> "a-effect a-entry b-effect " +enter: active (entry action) +stmt action body + stmt assign log + eval feature log -> "a-effect a-entry b-effect " + eval literal "b-entry " -> "b-entry " + eval operator + -> "a-effect a-entry b-effect b-entry " +transition: idle -> working (event: accept Go) diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.expected.json b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.expected.json new file mode 100644 index 0000000000..b0530e0adc --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.expected.json @@ -0,0 +1,32 @@ +{ + "type": "state", + "trace": true, + "events": [{"signal": "Go"}], + "outcomes": [ + { + "finalState": "active+active", + "outputs": {"log": {"type": "String", "value": "a-effect a-entry b-effect b-entry "}} + }, + { + "finalState": "active+active", + "outputs": {"log": {"type": "String", "value": "a-effect b-effect a-entry b-entry "}} + }, + { + "finalState": "active+active", + "outputs": {"log": {"type": "String", "value": "a-effect b-effect b-entry a-entry "}} + }, + { + "finalState": "active+active", + "outputs": {"log": {"type": "String", "value": "b-effect a-effect a-entry b-entry "}} + }, + { + "finalState": "active+active", + "outputs": {"log": {"type": "String", "value": "b-effect a-effect b-entry a-entry "}} + }, + { + "finalState": "active+active", + "outputs": {"log": {"type": "String", "value": "b-effect b-entry a-effect a-entry "}} + } + ], + "admissible": "Entry transitions in the regions of a parallel state: each effect precedes its own target's entry, the regions interleave" +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.seed-1.trace.golden new file mode 100644 index 0000000000..6b9b95c539 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.seed-1.trace.golden @@ -0,0 +1,31 @@ +exit: idle +enter: working +choice entering working: next left(entry), right(entry) (unordered; took right(entry) first) +stmt action body +choice entering working: next left(entry), boot->active(effect) (unordered; took left(entry) first) +stmt action body +choice entering working: next boot->active(effect), boot->active(effect) (unordered; took boot->active(effect) first) +stmt action body + stmt assign log + eval feature log -> "" + eval literal "a-effect " -> "a-effect " + eval operator + -> "a-effect " +choice entering working: next left.active(entry), boot->active(effect) (unordered; took left.active(entry) first) +enter: active (entry action) +stmt action body + stmt assign log + eval feature log -> "a-effect " + eval literal "a-entry " -> "a-entry " + eval operator + -> "a-effect a-entry " +stmt action body + stmt assign log + eval feature log -> "a-effect a-entry " + eval literal "b-effect " -> "b-effect " + eval operator + -> "a-effect a-entry b-effect " +enter: active (entry action) +stmt action body + stmt assign log + eval feature log -> "a-effect a-entry b-effect " + eval literal "b-entry " -> "b-entry " + eval operator + -> "a-effect a-entry b-effect b-entry " +transition: idle -> working (event: accept Go) diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.sysml b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.sysml new file mode 100644 index 0000000000..0151d2175b --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.sysml @@ -0,0 +1,32 @@ +package Test { + attribute def Go; + + state Machine { + attribute log : String = ""; + + entry; then idle; + state idle; + state working parallel { + state left { + entry action boot { } + transition boot do action { + assign log := log + "a-effect "; + } then active; + state active { + entry action { assign log := log + "a-entry "; } + } + } + state right { + entry action boot { } + transition boot do action { + assign log := log + "b-effect "; + } then active; + state active { + entry action { assign log := log + "b-entry "; } + } + } + } + + transition first idle accept Go then working; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.trace.golden new file mode 100644 index 0000000000..34ea612dff --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_effect_regions.trace.golden @@ -0,0 +1,30 @@ +exit: idle +enter: working +choice entering working: next left(entry), right(entry) (unordered; took left(entry) first) +stmt action body +choice entering working: next boot->active(effect), right(entry) (unordered; took boot->active(effect) first) +stmt action body + stmt assign log + eval feature log -> "" + eval literal "a-effect " -> "a-effect " + eval operator + -> "a-effect " +choice entering working: next left.active(entry), right(entry) (unordered; took left.active(entry) first) +enter: active (entry action) +stmt action body + stmt assign log + eval feature log -> "a-effect " + eval literal "a-entry " -> "a-entry " + eval operator + -> "a-effect a-entry " +stmt action body +stmt action body + stmt assign log + eval feature log -> "a-effect a-entry " + eval literal "b-effect " -> "b-effect " + eval operator + -> "a-effect a-entry b-effect " +enter: active (entry action) +stmt action body + stmt assign log + eval feature log -> "a-effect a-entry b-effect " + eval literal "b-entry " -> "b-entry " + eval operator + -> "a-effect a-entry b-effect b-entry " +transition: idle -> working (event: accept Go) diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.expected.json b/internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.expected.json new file mode 100644 index 0000000000..1eb1b44448 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.expected.json @@ -0,0 +1,6 @@ +{ + "type": "state", + "trace": true, + "events": [{"signal": "Enter"}], + "finalState": "inner" +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.sysml b/internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.sysml new file mode 100644 index 0000000000..a95172ea36 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.sysml @@ -0,0 +1,17 @@ +package Test { + attribute def Enter; + + state Machine { + entry; then outside; + state outside; + state A { + entry; then startRoute; + junction startRoute; + transition startRoute if false then never; + state never; + state inner; + } + + transition first outside accept Enter then A.inner; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.trace.golden new file mode 100644 index 0000000000..9fff09d1bc --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_explicit_inner.trace.golden @@ -0,0 +1,4 @@ +exit: outside +enter: A +enter: inner +transition: outside -> inner (event: accept Enter) diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.expected.json b/internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.expected.json new file mode 100644 index 0000000000..a91715ac94 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.expected.json @@ -0,0 +1,9 @@ +{ + "type": "state", + "trace": true, + "events": [{"signal": "Go"}], + "finalState": "accepted", + "outputs": { + "log": {"type": "Integer", "value": 0} + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.sysml b/internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.sysml new file mode 100644 index 0000000000..64944aef94 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.sysml @@ -0,0 +1,19 @@ +package Test { + attribute def Go; + + state Machine { + attribute log : Integer = 0; + entry; then idle; + state idle; + state working { + entry action boot { } + transition boot if false do action { + assign log := 9; + } then rejected; + transition boot then accepted; + state rejected; + state accepted; + } + transition first idle accept Go then working; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.trace.golden new file mode 100644 index 0000000000..19bf1437f9 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_guarded_effect_not_taken.trace.golden @@ -0,0 +1,6 @@ +exit: idle +enter: working (entry action) +stmt action body +eval literal false -> false +enter: accepted +transition: idle -> working (event: accept Go) diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.expected.json b/internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.expected.json new file mode 100644 index 0000000000..ddfd4639ce --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.expected.json @@ -0,0 +1,9 @@ +{ + "type": "state", + "trace": true, + "events": [{"signal": "Reset"}], + "finalState": "inner", + "outputs": { + "log": {"type": "Integer", "value": 12313} + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.sysml b/internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.sysml new file mode 100644 index 0000000000..d9b6eee73f --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.sysml @@ -0,0 +1,22 @@ +package Test { + attribute def Reset; + + state Machine { + attribute log : Integer = 0; + + entry; then start; + state start; + state outer { + entry action boot { assign log := log * 10 + 1; } + transition boot do action { + assign log := log * 10 + 2; + } then inner; + state inner { + entry action { assign log := log * 10 + 3; } + } + deep history resume; + transition first outer accept Reset then resume; + } + transition first start then outer; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.trace.golden new file mode 100644 index 0000000000..6ce033b446 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_history_restore.trace.golden @@ -0,0 +1,44 @@ +exit: start +enter: outer (entry action) +stmt action body + stmt assign log + eval feature log -> 0 + eval literal 10 -> 10 + eval operator * -> 0 + eval literal 1 -> 1 + eval operator + -> 1 +stmt action body + stmt assign log + eval feature log -> 1 + eval literal 10 -> 10 + eval operator * -> 10 + eval literal 2 -> 2 + eval operator + -> 12 +enter: inner (entry action) +stmt action body + stmt assign log + eval feature log -> 12 + eval literal 10 -> 10 + eval operator * -> 120 + eval literal 3 -> 3 + eval operator + -> 123 +transition: start -> outer +exit: inner +exit: outer +enter: outer (entry action) +stmt action body + stmt assign log + eval feature log -> 123 + eval literal 10 -> 10 + eval operator * -> 1230 + eval literal 1 -> 1 + eval operator + -> 1231 +enter: inner (entry action) +stmt action body + stmt assign log + eval feature log -> 1231 + eval literal 10 -> 10 + eval operator * -> 12310 + eval literal 3 -> 3 + eval operator + -> 12313 +transition: inner -> inner (event: accept Reset) diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_junction.expected.json b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction.expected.json new file mode 100644 index 0000000000..67bf085ff9 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction.expected.json @@ -0,0 +1,9 @@ +{ + "type": "state", + "trace": true, + "events": [{"signal": "Go"}], + "finalState": "active", + "outputs": { + "log": {"type": "Integer", "value": 123} + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_junction.sysml b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction.sysml new file mode 100644 index 0000000000..82fd56a62d --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction.sysml @@ -0,0 +1,22 @@ +package Test { + attribute def Go; + + state Machine { + attribute log : Integer = 0; + + entry; then idle; + state idle; + state working { + entry action boot { assign log := 1; } + transition boot then route; + junction route; + transition route if true do action { + assign log := log * 10 + 2; + } then active; + state active { + entry action { assign log := log * 10 + 3; } + } + } + transition first idle accept Go then working; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_junction.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction.trace.golden new file mode 100644 index 0000000000..86af2c5a31 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction.trace.golden @@ -0,0 +1,22 @@ +exit: idle +enter: working (entry action) +stmt action body + stmt assign log + eval literal 1 -> 1 +eval literal true -> true +stmt action body + stmt assign log + eval feature log -> 1 + eval literal 10 -> 10 + eval operator * -> 10 + eval literal 2 -> 2 + eval operator + -> 12 +enter: active (entry action) +stmt action body + stmt assign log + eval feature log -> 12 + eval literal 10 -> 10 + eval operator * -> 120 + eval literal 3 -> 3 + eval operator + -> 123 +transition: idle -> working (event: accept Go) diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.expected.json b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.expected.json new file mode 100644 index 0000000000..9bdc37dbcc --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.expected.json @@ -0,0 +1,6 @@ +{ + "type": "state", + "trace": true, + "events": [{"signal": "Enter"}, {"signal": "Go"}], + "finalState": "recovered" +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.sysml b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.sysml new file mode 100644 index 0000000000..9928437802 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.sysml @@ -0,0 +1,20 @@ +package Test { + attribute def Enter; + attribute def Go; + + state Machine { + entry; then idle; + state idle; + state blocked { + entry action boot { } + transition boot then route; + junction route; + transition route if false then never; + state never; + } + state recovered; + + transition first idle accept Enter then blocked; + transition first idle accept Go then recovered; + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.trace.golden b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.trace.golden new file mode 100644 index 0000000000..21e81ac989 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_entry_transition_junction_no_way_disables.trace.golden @@ -0,0 +1,3 @@ +exit: idle +enter: recovered +transition: idle -> recovered (event: accept Go) diff --git a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.check.expected.json b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.check.expected.json new file mode 100644 index 0000000000..1b4ed32be5 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.check.expected.json @@ -0,0 +1,10 @@ +{ + "verdict": "divergent", + "divergent": { + "log": [ + "\"go(effect);both(entry);r0(entry);split(effect);l1(entry);both(exit);\"", + "\"go(effect);both(entry);split(effect);l1(entry);r0(entry);both(exit);\"", + "\"go(effect);both(entry);split(effect);r0(entry);l1(entry);both(exit);\"" + ] + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.declared.trace.golden new file mode 100644 index 0000000000..ca56970d46 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.declared.trace.golden @@ -0,0 +1,46 @@ + eval feature x -> 0 + eval literal 1 -> 1 +eval operator == -> false +exit: idle +stmt action body + stmt assign log + eval feature log -> "" + eval literal "go(effect);" -> "go(effect);" + eval operator + -> "go(effect);" +enter: both (entry action) +stmt action body + stmt assign log + eval feature log -> "go(effect);" + eval literal "both(entry);" -> "both(entry);" + eval operator + -> "go(effect);both(entry);" +choice entering both: next split->l1(effect), r0(entry) (unordered; took split->l1(effect) first) +stmt action body + stmt assign log + eval feature log -> "go(effect);both(entry);" + eval literal "split(effect);" -> "split(effect);" + eval operator + -> "go(effect);both(entry);split(effect);" +choice entering both: next l1(entry), r0(entry) (unordered; took l1(entry) first) +enter: l1 (entry action) +stmt action body + stmt assign log + eval feature log -> "go(effect);both(entry);split(effect);" + eval literal "l1(entry);" -> "l1(entry);" + eval operator + -> "go(effect);both(entry);split(effect);l1(entry);" +enter: r0 (entry action) +stmt action body + stmt assign log + eval feature log -> "go(effect);both(entry);split(effect);l1(entry);" + eval literal "r0(entry);" -> "r0(entry);" + eval operator + -> "go(effect);both(entry);split(effect);l1(entry);r0(entry);" +transition: idle -> l1 (event: accept Go) +choice exiting both: next l1(exit), r0(exit) (unordered; took l1(exit) first) +exit: l1 +exit: r0 +exit: both (exit action) +stmt action body + stmt assign log + eval feature log -> "go(effect);both(entry);split(effect);l1(entry);r0(entry);" + eval literal "both(exit);" -> "both(exit);" + eval operator + -> "go(effect);both(entry);split(effect);l1(entry);r0(entry);both(exit);" +enter: done +transition: both -> done (event: accept Stop) diff --git a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.expected.json b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.expected.json index 490c9886f2..dfd6779abf 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.expected.json +++ b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.expected.json @@ -1,12 +1,29 @@ { "type": "state", - "schedule": "reverse", "trace": true, "events": [{"signal": "Go"}, {"signal": "Stop"}], - "finalState": "done", - "stateVisits": ["idle", "both", "l1", "r0", "done"], - "outputs": { - "x": {"type": "Integer", "value": 0}, - "log": {"type": "String", "value": "go(effect);both(entry);split(effect);l1(entry);r0(entry);both(exit);"} - } + "outcomes": [ + { + "finalState": "done", + "outputs": { + "x": {"type": "Integer", "value": 0}, + "log": {"type": "String", "value": "go(effect);both(entry);split(effect);l1(entry);r0(entry);both(exit);"} + } + }, + { + "finalState": "done", + "outputs": { + "x": {"type": "Integer", "value": 0}, + "log": {"type": "String", "value": "go(effect);both(entry);split(effect);r0(entry);l1(entry);both(exit);"} + } + }, + { + "finalState": "done", + "outputs": { + "x": {"type": "Integer", "value": 0}, + "log": {"type": "String", "value": "go(effect);both(entry);r0(entry);split(effect);l1(entry);both(exit);"} + } + } + ], + "admissible": "Entry transitions in the regions of a parallel state: each effect precedes its own target's entry, the regions interleave" } diff --git a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.seed-1.trace.golden new file mode 100644 index 0000000000..eb27dbbc30 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.seed-1.trace.golden @@ -0,0 +1,45 @@ + eval feature x -> 0 + eval literal 1 -> 1 +eval operator == -> false +exit: idle +stmt action body + stmt assign log + eval feature log -> "" + eval literal "go(effect);" -> "go(effect);" + eval operator + -> "go(effect);" +enter: both (entry action) +stmt action body + stmt assign log + eval feature log -> "go(effect);" + eval literal "both(entry);" -> "both(entry);" + eval operator + -> "go(effect);both(entry);" +choice entering both: next split->l1(effect), r0(entry) (unordered; took r0(entry) first) +enter: r0 (entry action) +stmt action body + stmt assign log + eval feature log -> "go(effect);both(entry);" + eval literal "r0(entry);" -> "r0(entry);" + eval operator + -> "go(effect);both(entry);r0(entry);" +stmt action body + stmt assign log + eval feature log -> "go(effect);both(entry);r0(entry);" + eval literal "split(effect);" -> "split(effect);" + eval operator + -> "go(effect);both(entry);r0(entry);split(effect);" +enter: l1 (entry action) +stmt action body + stmt assign log + eval feature log -> "go(effect);both(entry);r0(entry);split(effect);" + eval literal "l1(entry);" -> "l1(entry);" + eval operator + -> "go(effect);both(entry);r0(entry);split(effect);l1(entry);" +transition: idle -> l1 (event: accept Go) +choice exiting both: next l1(exit), r0(exit) (unordered; took l1(exit) first) +exit: l1 +exit: r0 +exit: both (exit action) +stmt action body + stmt assign log + eval feature log -> "go(effect);both(entry);r0(entry);split(effect);l1(entry);" + eval literal "both(exit);" -> "both(exit);" + eval operator + -> "go(effect);both(entry);r0(entry);split(effect);l1(entry);both(exit);" +enter: done +transition: both -> done (event: accept Stop) diff --git a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.sysml b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.sysml index e6d1b9b6a4..932d5ce738 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.sysml +++ b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.sysml @@ -1,7 +1,5 @@ -// A transition into a junction declared in one region of a parallel state enters -// the parallel state first: the segment out of the junction runs its effect -// after the parallel state's entry, as that region is entered, while the other -// region starts as usual. +// The route effect joins its region's entry front, after the parallel entry and +// before its target, interleaving with the other region's default entry. package Test { state Machine { attribute log : String = ""; diff --git a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.trace.golden index 54fab84e62..ca56970d46 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region.trace.golden @@ -13,6 +13,7 @@ stmt action body eval feature log -> "go(effect);" eval literal "both(entry);" -> "both(entry);" eval operator + -> "go(effect);both(entry);" +choice entering both: next split->l1(effect), r0(entry) (unordered; took split->l1(effect) first) stmt action body stmt assign log eval feature log -> "go(effect);both(entry);" diff --git a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region_metadata.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region_metadata.trace.golden index 54fab84e62..ca56970d46 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region_metadata.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_inside_orthogonal_region_metadata.trace.golden @@ -13,6 +13,7 @@ stmt action body eval feature log -> "go(effect);" eval literal "both(entry);" -> "both(entry);" eval operator + -> "go(effect);both(entry);" +choice entering both: next split->l1(effect), r0(entry) (unordered; took split->l1(effect) first) stmt action body stmt assign log eval feature log -> "go(effect);both(entry);" diff --git a/internal/ir/lower/entry_transition.go b/internal/ir/lower/entry_transition.go index 48681afebe..0443b40238 100644 --- a/internal/ir/lower/entry_transition.go +++ b/internal/ir/lower/entry_transition.go @@ -7,10 +7,8 @@ import ( "github.com/Open-MBEE/OpenSysML/internal/syntax/ast" ) -// EntryTransition is a transition out of a body's entry action, naming a state the -// body starts in: `entry; then s;` always, `entry; if c then s;` when c holds -// (SysML v2 7.18.3 EntryTransitionMember). A body's alternatives are kept in -// declaration order, the order the guards are tried in. +// EntryTransition is a transition out of a body's entry action. Alternatives +// are kept in declaration order, the order the guards are tried in. type EntryTransition struct { // Decl is the member as written: a TransitionMember, a SuccessionEdge, a // succession usage or a `first start then s;` marker. @@ -18,44 +16,40 @@ type EntryTransition struct { // Guard is nil for an unconditional entry transition. Guard ast.Node Target *ast.StateNode + Via *ast.PseudostateNode + Effect []StateBehavior // Scope is the scope Guard resolves in. Scope *symbols.Scope } -// EntryTransitionShapeFormat reports a transition out of the entry action written -// with a trigger or an effect, which chooses a starting state by its guard alone. -const EntryTransitionShapeFormat = "transition out of the entry action carries %s: a transition out of the entry action " + - "chooses the state its body starts in by its guard alone, `entry; if c then s;` or `entry; then s;` (SysML v2 7.18.3)" +const ( + EntryTransitionAccepterSourceMessage = "A transition with an accepter must have a state as its source. " + + "(SysML v2; pilot validateTransitionUsageTriggerActions)" + EntryTransitionShorthandEffectMessage = "a shorthand transition out of an entry action may carry a guard at most; " + + "write `entry action boot; transition boot do action mark then s;` to give the transition an explicit source " + + "(SysML v2 7.18.3 EntryTransitionMember)" +) // EntryTransitionTargetFormat reports a transition out of the entry action whose // target is a vertex the body cannot start in. const EntryTransitionTargetFormat = "transition out of the entry action reaches %s, " + - "which is not a state to start in (SysML v2 7.18.3)" + "which is not a state or junction/choice route the body can start in (SysML v2 7.18.3)" -// EntryTransitionShapeError marks a transition out of the entry action written -// with a trigger or an effect. +// EntryTransitionShapeError marks a triggered or shorthand effect transition +// out of the entry action. type EntryTransitionShapeError struct { Transition *ast.TransitionMember } func (e *EntryTransitionShapeError) Error() string { - return fmt.Sprintf(EntryTransitionShapeFormat, EntryTransitionCarries(e.Transition)) -} - -// EntryTransitionCarries names what a transition out of the entry action was -// written with beyond its guard: "a trigger", "an effect" or both. -func EntryTransitionCarries(transition *ast.TransitionMember) string { - switch { - case transition.Trigger != nil && len(transition.Effect) > 0: - return "a trigger and an effect" - case transition.Trigger != nil: - return "a trigger" + if e.Transition.Trigger != nil { + return EntryTransitionAccepterSourceMessage } - return "an effect" + return EntryTransitionShorthandEffectMessage } // EntryTransitionTargetError marks a transition out of the entry action whose -// Target is a vertex but not a state. +// target is not a state or an allowed junction/choice. type EntryTransitionTargetError struct { Target ast.Node } @@ -89,22 +83,41 @@ func (g *StateGraph) EntryOwner(owner ast.Node) ast.Node { return owner } -// UnconditionalStart is the state a body starts in whatever its guards say: its -// first entry transition's target when unguarded, else nil. owner is as for StartOf. +// UnconditionalStart is the state a body starts in whatever its guards say. func (g *StateGraph) UnconditionalStart(owner ast.Node) *ast.StateNode { transitions := g.StartOf(owner) if len(transitions) == 0 || transitions[0].Guard != nil { return nil } + if transitions[0].Via != nil { + return g.unconditionalEntryTarget(transitions[0].Via, nil) + } return transitions[0].Target } -// addEntryTransition records a transition out of a body's entry action, which -// designates its target as a state the machine may start in. +func (g *StateGraph) unconditionalEntryTarget(target ast.Node, seen map[*ast.PseudostateNode]bool) *ast.StateNode { + switch node := target.(type) { + case *ast.StateNode: + return node + case *ast.PseudostateNode: + if seen[node] || len(g.Transitions[node]) != 1 || g.Transitions[node][0].Guard != nil { + return nil + } + if seen == nil { + seen = make(map[*ast.PseudostateNode]bool) + } + seen[node] = true + return g.unconditionalEntryTarget(g.Transitions[node][0].Target, seen) + default: + return nil + } +} + +// addEntryTransition records a transition out of a body's entry action. func (g *StateGraph) addEntryTransition(owner ast.Node, transition *EntryTransition) { g.EntryTransitions[owner] = append(g.EntryTransitions[owner], transition) g.recordDeclaredIn(transition.Decl, transition.Scope) - g.designateInitial(transition.Target) + g.designateInitial(entryTransitionTarget(transition)) } // withOwnEntryTransitions runs collect over the members a body writes itself. @@ -128,11 +141,18 @@ func (g *StateGraph) redesignateInitials() { g.designatedInitials = make(map[*ast.StateNode]bool) for _, transitions := range g.EntryTransitions { for _, transition := range transitions { - g.designateInitial(transition.Target) + g.designateInitial(entryTransitionTarget(transition)) } } } +func entryTransitionTarget(transition *EntryTransition) ast.Node { + if transition.Via != nil { + return transition.Via + } + return transition.Target +} + // entryOwner is the body an entry transition written in state's body starts: the // region when state stands for one of a parallel state, else the state itself. func (g *StateGraph) entryOwner(state *ast.StateNode) ast.Node { @@ -142,9 +162,8 @@ func (g *StateGraph) entryOwner(state *ast.StateNode) ast.Node { return state } -// lowerEntryTransition lowers `entry; if c then s;` — a sourceless transition whose -// preceding member is the entry action — into an entry transition of entryOwner's -// body; owner is the body a `done` target completes. +// lowerEntryTransition lowers a sourceless transition whose preceding member is +// the entry action into an entry transition of entryOwner's body. func lowerEntryTransition(graph *StateGraph, member *ast.TransitionMember, owner, entryOwner ast.Node, scope *symbols.Scope) error { if member.Trigger != nil || len(member.Effect) > 0 { return &EntryTransitionShapeError{Transition: member} @@ -156,15 +175,33 @@ func lowerEntryTransition(graph *StateGraph, member *ast.TransitionMember, owner if err != nil || target == nil { return err } - state, ok := target.(*ast.StateNode) - if !ok { + entryScope := symbols.TriggerScope(scope, member) + return addEntryTransitionTarget(graph, member, target, entryOwner, member.Guard, nil, scope, entryScope) +} + +func addEntryTransitionTarget( + graph *StateGraph, + decl ast.Node, + target ast.Node, + owner ast.Node, + guard ast.Node, + effect []StateBehavior, + targetScope *symbols.Scope, + scope *symbols.Scope, +) error { + entry := &EntryTransition{Decl: decl, Guard: guard, Effect: effect, Scope: scope} + switch vertex := target.(type) { + case *ast.StateNode: + entry.Target = vertex + case *ast.PseudostateNode: + if vertex.Kind != ast.PseudostateJunction && vertex.Kind != ast.PseudostateChoice || + graph.declaredIn[vertex] != targetScope { + return &EntryTransitionTargetError{Target: target} + } + entry.Via = vertex + default: return &EntryTransitionTargetError{Target: target} } - graph.addEntryTransition(entryOwner, &EntryTransition{ - Decl: member, - Guard: member.Guard, - Target: state, - Scope: symbols.TriggerScope(scope, member), - }) + graph.addEntryTransition(owner, entry) return nil } diff --git a/internal/ir/lower/fork_plan.go b/internal/ir/lower/fork_plan.go index 3bf114477d..76db769bfe 100644 --- a/internal/ir/lower/fork_plan.go +++ b/internal/ir/lower/fork_plan.go @@ -145,8 +145,9 @@ func (g *StateGraph) defaultEntryInto(owner *ast.StateNode, region *ast.StateReg continue } for _, t := range g.EntryTransitions[body] { - if g.entersByDefault(owner, region, nil, t.Target) { - return "the entry transition naming " + t.Target.Name + target := entryTransitionTarget(t) + if state := g.defaultStart(owner, region, nil, target, nil); state != nil { + return "the entry transition naming " + vertexName(state) } } } diff --git a/internal/ir/lower/state_graph.go b/internal/ir/lower/state_graph.go index 843dd5a7f1..efbfd4ad21 100644 --- a/internal/ir/lower/state_graph.go +++ b/internal/ir/lower/state_graph.go @@ -99,6 +99,8 @@ type StateGraph struct { // absent for one declared directly in the machine. A history pseudostate // restores the configuration of its owner, so the owner must survive lowering. PseudostateOwner map[*ast.PseudostateNode]*ast.StateNode + // PseudostateRegion is the region its outgoing route segments run within, if any. + PseudostateRegion map[*ast.PseudostateNode]*ast.StateRegion // Terminates are the machine's terminate action usages (`action stop terminate;`) // in declaration order: a transition ending at one ends the machine's performance. @@ -343,6 +345,17 @@ func ToStateGraphWithEndpoints(stateMachineDecl ast.Node, scope *symbols.Scope, } graph.collectRegions(body) + for _, pseudo := range graph.Pseudostates { + if graph.PseudostateRegion[pseudo] == nil { + if owner := graph.PseudostateOwner[pseudo]; owner != nil { + region := graph.RegionOf[owner] + if region == nil { + region = graph.HiddenRegionOf[owner] + } + graph.PseudostateRegion[pseudo] = region + } + } + } if err := graph.resolveRunToCompletion(); err != nil { return nil, err } @@ -353,6 +366,7 @@ func ToStateGraphWithEndpoints(stateMachineDecl ast.Node, scope *symbols.Scope, return nil, err } } + graph.redesignateInitials() if err := graph.planForks(); err != nil { return nil, err } @@ -643,6 +657,7 @@ func newStateGraph(scope *symbols.Scope, endpoints EndpointResolver) *StateGraph States: make([]*ast.StateNode, 0), Pseudostates: make([]*ast.PseudostateNode, 0), PseudostateOwner: make(map[*ast.PseudostateNode]*ast.StateNode), + PseudostateRegion: make(map[*ast.PseudostateNode]*ast.StateRegion), TerminateOwner: make(map[*ast.Usage]*ast.StateNode), Transitions: make(map[ast.Node][]*Transition), CompositeStates: make(map[*ast.StateNode][]*ast.StateRegion), @@ -799,8 +814,30 @@ func (g *StateGraph) IsInitial(state *ast.StateNode) bool { } // designateInitial records state as one the machine may start in. -func (g *StateGraph) designateInitial(state *ast.StateNode) { - g.designatedInitials[state] = true +func (g *StateGraph) designateInitial(target ast.Node) { + switch node := target.(type) { + case *ast.StateNode: + g.designatedInitials[node] = true + case *ast.PseudostateNode: + g.designateRouteInitials(node, make(map[*ast.PseudostateNode]bool)) + } +} + +func (g *StateGraph) designateRouteInitials(pseudo *ast.PseudostateNode, seen map[*ast.PseudostateNode]bool) { + if seen[pseudo] { + return + } + seen[pseudo] = true + for _, transition := range g.Transitions[pseudo] { + switch target := transition.Target.(type) { + case *ast.StateNode: + g.designatedInitials[target] = true + case *ast.PseudostateNode: + if target.Kind == ast.PseudostateJunction || target.Kind == ast.PseudostateChoice { + g.designateRouteInitials(target, seen) + } + } + } } // machineMembers is the body of a state machine declaration. @@ -1037,6 +1074,7 @@ func collectRegionStates(graph *StateGraph, region *ast.StateRegion, parent *ast ps := pseudostateFromUsage(n, kind) graph.copyInherited(ps, n, scope) graph.addPseudostate(ps, scope) + graph.PseudostateRegion[ps] = region if parent != nil { graph.PseudostateOwner[ps] = parent } @@ -1055,6 +1093,7 @@ func collectRegionStates(graph *StateGraph, region *ast.StateRegion, parent *ast state = built case *ast.PseudostateNode: graph.addPseudostate(n, scope) + graph.PseudostateRegion[n] = region if parent != nil { graph.PseudostateOwner[n] = parent } @@ -1641,11 +1680,9 @@ func (g *StateGraph) startsAt(decl, guard ast.Node, body transitionBody, source, if err != nil || vertex == nil { return false, err } - start, ok := vertex.(*ast.StateNode) - if !ok { - return false, &EntryTransitionTargetError{Target: vertex} + if err := addEntryTransitionTarget(g, decl, vertex, body.entryOwner, guard, nil, body.scope, body.scope); err != nil { + return false, err } - g.addEntryTransition(body.entryOwner, &EntryTransition{Decl: decl, Guard: guard, Target: start, Scope: body.scope}) return true, nil } @@ -1911,12 +1948,7 @@ func collectSuccessionEdge(graph *StateGraph, n *ast.SuccessionEdge, body transi // subaction names the state it starts in (SysML 7.19.3), the same as // a named entry action with a succession out of it does. if sourceVertex == nil && isEntrySubaction(n.SourceMember) && targetVertex != nil { - target, ok := targetVertex.(*ast.StateNode) - if !ok { - return &EntryTransitionTargetError{Target: targetVertex} - } - graph.addEntryTransition(entryOwner, &EntryTransition{Decl: n, Target: target, Scope: scope}) - return nil + return addEntryTransitionTarget(graph, n, targetVertex, entryOwner, nil, nil, scope, scope) } if sourceVertex == nil { @@ -1936,6 +1968,21 @@ func collectSuccessionEdge(graph *StateGraph, n *ast.SuccessionEdge, body transi // state when it leaves the entry action, otherwise an edge between vertices. func collectTransitionMember(graph *StateGraph, n *ast.TransitionMember, body transitionBody) error { memberList, scope, owner, entryOwner := body.members, body.scope, body.owner, body.entryOwner + if n.Source != nil && graph.entryActionSource(body, n.Source) { + if n.Trigger != nil { + return &EntryTransitionShapeError{Transition: n} + } + if n.Target == nil { + return fmt.Errorf("transition %s names no target", orAnonymous(n.Name)) + } + target, err := graph.targetVertex(scope, n.Target, owner) + if err != nil || target == nil { + return err + } + entryScope := symbols.TriggerScope(scope, n) + return addEntryTransitionTarget(graph, n, target, entryOwner, n.Guard, + transitionEffects(n, entryScope, graph.resolver), scope, entryScope) + } // `transition initial then off;` out of the entry action names the // state the machine starts in, not an edge between two vertices. if n.Trigger == nil && len(n.Effect) == 0 { @@ -1963,6 +2010,15 @@ func collectTransitionMember(graph *StateGraph, n *ast.TransitionMember, body tr return nil } +func (g *StateGraph) entryActionSource(body transitionBody, source ast.Node) bool { + entry, ok := g.endpoints.Endpoint(body.scope, source) + if !ok { + return false + } + return ast.IsEntryAction(ast.EntryActions(body.members), entry) || + ast.IsEntryAction(ast.StateEntryActions(body.containingState), entry) +} + // collectStateNodeTransitions collects the transitions within a state's // substates and its own regions. func collectStateNodeTransitions(graph *StateGraph, n *ast.StateNode, body transitionBody) error { diff --git a/internal/ir/lower/transition_source_test.go b/internal/ir/lower/transition_source_test.go index 11298205df..d514ddf40a 100644 --- a/internal/ir/lower/transition_source_test.go +++ b/internal/ir/lower/transition_source_test.go @@ -204,19 +204,23 @@ func TestToStateGraph_EntryTransitionShape(t *testing.T) { }{ "trigger": { body: `entry; accept Go then idle; state idle;`, - want: fmt.Sprintf(EntryTransitionShapeFormat, "a trigger"), + want: EntryTransitionAccepterSourceMessage, }, "effect": { body: `entry; if true do action mark then idle; state idle;`, - want: fmt.Sprintf(EntryTransitionShapeFormat, "an effect"), + want: EntryTransitionShorthandEffectMessage, }, "trigger after an unguarded start": { body: `entry; then init; accept Go then active; state init; state active;`, - want: fmt.Sprintf(EntryTransitionShapeFormat, "a trigger"), + want: EntryTransitionAccepterSourceMessage, }, - "target is a pseudostate": { - body: `entry; then pick; choice pick; transition first pick then idle; state idle;`, - want: fmt.Sprintf(EntryTransitionTargetFormat, "the choice pick"), + "explicit-source trigger": { + body: `entry action boot { } transition boot accept Go then idle; state idle;`, + want: EntryTransitionAccepterSourceMessage, + }, + "target is a fork": { + body: `entry; then pick; fork pick; state idle;`, + want: fmt.Sprintf(EntryTransitionTargetFormat, "the fork pick"), }, } for name, tc := range cases { @@ -238,6 +242,57 @@ func TestToStateGraph_EntryTransitionShape(t *testing.T) { } } +func TestToStateGraph_EntryTransitionEffectAndRoute(t *testing.T) { + graph, err := ToStateGraph(stateUsageIn(t, ` + package test { + state Machine { + entry action boot { } + transition boot do action mark { } then route; + junction route; + transition first route then idle; + state idle; + } + } + `), nil) + if err != nil { + t.Fatalf("lower: %v", err) + } + entries := graph.StartOf(nil) + if len(entries) != 1 { + t.Fatalf("got %d entry transitions, want one", len(entries)) + } + entry := entries[0] + if entry.Target != nil || entry.Via == nil || entry.Via.Name != "route" { + t.Fatalf("entry target = (%v, %v), want route pseudostate", entry.Target, entry.Via) + } + if len(entry.Effect) != 1 { + t.Fatalf("entry effect has %d behaviors, want one", len(entry.Effect)) + } + if graph.Initial == nil || graph.Initial.Name != "idle" { + t.Fatalf("Initial = %v, want idle after the unguarded junction route", graph.Initial) + } +} + +func TestToStateGraph_EntryTransitionCannotTargetAnotherBodiesRoute(t *testing.T) { + _, err := ToStateGraph(stateUsageIn(t, ` + package test { + state Machine { + entry action boot { } + transition boot then inner::route; + state inner { + junction route; + state idle; + transition route then idle; + } + } + } + `), nil) + var targetErr *EntryTransitionTargetError + if !errors.As(err, &targetErr) { + t.Fatalf("lower error = %v, want an EntryTransitionTargetError", err) + } +} + // The member before the shorthand is named in the error when it is not a // vertex, whatever kind of member it is. func TestToStateGraph_SourcelessTransitionAfterANonVertex(t *testing.T) { diff --git a/internal/ir/view/behavior.go b/internal/ir/view/behavior.go index 8138311ea9..b74b2f6689 100644 --- a/internal/ir/view/behavior.go +++ b/internal/ir/view/behavior.go @@ -136,15 +136,28 @@ func (r *Renderer) entryEdges(view, machine *symbols.Symbol, graph *lower.StateG Geometry: r.memberGeometryOf(view, r.bodySymbol(machine, graph, body.owner), ast.StartFeature, out)} body.node.Children = append([]*Node{start}, body.node.Children...) for _, entry := range entries { - target, ok := nodes[entry.Target] + entryTarget := ast.Node(entry.Target) + if entry.Via != nil { + entryTarget = entry.Via + } + target, ok := nodes[entryTarget] if !ok { out.Notices = append(out.Notices, fmt.Sprintf("entry transition to %s of %s leaves the machine's own states; no edge is drawn", - behaviorNodeName(entry.Target), r.notationName(machine))) + behaviorNodeName(entryTarget), r.notationName(machine))) continue } doc := docOf(graph, entry.Decl, machine.DocName) + label := r.guardLabel(doc, entry.Guard) + if len(entry.Effect) > 0 { + effect := r.behaviorNames(doc, entry.Effect) + if label == "" { + label = "/" + effect + } else { + label += " / " + effect + } + } out.Edges = append(out.Edges, Edge{ - From: start.ID, To: target.ID, Label: r.guardLabel(doc, entry.Guard), Kind: EdgeTransition, + From: start.ID, To: target.ID, Label: label, Kind: EdgeTransition, Origin: nodeOrigin(doc, entry.Decl), Route: r.declaredRouteOf(view, machine, entry.Decl, out), Style: r.declaredEdgeDress(view, machine, entry.Decl, start.ID, target.ID, out), }) diff --git a/tests/parser/testdata/parse/state_entry_transition_effect.golden b/tests/parser/testdata/parse/state_entry_transition_effect.golden new file mode 100644 index 0000000000..80376f92bf --- /dev/null +++ b/tests/parser/testdata/parse/state_entry_transition_effect.golden @@ -0,0 +1,16 @@ +(RootNamespace + (Membership visibility="default" + (Package name="EntryTransition" library=false standard=false + (Membership visibility="default" + (Definition kind="action" abstract=false variation=false name="Mark")) + (Membership visibility="default" + (Definition kind="state" abstract=false variation=false name="Machine" + (EntryMember + (Membership visibility="default" + (Usage kind="action" name="boot" ref=false direction="none" composite=false derived=false ordered=false nonunique=false prefix="entry"))) + (TransitionMember source="boot" target="active" + (Membership visibility="default" + (Usage kind="action" name="mark" ref=false direction="none" composite=false derived=false ordered=false nonunique=false + (Relationship kind="typing" target=Mark + (*ast.QualifiedName))))) + (SubstateMember name="active")))))) \ No newline at end of file diff --git a/tests/parser/testdata/parse/state_entry_transition_effect.sysml b/tests/parser/testdata/parse/state_entry_transition_effect.sysml new file mode 100644 index 0000000000..9493514380 --- /dev/null +++ b/tests/parser/testdata/parse/state_entry_transition_effect.sysml @@ -0,0 +1,9 @@ +package EntryTransition { + action def Mark; + + state def Machine { + entry action boot { } + transition first boot do action mark : Mark then active; + state active; + } +} diff --git a/tools/referee/pssm/emit.go b/tools/referee/pssm/emit.go index 20d15b47de..62e3faebe3 100644 --- a/tools/referee/pssm/emit.go +++ b/tools/referee/pssm/emit.go @@ -139,22 +139,16 @@ func (e *emitter) fail(where, reason string) error { return &TranslateError{Test: e.test.ID, Where: where, Reason: reason} } -// nameVertices names every state and pseudostate by its path as an identifier, -// suffixing a name two vertices share so each is one endpoint. An initial -// pseudostate is named for the helper state startTarget may declare for it. +// nameVertices names each state or pseudostate endpoint by its path, suffixing +// a name two vertices share so each is one endpoint. func (e *emitter) nameVertices(regions []*Region) { var visit func([]*Region) visit = func(regions []*Region) { for _, r := range regions { for _, v := range r.Vertices { - if v.Kind == VertexFinal { - continue - } - base := identifier(v.Path()) - if v.Kind == VertexInitial { - base += "_start" + if v.Kind != VertexInitial && v.Kind != VertexFinal { + e.names[v] = e.take(identifier(v.Path())) } - e.names[v] = e.take(base) visit(v.Regions) } } @@ -501,13 +495,22 @@ func (e *emitter) stateBody(b *strings.Builder, depth int, name, path string, st if path != "" { entryName = path + initialSuffix } - var initialTarget string + var initial *entryStart if len(regions) == 1 { - if initialTarget, err = e.startEntry(b, inner, regions[0], where); err != nil { + if initial, err = e.startEntry(inner, regions[0], where); err != nil { return err } + if parts.entry == "" && initial != nil && initial.effectTransition { + regionPath := regions[0].Name + if path != "" { + regionPath = path + "/" + regionPath + } + entryName = regionPath + initialSuffix + } + } + if err := writeEntry(b, inner, entryName, parts.entry, initial); err != nil { + return err } - writeEntry(b, inner, entryName, parts.entry, initialTarget) if kept != nil { if err := e.keptBehaviors(w, kept, state, parts.exit, where); err != nil { return err @@ -658,14 +661,13 @@ func (w *indentWriter) Raw(text string) { w.b.WriteString(text) } func (w *indentWriter) MadeUp(string) {} -// startEntry spells a single region's initial transition as the destination of -// the state's entry; an empty region contributes no destination. -func (e *emitter) startEntry(b *strings.Builder, inner string, region *Region, where string) (string, error) { +// startEntry returns a single region's initial transition, if it has one. +func (e *emitter) startEntry(inner string, region *Region, where string) (*entryStart, error) { init, tr, err := e.initial(region, where) if err != nil || init == nil { - return "", err + return nil, err } - return e.startTarget(b, inner, init, tr, where) + return e.startTarget(inner, tr, where) } // initialSuffix names the entry action a state's or region's path is suffixed with. @@ -728,17 +730,38 @@ func (e *emitter) plainAction(bh *Behavior, ind, where string) (string, error) { return b.String() + ind + "}", nil } -// writeEntry emits a state's entry: bare `entry; then`, or an entry action -// (entry is its text after `action`) with or without a transition following. -func writeEntry(b *strings.Builder, inner, entryName, entry, initialTarget string) { - switch { - case entry == "" && initialTarget != "": - fmt.Fprintf(b, "%sentry; then %s;\n", inner, initialTarget) - case entry != "" && initialTarget != "": - fmt.Fprintf(b, "%sentry action %s%s\n%stransition %s then %s;\n", inner, spell(entryName), entry, inner, spell(entryName), initialTarget) - case entry != "": - fmt.Fprintf(b, "%sentry action%s\n", inner, entry) +type entryStart struct { + target string + effect []string + forceNamed bool + effectTransition bool +} + +// writeEntry emits a state's entry action and its initial transition. +func writeEntry(b *strings.Builder, inner, entryName, entry string, start *entryStart) error { + if start == nil { + if entry != "" { + fmt.Fprintf(b, "%sentry action%s\n", inner, entry) + } + return nil } + if entry != "" || start.forceNamed { + if entry == "" { + fmt.Fprintf(b, "%sentry action %s;\n", inner, spell(entryName)) + } else { + fmt.Fprintf(b, "%sentry action %s%s\n", inner, spell(entryName), entry) + } + fmt.Fprintf(b, "%stransition %s", inner, spell(entryName)) + if len(start.effect) > 0 { + b.WriteString(" do {\n") + writeStmts(b, inner+" ", start.effect) + b.WriteString(inner + "}") + } + fmt.Fprintf(b, " then %s;\n", start.target) + return nil + } + fmt.Fprintf(b, "%sentry; then %s;\n", inner, start.target) + return nil } // parallelRegion emits one region of an orthogonal state as a parallel substate @@ -756,11 +779,13 @@ func (e *emitter) parallelRegion(b *strings.Builder, depth int, path string, r * return err } if init != nil { - target, err := e.startTarget(b, inner+" ", init, tr, regionWhere(regionName)) + start, err := e.startTarget(inner+" ", tr, regionWhere(regionName)) if err != nil { return err } - fmt.Fprintf(b, "%s entry; then %s;\n", inner, target) + if err := writeEntry(b, inner+" ", regionName+initialSuffix, "", start); err != nil { + return err + } } if err := e.region(b, depth+2, r, path); err != nil { return err @@ -801,32 +826,27 @@ func (e *emitter) initial(r *Region, where string) (*Vertex, *Transition, error) return init, out, nil } -// startTarget spells where a region starts: an initial transition with an effect -// or a pseudostate target starts in a helper state whose completion carries it. -func (e *emitter) startTarget(b *strings.Builder, ind string, init *Vertex, tr *Transition, where string) (string, error) { +// startTarget spells a region's initial target and effect. +func (e *emitter) startTarget(ind string, tr *Transition, where string) (*entryStart, error) { target, err := e.target(tr, where) if err != nil { - return "", err - } - if tr.Effect == nil && (tr.Target == nil || !tr.Target.Kind.IsPseudostate()) { - return target, nil + return nil, err } - helper := e.names[init] - fmt.Fprintf(b, "%sstate %s;\n%stransition first %s", ind, helper, ind, helper) + start := &entryStart{target: target, effectTransition: tr.Effect != nil} + start.forceNamed = tr.Effect != nil || tr.Target.Kind.IsPseudostate() if tr.Effect != nil { - if _, err := e.binding(tr.Effect, effectOf(tr)); err != nil { - return "", err + var stmts []string + if hasParams(tr.Effect) { + stmts, err = e.boundEffect(tr.Effect, ind+" ", effectOf(tr), tr.Name+" effect") + } else { + stmts, err = e.plainBody(tr.Effect, effectOf(tr)) } - stmts, err := e.plainBody(tr.Effect, effectOf(tr)) if err != nil { - return "", err + return nil, err } - b.WriteString(" do {\n") - writeStmts(b, ind+" ", stmts) - b.WriteString(ind + "}") + start.effect = stmts } - fmt.Fprintf(b, " then %s;\n", target) - return helper, nil + return start, nil } // region emits a region's vertices other than its initial and final states (a diff --git a/tools/referee/pssm/emit_test.go b/tools/referee/pssm/emit_test.go index 3173cd4b61..c44ff726c6 100644 --- a/tools/referee/pssm/emit_test.go +++ b/tools/referee/pssm/emit_test.go @@ -134,9 +134,8 @@ func TestEmitTransitionFromOrthogonalRegionUsesScopedPaths(t *testing.T) { } } -// TestEmitInitialIntoPseudostate pins the rewrite of an initial transition -// into a junction: the region starts in a helper state whose completion -// transition reaches the junction, and the model lowers clean. +// TestEmitInitialIntoPseudostate pins that an initial junction route leaves +// the body's named entry action and the model lowers clean. func TestEmitInitialIntoPseudostate(t *testing.T) { m, err := emitFixture(t, "", ` @@ -156,9 +155,8 @@ func TestEmitInitialIntoPseudostate(t *testing.T) { } for _, want := range []string{ "junction S2_J2;", - "state S2_I_start;", - "transition first S2_I_start then S2_J2;", - "entry; then S2_I_start;", + "entry action 'S2.initial';", + "transition 'S2.initial' then S2_J2;", "transition first S2_J2 then S2_S2_1;", } { if !strings.Contains(m.Text, want) { @@ -170,8 +168,8 @@ func TestEmitInitialIntoPseudostate(t *testing.T) { } } -// TestEmitInitialWithEffect pins that an initial transition's effect rides a -// helper state's completion transition, in a single and in a parallel region. +// TestEmitInitialWithEffect pins that an initial transition's effect leaves +// the body's named entry action, in a single and in a parallel region. func TestEmitInitialWithEffect(t *testing.T) { m, err := emitFixture(t, "", ` @@ -206,16 +204,14 @@ func TestEmitInitialWithEffect(t *testing.T) { t.Fatal(err) } for _, want := range []string{ - "state S2_I_start;", - `transition first S2_I_start do {`, + "entry action 'S2.initial' {", + `transition 'S2.initial' do {`, `"T2.1(effect)"`, "then S2_S2_1;", - "transition 'S2.initial' then S2_I_start;", - "state S3_I_start;", - `transition first S3_I_start do {`, + "entry action 'S3/R1.initial';", + `transition 'S3/R1.initial' do {`, `"T3.1(effect)"`, "then S3_S3_1;", - "entry; then S3_I_start;", "entry; then S3_S3_2;", } { if !strings.Contains(m.Text, want) { @@ -225,19 +221,17 @@ func TestEmitInitialWithEffect(t *testing.T) { if appends := strings.Count(m.Text, `"T2.1(effect)";`) + strings.Count(m.Text, `"T3.1(effect)";`); appends != 2 { t.Errorf("initial effects are appended %d times, want once each:\n%s", appends, m.Text) } - if strings.Contains(m.Text, "entry action 'S3/R1.initial'") { - t.Errorf("model folds an initial effect into a region's entry action:\n%s", m.Text) + if strings.Contains(m.Text, "state S2_I_start;") || strings.Contains(m.Text, "state S3_I_start;") { + t.Errorf("model emits a helper state for an initial effect:\n%s", m.Text) } if problems := Validate(m); len(problems) > 0 { t.Errorf("%s\n%s", strings.Join(problems, "\n"), m.Text) } } -// TestEmitInitialHelperNameIsUnique pins that the helper state an initial -// transition starts in shares the vertex name registry, and that the registry -// reserves final names: a state spelled like a suffixed name keeps it, and -// the next collision probes past it. -func TestEmitInitialHelperNameIsUnique(t *testing.T) { +// TestEmitInitialEntryActionKeepsItsName pins that an effect-bearing initial +// transition uses the region's entry-action name without replacing its target. +func TestEmitInitialEntryActionKeepsItsName(t *testing.T) { m, err := emitFixture(t, "", ` @@ -257,22 +251,25 @@ func TestEmitInitialHelperNameIsUnique(t *testing.T) { t.Fatal(err) } for _, want := range []string{ + "entry action 'S2/R1.initial';", + `transition 'S2/R1.initial' do {`, + "then S2_I_start;", "state S2_I_start;", "state S2_I_start_2;", - "state S2_I_start_3;", - "then S2_I_start_3;", - "transition first S2_I_start_3 then S2_I_start_2;", - "entry; then S2_I_start;", + "transition first S2_I_start then S2_I_start_2;", } { if !strings.Contains(m.Text, want) { t.Errorf("model lacks %q:\n%s", want, m.Text) } } - for _, decl := range []string{"state S2_I_start;", "state S2_I_start_2;", "state S2_I_start_3;"} { + for _, decl := range []string{"state S2_I_start;", "state S2_I_start_2;"} { if n := strings.Count(m.Text, decl); n != 1 { t.Errorf("%q is declared %d times, want once:\n%s", decl, n, m.Text) } } + if strings.Contains(m.Text, "state S2_I_start_3;") { + t.Errorf("model emits a helper state:\n%s", m.Text) + } if problems := Validate(m); len(problems) > 0 { t.Errorf("%s\n%s", strings.Join(problems, "\n"), m.Text) } From 7e1a828a330c62e51c2f53a1e0c862efbf02f0bb Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Fri, 2 Oct 2026 22:09:37 +0000 Subject: [PATCH 03/17] test(runtime): admit both composite-entry interleavings Co-Authored-By: jason.han --- ..._anonymous_action_body.check.expected.json | 6 ++ ...nonymous_action_body.declared.trace.golden | 89 +++++++++++++++++++ .../state_anonymous_action_body.expected.json | 19 +++- ..._anonymous_action_body.seed-1.trace.golden | 89 +++++++++++++++++++ .../state_anonymous_action_body.sysml | 5 +- 5 files changed, 200 insertions(+), 8 deletions(-) create mode 100644 internal/exec/runtime/testdata/conformance/state_anonymous_action_body.check.expected.json create mode 100644 internal/exec/runtime/testdata/conformance/state_anonymous_action_body.declared.trace.golden create mode 100644 internal/exec/runtime/testdata/conformance/state_anonymous_action_body.seed-1.trace.golden diff --git a/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.check.expected.json b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.check.expected.json new file mode 100644 index 0000000000..a1e6374929 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.check.expected.json @@ -0,0 +1,6 @@ +{ + "verdict": "divergent", + "divergent": { + "log": ["321789", "321879"] + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.declared.trace.golden new file mode 100644 index 0000000000..92ad91769c --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.declared.trace.golden @@ -0,0 +1,89 @@ +exit: start +enter: working (entry action) +stmt action body + stmt declare k + eval literal 3 -> 3 + stmt while + iteration 1 + eval feature k -> 3 + eval literal 0 -> 0 + eval operator > -> true + stmt assign log + eval feature log -> 0 + eval literal 10 -> 10 + eval operator * -> 0 + eval feature k -> 3 + eval operator + -> 3 + stmt assign k + eval feature k -> 3 + eval literal 1 -> 1 + eval operator - -> 2 + iteration 2 + eval feature k -> 2 + eval literal 0 -> 0 + eval operator > -> true + stmt assign log + eval feature log -> 3 + eval literal 10 -> 10 + eval operator * -> 30 + eval feature k -> 2 + eval operator + -> 32 + stmt assign k + eval feature k -> 2 + eval literal 1 -> 1 + eval operator - -> 1 + iteration 3 + eval feature k -> 1 + eval literal 0 -> 0 + eval operator > -> true + stmt assign log + eval feature log -> 32 + eval literal 10 -> 10 + eval operator * -> 320 + eval feature k -> 1 + eval operator + -> 321 + stmt assign k + eval feature k -> 1 + eval literal 1 -> 1 + eval operator - -> 0 + iteration 4 + eval feature k -> 0 + eval literal 0 -> 0 + eval operator > -> false +enter: nstart +transition: start -> working +do: working +stmt action body + stmt assign log + eval feature log -> 321 + eval literal 10 -> 10 + eval operator * -> 3210 + eval literal 8 -> 8 + eval operator + -> 3218 +exit: nstart +enter: nested (entry action) +stmt action body + stmt assign log + eval feature log -> 3218 + eval literal 10 -> 10 + eval operator * -> 32180 + eval literal 7 -> 7 + eval operator + -> 32187 +transition: nstart -> nested +do: nested +stmt action body +exit: nested (exit action) +stmt action body +enter: done +transition: nested -> done +exit: done +exit: working (exit action) +stmt action body + stmt assign log + eval feature log -> 32187 + eval literal 10 -> 10 + eval operator * -> 321870 + eval literal 9 -> 9 + eval operator + -> 321879 +enter: finished +transition: working -> finished diff --git a/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.expected.json b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.expected.json index b3ddfa90ba..896e2683cc 100644 --- a/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.expected.json +++ b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.expected.json @@ -1,7 +1,18 @@ { "type": "state", - "finalState": "finished", - "outputs": { - "log": { "type": "Integer", "value": 321879 } - } + "outcomes": [ + { + "finalState": "finished", + "outputs": { + "log": { "type": "Integer", "value": 321789 } + } + }, + { + "finalState": "finished", + "outputs": { + "log": { "type": "Integer", "value": 321879 } + } + } + ], + "admissible": "A do step and a dispatch due at one instant: which goes first is open" } diff --git a/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.seed-1.trace.golden new file mode 100644 index 0000000000..92ad91769c --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.seed-1.trace.golden @@ -0,0 +1,89 @@ +exit: start +enter: working (entry action) +stmt action body + stmt declare k + eval literal 3 -> 3 + stmt while + iteration 1 + eval feature k -> 3 + eval literal 0 -> 0 + eval operator > -> true + stmt assign log + eval feature log -> 0 + eval literal 10 -> 10 + eval operator * -> 0 + eval feature k -> 3 + eval operator + -> 3 + stmt assign k + eval feature k -> 3 + eval literal 1 -> 1 + eval operator - -> 2 + iteration 2 + eval feature k -> 2 + eval literal 0 -> 0 + eval operator > -> true + stmt assign log + eval feature log -> 3 + eval literal 10 -> 10 + eval operator * -> 30 + eval feature k -> 2 + eval operator + -> 32 + stmt assign k + eval feature k -> 2 + eval literal 1 -> 1 + eval operator - -> 1 + iteration 3 + eval feature k -> 1 + eval literal 0 -> 0 + eval operator > -> true + stmt assign log + eval feature log -> 32 + eval literal 10 -> 10 + eval operator * -> 320 + eval feature k -> 1 + eval operator + -> 321 + stmt assign k + eval feature k -> 1 + eval literal 1 -> 1 + eval operator - -> 0 + iteration 4 + eval feature k -> 0 + eval literal 0 -> 0 + eval operator > -> false +enter: nstart +transition: start -> working +do: working +stmt action body + stmt assign log + eval feature log -> 321 + eval literal 10 -> 10 + eval operator * -> 3210 + eval literal 8 -> 8 + eval operator + -> 3218 +exit: nstart +enter: nested (entry action) +stmt action body + stmt assign log + eval feature log -> 3218 + eval literal 10 -> 10 + eval operator * -> 32180 + eval literal 7 -> 7 + eval operator + -> 32187 +transition: nstart -> nested +do: nested +stmt action body +exit: nested (exit action) +stmt action body +enter: done +transition: nested -> done +exit: done +exit: working (exit action) +stmt action body + stmt assign log + eval feature log -> 32187 + eval literal 10 -> 10 + eval operator * -> 321870 + eval literal 9 -> 9 + eval operator + -> 321879 +enter: finished +transition: working -> finished diff --git a/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.sysml b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.sysml index f058def753..479ca7a1b1 100644 --- a/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.sysml +++ b/internal/exec/runtime/testdata/conformance/state_anonymous_action_body.sysml @@ -1,9 +1,6 @@ package Test { // Entry, do and exit behaviors written as anonymous inline action bodies. - // Each digit records one statement, so the number shows the ordering: entry - // loop (3, 2, 1), the do body (8), the nested entry (7) that the region's - // initial transition reaches one step later, then the exit body (9) once - // the region has reached `done` as well as the do body having ended. + // The due do step and nested entry can occur in either order before exit. state def Bodies { attribute log : Integer = 0; From b938fe80cdbeb2c0cd9c12833e398d1074ae616e Mon Sep 17 00:00:00 2001 From: Devin AI <158243242+devin-ai-integration[bot]@users.noreply.github.com> Date: Fri, 2 Oct 2026 22:53:35 +0000 Subject: [PATCH 04/17] docs(states): derive entry-transition effects and write-granular change triggers, adjudicate PSSM movements Co-Authored-By: jason.han --- .../entry-transition-effects.added.md | 1 + .../state-change-trigger-writes.fixed.md | 1 + .../design/precise-semantics-alignment.md | 32 +++++--- .../design/region-order-scheduling.md | 8 ++ docs/project/behavior-semantic-oracle.md | 32 +++++++- docs/project/pssm-referee-baseline.json | 68 ++++++--------- docs/project/pssm-referee.md | 82 +++++++++++++------ docs/project/spec-compliance.md | 15 +--- internal/exec/runtime/robustness_test.go | 2 +- internal/exec/runtime/state_change_trigger.go | 4 +- .../exec/runtime/state_change_trigger_test.go | 43 ++++++++++ internal/exec/runtime/state_executor.go | 24 ++++-- ...ry_transition_effect_regions.expected.json | 2 +- ...ion_inside_orthogonal_region.expected.json | 2 +- 14 files changed, 212 insertions(+), 104 deletions(-) create mode 100644 changes/unreleased/entry-transition-effects.added.md create mode 100644 changes/unreleased/state-change-trigger-writes.fixed.md diff --git a/changes/unreleased/entry-transition-effects.added.md b/changes/unreleased/entry-transition-effects.added.md new file mode 100644 index 0000000000..103951f333 --- /dev/null +++ b/changes/unreleased/entry-transition-effects.added.md @@ -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; a transition whose entry would start a body through a route with no way through is not enabled. 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. diff --git a/changes/unreleased/state-change-trigger-writes.fixed.md b/changes/unreleased/state-change-trigger-writes.fixed.md new file mode 100644 index 0000000000..e0726d709f --- /dev/null +++ b/changes/unreleased/state-change-trigger-writes.fixed.md @@ -0,0 +1 @@ +- **Change triggers observe every completed write.** A state machine's `accept when ` 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. diff --git a/docs/internals/design/precise-semantics-alignment.md b/docs/internals/design/precise-semantics-alignment.md index 925f9f3794..5300e62afa 100644 --- a/docs/internals/design/precise-semantics-alignment.md +++ b/docs/internals/design/precise-semantics-alignment.md @@ -812,10 +812,10 @@ case arises only through the referee's translation. `state_junction_no_way_throu `robustness_junction_exit_route_test.go`, and `robustness_junction_join_test.go` (`junction_after_choice_keeps_runtime_error`, `junction_cycle_keeps_runtime_error`, `junction_unevaluable_guard_keeps_runtime_error`). **agrees** since the decision. *Join 003* -passes; *Junction 002* and *Junction 004* stay `fail` in the referee because their junction lies -after the start state the translation needs (`emit.go:startTarget`), so the transition the -runtime disables is that state's completion, not the compound transition PSSM disables (finding -11, open decision 8). *Choice 005* traces the same reach +passes, and so do *Junction 002* and *Junction 004* since the initial transition is written out +of the region's named entry action: the junction is then the body's own entry route, and a +transition whose entry would start a body through it is not enabled +(`state_route.go:defaultEntryRoutesAvailable`), the compound transition PSSM disables. *Choice 005* traces the same reach from the other side — its junction on the composite's default entry is read before `T2(effect)` and the composite's entry — and is refused on its acting guards before the order is reached; see [A guard whose behavior acts on the model](#a-guard-whose-behavior-acts-on-the-model). @@ -1035,11 +1035,14 @@ duration` when the state is entered (a composite's timer counts from entering th (`state_time_trigger_restarts_on_re_entry`); units are converted to seconds (`state_time_trigger_test.go`). **agrees** (by exclusion). -**SM40. Change triggers.** *v2/KerML:* §7.18.3 `accept when `, a `ChangeSignal` -accepted when its condition becomes true; the project takes a rising edge. *Runtime:* -`state_change_trigger.go` polls the conditions of the active configuration's transitions once -per `runStep`, after the do round and before the queued occurrence, firing on a false-to-true -edge through the same `dispatchInOrder` as a signal (`state_change_trigger_rising_edge`, +**SM40. Change triggers.** *v2/KerML:* §7.18.3 `accept when `, `Triggers.kerml` +`TriggerWhen`: a `ChangeSignal` sent when its condition changes from false to true, observed by +`ObserveChange` after each completed feature write (`FeatureWritePerformance` assigns when its +performance ends). *Runtime:* `feature_write_watch.go` re-evaluates, after every completed +outermost write, the conditions of the active configuration's transitions whose read set the +write touched, and `state_change_trigger.go` queues each rise and dispatches it once per +`runStep`, after the do round and before the queued occurrence, through the same +`dispatchInOrder` as a signal (`state_change_trigger_transient_rise`, `state_change_trigger_atomic_write`, (`state_change_trigger_rising_edge`, `state_change_trigger_event_order`, `state_change_trigger_autonomous`). **agrees** (by exclusion). **SM41. The shared clock: quiescence before time moves.** PSSM §2.3: a tool "may be limited to a @@ -2555,7 +2558,12 @@ sites of the runtime's fixed, the pool's order and the do step drawn on the entr apart by the source performing nothing, which neither v2 nor PSSM does. The three stay `fail`, their reasons citing the language difference. Whether that difference takes a *differs because v2 differs* row — moving the three to `differs-by-design` through - `tools/referee/pssm/rows.go:TestRows` — is open decision 8. + `tools/referee/pssm/rows.go:TestRows` — was open decision 8. *Withdrawn*: the reading + that v2 cannot place the effect holds for the shorthand `EntryTransitionMember` only. A + transition out of a named entry action is a `TransitionUsage` performed as a + `NonStateTransitionPerformance`, its effect after the entry action and before the + target's entry, within the entry; the emitter spells the initial transition that way and + the three pass (see the referee record). - *History 001-C*'s first half is about the **pool's order** (SM10): PSSM generates a completion event as its source is entered and dispatches in generation order (§8.5.9), so the entry draw decides the pool's order, which `scheduleTransitionEvents` @@ -2665,4 +2673,6 @@ Addressed to the maintainers; each gives the options and the lean. construct both languages have, and the runtime implements the v2 side; this one would name a construct v2 lacks, and a `differs-by-design` count that grows by three on a translation limit reads as conformance gained. The three reasons are precise and stable, and the bucket can be moved in a - change of its own if the maintainers read it otherwise. + change of its own if the maintainers read it otherwise. *Withdrawn*: the premise was the + shorthand's. A transition out of a named entry action carries an effect within the entry + (`TransitionPerformances.kerml` `NonStateTransitionPerformance`), and the three pass. diff --git a/docs/internals/design/region-order-scheduling.md b/docs/internals/design/region-order-scheduling.md index 2a1eae07c1..7db0993ebc 100644 --- a/docs/internals/design/region-order-scheduling.md +++ b/docs/internals/design/region-order-scheduling.md @@ -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 diff --git a/docs/project/behavior-semantic-oracle.md b/docs/project/behavior-semantic-oracle.md index 86393b8274..48b89bc606 100644 --- a/docs/project/behavior-semantic-oracle.md +++ b/docs/project/behavior-semantic-oracle.md @@ -1730,9 +1730,35 @@ 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. -### Entry transitions in the regions of a parallel state: each effect precedes its own target's entry, the regions interleave - -Derivation pending. +### 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. ## What the executor gets wrong diff --git a/docs/project/pssm-referee-baseline.json b/docs/project/pssm-referee-baseline.json index 34b96e43ef..b340d26469 100644 --- a/docs/project/pssm-referee-baseline.json +++ b/docs/project/pssm-referee-baseline.json @@ -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-02", + "develop": "b2d3b65004587bc0f7469e19ecc2e0e42c28063a" }, "buckets": { "differs-by-design": 5, - "fail": 11, + "fail": 6, "not-expressible": 34, - "pass": 53 + "pass": 58 }, "tests": [ { @@ -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)", @@ -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", @@ -1440,17 +1436,12 @@ "class": "extension", "row": "SM32", "rowKind": "agrees", - "bucket": "fail", - "reasons": [ - "reached a trace the suite does not admit: S1(entry)", - "admitted trace not reached: T3(effect)", - "reports on SM32 (Junction or join with no path through): agrees" - ], + "bucket": "pass", "expected": [ "T3(effect)" ], "reached": [ - "S1(entry)" + "T3(effect)" ], "runs": 1 }, @@ -1475,38 +1466,31 @@ "class": "extension", "row": "SM32", "rowKind": "agrees", - "bucket": "fail", - "reasons": [ - "reached a trace the suite does not admit: S1(entry)::T1.3(effect)::S1.2(exit)", - "admitted trace not reached: T3(effect)", - "reports on SM32 (Junction or join with no path through): agrees" - ], + "bucket": "pass", "expected": [ "T3(effect)" ], "reached": [ - "S1(entry)::T1.3(effect)::S1.2(exit)" + "T3(effect)" ], - "runs": 2 + "runs": 1 }, { "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", diff --git a/docs/project/pssm-referee.md b/docs/project/pssm-referee.md index bf2d0cde37..ab440077fe 100644 --- a/docs/project/pssm-referee.md +++ b/docs/project/pssm-referee.md @@ -223,8 +223,8 @@ differs* rows, only SM15 (a do activity and the machine competing for one occurr reached by an expressible test; SM36 and SM37 (local and internal transitions) have no spelling and their tests are not expressible, and A12, C6 and C9 are action and composite-structure rows no state-machine test exercises. SM11, SM28, SM30 and SM32 are now `agrees` rows: their -PSSM decisions are implemented. Junction 002 and Junction 004 still fail while citing SM32, -because an `agrees` citation does not change a trace mismatch's bucket. SM34 remains +PSSM decisions are implemented; Junction 002 and Junction 004 pass citing SM32, and an `agrees` +citation would not change a trace mismatch's bucket. SM34 remains *differs, v2 silent*, narrowed to when the join owner is left and cited by Join001. SM9 (when a completion guard is read) no failing test reaches, and SM45 (destroying a performing object), C3 (multi-valued connector ends) and C8 (a send with no receiver) are not state-machine rows @@ -232,7 +232,7 @@ and no test in the suite reaches them. ## Baseline -Recorded **2026-10-01** on develop commit **`deca2b0389f796b02fa1c30a387617d0613a034c`** with deferred signals written in the +Recorded **2026-10-02** on develop commit **`b2d3b65004587bc0f7469e19ecc2e0e42c28063a`** with deferred signals written in the standard buffer / accept-loop / exit-flush encoding the migrator writes (the `defer` state member, an OpenSysML extension, and the runtime's deferral machinery are removed), with entry, do and effect behaviors bound to the triggering event's data, exit behaviors to the leaving transition's payload, the @@ -240,7 +240,8 @@ behaviors returning the call's outputs, the tester's calls and traces driven in the tester's order and standalone machines read as targets, with completion events queued in the order their sources are entered and a due do step of an entered state drawn against the sibling regions' remaining entry units (the pool's order following the entry draw and the do step on the -entry front, finding 11's two runtime parts), the order of orthogonal +entry front, finding 11's two runtime parts), a region's initial transition spelled as a transition +out of its named entry action whose effect and route are units of the region's entry front, the order of orthogonal regions drawn as choice points at finding 9's four sites (region entry, region exit, the units of the firings one occurrence selects, a due do step against the dispatch, drawn per token move of the do flow), `terminate` executing @@ -255,15 +256,47 @@ The regenerated JSON and the bucket figures below are the current baseline. | Bucket | Tests | |---|---:| -| `pass` | 53 | -| `fail` | 11 | +| `pass` | 58 | +| `fail` | 6 | | `not-expressible` | 34 | | `differs-by-design` | 5 | | **Total** | **103** | ### Movements since the previous baseline -The current baseline records **53 `pass`**, **11 `fail`**, **34 `not-expressible`** and **5 +The current baseline records **58 `pass`**, **6 `fail`**, **34 `not-expressible`** and **5 +`differs-by-design`** tests, from 53 / 11 / 34 / 5. Five tests moved, each from `fail` to +`pass`; no other test's bucket, reasons or reached set changed. All five turn on how a region's +initial transition is spelled. The emitter used to translate it, when it had an effect or ended +at a pseudostate, as the completion of a behavior-less helper start state, on the reading that an +entry transition carries a guard at most (§7.18.3 `EntryTransitionMember`). That holds for the +shorthand only: a transition out of a *named* entry action, `entry action 'R.initial'; transition +'R.initial' do { … } then s;`, is a `TransitionUsage` whose source is an action, performed as a +`NonStateTransitionPerformance` that follows the entry action within the entry, its effect before +the target's entry (`TransitionPerformances.kerml`; the pinned pilot accepts the shape). The +emitter now writes that (`emit.go:startEntry`, `writeEntry`), the runtime executes such a +transition's effect and junction or choice route as part of entering the body +(`state_executor.go:startIn`), and in a region of a parallel state the effect is a unit of the +region's entry queue ([the derivation](behavior-semantic-oracle.md#effects-on-the-way-into-the-regions-of-a-parallel-state-each-precedes-its-own-targets-entry-the-regions-interleave)). Finding 11's +language difference and open decision 8 are withdrawn with it. + +| Test | Cause | Movement | Adjudication | +|---|---|---|---| +| Entering 010 | translation limitation, finding 11 (withdrawn) | `fail` → `pass`, 4 → 20 runs | Expected. `T2.1(effect)` is a unit of region 2's entry queue, so it falls before, between or after region 1's explicit entry of `S1.1`; the three admitted orders are reached and nothing else | +| Entering 011 | translation limitation, finding 11 (withdrawn) | `fail` → `pass`, 4 → 40 runs | Expected. Each region's initial effect precedes its own target's entry and interleaves with the other region's two units: all six admitted orders, nothing else | +| Junction 002 | translation limitation (the helper start state), SM32 | `fail` → `pass` | Expected. `S1`'s initial transition now leads from its entry action into `S1_Junction1`, whose guards are all false, so the transition on `Start` into `S1` has no way through and is not enabled (SM32, `state_route.go:defaultEntryRoutesAvailable`); `Continue` fires `T3`, the trace PSSM admits. Before, the junction lay after the helper state, whose completion was what the runtime disabled, after `S1(entry)` | +| Junction 004 | translation limitation (the helper start state), SM32 | `fail` → `pass`, 2 → 1 runs | Expected. As *Junction 002*, the junction with no way through being region 2's initial route inside the parallel `S1`: the default entry of the sibling region is checked with the transition's explicit target, so the transition into `S1` is not enabled and `T3` fires | +| Junction 005 | translation limitation, finding 11 (withdrawn); runtime gap | `fail` → `pass`, 4 → 20 runs | Expected. Region 2's `T2.1(effect)` is a unit of its entry queue, and `T1.3(effect)`, the segment out of the region-1 junction the entering transition targets, is now a unit of region 1's queue after `S1(entry)` (`state_region_entry.go:enterRegion`) rather than run before either region is entered; the three admitted orders are reached, `S2.1`'s real completion still dispatched after the front | + +The six that remain `fail` are each adjudicated below: *Transition 017*, *Exiting 002*, +*History 001-C* and *History 002-B* on suite defects recorded in `omg-issues.md`, *Join001* on +SM34 (*differs, v2 silent*) and the suite's malformed trace, and *Transition 019* on the order +of silent target entries against the `T*.3` effects, where v2 orders the completion pool by +entry and the suite by effect. + +### Movements before that + +The baseline before that recorded **53 `pass`**, **11 `fail`**, **34 `not-expressible`** and **5 `differs-by-design`** tests, from 52 / 12 / 34 / 5. The count change is *Join003*, which moved from `fail` to `pass`: its first completion segment now arrives on its own occurrence, and the second is not enabled because the join's only way out is guarded false. @@ -487,7 +520,6 @@ table — and no bucket moves. | Test | Finding | Movement | Adjudication | |---|---|---|---| | Transition 017 | 11 (the pool's order, fixed), suite defect | `fail` → `fail`, reason changed | Expected. The three admitted traces that dispatch `T3.1.2(effect)`, the completion of `S3.1`'s region, before `T2.2(effect)`, the completion of `S1`'s other region — `T2(effect)::S1(entry)::T3.1.2(effect)::T2.2(effect)::S3.1(doActivity)::T3.2(effect)`, `…::T3.1.2(effect)::S3.1(doActivity)::T2.2(effect)::…` and `…::S3.1(doActivity)::T3.1.2(effect)::T2.2(effect)::…` — are reached: region 3 drawn first at `entering S1` puts `S3.1.1`'s completion into the pool ahead of `S2.1`'s, and the do step falls before, between or after the two dispatches as before. Six of the eight admitted traces are reached; the two still missing fire `T3.2`, `S3.1`'s own completion transition, before `T3.1.2`, the completion out of its region, the suite's defect recorded in [`omg-issues.md`](omg-issues.md#pssm-transition-017-admits-a-parents-completion-before-its-regions). `fail` citing the defect alone; finding 11's part of the reason is closed | -| Entering 011 | 11 (an initial transition's effect, a completion effect in v2) | `fail` → `fail`, reason changed | Expected (the enumeration's `2 of 6`). Both regions' initial transitions have an effect, spelled as a completion out of a start state; the two start states' completions now dispatch in the order the entry draw entered them, so `S1(entry)::T1.1(effect)::S1.1(entry)::T2.1(effect)::S1.2(entry)` is reached beside `S1(entry)::T2.1(effect)::S1.2(entry)::T1.1(effect)::S1.1(entry)`. The four still missing interleave one region's effect with the other's entry, UML's initial-transition effect as an entry unit, which no v2 completion gives (finding 11, the alignment note's open decision 8); the reason stands on them | | History 001-C | 11 (the pool's order, fixed; the suite's defect) | `fail` → `fail`, reason changed | Expected (the enumeration's `2 of 2` for the first half). The first entry of `S1` now dispatches `S2.1`'s completion before `S1.1`'s when region 2 is drawn first, so `S1(entry)::S2.2(entry)::S1.1(exit)::S1.2(entry)::…` is reached beside the trace the PSSM text prints. The ten still missing fire `S1.1(exit)::S1.2(entry)` inside the step that restores region 2, the suite's defect recorded in [`omg-issues.md`](omg-issues.md#pssm-history-001-c-and-002-b-admit-a-completion-inside-the-restore-and-contradict-each-other); the reason stands on them | | History 002-B | 11 (the pool's order, fixed; the suite's defect) | `fail` → `fail`, reason changed | Expected (the enumeration's `1 of 2, 1 extra / 2 of 3`). After the restore, region 1's default entry of `S1.1` and region 2's restored `S2.2` with its initial `S2.2.1` each generate a completion, dispatched now in the order the entry draw entered them, so `…::T3(effect)::S1(entry)::S2.2(entry)::S2.2.1(exit)::T2.2.2(effect)::S2.2.2(entry)::S1.1(exit)::S1.2(entry)::S1(exit)`, the order the specification's own text gives, is reached beside the one reached before. The first entry of `S1` likewise dispatches `S2.1`'s completion first when region 2 is drawn first, `S1(entry)::S2.1(exit)::S2.2(entry)::S1.1(exit)::S1.2(entry)::…`, the order §8.5.9 gives and *History 001-C* admits for the identical half — two traces, one per restore order, which this test does not register. Two of the six admitted are reached and two unregistered ones; the four still missing — three that dispatch `S2.2.1`'s completion, generated a step later, before `S1.1`'s, and one that fires `T1.2` inside the restore — are the suite's defect, recorded in `omg-issues.md` as above; the reason stands on them and on the two unregistered traces | @@ -593,7 +625,7 @@ on what remains missing. No count moved between the baseline of develop `bcc6b13e0` (with the junction branch-choice fix, 2026-09-15) and the one that followed it (develop `46828f14f`, 2026-09-16). The baseline file changed all the same: the adjudication of -the fourteen failures it left unattributed ([below](#fail-11)) added four tests to the +the fourteen failures it left unattributed ([below](#fail-6)) added four tests to the committed table — *Junction 004* and *Join003* on SM32, *Join001* and *Transition 019* on SM34, both *differs, v2 silent* rows — so their rows now carry the row and its verdict, and their reasons the *reports on* line. All four stay `fail`, as a test mapped to a tool-choice @@ -740,16 +772,16 @@ short trace to a budget exhaustion: with SM11 its `S1` now completes and fires ` history, and the history-record timing of finding 7 makes that re-enter `S1.1` without end. The remaining failures' reasons are byte-identical to the previous baseline's. -### `pass` (53) +### `pass` (58) Behavior 001, Behavior 002, Behavior 003 A, Behavior 003 B, Transition 001, Transition 007, Transition 011 C, Transition 015, Transition 016, Transition 020, Transition 022, Event 001, Event 002, Event 008, Event 009, Event 010, Event 015, Event 016 A (reports on SM11), Event 016 B, Event 017 A, Event 017 B, Event 018, Event 019 A, Event 019 B, Event 019 C, Event 019 D, Event 019 E, Entering 004, -Entering 005, Exiting 001, Exiting 003, Exiting 005, Fork 002, Choice 001 and Choice 002 (report on SM30), Choice 003, +Entering 005, Entering 010, Entering 011, Exiting 001, Exiting 003, Exiting 005, Fork 002, Choice 001 and Choice 002 (report on SM30), Choice 003, Choice 004, Final001 (reports on SM11), Deferred 002, History 001-A, History 001-B, History 001-D, History 002-A, History 002-C (reports on SM28), History 002-D, Join002, Join003, Junction 001, -Junction 003, Standalone 003, Terminate 001, Terminate 002. +Junction 002 and Junction 004 (report on SM32), Junction 003, Junction 005, Standalone 003, Terminate 001, Terminate 002. ### `differs-by-design` (5) @@ -761,9 +793,9 @@ Junction 003, Standalone 003, Terminate 001, Terminate 002. | Deferred 004 A | SM7 | `S1.1(exit)::T1.2(effect)::S2.1(exit)::T2.2(effect)::S1(exit)::T4(effect)` — the sibling region's `T2.2` fires on `Continue` at once; PSSM holds it until `S1.1` releases the occurrence | | Deferred 004 B | SM7 | `S1.1.1(exit)::T1.1.2(effect)::S1.1(exit)::S2.1(exit)::T2.2(effect)::S1(exit)` — the same with the deferring state nested one level deeper than the sibling's transition | -### `fail` (11) +### `fail` (6) -Every failure is accounted for. Three cite a note row, six cite a finding recorded +Every failure is accounted for. One cites a note row, three cite a finding recorded [below](#findings-about-our-own-conformance), and two additional failures are described after those tables: *Transition 019* (silent target-state entry order versus effect order) and *Exiting 002* (a suite defect). The failures citing a note row or finding are second opinions on @@ -771,15 +803,13 @@ the referenced rule or finding; those citations do not themselves determine the a translation defect: each translated model was read against the test's UML, and every construct the test uses reaches the run. -#### Citing a note row (3) +#### Citing a note row (1) | Test | Row | What the run shows | |---|---|---| -| Junction 002 | SM32 | Reaches `S1(entry)` while PSSM admits `T3(effect)`. The junction is after the helper start state, so the disabled transition is that state's completion (finding 11, open decision 8). The trace mismatch remains `fail` although SM32 is now `agrees` | -| Junction 004 | SM32 | Reaches `S1(entry)::T1.3(effect)::S1.2(exit)` while PSSM admits `T3(effect)`. As in *Junction 002*, the junction is after the helper start state, so the disabled transition is that state's completion (finding 11, open decision 8); the SM32 citation is `agrees`, but the trace mismatch remains `fail` | | Join001 | SM34 | The run leaves `S1` after the last incoming effect, where PSSM leaves it before that effect. Its second registered trace is malformed: it names nonexistent `S1.2`, repeats `T2.4` and omits `T2.3` ([suite defect](omg-issues.md#pssm-join-001-admits-a-malformed-trace)) | -#### Citing a finding (6) +#### Citing a finding (3) One line per test, from the baseline's `reasons`: what the run reached that the suite does not admit (`—` when every reached trace is admitted and the failure is only a missing one), and @@ -789,11 +819,8 @@ quoted and the number given. The full sets are in the baseline file. | Test | Finding | Reached, not admitted | Admitted, not reached | |---|---|---|---| | Transition 017 | suite defect (finding 11's part, the pool's order, fixed) | — | `T2(effect)::S1(entry)::T2.2(effect)::T3.2(effect)::S3.1(doActivity)::T3.1.2(effect)` and `T2(effect)::S1(entry)::T2.2(effect)::T3.2(effect)::T3.1.2(effect)::S3.1(doActivity)` (six of the eight admitted orders are reached: the do activity's segment before, between and after the two completions' dispatches, the completions `T2.2` and `T3.1.2` in either order — PSSM's pool holds them in the order their sources were entered (§8.5.9), which the entry draw at `entering S1` decides, and the runtime queues each as its source's entry unit is performed). The two missing fire `T3.2`, `S3.1`'s completion transition, before `T3.1.2`, the completion out of its own region, and run the do activity's segment after `S3.1` was left; they contradict the test's expected sequence and `StatePerformances.kerml` alike and are the suite's defect recorded in [`omg-issues.md`](omg-issues.md#pssm-transition-017-admits-a-parents-completion-before-its-regions) — no runtime reaches them, so the test stays `fail` on them | -| Entering 010 | 11 (an initial transition's effect, a completion effect in v2) | — | `S1(entry)::T2.1(effect)::S1.1(entry)::S2.1(entry)` and `S1(entry)::T2.1(effect)::S2.1(entry)::S1.1(entry)` (the third admitted order is reached; both run `T2.1(effect)`, the second region's initial transition's effect, before the first region's explicit target `S1.1` is entered. UML runs that effect as part of the region's default entry, so PSSM admits it anywhere against the sibling's entry units; SysML v2 has no place for an effect on an entry transition, so the referee spells it as the effect of a completion transition out of a start state, which the runtime dispatches as a step of its own after the entry, as it does every v2 completion. Folding the effect into the target's entry action instead is refused by this very test: region 1's initial transition `T1.1` has an effect too, and its target `S1.1` is the one the tester enters explicitly, so the fold runs `T1.1(effect)` on an entry that bypasses the initial transition — a trace in none of the three admitted; the design note's candidate table has the enumeration) | -| Entering 011 | 11 (an initial transition's effect, a completion effect in v2) | — | `S1(entry)::T1.1(effect)::T2.1(effect)::S1.1(entry)::S1.2(entry)` and 3 more orders of the two regions' initial effects and entries (two of the six admitted orders are reached, each region's initial effect and entry whole, in the order the entry draw entered the two start states; as *Entering 010*, with an initial effect in each region. The four missing interleave one region's effect with the other's entry. The fold into the target's entry action reaches the same two and no refused trace, and no more: one entry action is one unit, so `T1.1(effect)` cannot be split from `S1.1(entry)` around the sibling's units as the other four admitted orders split it) | | History 001-C | 11 (the suite's defect; the pool's order, fixed) | — | `S1(entry)::S1.1(exit)::S1.2(entry)::S2.2(entry)::S2.2.1(exit)::S2.2.2(entry)::S1(exit)::S1(entry)::S1.1(exit)::S1.2(entry)::S2.2(entry)::S2.2.2(entry)::S1(exit)` and 9 more orders of the two regions' entries and exits (two of the twelve admitted orders are reached, the one the PSSM text prints and the one that dispatches `S2.1`'s completion before `S1.1`'s after the first entry of `S1` — the pool in the order the regions were entered, which the runtime's queue follows). The ten missing fire `S1.1(exit)::S1.2(entry)`, a completion the default entry of region 1 enables, *inside* the step that restores region 2, before or between `S2.2(entry)::S2.2.2(entry)`; the test's own note ends the restoring step first ("This completes the step started by the firing of `T4`. When dispatched, the completion event occurrence generated by `S1.1` triggers `T1.2`"), and six of the ten split the firing around a restored entry, which *History 002-B* forbids — the suite's defect recorded in [`omg-issues.md`](omg-issues.md#pssm-history-001-c-and-002-b-admit-a-completion-inside-the-restore-and-contradict-each-other) | | History 002-B | 11 (the suite's defect; the pool's order, fixed) | `S1(entry)::S2.1(exit)::S2.2(entry)::S1.1(exit)::S1.2(entry)::…` (two traces, one per order of the restore's two completions) | `…::S1(exit)::T3(effect)::S1(entry)::S1.1(exit)::S1.2(entry)::S2.2(entry)::S2.2.1(exit)::T2.2.2(effect)::S2.2.2(entry)::S1(exit)` and 3 more orders of the two regions' entries and exits (two of the six admitted orders are reached, the one the PSSM text prints and the one that dispatches region 2's restored completion first after the restore, `S2.2(entry)::S2.2.1(exit)::T2.2.2(effect)::S2.2.2(entry)::S1.1(exit)::S1.2(entry)`, which the specification's text gives). The two reached and not admitted dispatch `S2.1`'s completion before `S1.1`'s after the first entry of `S1`, the order §8.5.9's pool gives when region 2 is entered first and the one *History 001-C* admits for the identical half. Three of the missing dispatch `S2.2.1`'s completion, generated by `T2.2`'s firing in the second step, before `S1.1`'s, generated by the first step's entry, which §8.5.9's pool cannot do in any entry order; one more fires `S1.1(exit)::S1.2(entry)` inside the step that restores region 2, which the test's own note ends first ("At the end of the RTC step … the state machine is in configuration `S1[S1.1, S2.2[S2.2.1]]`. The next step consists in the firing of `T1.2`"). The suite's defect, recorded in [`omg-issues.md`](omg-issues.md#pssm-history-001-c-and-002-b-admit-a-completion-inside-the-restore-and-contradict-each-other) | -| Junction 005 | 11 (an initial transition's effect, a completion effect in v2) | — | `S1(entry)::T2.1(effect)::S2.1(entry)::T1.3(effect)::S1.2(exit)::S1(exit)` and `S1(entry)::T2.1(effect)::T1.3(effect)::S2.1(entry)::S1.2(exit)::S1(exit)` (the third admitted order, `T1.3(effect)` first after `S1(entry)`, is reached: the second region's initial effect `T2.1` and its target's entry are admitted before or around the junction segment's effect, as *Entering 010*'s. `S2.1`'s completion out of `S1`, a real one, is admitted only after `T1.3(effect)` in all three, where the runtime dispatches it. The fold into the target's entry action has no target here: `T2.1` ends at a junction, whose way out a guard decides, so the effect has no one state's entry to join) | Every reason in full — each extra trace, each missing trace, each error — is in the baseline file's `reasons`. @@ -984,8 +1011,11 @@ the runtime; a `fail` cites a tool choice, a translation limit or the suite's de ends at a junction). *Junction 005* shows the class is right — `S2.1`'s real completion is admitted only after the sibling's remaining entry unit — so no runtime rule reaches the three without telling a start state's completion from a real one, which neither v2 nor PSSM does. - Whether the difference takes a *differs because v2 differs* row is the alignment note's open - decision 8; the three stay `fail` citing it. *History 001-C*'s first half wants the **pool's** + Whether the difference takes a *differs because v2 differs* row was the alignment note's open + decision 8; the three stayed `fail` citing it. **Withdrawn**: the premise was the shorthand's. + A transition out of a named entry action carries an effect and is performed within the entry, + so the emitter spells the initial transition that way and the three pass (the movements since + the previous baseline). *History 001-C*'s first half wants the **pool's** **order** to follow the entry draw (§8.5.9: completion events dispatch in the order generated, which the order the regions were entered decides), where the runtime queued them after the move in declaration order (`scheduleTransitionEvents`) — one of the two parts of the finding that @@ -1055,16 +1085,16 @@ detail. By root cause: | A transition into an active ancestor re-entered it | runtime defect, SM35 (fixed) | Transition 011 C | `pass` | | Several completion transitions out of one state were not one choice | runtime defect, SM19 (fixed) | Event 015 | `pass` | | A guard whose behavior acts on the model | translation defect, the classifier (a construct with no translation) | Choice 005 | `not-expressible` | -| A junction or join with no way through | formerly missing alignment text; SM32 is now decided and implemented (`agrees`) | Junction 004, Join003 | Join003 `pass`; Junction 004 remains `fail` on the translated helper-state trace mismatch while citing SM32 as `agrees` | +| A junction or join with no way through | formerly missing alignment text; SM32 is now decided and implemented (`agrees`) | Junction 004, Join003 | Join003 and Junction 004 `pass`, Junction 004 once the initial route is written out of the entry action | | When the join owner is left | SM34 remains *differs, v2 silent*: PSSM leaves it before the final segment effect, the runtime after | Join001; Transition 019 (its remaining ordering mismatch is not SM34) | Join001 remains `fail`, citing SM34; Transition 019 remains `fail` on silent target-entry/effect ordering without an SM34 citation | | Region entry, exit and firing-unit order is not a recorded choice | runtime gap, finding 9 (fixed at these sites) | Exiting 001, Exiting 003 | `pass` | | A do step against the dispatch at the head of the pool is not a recorded choice | runtime gap, finding 9 (fixed at this site, at do-action granularity) | Behavior 003 A | `pass` | | A do activity's first segment registered as always before the next dispatch | suite defect (the suite admits both orders elsewhere) | Exiting 002 | `fail`, citing the defect | -| An initial transition's effect is a completion effect in v2 | language difference, finding 11 (adjudicated; the row is open decision 8 of the alignment note) | Entering 010, Entering 011 | `fail`, citing finding 11 | +| An initial transition's effect is a completion effect in v2 | translation limitation, finding 11 (withdrawn: a transition out of a named entry action carries the effect within the entry) | Entering 010, Entering 011 | `pass` | | The pool's order does not follow the entry draw | runtime gap, finding 11 (fixed: completions queued as their sources are entered) | History 001-C (one trace, reached), Transition 017 (three, reached) | `fail`, citing the suite's defects for the rest | | A completion dispatched inside the step that restores the sibling region | suite defect, finding 11 (recorded in `omg-issues.md`) | History 001-C, History 002-B | `fail`, citing finding 11 | | A do step against a sibling's entry unit is not a recorded choice | runtime gap, finding 11 (fixed: a due do step is a unit of its region's queue on the entry front) | Terminate 002 | `pass` | -| A junction segment's effect before its owner's entry | runtime defect, finding 10 (fixed) | Junction 005 | `fail`, citing finding 11 for the initial transition's effect, admitted before or around the segment's effect once the segment's effect follows `S1(entry)` | +| A junction segment's effect before its owner's entry | runtime defect, finding 10 (fixed) | Junction 005 | `pass`, once the segment's effect and the sibling's initial effect are units of their regions' entry queues | *Fork 002* and *Join001*, which finding 6's fix brought out of `not-expressible` after that baseline, are attributed with them: *Fork 002* to finding 9 (region entry order, now `pass`) diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 943b049a15..1d081129dc 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -788,7 +788,7 @@ checked after the result is bound is not a form the runtime offers, and none is | A succession out of a state body's own entry subaction names the state it starts in (`entry; then off;`), which is how a machine designates where it starts | `lower/entry_transition.go` `addEntryTransition`, `UnconditionalStart`; `lower/state_graph.go` collectTransitions SuccessionEdge case + `isEntrySubaction` | `lower/state_notation_test.go:TestToStateGraph_EntrySuccessionNamesInitialState`, `lower/transition_source_test.go:TestToStateGraph_UnguardedEntryTransitionIsInitial`, `state_entry_succession_initial.sysml` conformance, `tests/parser/testdata/parse/behavior_exhibit_state_body.golden` | ✅ Faithful | | A state body's two-ended `first a then b;` is the `SuccessionAsUsage` a -> b that `succession first a then b;` spells with its keyword (SysML.xtext `SuccessionAsUsage` under `StateBodyItem`), so it lowers to the same completion (trigger-less) transition, resolving nested, qualified, chained (`c.c1`), region-local and pseudostate endpoints as a `succession` does, and designates no initial state; a machine whose only edges are such successions and no entry marker has no initial state, reported as an exhibited machine with none is. A succession end written as a feature chain names the nested vertex the qualified spelling names — `c.c1` and `c::c1` are one endpoint, as source or target, in either spelling, and the chain's first segment reaches a vertex nested anywhere in the machine (`c1.deep` for `c::c1::deep`) as a qualified end's does — and one whose member, or whose operand, is not a vertex is reported as a qualified end naming none is | `parser/behavior.go` (state-body `first` dispatch: a guarded `first a if g then b;` is a transition, a two-ended `first a then b;` a `SuccessionAsUsage`, and only a one-ended `first a;` an `InitialNode`); `parser/parser.go` `bodyContext.carriesActions` (a state body carries vertices, not a token flow); `parser/succession.go` `atTwoEndedFirst`, `atChainedFirstSuccession`; `resolve/references.go` `connectorEnd` (state-machine succession ends are endpoints, a chained end its operand then its member); `resolve/transition.go` `ResolveEndpointRef`, `resolveEndpointChain`, `lookupEndpointChain`, `VertexInScope` (over `endpointParts`); `lower/endpoints.go` `EndpointRef`, `EndpointResolver.Endpoint` (a name or a feature chain); `lower/state_graph.go` `collectUsageTransitions` → `addCompletion`, `vertexFor` (over `endpointPrefix`); `passes/state_transition.go` `checkEndpoint`, `endpointName` | `parse/state_body_first_succession.golden` (state definition, state usage, nested state, exhibited state, qualified ends, inherited `start`, guarded `first … if … then`, an action body's `first` kept as an initial node), `lower/state_graph_nested_test.go:TestKeywordlessSuccessionLowersLikeTheSuccessionKeyword`, `lower/state_notation_test.go:TestToStateGraph_InitialDesignationIsRecordedOnTheGraph`, `passes/state_transition_test.go:TestStateBodyFirstIsASuccession`, `passes/succession_endpoint_test.go:TestEndpointNamingNoMemberIsReported` (an unresolved end of either spelling), `:TestStateSuccessionEndpointSpellingsAcceptVertices`, `:TestStateSuccessionChainedEndpointsAcceptNestedVertices`, `:TestResolvedStateEndpointNotVertexIsReported` (`outer.mode`), `lower/state_graph_nested_test.go:TestSuccessionChainedEndpointsNameNestedVertices`, `resolve/references_test.go`, `export/behavior_test.go` (a `sysml:SuccessionAsUsage`, no `sysx:InitialNode`), conformance `state_first_succession_chain.sysml` (`entry; then a;` with `first a then b; first b then c; first c then done;` completes with the log `"a b c "`), `state_first_succession_without_entry.sysml` (`first b then c;` alone: no initial state), `state_first_succession_chained_endpoint.sysml` (`b.b1`, `b::b2`, `c1.deep`, `c.c1.deep` as source and target of both spellings), `robustness_test.go:object_exhibited_machine_whose_only_edge_is_a_first_succession` | ✅ Faithful (previously the two-ended form parsed as an `InitialNode` with a successor and lowered as an entry transition into `b`, so the machine started in `b` without an entry marker and, beside `entry; then a;`, never left `a`; the pinned pilot accepts the keyword-less spelling without diagnostics) | | A one-ended `first a;` in a state body orders nothing: a state body has no token flow for an initial node to start | `passes/state_transition.go` `CodeFirstNamesNoTarget` (constraint tier, an error in every mode), beside the notation tier's `nonstandard-notation` warning that the production exists in an action body alone; `lower/transition_source.go` `IsStateSource` (an `InitialNode` is not a state source) | `passes/state_transition_test.go:TestOneEndedFirstInAStateBodyIsReported`, `:TestTransitionToFirstMarkerIsIllegal`, `passes/nonstandard_notation_test.go:TestOneEndedFirstOutsideAnActionBodyIsAnExtension`, `robustness_test.go:state_transition_endpoint_naming_a_first_marker` | ✅ Faithful (reported, never a silent no-op: the lowering has no vertex for it and a transition naming it as an endpoint is refused) | -| Guarded entry transitions — SysML v2 §7.18.3 `EntryTransitionMember` (`entry; if cold then heating; if not cold then idle;`, `entry assign x := …; if c then s;`, `entry action boot { } if c then s;`, `transition boot if c then s;`): the transitions out of a body's entry action choose the state the body starts in. They are tried in declaration order each time the body is entered — at machine start and whenever a transition enters the composite state, orthogonal region or exhibited state whose body they belong to — after the entry action itself has run, and the first whose guard holds is entered; an unguarded `then s;` among them is taken when reached; when alternatives are written and none holds the machine has nowhere to start. A typed or specializing state that writes entry transitions of its own starts by them alone, the inherited ones being replaced as its own entry behavior replaces the inherited one; one writing none keeps the inherited start. An entry transition carries a guard at most: a trigger, an effect, or a target that is not a state is ill-formed | `lower/entry_transition.go` `EntryTransition`, `StateGraph.EntryTransitions` (keyed by the body's owner, kept in declaration order), `withOwnEntryTransitions` (a body's own alternatives replace the inherited ones, from `lower/state_graph.go` `collectGroupTransitions`), `StateGraph.StartOf`, `lowerEntryTransition` (typed `EntryTransitionShapeError` for a trigger or effect, `EntryTransitionTargetError` for a non-state target); `lower/state_graph.go` `machineState` (the machine's own entry behavior runs before its alternatives are tried); `runtime/state_executor.go` `startIn`, `entryGuardHolds`, `enterStartOf` (from `initialize`, `transitionToInto`, `enterRegionsInto`, which enters a region of a parallel state through the substate standing for it, so its entry behavior has run and its guards read that substate's own attributes; the state it descends to is the one the active configuration records for its region, the one events are scheduled from, and the one checked for completion, so an alternative into `done` completes the machine as it starts), `completeIfDone` (judges a composite state complete once its every region started in `done`), `runtime/state_region_transition.go` `moveBetweenRegions`, `enterOutside`; `runtime/errors.go` `ErrNoEntryTransitionHolds`; `passes/state_transition.go` `checkEntryTransition` (`CodeEntryTransitionShape`, `CodeEntryTransitionTarget`); `view/behavior.go` `stateMachineNode` (the state rendering draws each body's entry transitions as edges out of its `start`, in declaration order and carrying the guard as transition edges do, and marks only `StateGraph.UnconditionalStart` `initial`), `view/mermaid.go` `writeStateNode` (`[*] --> s : [guard]` inside the body) | `lower/transition_source_test.go:TestToStateGraph_GuardedEntryTransitionsKeepDeclarationOrder`, `:TestToStateGraph_EntryTransitionShape` (trigger, effect, trigger after an unguarded start, pseudostate target), `passes/state_transition_test.go:TestGuardedEntryTransitionIsLegal`, `:TestEntryTransitionShapeIsReported`, `:TestTransitionOutOfEntryActionIsLegal`, `:TestTriggeredTransitionOutOfEntryActionIsNotAVertex`, `:TestEntryActionTransitionIntoPseudostateIsNotAVertex`, `view/render_test.go:TestStateRenderingDrawsGuardedEntryTransitions` (+ goldens `state-entry.text.golden`, `state-entry.mermaid.golden`: machine, composite-state and orthogonal-region alternatives), conformance `state_entry_transition_guard_first.sysml`, `state_entry_transition_guard_second.sysml`, `state_entry_transition_default.sysml` (unguarded alternative), `state_entry_action_transition_guarded.sysml` (named entry action, `transition boot if c then s;`), `state_entry_transition_nested_regions.sysml` (+ trace golden: machine, composite-state and orthogonal-region alternatives, the machine's `entry assign` read by its guards), `state_entry_transition_reentry.sysml` (+ trace golden: a composite state's alternatives re-tried on each entry, `state_usages_independent.sysml` starting each typed usage by its inherited entry transition), `state_entry_transition_region_composite.sysml` (+ trace golden: a region's transition into a composite state whose alternative chooses a nested state, which then answers the next signal), `state_entry_transition_done.sysml` (an alternative into `done` completes the machine as it starts, after its exit behavior), `state_entry_transition_nested_done.sysml` (a transition into a parallel state whose every region starts in `done` completes the machine), goldens `state_entry_transition_guarded.sysml` (guarded and unguarded alternatives after `entry;`, an entry assignment and a named entry action, in a composite state, an orthogonal region and an exhibited state; accepted clean by the pinned pilot), `state_target_transition_placements.sysml` (`entry; then s;` at each depth), `robustness_test.go:no_entry_transition_guard_holds`, `:entry_transition_target_is_not_a_state`, `:entry_transition_carries_a_trigger`, `:entry_transition_into_done_completes_at_initialize`, `:named_entry_action_transition_into_done_completes_at_initialize` (`transition begin then done;` and `succession first begin then done;` out of a named entry action complete the same way, a declared state `done` being entered instead), `:own_entry_transitions_replace_inherited_ones` (a specializing machine, a typed usage, a guarded typed usage and a typed orthogonal region start where their own alternatives say; a usage redeclaring only the entry behavior keeps the inherited start), `:region_entry_transitions_into_done_complete_at_initialize`, `:nested_regions_into_done_complete_at_initialize`, `:transition_into_nested_regions_in_done_completes`, `:region_start_descends_through_entry_transitions`, `:region_entry_guards_read_the_region_state_attributes`, `:leaving_regions_descends_through_entry_transitions` | ✅ Faithful (every accepted shape, the trigger and effect rejections and the attribute-target rejection were refereed against the pinned pilot both ways, see `pilot-differential.md`; a pseudostate target cannot be refereed, the pilot having no `choice`/`junction` grammar, and an action-usage target the pilot accepts is reported here by the endpoint rule every transition is held to) | +| Guarded entry transitions — SysML v2 §7.18.3 `EntryTransitionMember` (`entry; if cold then heating; if not cold then idle;`, `entry assign x := …; if c then s;`, `entry action boot { } if c then s;`, `transition boot if c then s;`): the transitions out of a body's entry action choose the state the body starts in. They are tried in declaration order each time the body is entered — at machine start and whenever a transition enters the composite state, orthogonal region or exhibited state whose body they belong to — after the entry action itself has run, and the first whose guard holds is entered; an unguarded `then s;` among them is taken when reached; when alternatives are written and none holds the machine has nowhere to start. A typed or specializing state that writes entry transitions of its own starts by them alone, the inherited ones being replaced as its own entry behavior replaces the inherited one; one writing none keeps the inherited start. The shorthand carries a guard at most (`GuardedTargetSuccession`); a transition out of a named entry action, `entry action boot; transition boot do { … } then s;`, is a `TransitionUsage` whose source is an action, a `NonStateTransitionPerformance` (`TransitionPerformances.kerml`, `Actions.sysml` `DecisionTransitionAction`), so it may carry an effect, run after the entry action and before its target's entry as part of entering the body, and may target a junction or choice of the same body, whose route is resolved after the entry action; in a region of a parallel state the effect is a unit of that region's entry queue, interleaving with the sibling regions' ([the derivation](behavior-semantic-oracle.md#effects-on-the-way-into-the-regions-of-a-parallel-state-each-precedes-its-own-targets-entry-the-regions-interleave)). A trigger needs a state source (the pilot's `validateTransitionUsageTriggerActions`), and a shorthand effect, a fork or join target, or a pseudostate of another body are ill-formed. A transition whose entry would start a body through a route with no way through is not enabled (SM32) | `lower/entry_transition.go` `EntryTransition`, `StateGraph.EntryTransitions` (keyed by the body's owner, kept in declaration order), `withOwnEntryTransitions` (a body's own alternatives replace the inherited ones, from `lower/state_graph.go` `collectGroupTransitions`), `StateGraph.StartOf`, `lowerEntryTransition`, `addEntryTransitionTarget` (`EntryTransition.Effect`, `.Via`; typed `EntryTransitionShapeError` for a trigger or shorthand effect, `EntryTransitionTargetError` for any other target), `UnconditionalStart`; `lower/state_graph.go` `machineState` (the machine's own entry behavior runs before its alternatives are tried); `runtime/state_executor.go` `startIn`, `runEntryEffect`, `followEntryRoute`, `entryGuardHolds`, `enterStartOf`; `runtime/state_unit_front.go` `entryTransitionEffectHead`, `runtime/state_region_entry.go` `startHead`, `enterRegion`; `runtime/state_route.go` `defaultEntryRoutesAvailable` (from `initialize`, `transitionToInto`, `enterRegionsInto`, which enters a region of a parallel state through the substate standing for it, so its entry behavior has run and its guards read that substate's own attributes; the state it descends to is the one the active configuration records for its region, the one events are scheduled from, and the one checked for completion, so an alternative into `done` completes the machine as it starts), `completeIfDone` (judges a composite state complete once its every region started in `done`), `runtime/state_region_transition.go` `moveBetweenRegions`, `enterOutside`; `runtime/errors.go` `ErrNoEntryTransitionHolds`; `passes/state_transition.go` `checkEntryTransition` (`CodeEntryTransitionShape`, `CodeEntryTransitionTarget`); `view/behavior.go` `stateMachineNode` (the state rendering draws each body's entry transitions as edges out of its `start`, in declaration order and carrying the guard as transition edges do, and marks only `StateGraph.UnconditionalStart` `initial`), `view/mermaid.go` `writeStateNode` (`[*] --> s : [guard]` inside the body) | `lower/transition_source_test.go:TestToStateGraph_GuardedEntryTransitionsKeepDeclarationOrder`, `:TestToStateGraph_EntryTransitionShape` (trigger, effect, trigger after an unguarded start, pseudostate target), `:TestToStateGraph_EntryTransitionEffectAndRoute`, `:TestToStateGraph_EntryTransitionCannotTargetAnotherBodiesRoute`, `passes/state_transition_test.go:TestGuardedEntryTransitionIsLegal`, `:TestEntryTransitionShapeIsReported`, `:TestTransitionOutOfEntryActionIsLegal`, `:TestTriggeredTransitionOutOfEntryActionIsRejected`, `:TestEntryActionTransitionIntoJunctionIsClean`, `:TestEntryActionTransitionIntoChoiceIsClean`, `:TestEntryActionTransitionIntoJunctionInAnotherBodyIsReported`, conformance `state_entry_transition_effect.sysml`, `state_entry_transition_effect_regions.sysml` (explored: three orders), `state_entry_transition_junction.sysml`, `state_entry_transition_choice.sysml`, `state_entry_transition_guarded_effect_not_taken.sysml`, `state_entry_transition_explicit_inner.sysml`, `state_entry_transition_history_restore.sysml`, `state_entry_transition_junction_no_way_disables.sysml` (each + trace golden), golden `state_entry_transition_effect.sysml`, `robustness_entry_transition_effect_test.go:TestRuntimeRobustnessEntryTransitionEffect`, `view/render_test.go:TestStateRenderingDrawsGuardedEntryTransitions` (+ goldens `state-entry.text.golden`, `state-entry.mermaid.golden`: machine, composite-state and orthogonal-region alternatives), conformance `state_entry_transition_guard_first.sysml`, `state_entry_transition_guard_second.sysml`, `state_entry_transition_default.sysml` (unguarded alternative), `state_entry_action_transition_guarded.sysml` (named entry action, `transition boot if c then s;`), `state_entry_transition_nested_regions.sysml` (+ trace golden: machine, composite-state and orthogonal-region alternatives, the machine's `entry assign` read by its guards), `state_entry_transition_reentry.sysml` (+ trace golden: a composite state's alternatives re-tried on each entry, `state_usages_independent.sysml` starting each typed usage by its inherited entry transition), `state_entry_transition_region_composite.sysml` (+ trace golden: a region's transition into a composite state whose alternative chooses a nested state, which then answers the next signal), `state_entry_transition_done.sysml` (an alternative into `done` completes the machine as it starts, after its exit behavior), `state_entry_transition_nested_done.sysml` (a transition into a parallel state whose every region starts in `done` completes the machine), goldens `state_entry_transition_guarded.sysml` (guarded and unguarded alternatives after `entry;`, an entry assignment and a named entry action, in a composite state, an orthogonal region and an exhibited state; accepted clean by the pinned pilot), `state_target_transition_placements.sysml` (`entry; then s;` at each depth), `robustness_test.go:no_entry_transition_guard_holds`, `:entry_transition_target_is_not_a_state`, `:entry_transition_carries_a_trigger`, `:entry_transition_into_done_completes_at_initialize`, `:named_entry_action_transition_into_done_completes_at_initialize` (`transition begin then done;` and `succession first begin then done;` out of a named entry action complete the same way, a declared state `done` being entered instead), `:own_entry_transitions_replace_inherited_ones` (a specializing machine, a typed usage, a guarded typed usage and a typed orthogonal region start where their own alternatives say; a usage redeclaring only the entry behavior keeps the inherited start), `:region_entry_transitions_into_done_complete_at_initialize`, `:nested_regions_into_done_complete_at_initialize`, `:transition_into_nested_regions_in_done_completes`, `:region_start_descends_through_entry_transitions`, `:region_entry_guards_read_the_region_state_attributes`, `:leaving_regions_descends_through_entry_transitions` | ✅ Faithful (every accepted shape, the trigger and shorthand-effect rejections and the attribute-target rejection were refereed against the pinned pilot both ways, see `pilot-differential.md`, and the pilot accepts a named entry action's transition with an effect; a pseudostate target cannot be refereed, the pilot having no `choice`/`junction` grammar, and an action-usage target the pilot accepts is reported here by the endpoint rule every transition is held to) | | A transition out of a state body's own entry action names the state it starts in (`entry action initial { } transition initial then off;`), the entry action standing in for a start pseudostate (SysML v2 §7.19.3) | `ast/state_entry.go` `EntryActions`/`StateEntryActions`/`IsEntryAction`; `resolve/transition.go` `startAction`; `passes/state_transition.go` `machine.startActions`; `lower/state_graph.go` `startsAt` | `resolve/transition_test.go`, `passes/state_transition_test.go:TestTransitionOutOfEntryActionIsLegal`, `lower/state_notation_test.go`, `state_entry_action_transition_initial.sysml` conformance | ✅ Faithful (an ordinary action named as an endpoint is still reported) | | Termination when a transition reaches `done` | `state_executor.go` completeIfDone (see the completion rule below) | `state_simple.sysml` | ✅ Faithful | | State entry actions | `state_executor.go:749` enterState | `state_do_behavior.sysml` | ✅ Faithful | @@ -840,7 +840,7 @@ checked after the result is bound is not a form the runtime offers, and none is | CallEvent triggers (`accept op(param)` notation, operation and argument matching, arguments bound for guard/effect) | `parser/behavior.go` parseTriggerEvent/parseCallEvent; `symbols/bodyscopes.go` triggerParameterDefiner (parameters are members of the transition, reachable from its own guard/effect); `state_executor.go` matchesEvent EventCall case, bindTriggerArguments, InvokeOperation; `perform.go` `callPayload` (a queued call carries the declaration its arguments select among the owner's same-named operations, `Call.Declared`), `callTriggerOperations` (a trigger names the declarations with an input for each of its parameters, those with exactly its parameters when any has — all of several differing in their parameters' types alone, since the notation writes no types — so a call of a declared operation fires only the triggers naming its declaration, as a UML `CallEvent` names one operation) | `tests/parser/testdata/parse/state_call_trigger.golden`, `lower/trigger_test.go:TestTriggerClassification_CallTrigger`, `model/behavior_body_resolve_test.go` call-trigger parameter cases, `state_call_trigger{,_guard,_nested,_regions}.sysml` conformance, `signal_test.go:TestCallEventMatchesOperationName`, `:TestRejectedCallLeavesNoArgumentsBehind`, `robustness_test.go:call_of_unhandled_operation`, `:call_argument_of_wrong_type`, `robustness_call_results_test.go:TestRuntimeRobustnessCallResults/overload_fires_the_trigger_naming_its_declaration` | ✅ Faithful (a call trigger on an enclosing composite state sees the invocation while a substate is active) | | A synchronous call of an operation a call trigger accepts returns to the caller once the run-to-completion step the call event triggers is done, with the values the behaviors that step fires — the transition's effect, an entry or an exit — returned or assigned to the operation's `out`/result parameters, by name, the last write winning — the parameters the operation declares as a member of the machine's owner (or of the machine itself when it stands alone) when it declares one, among several so named the one the call's arguments select as a call in the model would (`ErrAmbiguousInvocation` before the call is queued when they select none), the arguments checked against that declaration's inputs as an invocation's are (`ErrUnboundParameter` before the call is queued for an unbound or unknown one, `ErrTypeMismatch` for one of the wrong type, an omitted input carrying its default), the call event carrying that declaration so it fires only the triggers naming it — an `inout` the step writes nothing to going back as the caller passed it, since its parameter value is the argument until a behavior writes it (PSSM §8.5.9 `CallEventExecution`) — every output the step returned when the trigger names no declared operation; a call a state defers holds its caller through the machine's later steps until it is recalled and dispatched; a call the run leaves queued or deferred has not returned, and one no transition accepts is discarded and returns nothing (PSSM §8.5.9 `CallEventOccurrence`; the caller is released only after the step) | `runtime/perform.go` `StateExecutor.Call` (queues the call event with `InvokeOperation`, runs the machine at the current instant until that event has been dispatched — `callReleased` stops the run loop after the unit dispatching it, so events the step queued and timers it armed stay for the machine's later runs, while a deferred call keeps the run going through the steps until it is recalled — and reports a held call as `ErrCallNotReturned` through `eventDisposition`), `pendingCall` (captured by `snapshot.go` `capture` and `held_image_behavior.go` `imagedState`, so an undone step or a materialized image restores the call as it stood), `callPayload` (the declaration through `invoke_operation.go` `memberCalled`, the selection `InvokeOperation` makes, its inputs through `operationInputs`, the check `InvokeOperation` makes, and each input's value or default checked against its parameter as an assignment is, `callInputs`), `newPendingCall`, `callTaken` and `recordCallOutput` (outputs kept only from a behavior the pending call's own event fires, not from nested behavior another occurrence runs, and only under the names the declared operation returns, so a helper's other `inout`/`out` stays the object's own; a declared `inout` argument fills in under a transition that fired on the call and no behavior wrote to, so a discarded call still returns nothing); `action_frame.go` `performanceOwner.returnAround` and `assignEnclosingBy` route a nested action's `return` or output assignment to the enclosing behavior's parameter of that name (`action_executor.go`, `calc_statements.go`, `state_statements.go` hosts) | `conformance/state_call_trigger_results.sysml` (`.expected.json`, trace golden: `compute` doubled by the effect, negated by the entry), `robustness_call_results_test.go:TestRuntimeRobustnessCallResults` (held, recalled, untaken, empty, repeated and erroring calls; the caller released before the completion step its call queued and before a timer it armed, a signal queued ahead dispatched first, a declared operation returning its own parameters alone, an `inout` argument returned as passed, as written and not at all when nothing takes the call; an overloaded operation returning the outputs of the declaration the arguments select, firing the trigger naming that declaration, and refused as ambiguous when they select none; a call leaving a declared input unbound or naming none, or carrying a wrong-typed one, refused before it is queued; an omitted input carrying its default; a calc and a constraint returning their result alone; a rolled-back step restoring the call), `call_capture_test.go:TestStateCaptureTakesThePendingCall`, `:TestHeldImageCarriesThePendingCall` | ✅ Faithful | | Sourceless transitions (`accept … then`, `if … then`, `then`, `transition if … then`, `transition then`) — SysML v2 §7.18.3 `TargetTransitionUsage`: a transition usage written without a source part, whose source "is taken to be the closest lexically previous state usage" in the body that declares it, so it is a member of the body that declares the state it leaves, written after that state, at any depth (a state def body, an exhibited or performed state usage body, a composite state's body, an orthogonal region's body); the pilot's `UsageUtil.getPreviousFeature` derives it the same way, looking back over the other transitions chained off that state. A pseudostate declared before the shorthand is not that state usage: a `choice`, `junction`, `join` or `fork` is left by `transition first … then …;` only | `ast/transition_source.go` `ImplicitTransitionSource` (the previous-member rule over the complete ordered body, looking past the sourceless transitions chained off the same state and the succession `then state s;` lists after `s`); `lower/transition_source.go` `ImplicitSource`, `IsEntryTransition`, `IsStateSource` (a `PseudostateNode`, `InitialNode` or `FinalNode` is not a state source), the typed `ErrNoTransitionSource` and `TransitionSourceError` (`TransitionSourceNotVertexFormat`, `TransitionSourceRegionFormat`, `TransitionSourcePseudostateFormat`, `TransitionSourceMarkerFormat`); `lower/state_graph.go` `lowerTransitionMember` lowers the shorthand from the vertex the rule names, over the inherited and own members `lower/state_inheritance.go` materialises with their owner and scope; `passes/state_transition.go` `(*transitionChecker).checkImplicitSource` reports the same rule at the constraint tier (`CodeNoTransitionSource`, `CodeTransitionSourceNotVertex`) | `parser/behavior_test.go` `TestParseStateBody_SourcelessTransitionForms`, goldens `state_target_transition_guard.sysml` and `state_target_transition_placements.sysml` (top-level, composite, orthogonal-region placements with trigger, guard, effect and dotted targets, each `source=""`; both accepted clean by the pinned pilot), `lower/transition_source_test.go` (`TestToStateGraph_SourcelessTransitionLeavesThePrecedingState`, `:…InheritedSourcelessTransitionLeavesEachMaterialization`, `:…SourcelessTransitionWithNothingBefore`, `:…SourcelessTransitionAfterANonVertex` — start marker, explicit transition, succession usage, triggered and guarded shorthand after a `choice`, triggered shorthand after a `join`, `:…SourcelessTransitionAfterARegion`), `passes/state_transition_test.go:TestSourcelessAcceptTransitionIsLegal`, `:TestSourcelessTransitionChainAndSuccessionAreLegal`, `:TestSourcelessTransitionWithNothingBeforeIsReported`, `:TestSourcelessTransitionAfterANonVertexIsReported` (a pseudostate before the shorthand among them, and the explicit `transition first pick …` form it names staying legal), `:TestSourcelessTransitionAfterARegionIsReported`, conformance `accept_then_transition.sysml`, `state_target_transition_top_level_timed.sysml` (+ trace golden), `state_target_transition_nested_timed.sysml` (+ trace golden: one firing, one entry action, no self-loop), `state_target_transition_guard.sysml`, `state_target_transition_after_do_action.sysml`, `robustness_test.go:sourceless_transition_with_nothing_before`, `:sourceless_transition_after_a_non_state` (a `do` action, an attribute, a `choice` pseudostate) | ✅ Faithful (the earlier reading — the shorthand written *inside* the state it leaves, with that containing state as its source, and refused at the machine's top level — was wrong: the pinned pilot rejects the nested placement with parse errors (`no viable alternative at input 'accept'`), and accepts the flat placement this implementation now lowers, so `accept_then_transition.sysml` was rewritten into the flat form. A shorthand written first in its body, or after a member that is not a state of this machine — a `do` action, an attribute, an `in` parameter, a written succession, documentation, a pseudostate, a region of a parallel state — is reported by the constraint tier with the member named, and the lowering keeps the same typed errors as a backstop; the pilot rejects each of those placements it can parse too, by its grammar or by `A transition with an accepter must have a state as its source`, and has no grammar for `choice`/`junction` to referee the pseudostate placement against) | -| ChangeEvent triggers (when expr) | `state_executor.go` matchesEvent, RunToCompletion (polls after each micro-step and again at quiescence); `state_change_trigger.go` pollChangeEvents, SuspendReason | `state_executor_test.go:TestStateChangeEvent`, `state_change_trigger_test.go:TestChangeTriggerRunsWithoutAnExternalPoll`, `:TestChangeTriggerFiresOnRiseFromDoBehavior`, `:TestChangeTriggerDoesNotRefireUnchangedCondition`, `:TestChangeTriggerFalseConditionIsReported`, `conformance/state_change_trigger_autonomous.sysml`, `:state_change_trigger_rising_edge.sysml`, `:state_change_trigger_event_order.sysml` + trace golden | ⚠️ Approximate (driven by the run itself and fired on the condition rising; KerML has no clock, so re-testing once per micro-step is a tool-defined cadence — see the known limitation) | +| ChangeEvent triggers (when expr) — `Triggers.kerml` `TriggerWhen` returns a `ChangeSignal`, "a signal to be sent when the Boolean result of its changeCondition Expression changes from false to true" (`Observation.kerml`), and `ObserveChange` waits while the condition is false and sends the signal once it is true, then waits again. The condition's result can change only when a feature it reads is written, and a write is seen only once complete: a `FeatureWritePerformance` assigns its replacement values "at time its performance ends", and a `FeatureMonitorPerformance` compares a before time slice with an after snapshot that must differ (`FeatureReferencingPerformances.kerml`). So the conditions of the active configuration's transitions are re-evaluated after every completed outermost write that changes a feature they read, and each false-to-true rise queues one change signal, consumed by the next dispatch; a rise followed by a fall within one run-to-completion step still fires, while a value one assignment writes and replaces before it completes is never observed. KerML has no clock, so the library's own granularity is the completed write. A machine that cannot progress reports which condition it waits on | `feature_write_watch.go` `beginFeatureWrite`/`endFeatureWrite` (nested writes coalesced into the outermost one, compared before/after), `noteStateDataWrite`, `beginChangeRead`; `instance.go` `storeFeatureValue`; `binding.go`, `classifier_behavior.go` (bound and occurrence writes inside the same bracket); `dependents.go` `noteRead` (the condition's read set); `state_change_trigger.go` `changeConditionHolds`, `observeFeatureWrite`, `observeStateDataWrite`, `observeChangedValue`, `pollChangeEvents`, `SuspendReason`; `state_executor.go` `matchesEvent`, `RunToCompletion`; `snapshot.go`, `held_image_behavior.go`, `check_state.go` (observed, pending and read-set state carried by snapshots, held images and check-state keys) | `state_executor_test.go:TestStateChangeEvent`, `state_change_trigger_test.go:TestChangeTriggerRunsWithoutAnExternalPoll`, `:TestChangeTriggerFiresOnRiseFromDoBehavior`, `:TestChangeTriggerDoesNotRefireUnchangedCondition`, `:TestChangeTriggerFalseConditionIsReported`, `conformance/state_change_trigger_autonomous.sysml`, `:state_change_trigger_rising_edge.sysml`, `:state_change_trigger_event_order.sysml` + trace golden, `:TestChangeTriggerKeepsOutsideWriteRiseUntilPoll` (a rise and fall between polls fires), `:TestChangeTriggerIgnoresRiseInsideOneWrite` (a rise and fall inside one outermost write does not), conformance `state_change_trigger_transient_rise.sysml` (+ trace golden: a condition true and false again inside one step fires), `state_change_trigger_atomic_write.sysml` (+ trace golden: a write whose bound feature follows it raises no rise), golden `state_change_trigger_transient_rise.sysml`, `robustness_change_trigger_writes_test.go:TestRuntimeRobustnessChangeTriggerWrites` | ✅ Faithful | | TimeEvent triggers (`accept after ` relative, `accept at