Skip to content

fix(runtime): = values in action, calc, block and state bodies hold at all times - #842

Merged
HuiJun merged 14 commits into
developfrom
fix/body-feature-value-bindings
Oct 8, 2026
Merged

HuiJun merged 14 commits into
developfrom
fix/body-feature-value-bindings

Conversation

@devin-ai-integration

@devin-ai-integration devin-ai-integration Bot commented Oct 3, 2026 •

Copy link
Copy Markdown
Contributor

What and why

A feature written with = inside an action, calculation, statement block or state machine was evaluated once, when the body started. The same declaration on a part already tracked what it read. For example:

action act {
    attribute a : Integer := 0;
    attribute s : Integer = a * 2;
    out attribute r : Integer;
    first start;
    then action w { assign a := 5; }
    then action k { assign r := s; }
    then done;
}

sysml -action U::act reported a = 5, s = 0, r = 0. It now reports s = 10, r = 10. State-machine data had the same problem: after assign a := 5 in a transition effect, s stayed 0, so accept when s > 3 never fired.

Body and state value stores are now backed by dependency cells that reuse the existing object-level mechanism in dependents.go; there is no separate recomputation path:

  • Lowering: lower.Declare, lower.Attribute and lower.Feature carry a Binding flag, true for a value written with = and false for := and default. Executors read the flag and never inspect declaration syntax.
  • Shared derivation loop: deriveFeatureValue's stale-retry loop is factored into deriveWith, which body cells reuse (body_bindings.go deriveBodyCell).
  • Reads: a read goes through noteRead, so a derivation records it.
  • Writes: a write goes through beforeWrite/afterWrite, so whatever read the written feature is unmaterialized and derived again on its next read.
  • What a write does to the cell:
    • An assign to an = cell keeps the assigned value and stops tracking, the same as object-level values.
    • A value supplied by a flow or an argument also counts as a write.
    • Write refusal for derived and constant features is unchanged.
    • A binding that reads itself reports ErrCyclicFeatureValue.
  • Performance end: a cell that is still tracking is derived once more and then frozen. This is tool-defined because the language does not say what later reads of an ended occurrence see. It is documented in spec-compliance.md.
  • State exit and re-entry: leaving a state invalidates whatever read the attributes of the exiting state. Re-entering it restarts its unwritten = attributes so they track again for the new visit; written attributes keep their value.
  • Every way the root ends: completion, completion with no flow, and terminate all go through completeRoot, which freezes the root cells before the performance ends.
  • Result errors: ResultsWithError reports the first binding that fails to derive (for example, one reading a destroyed object while the action waits) and omits that feature. Results keeps its map-only signature. The Context entry points that return action results propagate the error, as StateDataWithError already does for states.
  • Snapshots, held images and explore/check keys: snapshots and held images carry the cells. Explore/check keys spell each cell's value, or unset, together with whether it is tracking, written or frozen. Values that are still tracking restore unmaterialized and are derived again lazily.
  • Occurrence mirroring: a performance's occurrence feature is linked as a dependent of its body cell. Object-level readers therefore see the current derived value instead of the value from when the body started.

Known limitation: a body-local calc usage lowered as DeclareUsage (calc k1 : Rhs { in x = x; } inside a block) still evaluates its = pins once per declaration, so the pins do not follow later writes. This is recorded in the compliance row, pinned by TestRuntimeRobustnessBodyFeatureBindings/calc_usage_remains_one_shot, and named at the execution site.

Changed answers in existing fixtures

Two existing fixtures change answers. Both changes follow from the specification. No other existing fixture, trace golden or corpus expectation changes.

action_step_multiplicity_shared_writers: this fixture declares attribute l : Integer = c in each of a[3], and w does assign c := l + 1.

  • Under =, l is bound to the current c for the whole performance (KerML 1.0 §7.3.4.5, §7.4.9), so every interleaving ends at c = 3.
  • Explore goes from {1,2,3} to {3}, and check goes from divergent to agreed at c = 3.
  • The fixture's comment ("each performance snapshots shared c in its own l") describes an initial value, which is written :=.
  • The new sibling action_step_multiplicity_shared_writers_initial uses l := c and keeps {1,2,3} with a divergent check, so the race coverage is kept.

action_inherited_default_root: Base declares in x : Integer = 3; in z : Integer = x * 2;, and Derived does assign x := 10 and then assign r := z.

  • Nothing supplies z, so its = binds it to x * 2 for the performance, and z follows the assigned x: z = r = 20, previously 6.
  • The comment is rewritten to describe the binding.
  • New sibling action_inherited_default_root_fallback: in z : Integer default x * 2 keeps 6.
  • New fixture action_inherited_supplied_parameter: a supplied argument (Base(x = 3, z = 7)) is a write and stays at 7 after x changes.

To let the shared-writers fixture state its single explored result as outputs beside exploreBudget, the conformance schema now accepts a budget beside a single action or state result. A budget with no result, and an outcomes list holding only one result, are still schema errors.

Specification basis

  • KerML 1.0 §7.3.4.5 (FeatureValue): with isDefault = false, the feature is bound to the expression's result for the life of the featuring occurrence.
  • KerML 1.0 §7.4.9 (binding connectors): both ends of a binding hold equal values.
  • An action or state performance is an Occurrence (Actions::Action :> Performance, States::StateAction), so its body features follow the same rule as object features.
  • KerML 1.0 §7.4.7: a supplied argument redefines a parameter's value.

docs/project/spec-compliance.md:

  • The = row is extended from object-level values to performance, body and state cells, and gains a section covering the end-of-performance freeze, supplied pins and the calc-usage limitation (⚠️ for that limitation).
  • The inherited-parameter row now describes the binding, with the fallback and supplied cases.

How it was verified

  • New conformance fixtures:
    • action body, nested action node, statement blocks (if/while/for), calc body, constraint body;
    • state data with a change guard (a write to a is seen as a change of s), state attributes, entry/do/exit locals;
    • :=, a write to an = feature, read-only features, a flow-supplied pin, occurrence mirroring;
    • the two siblings above and the supplied-parameter case.
  • Trace golden action_body_feature_binding.trace.golden.
  • Parser golden body_feature_bindings.
  • Lowering test TestLoweredBodyFeaturesPreserveValueOperators.
  • TestRuntimeRobustnessBodyFeatureBindings cases: a cycle, a read of a destroyed object, a state exit, a write that stops tracking, read-only features, the step budget during a re-derivation, snapshot/restore mid-performance followed by a write and a read, a held image, replay, and the calc-usage limitation.
  • Passed locally:
    • go build ./..., go vet ./..., gofmt -l . (empty), go test ./...
    • make lint, make docs-check, python3 scripts/changelog.py check
    • go test -race ./internal/exec/runtime/... ./internal/ir/lower/...
    • the training, pilot, PSSM and RDF round-trip corpus gates (training corpus clean, training_examples_expected.txt untouched) and the pilot XMI identity gate

Checklist

  • make test and make lint pass locally
  • Tests added or updated for the change
  • Documentation extended where it already covers the surface (see CONTRIBUTING.md)
  • Changelog entry added as changes/unreleased/<slug>.<section>.md, not as an edit to CHANGELOG.md
  • baselines regenerated and make docs-counts run if a gate count moved (compliance rows need nothing: the census is counted at docs build)
  • No internal work-item labels (waves, slices, F4, K5) in the body, docs, or changelog

devin-ai-integration Bot and others added 2 commits October 3, 2026 02:44
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
@devin-ai-integration

Copy link
Copy Markdown
Contributor Author

I'll fix CI failures and address comments from users with write access. I'll skip comments containing "(aside)".

  • Disable automatic comment, CI, and merge conflict monitoring

@devin-ai-integration
devin-ai-integration Bot marked this pull request as ready for review October 3, 2026 04:15
devin-ai-integration[bot]

This comment was marked as resolved.

devin-ai-integration Bot and others added 3 commits October 3, 2026 05:01
Co-Authored-By: jason.han <hanhuijun@gmail.com>
…alue-bindings

Co-Authored-By: jason.han <hanhuijun@gmail.com>

# Conflicts:
#	internal/ir/lower/action_graph.go
…alue-bindings

Co-Authored-By: jason.han <hanhuijun@gmail.com>

# Conflicts:
#	internal/exec/runtime/held_image_behavior.go
devin-ai-integration[bot]

This comment was marked as resolved.

devin-ai-integration Bot and others added 2 commits October 3, 2026 21:23
Co-Authored-By: jason.han <hanhuijun@gmail.com>
Co-Authored-By: jason.han <hanhuijun@gmail.com>
@devin-ai-integration

Copy link
Copy Markdown
Contributor Author

This branch now conflicts with develop. Conflicting files, and the merged PRs that changed them:

To resolve: merge current develop into this branch with an ordinary merge commit (no rebase or force-push).
Reconcile the code conflicts with #864's statement-order scheduling (calc, constraint and case-step bodies) rather than taking one side; a conflict that needs a design decision should be raised on this PR, not guessed.

Planned merge order for the execution PRs: #844 → #850 → #838 → (#851 → #853 → #857) → #830 → #833 → #842 → #837 → #834 → #816.

Re-run the full gate (go build ./..., go vet ./..., gofmt -l ., make lint, make docs-check, go test ./...) and wait for green CI before marking ready.

@devin-ai-integration

Copy link
Copy Markdown
Contributor Author

Hold on pushes: please don't push to this branch, including develop merges or empty commits to retrigger CI, until a maintainer says the CI runners are free. Prepare the conflict resolution locally and push it then.

…s-develop-merge

Co-Authored-By: jason.han <hanhuijun@gmail.com>

# Conflicts:
#	internal/exec/runtime/frame.go
#	internal/exec/runtime/statements.go
…s-develop-merge

Co-Authored-By: jason.han <hanhuijun@gmail.com>

# Conflicts:
#	internal/exec/runtime/action_executor.go
#	internal/exec/runtime/frame.go
#	internal/exec/runtime/state_executor.go
#	internal/exec/runtime/state_statements.go
devin-ai-integration[bot]

This comment was marked as resolved.

devin-ai-integration Bot and others added 4 commits October 8, 2026 13:48
…llocated

markUnvalued allocated the map on a copy of the frame, so the mark was lost
whenever the frame held no unvalued name yet; calcRun.bindingsFrame then read a
case-local the run left unvalued through to the enclosing binding of the same
name. Mark through a pointer, and drop the pre-allocation the constraint result
no longer needs.

Co-Authored-By: jason.han <hanhuijun@gmail.com>
…n a slow runner

Co-Authored-By: jason.han <hanhuijun@gmail.com>
@devin-ai-integration devin-ai-integration Bot mentioned this pull request Oct 8, 2026
6 tasks done
@HuiJun
HuiJun merged commit 85a001a into develop Oct 8, 2026
24 checks passed
@HuiJun
HuiJun deleted the fix/body-feature-value-bindings branch October 8, 2026 16:44
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant