diff --git a/changes/unreleased/order-marks-chained-places.fixed.md b/changes/unreleased/order-marks-chained-places.fixed.md new file mode 100644 index 0000000000..6cc1d8801e --- /dev/null +++ b/changes/unreleased/order-marks-chained-places.fixed.md @@ -0,0 +1 @@ +- A value reached through a part (`sensor.raw` written by racing branches, `sensor.scaled = raw * 10`, a value read from either after the join) is now reported `order-dependent` where `-schedule explore` proves more than one outcome: the result surface read what a part's object holds under a fresh run, losing the run's marks, and an object's feature valued by an expression recorded nothing of what it read; the place is the part's, so two parts of one definition hold two values of its feature and `left.raw` racing leaves `right.raw` bare. A sibling branch reading a feature its sibling writes in the same step now marks what it writes from the read (`z := x` beside `x := 1`: `z` open), while the feature written once (`x`) stays bare, as does what a branch writes from no such read; a conformance test asserts over every order fixture that the names marked are exactly those exploration varies. diff --git a/cmd/sysml/check_engine_test.go b/cmd/sysml/check_engine_test.go index ac6c3b0a08..595765f386 100644 --- a/cmd/sysml/check_engine_test.go +++ b/cmd/sysml/check_engine_test.go @@ -576,11 +576,11 @@ func TestEngineCheckWitnessOfBehaviorsOnOneClockReplays(t *testing.T) { t.Fatal(err) } if !strings.HasPrefix(string(content), "object #1 = Shine::Lamp#1\nt=3.0: action peek of object #1 first of action peek of object #1, state machine glow of object #1\nt=3.0: "+c.first+" first of action peek of object #1, state machine glow of object #1\n\n") || - !strings.Contains(string(content), "choice at t=3.0: due action peek of object #1, state machine glow of object #1 (unordered; ran "+c.first+" first; order-dependent: lit)") { + !strings.Contains(string(content), "choice at t=3.0: due action peek of object #1, state machine glow of object #1 (unordered; ran "+c.first+" first; order-dependent: saw)") { t.Errorf("witness %d:\n%s", c.n, content) } replayed := check(t, binary, lampModel, "-schedule", "replay:"+name(c.n), "-trace", "-instantiate", "Shine::Lamp", "-action", peek, "-state", glow, "-advance", "3") - wantReport(t, replayed, 0, "ran "+c.first+" first; order-dependent: lit)", "saw = "+c.saw, "Current state: on", + wantReport(t, replayed, 0, "ran "+c.first+" first; order-dependent: saw)", "saw = "+c.saw, "Current state: on", "standing: value (observed: 1 run under replay:"+name(c.n)+")") } } diff --git a/docs/internals/design/scheduling.md b/docs/internals/design/scheduling.md index 39cc406e98..85758da711 100644 --- a/docs/internals/design/scheduling.md +++ b/docs/internals/design/scheduling.md @@ -113,8 +113,19 @@ already uses — `check_reduce.go`, `future_footprint.go`; there is no second co `Footprint.DependentBy` pairwise over the footprints less control convergence (meeting at a join or both completing a performance changes no value). No dependent pair: the alternatives commute, the choice is `Independent`, and the run's values do not depend on it. A dependent pair: the - choice is unresolved, and `Touches` names the features a write of either meets in the other - (`Relation.PlaceMeets`); a pair that meets only on a channel or through a dynamic target + choice is unresolved, and `Touches` names the places whose values the order decides + (`touchMeeting`, `Relation.PlaceMeets`): a place both alternatives write, and, where a write of + one meets a *read* of the other, what the reading alternative writes from that read — the + statements of its body whose flow reads the place (`lower.Footprint.Flows`, one data flow per + statement, `Footprint.WritesReading`), or every write of the alternative when the read is not a + statement's (a guard's) or the move is described whole. The rule throughout: a value is marked + if and only if exploration proves more than one outcome for it. So the place read is not + touched by the meeting — a once-written feature read by a racing sibling holds one value + whichever order ran, and a mark on it would assert an openness exploration refutes — while + what the reader writes from it is (`action_order_sibling_read_of_racing_write`: `z` open, `x` + bare). A pin is + each performance's own, delivered to rather than raced for, and is neither touched nor a read + that touches (`shared`). A pair that meets only on a channel or through a dynamic target (`Footprint.Dynamic`: a property read or a chained target the declarations do not decide) touches every write of both, conservatively. - `classifyExclusive` is for alternatives of which one runs and the others do not — a decision's @@ -172,7 +183,19 @@ tracker and never by re-reading declarations in the runtime: the places behind `Touches`) with itself (`orderMarks.seed`, from `Context.noteFrom`): another order may have written them otherwise. A value reported under a name reads the marks of the places that name denotes as `choiceTouches` resolves them (`placeNamed`: a bare name is the - behavior's own feature, `this.` the performing object's). + behavior's own feature, `this.` the performing object's, `.` a feature of the + object a part of the behavior denotes, which no performer owns). A place is the feature written + whatever path reaches it: `assign sensor.raw := 1` through the part `sensor` writes the place of + `Sensor::raw` (`footprintBuilder.path`), the same place a later `sensor.raw` reads, so a chained + feature stands open where a plain one would (`action_order_chained_write_of_racing_writers`, + `action_order_chained_two_level_write`). The place remembers the feature it was reached + through (`Place.Via`, the part's object `Instance.heldBy` for a write or derivation the run + makes); whether two such places hold one value is the run's to say (`Context.heldAlike`: the + parts denote an object in common), not the declarations' (`Place.Conflicts` stays + conservative for the checker's reduction, as features may alias). So `left.raw` racing + leaves `right.raw`, `right.scaled` and a read of them bare, while `twin = cell` writing + `twin.mark` races `cell.mark` (`action_order_chained_parts_apart`, + `action_order_chained_alias_of_racing_writers`). - **Propagate.** A move with footprint `fp` that writes `w` leaves `w` standing on what `fp` read — the union of the marks of every place in `fp.Reads` — together with the *control* the move runs under; a footprint the declarations do not decide (`fp.Dynamic`: a property read, a chained @@ -182,7 +205,14 @@ tracker and never by re-reading declarations in the runtime: performance's inputs stand on what they are bound from as it begins and its outputs, as it ends, on those and on what its body left on its own pins (`performances.markPerformance` over `BindingFootprints`: features, pin bindings, flows and the accepted payload, less the body's - statements, which are recorded one by one). + statements, which are recorded one by one). A feature valued by an expression is rewritten with + what its expression read as it is derived, the behavior's own (`deriveBodyCell`) and an object's + (`Instance.materializeDerived`: `sensor.scaled = raw * 10` stands where `raw` does) alike + (`Context.deriveMarks` over `lower.ExpressionFootprint`). Reporting reads under the run that + produced the values: `ActionExecutor.ResultsWithError` derives what a part's object holds under + the executor's own run state (`enterRun`), since a derivation begun as a run of its own would + install a fresh state and the marks of the run just ended would be gone before the surface read + them — which is how a value reached through a part was once reported bare. - **Clear.** Since the write *replaces* the marks of `w`, a write that reads nothing order-dependent, under no control, clears `w` from that point on: the mark describes the value. It replaces the marks of the one declaration it writes (`samePlace`): a same-named feature of diff --git a/docs/project/behavior-semantic-oracle.md b/docs/project/behavior-semantic-oracle.md index b9702c23db..b418c83c13 100644 --- a/docs/project/behavior-semantic-oracle.md +++ b/docs/project/behavior-semantic-oracle.md @@ -2451,6 +2451,69 @@ by an expression stands on the places its lowered expression reads, through feat in turn, at the moment it is read, and a write from it stands on those places as a write from them directly would. +### A feature reached through a part stands on the choice points its writers race at + +Fixtures: `action_order_chained_write_of_racing_writers`, `action_order_chained_two_level_write`, +`action_order_chained_read_of_unraced_stays_bare`, `action_order_chained_parts_apart`, +`action_order_chained_alias_of_racing_writers` (golden, explored). + +``` +part def Sensor { attribute raw : Integer = 0; attribute scaled : Integer = raw * 10; } +part sensor : Sensor; +start → split ⇉ a { sensor.raw := 1 } ─┐ + ⇉ b { sensor.raw := 2 } ─┘→ sync → derive { z := sensor.raw; zz := sensor.scaled } → done +``` + +Derived constraints: + +- `sensor.raw` is a feature of the one object the action's part denotes, reached through the + part by a feature chain (KerML 1.1 §7.3.4.6); the two branches write that one place, and + `sensor.scaled` is bound to an expression over it, computed as it is read. +- `sync` follows both writes, so the reads after it see the `raw` that stands after both: + `{raw = 1, scaled = 10, z = 1, zz = 10}` or `{raw = 2, scaled = 20, z = 2, zz = 20}`. A chain two + parts deep (`car.engine.rpm`) names one place the same way. + +Open: the order of the two branches, exactly as for a feature of the action's own. A place is +the feature written whatever path reaches it, so the chained place stands open where a plain +one would, and so does everything read or computed from it. A feature reached through a part +that no racing branch writes (`sensor.raw` written once before the fork while `x` races) is +fixed, and a value read from it after the join is fixed with it. Two parts of one definition +(`left`, `right : Sensor`) hold two values of its feature: `left.raw` racing leaves `right.raw`, +`right.scaled` and a value read from them fixed; a reference part bound to a part (`ref part twin = cell`) +holds the same object, so `twin.mark` written beside `cell.mark` races it. + +Pinned outcome: the admissible set of two members in each fixture, stated as `outcomes` citing +this section. The default run reports `sensor.raw`, `sensor.scaled`, `z` and `zz` up to the same +two choice points (`orderDependent` states each `2`); in the two-level fixture `z` alone, the +chained place itself not being among the results; in the unraced fixture `x` and the read of it +alone, the chained reads bare; in the two-parts fixture `left.raw` and `left.scaled` alone. + +### A read racing a write of the same feature stands on the choice point between them + +Fixture: `action_order_sibling_read_of_racing_write` (golden, explored). + +``` +start → split ⇉ a { x := 1 } ─┐ + ⇉ b { z := x } ─┘→ sync → done +``` + +Derived constraints: + +- Neither branch is ordered before the other (no HappensBefore between them), so `b` reads + `x` either before or after `a` writes it: `{x = 1, z = 0}` or `{x = 1, z = 1}`. +- `x` holds `1` in every linearization: the one write of it is not raced by another write. + +Open: the order of the two branches, as for two writers of one feature, met here by a write +and a read of the same place. The write cannot commute with the read, so the choice point +touches what the reading branch writes from the place: `z` is open with the single choice +point. `x` is not: one write of it stands whichever order ran, so a mark on it would assert an +openness exploration refutes. A write of the reading branch standing on no read the other +writes (`doneA := true` beside `total := total + 1`) is fixed the same way. + +Pinned outcome: the admissible set of two members, stated as `outcomes` citing this section. +The default run reports `z` up to the one choice point and `x` bare (`orderDependent` states +`z: 1`). + ### A guard reading an order-dependent value leaves what its branch writes order-dependent Fixture: `action_order_guard_reads_racing_writer` (golden, explored). diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 78a9c63eee..ac89accd69 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -824,7 +824,7 @@ remain one-shot. | A terminate action usage's body is an ordinary `ActionBody` (SysML.xtext `TerminateActionUsage`), so it states successions as any action body does, and its implicit `TerminateAction::terminateOccurrence` (`Actions.sysml`) is a subaction no succession orders against the body's others: it may end the usage's performance before, between or after them, an output pin left unwritten then binding no value ([derivation](behavior-semantic-oracle.md#a-terminate-action-usages-body-and-its-implicit-terminate-each-is-performed-in-which-order-is-open)) | `lower/action_subflow.go` `lowerTerminateNode` (the body, or the flow it states as a block, then the terminate it stands for); `runtime/action_terminate.go` (a `terminate` naming the usage inside its own body ends the usage's performance) | `action_terminate_usage_body_ends_itself.sysml`, `_body_ends_itself_binds_pin`, `_in_block_names_itself`, `_with_body`, `_binds_output_pin`, `_in_block_binds_pin`, `_body_performs_action` (explored and checked to their full outcome sets, the unbound-pin multiplicity violation among them); `TestRuntimeRobustnessTerminateBodyFlow` (a stated flow runs, a `then` chain reaches the terminate early, a succession cycle and a succession to an unknown step are typed errors) | ⚠️ Approximate: `declared` and `reverse` perform the implicit terminate after the body, a tool-defined linearization; action usages written in an `if` or loop block with no succession between them keep declaration order under every policy | | A witness is a run that can be run again: the `replay:` policy reads a file of `input = ` lines — the inputs a solver chose, each as `InputTaken.String` spells them (a rational exactly, an enumeration or variation-point constructor by its qualified name), any number of them or none, so a stage-1 or `check` witness without them replays as before — followed by choice lines — each as `ChoiceTaken.String` spells them, one per line or joined by `; `, up to the first blank line, so a checker's witness file with a trace body after its header serves as it stands — fixes the inputs on the action as it starts, before its defaults and ahead of the moves, through the same path a caller's `Start` values take, refusing one naming a feature the action does not declare or cannot take with the typed `WitnessInputError` naming it, and resolves the run's choice points in that order, each line having to name the step the run is at and pick among the alternatives it offers, then as `reverse` picks, one token a step, once the lines are spent; a line the run cannot follow — a pick not offered, a step already passed — or one left over at the end fails the run with the typed `ReplayError` naming the move, its choice and what the run faced (`Context.Unfollowed`), never silently running another linearization; a file that is empty or whose lines spell no choice is `SchedulePolicyError` as the policy is parsed, while a header of `no choice points` alone is the witness of a run with none and follows it; accepted wherever a policy is spelled (`sysml -schedule`, `%schedule`, a conformance case's `schedule` pin) except the wire, where a request carries no file of the caller's and the spelling is `INVALID_ARGUMENT` | `runtime/replay.go` `ParseWitness`, `parseInput`, `InputTaken`, `inputParseError`, `WitnessInputError`, `ParseChoices`, `ChoiceParseError`, `ReplayPolicy`, `SchedulePolicy.Replay`, `SchedulePolicy.Witness`; `runtime/action_executor.go` `ActionExecutor.fixWitnessInputs`, `runtime/replay.go` `Context.Unfollowed`, `ReplayError`, `ErrReplayRefused`, `replayRun.beginStep`, `replayRun.choose`; `runtime/scheduler.go` `ParseSchedulePolicy` (`replay:`), `ReplaySpelling`, `SchedulePolicyNames`; `grpc/service.go` `schedulePolicy` (the wire refusal); `cmd/sysml/usage.go` (the `-schedule` help) | `runtime/replay_input_test.go:TestParseInputReadsEverySpelling`, `:TestParseWitnessReadsInputsBeforeChoices`, `:TestReplayFixesWitnessInputs`; `smt/input_engine_test.go:TestEngineWitnessWithInputsReplaysThroughTheStart`, `:TestEngineWitnessWithoutInputsReplaysAsBefore`; `runtime/replay_test.go:TestParseChoicesRejectsWhatSpellsNoChoice`, `:TestParseChoicesStopsAtBlankLine`, `:TestParseReplayPolicy`, `repl/checker_test.go:TestReplayStepsAWitnessOfNoChoice`, `cmd/sysml/check_engine_test.go:TestEngineCheckWitnessOfNoChoiceReplays`, `:TestReplayFollowsActionWitnesses`, `:TestReplayFileReproducesTheExploredRun` (every witness `explore` tables replays to its run's trace), `:TestReplayFollowsStateWitnesses`, `:TestReplayRefusesAMoveNotEnabled`, `:TestReplayFallsBackToReverse`, `:TestReplayReadsAStepsOrderInEitherPlace`, `:TestReplayProbeLeavesTheWitnessInPlace`, `check_loop_replay_test.go:TestCheckWitnessesOfALoopingDoRoundReplay` (a `do` body looping through timed waits past the witness's last line, top-level), `:TestCheckWitnessesOfAnInlinePerformanceReplay` (an order recorded at the performer's step, resolved in the inner flow), `robustness_replay_test.go:TestRuntimeRobustnessReplay` (an inner order naming a token of no flow, or mixing two, refused; a witness ending before the run), `conformance/state_do_action_loop_timed_exit` + `.check.expected.json`; `cmd/sysml/spacecraft_showcase_test.go:TestEngineCheckWitnessesTheSpacecraftRaceAndReplaysEach` (every witness `-engine check` writes replays to its values); `grpc/schedule_test.go:TestAReplayScheduleIsInvalidArgument`; `smt/referee_test.go:TestRefereeCorpus`, `:TestRefereeInputs` (every solver witness, with its inputs, replayed under it) | ✅ As designed (an OpenSysML policy, like the others; no run under another policy changes) | | A choice point is reported wherever the executor had several enabled alternatives the library does not order, and nowhere else: several steppable tokens in one step (`token order`), several holding guards of one decision (`decision branch`), several tokens writing one feature in one step (`write order`), several enabled transitions out of one state for one event (`transition`), the next unit among the firings transitions in several regions selected for one event make (`region order`), the next entry among the regions a composite state, a fork or a history enters (`entry order`), and the next exit among the regions a state leaves (`exit order`). Each is one trace line `choice : (unordered; took )`, one informational diagnostic with code `choice-point` at the node, decision, feature or state that made it, and a count on the debugger's summary line; none is an error, and a run under a fixed policy reports the same set another fixed policy would have had to make on the linearization it took | `choice.go` `ChoiceKind` (`ChoiceTokenOrder`, `ChoiceDecisionBranch`, `choiceWriteOrder`, `ChoiceTransition`, `ChoiceRegionOrder`, `choiceEntryOrder`, `choiceExitOrder`), `ChoicePoint.String` (the trace line), `ChoicePoint.Describe`, `ChoicePoint.Diagnostic` (`SeverityInfo`, code `ChoiceDiagnosticCode`), `Context.noteChoice`, `Context.Notes`, `Context.Choices`, `ActionExecutor.Notes`/`StateExecutor.Notes`; `action_choice.go` `noteTokenOrder`, `ActionExecutor.chooseBranch`, `stepWriteLedger.noteChoices`; `state_executor.go` `transitionChoice`, `StateExecutor.dispatchInOrder`; `repl/trace.go` `Session.noteSummary` (`N choice points; %trace on to see them`, or the lines themselves under `%trace on`); `grpc/convert.go` `RunNoteDiagnosticsToProto` (the `diagnostics` of `ExecuteActionResponse`, `ExecuteStateResponse` and `RunAnalysisResponse`) | `choice_test.go:TestChoicePointRendering`, `:TestChoicesResetPerRun`, `:TestTransitionChoiceNamesStateAndEvent`, `:TestWriteConflictChoice`, `:TestSharedMessageAcceptIsAChoice`, `:TestAncestorPriorityIsNotAChoice`; `explore_test.go:TestExploreSiblingRegionOrder` (the `region order` kind); `conformance/action_choice_fork_token_order`, `action_choice_decision_overlapping_guards`, `action_choice_same_step_write_conflict`, `state_choice_transition_conflict`, `state_explore_region_order`, each `+ .trace.golden` carrying its `choice` line; `repl/choice_test.go:TestStepReportsChoicePoints`, `:TestStepChoiceSummaryWithTraceOn`, `:TestContinueReportsChoicePoints`, `:TestAdvanceReportsChoicePoints`; `grpc/choice_test.go:TestExecuteAction_ChoicePointDiagnostics`, `:TestExecuteState_ChoicePointDiagnostics`, `:TestRunAnalysis_ChoicePointDiagnostics`; `conformance_test.go:TestConformanceDiagnosticsGate` (an informational note is no failure of a conformance case) | ✅ Faithful (the ancestor-priority case between a substate's transition and its enclosing state's is ordered by SysML v2/KerML and is not reported — `state_choice_ancestor_priority_not_reported`, `state_choice_ancestor_outranked_not_reported`) | -| A default run reports its values only up to the partial order the library fixes: `HappensBefore` holds between the occurrences a succession joins and between a send and its accept (Kernel Semantic Library `Occurrences.kerml`, `Performances.kerml`, KerML 1.1 §9.2.4 Occurrences, §9.2.6 Performances), and nothing orders the rest, so a linearization's value of a feature two unordered alternatives both write is one of several the model admits, not the result. Each recorded choice point is classified from the lowered footprints the checker's reduction uses: alternatives that write what another reads or writes, or send and accept on one channel, conflict (a property read or a chained target the declarations do not decide counts as conflicting); alternatives that commute are `independent`, one outcome by construction, and mark nothing. A value a conflicting alternative wrote prints with the marker `x = 1 (order-dependent; 2 choice points — explore shows the set)` on every surface, and so does a value computed from it: a write stands on what its footprint read and on the control it ran under (a guard or condition read, a branch or transition drawn), a message carries what its payload stood on to the accept that binds it, a performance's outputs stand on its inputs, a feature valued by an expression (`attribute y : Integer = x + 1`, a FeatureValue that is not initial, KerML 1.1 §7.3.4.2) stands on what its expression reads at the moment it is read, through features so valued in turn, and a write that reads nothing order-dependent clears the mark; a value nothing order-dependent reached prints as before | `order_dependence.go` `classifyChoice`, `classifyExclusive`, `classifyBy`, `choice.go` `ChoicePoint.Independent`/`Touches`, `order_dependence.go` `Context.OrderDependent`, `OrderDependenceText`; `order_marks.go` `orderMarks.seed`/`rewrite`, `Context.propagateMarks`, `standingOf`, `underControl`, `acceptMarks` (from `statements.go` `stmtEngine.statement`, `ifStatement`, `iteration`, `statementUnder`; `action_executor.go` `stepToken`, `stepDecisionNode`, `awaitSignal`; `action_statements.go` `markPerformance` over `lower.ActionGraph.BindingFootprints`; `state_executor.go` `taking`, `bindAcceptPayload`; `signal.go` `Message.dependence`); per site `action_choice.go` `noteTokenOrder` (`stepOrder.able`), `stepWriteLedger.noteChoices`, `chooseBranch`; `advance.go` `runDue`; `check_run.go` `drawOwner`; `state_unit_front.go` `drain`, `drawOnPath` over `unitQueue.footprint` (`state_unit_footprint.go`); `state_executor.go` `nextEvent` (`state_unit_footprint.go` `eventFootprint`), `state_executor.go` `stepOrderChoice`, `regionOrderChoice` (a do round by `doStepFootprint`; a join by `lower/state_footprint.go` `JoinSegmentFootprints`: each pending segment's trigger, guard and effects with the exits from its source up to the join's owner, less the owner's exit and the way out every order shares), `state_route.go` `branchPoint` over `lower/state_footprint.go` `BranchFootprintsFrom` (a junction or choice branch for the state the transition left: the states exited and entered with the branch's guard and effects, less the exits every branch shares; `BranchFootprints` when no origin is known); `order_dependence.go` `ChoicePoint.touch` (a bare name is the behavior's own feature, `this.` the performing object's, so a write to one never marks the other); `state_run_to_completion.go` `entryStep`; `statements.go` `pickStatement` (`lower.StatementOrder.Dependent`); `lower/footprint.go` `footprintBuilder.boundValue`, `redefined` (a lowered footprint reads through a feature valued by an expression, a redefining feature through the value of the one it redefines along `semantics.ParameterRedefinitionChain`, explicit or by position); `order_marks.go` `Context.deriveMarks` from `body_bindings.go` `deriveBodyCell` (the derived feature's place is rewritten with what its expression read); `smt/encode.go` `Encoding.collectDerived`, `Encoding.deriveValues`, `env.evaluate` (the SMT engine defines a feature valued by an expression over other features by its expression in every state and substitutes it at every read, rather than hold it at its starting value); surfaces `repl/run.go` `namedValue`, `repl/meta.go` `formatFeatureValue`, `choice.go` `ChoicePoint.Standing`, `grpc/service.go` `orderDependent`, `grpc/convert.go` `RunNoteDiagnosticsToProto` | `robustness_order_dependence_test.go:TestRuntimeRobustnessOrderDependence`, `robustness_order_dependence_transitive_test.go:TestRuntimeRobustnessOrderDependenceTransitive`; conformance `action_explore_three_writers` (`orderDependent` `x: 2`), `action_order_derived_from_racing_writers` (`x: 2, y: 2`), `action_order_bound_read_of_racing_writer` (`x: 2, y: 2`; `y = x + 1` read after the join), `action_order_write_from_bound_read` (`x: 2, y: 2, z: 2`; `w := x + 1` bare), `action_order_bound_chain_of_racing_writer` (`v: 2, x: 2, y: 2, z: 2`), `action_order_bound_read_of_unraced_stays_bare` (`x: 2`; `q = p + 1` bare), `action_order_inherited_bound_read_of_racing_writer` (`x: 2, y: 2, z: 2`; `attribute :>> y;` bound as `Base::y = x + 1`), `action_order_positional_bound_read_of_racing_writer` (`out yRace : Integer;` redefining `out yBase : Integer = x + 1` by position), `action_order_guard_reads_racing_writer` (`x: 2, mode: 2`), `action_order_inherited_guard_reads_racing_writer` (`go: 2, mode: 2`; the guard read in the scope of the succession's declaration), `action_order_independent_sibling_stays_bare` (`x: 2, y: 2`; `p`, `q` bare), `action_order_through_performed_action` (`x: 2, result: 2`), `action_order_send_payload_from_racing_writer` (`x: 2, total: 2`), `state_order_effect_reads_racing_attribute` (`last: 1, derived: 1`), `action_order_rewrite_clears_mark` (none), `action_order_independent_branches` (none), `action_order_overlapping_guards` (`mode: 1`), `state_order_regions_conflict` (`last: 1`), `state_order_regions_independent` (none), `state_order_do_round_conflict` (`log: 1`), `state_junction_several_enabled_branches` (`route: 1`), `state_junction_shared_exit_not_branch_dependent` (`route: 1`, `log` fixed), each with its golden trace; `grpc/choice_test.go`, `grpc/schedule_test.go`, `repl/choice_test.go` | ✅ Faithful (the choice points a value stands on follow the data: a value computed from an order-dependent one, through an assignment, a feature valued by an expression over it, a guard or condition read, a performed action's parameters, a message's payload or a transition's effect, carries the same marks; a write that reads nothing order-dependent clears them; `explore` enumerates the set) | +| A default run reports its values only up to the partial order the library fixes: `HappensBefore` holds between the occurrences a succession joins and between a send and its accept (Kernel Semantic Library `Occurrences.kerml`, `Performances.kerml`, KerML 1.1 §9.2.4 Occurrences, §9.2.6 Performances), and nothing orders the rest, so a linearization's value of a feature two unordered alternatives both write is one of several the model admits, not the result. Each recorded choice point is classified from the lowered footprints the checker's reduction uses: alternatives that write what another reads or writes, or send and accept on one channel, conflict (a property read or a chained target the declarations do not decide counts as conflicting); alternatives that commute are `independent`, one outcome by construction, and mark nothing. A conflicting pair touches the place both write and, where a write of one meets a read of the other, what the reading alternative writes from that read (the statements whose flow reads it, or every write when the read is a guard's), not the place read, which one write fixes whichever order ran; a pin, each performance's own, is neither. A place is the feature written whatever path reaches it, so a feature reached through a part (`sensor.raw`, `car.engine.rpm`) stands open as a plain one would, and a part's feature valued by an expression (`scaled = raw * 10`) stands where its expression reads, as the behavior's own does; the place is the part's (`Place.Via`, whether two hold one value decided by the objects the parts denote, so aliases `twin = cell` race and two parts of one definition do not): `left.raw` racing leaves `right.raw` bare. A value a conflicting alternative wrote prints with the marker `x = 1 (order-dependent; 2 choice points — explore shows the set)` on every surface, and so does a value computed from it: a write stands on what its footprint read and on the control it ran under (a guard or condition read, a branch or transition drawn), a message carries what its payload stood on to the accept that binds it, a performance's outputs stand on its inputs, a feature valued by an expression (`attribute y : Integer = x + 1`, a FeatureValue that is not initial, KerML 1.1 §7.3.4.2) stands on what its expression reads at the moment it is read, through features so valued in turn, and a write that reads nothing order-dependent clears the mark; a value nothing order-dependent reached prints as before | `order_dependence.go` `classifyChoice`, `classifyExclusive`, `classifyBy`, `touchMeeting`, `touchWritesMet`, `shared`, `choice.go` `ChoicePoint.Independent`/`Touches`, `order_dependence.go` `Context.OrderDependent`, `placeNamed` (`.` a feature of the object a part denotes, the part the place was reached through), `OrderDependenceText`; `lower/footprint.go` `Footprint.Flows`, `Footprint.WritesReading`, `footprintBuilder.statements` (one data flow per statement), `footprintBuilder.path` (a chained target is the place of the feature it reaches, `Place.Via` the feature it is reached through), `Place.Via`; `action_executor.go` `ActionExecutor.ResultsWithError` (what a part's object holds is derived under the executor's own run, so the run's marks are read, not a fresh run's); `instance.go` `Instance.materializeDerived` (an object's feature valued by an expression is marked with what it read), `Instance.heldBy`; `order_marks.go` `Context.heldAlike`/`partsShareObject`, `order_dependence.go` `ChoicePoint.meets`, `Context.partNamedHolds`; `action_choice.go` `noteObjectWrite` (a write-order choice touches the part's place); `order_marks.go` `orderMarks.seed`/`rewrite`, `Context.propagateMarks`, `standingOf`, `underControl`, `acceptMarks` (from `statements.go` `stmtEngine.statement`, `ifStatement`, `iteration`, `statementUnder`; `action_executor.go` `stepToken`, `stepDecisionNode`, `awaitSignal`; `action_statements.go` `markPerformance` over `lower.ActionGraph.BindingFootprints`; `state_executor.go` `taking`, `bindAcceptPayload`; `signal.go` `Message.dependence`); per site `action_choice.go` `noteTokenOrder` (`stepOrder.able`), `stepWriteLedger.noteChoices`, `chooseBranch`; `advance.go` `runDue`; `check_run.go` `drawOwner`; `state_unit_front.go` `drain`, `drawOnPath` over `unitQueue.footprint` (`state_unit_footprint.go`); `state_executor.go` `nextEvent` (`state_unit_footprint.go` `eventFootprint`), `state_executor.go` `stepOrderChoice`, `regionOrderChoice` (a do round by `doStepFootprint`; a join by `lower/state_footprint.go` `JoinSegmentFootprints`: each pending segment's trigger, guard and effects with the exits from its source up to the join's owner, less the owner's exit and the way out every order shares), `state_route.go` `branchPoint` over `lower/state_footprint.go` `BranchFootprintsFrom` (a junction or choice branch for the state the transition left: the states exited and entered with the branch's guard and effects, less the exits every branch shares; `BranchFootprints` when no origin is known); `order_dependence.go` `ChoicePoint.touch` (a bare name is the behavior's own feature, `this.` the performing object's, so a write to one never marks the other); `state_run_to_completion.go` `entryStep`; `statements.go` `pickStatement` (`lower.StatementOrder.Dependent`); `lower/footprint.go` `footprintBuilder.boundValue`, `redefined` (a lowered footprint reads through a feature valued by an expression, a redefining feature through the value of the one it redefines along `semantics.ParameterRedefinitionChain`, explicit or by position); `order_marks.go` `Context.deriveMarks` from `body_bindings.go` `deriveBodyCell` (the derived feature's place is rewritten with what its expression read); `smt/encode.go` `Encoding.collectDerived`, `Encoding.deriveValues`, `env.evaluate` (the SMT engine defines a feature valued by an expression over other features by its expression in every state and substitutes it at every read, rather than hold it at its starting value); surfaces `repl/run.go` `namedValue`, `repl/meta.go` `formatFeatureValue`, `choice.go` `ChoicePoint.Standing`, `grpc/service.go` `orderDependent`, `grpc/convert.go` `RunNoteDiagnosticsToProto` | `robustness_order_dependence_test.go:TestRuntimeRobustnessOrderDependence`, `robustness_order_dependence_transitive_test.go:TestRuntimeRobustnessOrderDependenceTransitive`; conformance `action_explore_three_writers` (`orderDependent` `x: 2`), `action_order_derived_from_racing_writers` (`x: 2, y: 2`), `action_order_bound_read_of_racing_writer` (`x: 2, y: 2`; `y = x + 1` read after the join), `action_order_write_from_bound_read` (`x: 2, y: 2, z: 2`; `w := x + 1` bare), `action_order_bound_chain_of_racing_writer` (`v: 2, x: 2, y: 2, z: 2`), `action_order_bound_read_of_unraced_stays_bare` (`x: 2`; `q = p + 1` bare), `action_order_chained_write_of_racing_writers` (`sensor.raw: 2, sensor.scaled: 2, z: 2, zz: 2`), `action_order_chained_two_level_write` (`z: 2` from `car.engine.rpm`; `m` bare), `action_order_chained_read_of_unraced_stays_bare` (`x: 2, w: 2`; `sensor.raw`, `sensor.scaled` written before the fork bare), `action_order_sibling_read_of_racing_write` (`z: 1`; `x`, written once, bare), `action_order_chained_parts_apart` (`left.raw: 2, left.scaled: 2`; `right.raw`, `right.scaled`, `z` read from `right.raw` bare), `action_order_chained_alias_of_racing_writers` (`cell.mark`, `z: 2` through `ref part twin = cell`), `state_order_guard_and_effect_read_racing_write` (`route: 1, seen: 1`, the junction branch's two writes under a guard read racing the write; `armed` bare), `order_marks_differential_test.go:TestOrderMarksAgreeWithExploredOutcomes` (over every `action_order_*` and `state_order_*` case, the names marked equal the names exploration finds at more than one value, two pinned approximations aside), `action_order_inherited_bound_read_of_racing_writer` (`x: 2, y: 2, z: 2`; `attribute :>> y;` bound as `Base::y = x + 1`), `action_order_positional_bound_read_of_racing_writer` (`out yRace : Integer;` redefining `out yBase : Integer = x + 1` by position), `action_order_guard_reads_racing_writer` (`x: 2, mode: 2`), `action_order_inherited_guard_reads_racing_writer` (`go: 2, mode: 2`; the guard read in the scope of the succession's declaration), `action_order_independent_sibling_stays_bare` (`x: 2, y: 2`; `p`, `q` bare), `action_order_through_performed_action` (`x: 2, result: 2`), `action_order_send_payload_from_racing_writer` (`x: 2, total: 2`), `state_order_effect_reads_racing_attribute` (`last: 1, derived: 1`), `action_order_rewrite_clears_mark` (none), `action_order_independent_branches` (none), `action_order_overlapping_guards` (`mode: 1`), `state_order_regions_conflict` (`last: 1`), `state_order_regions_independent` (none), `state_order_do_round_conflict` (`log: 1`), `state_junction_several_enabled_branches` (`route: 1`), `state_junction_shared_exit_not_branch_dependent` (`route: 1`, `log` fixed), each with its golden trace; `grpc/choice_test.go`, `grpc/schedule_test.go`, `repl/choice_test.go` | ✅ Faithful (the choice points a value stands on follow the data: a value computed from an order-dependent one, through an assignment, a feature valued by an expression over it, a guard or condition read, a performed action's parameters, a message's payload or a transition's effect, carries the same marks; a write that reads nothing order-dependent clears them; `explore` enumerates the set) | | A guard the executor reads only to report a choice — one after the branch or transition already taken — that fails to evaluate is no alternative and no error: a guard with no result is not true, so its succession is not selected, the run is unchanged, and the failure is an informational `guard-unevaluable` note, while the same failure at the guard the run does take still fails the run | `choice.go` `UnevaluableGuard`, `UnevaluableGuard.Diagnostic` (`SeverityInfo`, code `UnevaluableGuardCode`), `action_choice.go` `ActionExecutor.noteUnevaluableGuard`, `choice.go` `Context.unevaluableGuards`; `action_choice.go` `ActionExecutor.noteUnevaluableGuard`; `action_executor.go` `probeGuard` (a `beginProbe` preview that restores the budget, the trace, every effect and the object identities it took); `state_executor.go` `probeTransition`, `unevaluableTransition`; `state_route.go` `probeBranch` (a choice pseudostate's later branch); `state_change_trigger.go` `probeChangeGuard` | `conformance/action_choice_unevaluable_guard` + `.expected.json` + `.trace.golden`; `conformance/state_choice_unevaluable_transition` + `.expected.json` + `.trace.golden`; `conformance/state_choice_unevaluable_branch` + `.expected.json` + `.trace.golden`; `choice_test.go:TestLaterGuardErrorIsNotAChoiceNorAFailure`, `:TestLaterChoiceGuardErrorIsNotAChoiceNorAFailure`, `:TestFirstTransitionFailureStillFailsTheRun`, `:TestLaterGuardIsProbedWithoutCost`, `:TestLaterChangeGuardErrorIsNotAChoiceNorAFailure`, `:TestProbedGuardLeavesObjectIdentitiesUntouched`; `grpc/choice_test.go:TestExecuteAction_UnevaluableGuardDiagnostics`; `repl/choice_test.go:TestStepReportsUnevaluableGuards`; `robustness_action_flow_test.go:decision_no_satisfied_guard` (the taken path still fails) | ✅ Faithful (SysML v2 §7.17.3 selects a succession whose guard is true; a guard that cannot be evaluated is not true, and reading it changed nothing) | | A conformance case that admits several outcomes states the whole set: `outcomes` lists every admissible outcome in full — never "anything" — and `admissible` cites the section of `behavior-semantic-oracle.md` that derives the set; a `.trace.order` beside it states the partial order the library does fix as `earlier < later` over trace labels. The harness checks the run's outcome is exactly one listed member, checks the trace against every order constraint, then explores the case and fails on a listed outcome no linearization reached, a reached outcome the list omits, and a hit budget — each naming the outcome and a witness choice sequence | `conformance_test.go` `ExpectedOutcome.Outcomes`/`Admissible`, `explore.go` `ExploreBudget`, `conformance_test.go` `admissibleSchemaProblems` (an `outcomes` list needs two or more full outcomes, an `admissible` title the oracle has, and no single-outcome fields beside it), `matchOutcome`, `runConformanceCase`, `exploreConformanceCase`; `trace_test.go` `checkTraceOrder`, `parseOrderConstraints`, `orderViolations`; `testdata/conformance/README.md` (the schema) | `conformance_test.go:TestAdmissibleOutcomesSchema`, `:TestMatchOutcomeRequiresExactlyOne`, `:TestExecutionConformance` (`exploreConformanceCase` over every `outcomes` case), `:TestExecutionConformanceUnderPolicies`; `trace_test.go:TestTraceOrderViolationFails`, `:TestExecutionTrace`; `conformance/action_explore_three_writers` (`outcomes` of three, `.trace.order` of six constraints; explored in six runs), `action_choice_shared_message_accept`, `action_choice_fork_token_order` (one outcome, a `.trace.order` admitting the tokens either way), `state_explore_region_order` | ✅ Faithful (a case without `outcomes` is not explored by the harness, so a fixture pinning one linearization of an unobservable openness stays a one-outcome case; the oracle names which fixtures those are) | | Exploration is bounded and distinguishes setup failures from runtime outcomes: the budget is runs (1024 by default) and choice points per run (64), and a budget hit ends the search as `incomplete: budget hit after N runs`, naming `runs` before `depth`; a fresh-context or root-executor creation failure, or a pure structural start-check failure before root behavior runs, means no linearization ran and is returned without outcomes, while a failure during initial model behavior or later is an error outcome. Any runtime-error linearization makes the verdict fail, including an incomplete exploration; only an incomplete search without a witnessed failure is unresolved, and only a complete search without failures proves the outcome set. JSON and the wire include `failedLinearizations` / `failed_linearizations` only when nonzero; standing evidence names the failing count | `runtime/explore.go` `SetupError`, `Exploration.FailedLinearizations`; `runtime/context.go` root action/state setup classification; `runtime/explore_queue.go` `ExploreWith`, `exploreQueue.work`; `runtime/check.go` checker setup failure; `analysis/explore.go` proof strength; `analysis/standing.go` `Result.evidence`; `repl/explore.go` `explorationVerdict`; `cmd/sysml/report.go` `checkExploration`; `grpc/explore.go` `Service.explore` | `runtime/robustness_explore_failures_test.go:TestRuntimeRobustnessExploreFailures`; `analysis/explore_test.go`; `repl/explore_test.go:TestRunActionExploreSetupFailureRunsNoLinearization`, `:TestRunActionExplorePartialFailureFailsTheVerdict`; `cmd/sysml/run_test.go:TestExploreSetupFailureIsNotAnOutcome`, `:TestExplorePartialFailureFailsAndReportsTheFailedRun`, `:TestExploreInitialEntryFailureIsAnOutcome`; `grpc/explore_test.go:TestExploreSetupFailureIsReturnedInTheResponse`, `:TestExploreReportsAFailingRunAsAnOutcome` | ✅ Faithful (setup failures produce no outcome, while a witnessed runtime failure prevents a proof claim) | diff --git a/internal/exec/runtime/action_choice.go b/internal/exec/runtime/action_choice.go index a3d3be7eb4..a133d14f88 100644 --- a/internal/exec/runtime/action_choice.go +++ b/internal/exec/runtime/action_choice.go @@ -35,6 +35,7 @@ type destWrites struct { label string // the destination as a trace names it: `x`, or `x of object #3` feature string // the feature written, as the write spelled it sym *symbols.Symbol // the feature's declaration, nil when none resolves + via *symbols.Symbol // the part or item the written object is held as, nil for none file string span source.Span last []stepWrite @@ -90,7 +91,7 @@ func (e *performances) beginTokenStep(id int64) func() { func (e *performances) noteFrameWrite(f *actionFrame, name string, value Value) { sym := e.ctx.featureDeclared(f.scope, name) key := f.key(name) - e.ctx.noteWrite(writeDest{holder: f, name: key}, key, name, sym, value) + e.ctx.noteWrite(writeDest{holder: f, name: key}, key, name, sym, nil, value) } // noteObjectWrite records a write the running token made to a feature obj holds, @@ -104,13 +105,13 @@ func (ctx *Context) noteObjectWrite(obj *Instance, name string, value Value) { sym = fv.Feature.Symbol } } - ctx.noteWrite(dest, fmt.Sprintf("%s of object #%d", name, obj.ID), name, sym, value) + ctx.noteWrite(dest, fmt.Sprintf("%s of object #%d", name, obj.ID), name, sym, obj.heldBy(), value) } // noteWrite records a write the running token made to dest, labelled as a trace // names it and under the feature's name and declaration; destinations several // tokens wrote are reported once the step ends. -func (ctx *Context) noteWrite(dest writeDest, label, feature string, sym *symbols.Symbol, value Value) { +func (ctx *Context) noteWrite(dest writeDest, label, feature string, sym, via *symbols.Symbol, value Value) { ledger := ctx.stepWrites if ledger == nil || ledger.writer == 0 { return @@ -118,7 +119,7 @@ func (ctx *Context) noteWrite(dest writeDest, label, feature string, sym *symbol w := stepWrite{token: ledger.writer, value: value} d := ledger.writes[dest] if d == nil { - d = &destWrites{label: label, feature: feature, sym: sym} + d = &destWrites{label: label, feature: feature, sym: sym, via: via} if sym != nil { d.file, d.span = sym.DocName, sym.DeclSpan } @@ -159,7 +160,7 @@ func (l *stepWriteLedger) noteChoices(e *performances) { File: d.file, Span: d.span, Touches: []string{d.feature}, - touched: []lower.Place{{Sym: d.sym, Name: d.feature}}, + touched: []lower.Place{{Sym: d.sym, Name: d.feature, Via: d.via}}, }) } } @@ -369,6 +370,7 @@ func (e *ActionExecutor) noteTokenOrder(step int, order stepOrder, schedule *tok File: e.action.DocName, Span: e.action.DeclSpan, } + choice.alike = e.ctx.heldAlike classifyChoice(&choice, fps, nil) e.noteChoice(choice) } diff --git a/internal/exec/runtime/action_executor.go b/internal/exec/runtime/action_executor.go index c8356f376d..6d6018eeed 100644 --- a/internal/exec/runtime/action_executor.go +++ b/internal/exec/runtime/action_executor.go @@ -3567,6 +3567,11 @@ func (e *ActionExecutor) Results() map[string]Value { // ResultsWithError returns the values the action's features hold and the first binding // derivation error; a feature whose binding fails to derive is omitted. func (e *ActionExecutor) ResultsWithError() (map[string]Value, error) { + // A binding derived to answer is a read of this run: deriving it under a run + // of its own would install that run, losing this one's marks to the caller. + if e.driven.state != nil { + defer e.ctx.enterRun(e.driven.state)() + } results := make(map[string]Value, len(e.root.data)) err := e.root.collect("", results) if e.occurrence != nil { diff --git a/internal/exec/runtime/action_statements.go b/internal/exec/runtime/action_statements.go index b1232355e0..ba5dacd266 100644 --- a/internal/exec/runtime/action_statements.go +++ b/internal/exec/runtime/action_statements.go @@ -379,7 +379,7 @@ func (e *performances) markPerformance(graph *lower.ActionGraph, node ast.Node, by := slices.Clone(e.ctx.controls) for _, w := range fp.Writes { if w.Local { - by = unionSerials(by, e.ctx.run.marks.at(w)) + by = unionSerials(by, e.ctx.run.marks.at(w, e.ctx.heldAlike)) } } e.ctx.writeMarks(fp.Writes, by) diff --git a/internal/exec/runtime/advance.go b/internal/exec/runtime/advance.go index 5912290fdd..e315d87bb0 100644 --- a/internal/exec/runtime/advance.go +++ b/internal/exec/runtime/advance.go @@ -265,6 +265,7 @@ func (ctx *Context) drawDueOrder(due []clockWaiter) (int, error) { choice.Alternatives[i] = w.dueLabel() fps[i] = futures.executorFuture(w) } + choice.alike = ctx.heldAlike classifyChoice(&choice, fps, func(i, j int) lower.Relation { return ctx.relation(due[i], due[j]) }) scheduling := ctx.scheduling() pick := scheduling.choose(choice, nil) diff --git a/internal/exec/runtime/check_reduce.go b/internal/exec/runtime/check_reduce.go index f62337f326..4ee02f3750 100644 --- a/internal/exec/runtime/check_reduce.go +++ b/internal/exec/runtime/check_reduce.go @@ -146,6 +146,7 @@ func unionFootprints(f, g lower.Footprint) lower.Footprint { Dynamic: f.Dynamic || g.Dynamic, Creates: f.Creates || g.Creates, Routes: f.Routes || g.Routes, + Flows: append(slices.Clone(f.Flows), g.Flows...), } } diff --git a/internal/exec/runtime/check_run.go b/internal/exec/runtime/check_run.go index 7714fcb8bb..c2d9e26f9a 100644 --- a/internal/exec/runtime/check_run.go +++ b/internal/exec/runtime/check_run.go @@ -109,6 +109,7 @@ func (r *invocationRun) drawOwner(execs []checkedExecutor) (int, error) { for i, exec := range execs { fps[i] = futures.executorFuture(exec) } + choice.alike = r.ctx.heldAlike classifyChoice(&choice, fps, func(i, j int) lower.Relation { return r.ctx.relation(execs[i], execs[j]) }) scheduling := r.ctx.scheduling() pick := scheduling.choose(choice, nil) diff --git a/internal/exec/runtime/choice.go b/internal/exec/runtime/choice.go index 4c24edd74f..f5ef71bb93 100644 --- a/internal/exec/runtime/choice.go +++ b/internal/exec/runtime/choice.go @@ -142,6 +142,9 @@ type ChoicePoint struct { Touches []string // touched are the places written behind Touches, with the features they resolve to. touched []lower.Place + // alike is the run's word on whether two part-held places are one value; nil + // for a choice classified by the declarations alone. + alike func(p, q lower.Place) bool // serial names the choice to the marks of the run's values (order_marks.go). serial int64 diff --git a/internal/exec/runtime/choice_test.go b/internal/exec/runtime/choice_test.go index c66acc2602..f901dd9169 100644 --- a/internal/exec/runtime/choice_test.go +++ b/internal/exec/runtime/choice_test.go @@ -991,7 +991,9 @@ func TestNotesOfATransitionBlockedBeforeFiringAreDropped(t *testing.T) { } want := []string{ "choice entering work: next a1(entry), b1(entry) (unordered; took a1(entry) first; independent)", - "choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: level)", + // The one write of `level` stands whichever region fires first; b's guards + // read it and write no feature, so the dependent order touches no value. + "choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent)", } if got := noteStrings(ctx.Notes()); !slices.Equal(got, want) { t.Fatalf("notes %v, want the entry and region-order choices alone: %v", got, want) diff --git a/internal/exec/runtime/instance.go b/internal/exec/runtime/instance.go index 1ddcf259be..26567204a6 100644 --- a/internal/exec/runtime/instance.go +++ b/internal/exec/runtime/instance.go @@ -1328,7 +1328,13 @@ func (inst *Instance) materializeDerived(ctx *Context, fv *FeatureValue, name st if ctx.takeShared(inst, fv) { return fv, nil } - return inst.holdDerived(ctx, fv, name, func() (Value, error) { return ctx.evalFeatureValueDefault(inst, fv, name) }) + held, err := inst.holdDerived(ctx, fv, name, func() (Value, error) { return ctx.evalFeatureValueDefault(inst, fv, name) }) + if err == nil && fv.body == nil { + place := bindingPlace(fv.Feature.Symbol, name) + place.Via = inst.heldBy() + ctx.deriveMarks(place, ctx.defaultScope(inst, fv), fv.Feature.DefaultValue) + } + return held, err } // holdDerived holds what derive states for the feature, recording what it reads, once @@ -1897,10 +1903,7 @@ func (ctx *Context) evalFeatureValueDefault(inst *Instance, fv *FeatureValue, na if r := ctx.model.resolver; r != nil && r.IsOccurrenceThis(fv.Feature.Symbol) { return ctx.objectValue(ctx.contextOccurrence(inst)) } - scope := fv.Feature.DefaultScope() - if scope == nil { - scope = inst.Type.OwnerScope - } + scope := ctx.defaultScope(inst, fv) ec := NewEvalContextIn(ctx, scope, ctx.bindingContext(inst, fv.Feature)) if isBehaviorDefKind(inst.Type.Kind) { // A feature default of a behavior def is evaluated on the def's @@ -1921,6 +1924,15 @@ func (ctx *Context) evalFeatureValueDefault(inst *Instance, fv *FeatureValue, na return val, nil } +// defaultScope is the scope a feature's value expression is read in: the one it +// was declared in, else the one the object's type is. +func (ctx *Context) defaultScope(inst *Instance, fv *FeatureValue) *symbols.Scope { + if scope := fv.Feature.DefaultScope(); scope != nil { + return scope + } + return inst.Type.OwnerScope +} + // subjectMemberValue reads a subject's value expression that is a qualified feature name of // self's type (`subject subj default Case::result;` on a case object) as self's own member. func (ctx *Context) subjectMemberValue(feat *EffectiveFeature, self *Instance, scope *symbols.Scope, expr ast.Node) (Value, bool, error) { @@ -1946,3 +1958,22 @@ func (ctx *Context) qualifiedMemberOf(self *Instance, scope *symbols.Scope, expr } return fv.HeldValue(), true, nil } + +// heldBy is the one part or item usage the object is held as the value of, nil +// where none or more than one classifies it so. +func (inst *Instance) heldBy() *symbols.Symbol { + if inst.Type != nil && (inst.Type.Kind == symbols.SymbolPartUsage || inst.Type.Kind == symbols.SymbolItemUsage) { + return inst.Type + } + var held *symbols.Symbol + for _, sym := range inst.classifiers { + if sym.Kind != symbols.SymbolPartUsage && sym.Kind != symbols.SymbolItemUsage { + continue + } + if held != nil && held != sym { + return nil + } + held = sym + } + return held +} diff --git a/internal/exec/runtime/order_dependence.go b/internal/exec/runtime/order_dependence.go index b624b93385..d5aaed6ddd 100644 --- a/internal/exec/runtime/order_dependence.go +++ b/internal/exec/runtime/order_dependence.go @@ -64,26 +64,57 @@ func onValues(fp lower.Footprint) lower.Footprint { return fp } -// touchMeeting adds the writes of two dependent alternatives that meet a place of -// the other's; when none does (the alternatives meet on the bus, on control, or -// one is dynamic) every write of both may stand at an order-dependent value. +// touchMeeting adds the places of two dependent alternatives whose values the +// order decides: a place both write, and what one writes from a read of a place +// the other writes, which sees it before or after. When no place meets (the +// alternatives meet on the bus, on control, or one is dynamic) every write of +// both may stand at an order-dependent value. func (c *ChoicePoint) touchMeeting(f, g lower.Footprint, rel lower.Relation) { + met := c.touchWritesMet(f, g, rel) + met = c.touchWritesMet(g, f, rel) || met + if !met { + c.touchWrites(f, g) + } +} + +// touchWritesMet touches the writes of f that meet a write of g, and the writes +// of g standing on a read of g that a write of f meets; it reports whether any did. +func (c *ChoicePoint) touchWritesMet(f, g lower.Footprint, rel lower.Relation) bool { met := false for _, p := range f.Writes { - if rel.PlaceMeets(p, g.Reads) || rel.PlaceMeets(p, g.Writes) { + if c.meets(rel, p, g.Writes) { c.touch(p) met = true } - } - for _, q := range g.Writes { - if rel.PlaceMeets(q, f.Reads) || rel.PlaceMeets(q, f.Writes) { - c.touch(q) + if c.meets(rel, p, g.Reads) { + // A pin is each performance's own, delivered to, not raced for: a read of + // one sees what arrived, whichever order the moves ran. + if shared(p) { + for _, q := range g.WritesReading(func(r lower.Place) bool { return c.meets(rel, p, []lower.Place{r}) }) { + c.touch(q) + } + } met = true } } - if !met { - c.touchWrites(f, g) + return met +} + +// meets reports whether p may name the value of a place among qs: the +// declarations' answer, narrowed by what the run knows two parts denote. +func (c *ChoicePoint) meets(rel lower.Relation, p lower.Place, qs []lower.Place) bool { + for _, q := range qs { + if rel.PlaceMeets(p, []lower.Place{q}) && (c.alike == nil || c.alike(p, q)) { + return true + } } + return false +} + +// shared reports whether a place is one slot every move names, which a choice +// point records: not a performance's pin or a node's own feature, nor a state. +func shared(p lower.Place) bool { + return !(p.Local && p.Node != nil || p.State != nil) } // classifyExclusive marks a choice among alternatives of which one runs and the @@ -105,10 +136,10 @@ func (c *ChoicePoint) touchWrites(fps ...lower.Footprint) { } func (c *ChoicePoint) touch(p lower.Place) { - if p.Local && p.Node != nil || p.State != nil { + if !shared(p) { return } - if !slices.ContainsFunc(c.touched, func(q lower.Place) bool { return q.Name == p.Name && q.Sym == p.Sym }) { + if !slices.ContainsFunc(c.touched, func(q lower.Place) bool { return q.Name == p.Name && q.Sym == p.Sym && q.Via == p.Via }) { c.touched = append(c.touched, p) } name := p.String() @@ -153,12 +184,17 @@ func (ctx *Context) placeNamed(p lower.Place, name string, selves []*Instance) b if p.Sym != nil && qualifier != "" && qualifier != "this" && ctx.run.marks.performed(lastSegment(qualifier)) { return declaredUnder(p.Sym, lastSegment(qualifier)) } + if p.Via != nil && qualifier != "" && qualifier != "this" && !ctx.partNamedHolds(p.Via, lastSegment(qualifier)) { + return false // held by a part other than the one named + } holder := ctx.performerOwning(selves, p.Sym) switch { case p.Sym == nil, len(selves) == 0: return true case qualifier == "": return holder == nil + case qualifier != "this" && holder == nil: + return true // a feature of an object a part of the action denotes, no performer's own default: return len(selves) == 1 && holder == selves[0] } @@ -249,3 +285,17 @@ func (ctx *Context) UnresolvedChoices() int { } return count } + +// partNamedHolds reports whether the part named beside via may hold what via +// holds: via itself, a sibling denoting an object in common, or one the +// declarations do not place. +func (ctx *Context) partNamedHolds(via *symbols.Symbol, name string) bool { + if via.Name == name || via.OwnerScope == nil { + return true + } + sibling, ok := via.OwnerScope.LookupLocal(name) + if !ok { + return true + } + return ctx.partsShareObject(via, sibling) +} diff --git a/internal/exec/runtime/order_marks.go b/internal/exec/runtime/order_marks.go index 823b658140..0ff8ce2273 100644 --- a/internal/exec/runtime/order_marks.go +++ b/internal/exec/runtime/order_marks.go @@ -106,10 +106,10 @@ func (m *orderMarks) add(p lower.Place, by []int64) { } // of is what a read of the place stands on: every entry the place may name. -func (m *orderMarks) of(p lower.Place) []int64 { +func (m *orderMarks) of(p lower.Place, alike func(p, q lower.Place) bool) []int64 { var out []int64 for _, e := range m.entries { - if e.place.Conflicts(p) { + if e.place.Conflicts(p) && alike(e.place, p) { out = unionSerials(out, e.by) } } @@ -118,10 +118,10 @@ func (m *orderMarks) of(p lower.Place) []int64 { // at is what the one declaration the place names stands on, the marks a rewrite // of the place replaces; a read, which may reach same-named places, uses of. -func (m *orderMarks) at(p lower.Place) []int64 { +func (m *orderMarks) at(p lower.Place, alike func(p, q lower.Place) bool) []int64 { var out []int64 for _, e := range m.entries { - if samePlace(e.place, p) { + if samePlace(e.place, p) && alike(e.place, p) { out = unionSerials(out, e.by) } } @@ -141,11 +141,11 @@ func (m *orderMarks) all() []int64 { // choice drawn at this instant of the clock left on it, which the write is not // ordered after. Only the place itself is rewritten: a same-named place of // another declaration may hold a different value, which the write leaves as it was. -func (m *orderMarks) rewrite(p lower.Place, by []int64, now float64) { +func (m *orderMarks) rewrite(p lower.Place, by []int64, now float64, alike func(p, q lower.Place) bool) { kept := slices.Clone(by) entries := m.entries[:0] for _, e := range m.entries { - if !samePlace(e.place, p) { + if !samePlace(e.place, p) || !alike(e.place, p) { entries = append(entries, e) continue } @@ -254,7 +254,7 @@ func (ctx *Context) readStanding(deps []int64, fp lower.Footprint, dynamicAll bo return unionSerials(deps, marks.all()) } for _, r := range fp.Reads { - deps = unionSerials(deps, marks.of(ctx.placeOf(r))) + deps = unionSerials(deps, marks.of(ctx.placeOf(r), ctx.heldAlike)) } return deps } @@ -264,11 +264,21 @@ func (ctx *Context) readStanding(deps []int64, fp lower.Footprint, dynamicAll bo // computed from them would. Deriving is a read, not a move, so it stands on no // control; a derivation reading nothing order-dependent clears the mark, as a // clean write does. +// For a feature of an object held via a feature, the expression's bare names +// are that object's own, held the same way. func (ctx *Context) deriveMarks(place lower.Place, scope *symbols.Scope, value ast.Node) { if place.Name == "" || value == nil { return } fp := ctx.model.expressionFootprint(scope, value) + if place.Via != nil { + fp.Reads = slices.Clone(fp.Reads) + for i := range fp.Reads { + if fp.Reads[i].Via == nil && fp.Reads[i].Node == nil && !fp.Reads[i].Local { + fp.Reads[i].Via = place.Via + } + } + } ctx.writeMarks([]lower.Place{place}, ctx.readStanding(nil, fp, true)) } @@ -305,7 +315,7 @@ func (ctx *Context) writeMarks(places []lower.Place, by []int64) { return } for _, w := range places { - ctx.run.marks.rewrite(ctx.placeOf(w), by, ctx.clock.now) + ctx.run.marks.rewrite(ctx.placeOf(w), by, ctx.clock.now, ctx.heldAlike) } } @@ -356,3 +366,34 @@ func commonReach(graph *lower.ActionGraph, successors []lower.ActionEdge) map[as } return common } + +// heldAlike reports whether two places of one declaration may hold one value in +// this run: yes unless each is reached through a part and the two parts denote no +// object in common (`left.raw` beside `right.raw`; `twin = cell` denote one). +func (ctx *Context) heldAlike(p, q lower.Place) bool { + if p.Via == nil || q.Via == nil || p.Via == q.Via { + return true + } + return ctx.partsShareObject(p.Via, q.Via) +} + +// partsShareObject reports whether the objects two features denote overlap, true +// where the run does not know what either denotes. +func (ctx *Context) partsShareObject(a, b *symbols.Symbol) bool { + as, ok := ctx.liveOccurrences(a) + if !ok { + return true + } + bs, ok := ctx.liveOccurrences(b) + if !ok { + return true + } + for _, x := range as { + for _, y := range bs { + if x == y { + return true + } + } + } + return false +} diff --git a/internal/exec/runtime/order_marks_differential_test.go b/internal/exec/runtime/order_marks_differential_test.go new file mode 100644 index 0000000000..a147dbef99 --- /dev/null +++ b/internal/exec/runtime/order_marks_differential_test.go @@ -0,0 +1,149 @@ +package runtime + +import ( + "context" + "os" + "path/filepath" + "slices" + "sort" + "strings" + "testing" + + "github.com/Open-MBEE/OpenSysML/internal/semantic/resolve" + "github.com/Open-MBEE/OpenSysML/internal/semantic/semantics" + "github.com/Open-MBEE/OpenSysML/internal/syntax/parser" + "github.com/Open-MBEE/OpenSysML/internal/syntax/source" + "github.com/Open-MBEE/OpenSysML/tests/fixtures" +) + +// orderMarkApproximations pins the order fixtures whose marks are known not to agree +// with exploration, each with the names marked and the names varying as they stand, +// so a movement either way is seen; the reason says what approximates. +var orderMarkApproximations = map[string]struct { + marked, varying []string + reason string +}{ + "action_order_explicit_argument_binds_pin": { + marked: []string{"dep.result", "dep.x", "derived", "fixed", "lit.result", "x", "y"}, + varying: []string{"dep.result", "dep.x", "derived", "x", "y"}, + reason: "a performed action's footprint is dynamic, so its outputs stand on every mark, a literal argument's included", + }, + "action_order_send_payload_from_racing_writer": { + marked: []string{"receiver.msg", "total", "x"}, + varying: []string{"msg", "total", "x"}, + reason: "an accept's payload is reported twice, as the node's pin and under its bare name: the pin is marked, the bare name is not, and the outcome spells the pin's object alike", + }, +} + +// Over every order fixture, the outputs the default run marks order-dependent are +// exactly those exploration finds at more than one value: a mark where every +// linearization agrees is a false positive, a bare value that varies a false negative. +// The pinned approximations are held where they stand. +func TestOrderMarksAgreeWithExploredOutcomes(t *testing.T) { + conformanceDir := filepath.Join("testdata", "conformance") + entries, err := os.ReadDir(conformanceDir) + if err != nil { + t.Fatal(err) + } + cases := 0 + for _, entry := range entries { + name := entry.Name() + if !strings.HasSuffix(name, ".expected.json") || !strings.HasPrefix(name, "action_order_") && !strings.HasPrefix(name, "state_order_") { + continue + } + caseName := strings.TrimSuffix(name, ".expected.json") + expected := loadExpectedOutcome(t, conformanceDir, caseName) + if len(expected.Outcomes) == 0 || len(expected.Performers) > 0 { + continue + } + cases++ + t.Run(caseName, func(t *testing.T) { + marked, varying := markedAndVaryingOutputs(t, conformanceDir, caseName, expected) + if pinned, ok := orderMarkApproximations[caseName]; ok { + if !slices.Equal(marked, pinned.marked) || !slices.Equal(varying, pinned.varying) { + t.Errorf("default run marks %v order-dependent and exploration varies %v; pinned as %v and %v (%s)", + marked, varying, pinned.marked, pinned.varying, pinned.reason) + } + return + } + if !slices.Equal(marked, varying) { + t.Errorf("default run marks %v order-dependent; exploration varies %v", marked, varying) + } + }) + } + if cases == 0 { + t.Fatal("no order fixture with an admissible set found") + } +} + +// markedAndVaryingOutputs runs the case once under its pinned policy and reports the outputs +// marked order-dependent, then explores it and reports the outputs with more than one value. +func markedAndVaryingOutputs(t *testing.T, conformanceDir, caseName string, expected ExpectedOutcome) (marked, varying []string) { + t.Helper() + sysmlPath := fixtures.ModelPath(conformanceDir, caseName) + data, err := os.ReadFile(sysmlPath) + if err != nil { + t.Fatal(err) + } + src := source.New(sysmlPath, data) + p := parser.New(src) + file := p.ParseFile() + if len(p.Diagnostics) > 0 { + t.Fatalf("parse %s: %v", sysmlPath, p.Diagnostics) + } + idx, sources := indexCaseDocuments(t, conformanceDir, src, file, expected) + resolver := resolve.New(idx) + model := semantics.NewModel(resolver) + model.SetSourceText(source.TextOf(sources, nil)) + fresh := func() *Context { + ctx := NewContext(typedModel(model, resolver), 10000) + applyCaseDraws(t, ctx, expected) + return ctx + } + run := conformanceRun(t, idx, sysmlPath, expected) + + ctx := fresh() + if err := ctx.SetSchedule(casePolicy(t, expected, DefaultSchedulePolicy)); err != nil { + t.Fatal(err) + } + outcome, err := run(ctx) + if err != nil { + t.Fatalf("default run: %v", err) + } + names := make([]string, 0, len(outcome.Outputs)) + for name := range outcome.Outputs { + names = append(names, name) + } + for name := range ctx.OrderDependentAmong(names) { + marked = append(marked, name) + } + sort.Strings(marked) + + policy, err := ExplorePolicy(expected.ExploreBudget.budget()) + if err != nil { + t.Fatal(err) + } + exploration, err := Explore(context.Background(), policy, func() (*Context, error) { return fresh(), nil }, run) + if err != nil { + t.Fatalf("explore: %v", err) + } + if !exploration.Complete() { + t.Fatalf("exploration %s", exploration.Status()) + } + texts := make(map[string]map[string]bool) + for _, explored := range exploration.Outcomes { + for _, out := range explored.Outcome.outputsSpelled(func(name string) string { return name }, false) { + if texts[out.Name] == nil { + texts[out.Name] = make(map[string]bool) + } + texts[out.Name][out.Text] = true + } + } + for name, values := range texts { + if len(values) > 1 { + varying = append(varying, name) + } + } + sort.Strings(varying) + return marked, varying +} diff --git a/internal/exec/runtime/state_executor.go b/internal/exec/runtime/state_executor.go index 4723f8eddb..b63cbd5fa7 100644 --- a/internal/exec/runtime/state_executor.go +++ b/internal/exec/runtime/state_executor.go @@ -1146,6 +1146,7 @@ func (e *StateExecutor) nextEvent() (Event, error) { choice.Alternatives[i] = e.eventLabel(tied[i]) fps[i] = e.eventFootprint(tied[i]) } + choice.alike = e.ctx.heldAlike classifyChoice(&choice, fps, nil) scheduling := e.ctx.scheduling() choice.Taken = scheduling.choose(choice, nil) @@ -1707,6 +1708,7 @@ func (e *StateExecutor) regionOrderChoice(where string, states []*ast.StateNode, for i, state := range states { fps[i] = footprint(state) } + choice.alike = e.ctx.heldAlike classifyChoice(&choice, fps, nil) choice.Taken = e.ctx.scheduling().choose(choice, nil) choice.Span = states[choice.Taken].Span() @@ -4297,6 +4299,7 @@ func (e *StateExecutor) stepOrderChoice(due []*doAction, dispatch string) Choice for _, act := range due { steps = unionFootprints(steps, doStepFootprint(e, act.state)) } + choice.alike = e.ctx.heldAlike classifyChoice(&choice, []lower.Footprint{steps, dispatchFootprint(e)}, nil) return choice } diff --git a/internal/exec/runtime/state_run_to_completion.go b/internal/exec/runtime/state_run_to_completion.go index 21a6d4cc0e..cce5157d94 100644 --- a/internal/exec/runtime/state_run_to_completion.go +++ b/internal/exec/runtime/state_run_to_completion.go @@ -241,6 +241,7 @@ func (e *StateExecutor) entryStep(progress *dueProgress) (bool, error) { File: e.stateMachine.DocName, Span: e.stateMachine.DeclSpan, } + choice.alike = e.ctx.heldAlike classifyChoice(&choice, fps, nil) choice.Taken = e.ctx.scheduling().choose(choice, nil) if err := e.ctx.scheduling().refusal(); err != nil { diff --git a/internal/exec/runtime/state_unit_front.go b/internal/exec/runtime/state_unit_front.go index 3224eeb8c2..c636fb1cc2 100644 --- a/internal/exec/runtime/state_unit_front.go +++ b/internal/exec/runtime/state_unit_front.go @@ -522,6 +522,7 @@ func (e *StateExecutor) drawOnPath(head unitHead) error { alternatives = append(alternatives, head.label) fps = append(fps, e.headFootprint(head)) choice := ChoicePoint{Kind: choiceEntryOrder, Where: head.site, Alternatives: alternatives, File: e.stateMachine.DocName} + choice.alike = e.ctx.heldAlike classifyChoice(&choice, fps, nil) pick := e.ctx.scheduling().choose(choice, nil) if err := e.ctx.scheduling().refusal(); err != nil { @@ -596,6 +597,7 @@ func (f *unitFront) drain() (err error) { for i, q := range ready { fps[i] = q.footprint } + choice.alike = f.exec.ctx.heldAlike classifyChoice(&choice, fps, nil) pick = f.exec.ctx.scheduling().choose(choice, nil) if err := f.exec.ctx.scheduling().refusal(); err != nil { diff --git a/internal/exec/runtime/statements.go b/internal/exec/runtime/statements.go index 50673da4b3..fc5f297773 100644 --- a/internal/exec/runtime/statements.go +++ b/internal/exec/runtime/statements.go @@ -824,6 +824,7 @@ func (e *stmtEngine) pickStatement(stmts []lower.Statement, next []int, order *l Where: statementsWherePrefix + e.host.describe(), Alternatives: alts, } + choice.alike = e.ctx.heldAlike classifyBy(&choice, fps, func(a, b int) bool { return order.Dependent(next[a], next[b], divided) }, func(int, int) lower.Relation { return lower.Relation{} }) if e.ctx.statementOrderSweep != nil { diff --git a/internal/exec/runtime/testdata/conformance/action_explore_statement_order_calc.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_explore_statement_order_calc.seed-1.trace.golden index 18699a96c1..e2e6ab790c 100644 --- a/internal/exec/runtime/testdata/conformance/action_explore_statement_order_calc.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/action_explore_statement_order_calc.seed-1.trace.golden @@ -1,5 +1,5 @@ step 1: token 1@s -choice statements in action node s: next 1 assign v, 2 assign doubled (unordered; took 2 assign doubled first; order-dependent: v) +choice statements in action node s: next 1 assign v, 2 assign doubled (unordered; took 2 assign doubled first; order-dependent: doubled) stmt assign doubled enter calc test::CalcOrder::s::t eval feature v -> 1.0 diff --git a/internal/exec/runtime/testdata/conformance/action_explore_statement_order_dependent.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_explore_statement_order_dependent.seed-1.trace.golden index 247145848a..254f5375f4 100644 --- a/internal/exec/runtime/testdata/conformance/action_explore_statement_order_dependent.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/action_explore_statement_order_dependent.seed-1.trace.golden @@ -1,5 +1,5 @@ step 1: token 1@s -choice statements in action node s: next 1 assign x, 2 assign y (unordered; took 2 assign y first; order-dependent: x) +choice statements in action node s: next 1 assign x, 2 assign y (unordered; took 2 assign y first; order-dependent: y) stmt assign y eval feature x -> 0 stmt assign x diff --git a/internal/exec/runtime/testdata/conformance/action_explore_statement_order_if.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_explore_statement_order_if.seed-1.trace.golden index 4ab8e3cba0..afe621c475 100644 --- a/internal/exec/runtime/testdata/conformance/action_explore_statement_order_if.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/action_explore_statement_order_if.seed-1.trace.golden @@ -1,5 +1,5 @@ step 1: token 1@s -choice statements in action node s: next 1 if, 2 assign x (unordered; took 2 assign x first; order-dependent: x) +choice statements in action node s: next 1 if, 2 assign x (unordered; took 2 assign x first; order-dependent: y) stmt assign x eval literal 1 -> 1 stmt if diff --git a/internal/exec/runtime/testdata/conformance/action_explore_statement_order_read_first.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_explore_statement_order_read_first.seed-1.trace.golden index 8061bcd88e..50f0dfaea7 100644 --- a/internal/exec/runtime/testdata/conformance/action_explore_statement_order_read_first.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/action_explore_statement_order_read_first.seed-1.trace.golden @@ -1,5 +1,5 @@ step 1: token 1@s -choice statements in action node s: next 1 assign y, 2 assign x (unordered; took 2 assign x first; order-dependent: x) +choice statements in action node s: next 1 assign y, 2 assign x (unordered; took 2 assign x first; order-dependent: y) stmt assign x eval literal 1 -> 1 stmt assign y diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.check.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.check.expected.json new file mode 100644 index 0000000000..8f20489e8f --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.check.expected.json @@ -0,0 +1,4 @@ +{ + "verdict": "divergent", + "divergent": {"z": ["1", "2"]} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.declared.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.declared.trace.golden new file mode 100644 index 0000000000..4753960b89 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.declared.trace.golden @@ -0,0 +1,19 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign cell.mark + eval literal 1 -> 1 +materialize: cell #1 +stmt assign twin.mark + eval literal 2 -> 2 + eval feature cell -> instance#1 + eval feature twin -> instance#1 +choice step 3: writes mark of object #1 := 1 by token 2, mark of object #1 := 2 by token 3 (unordered; mark of object #1 := 2 by token 3 stood; order-dependent: mark) +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: mark) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z + eval feature cell -> instance#1 + eval feature twin -> instance#1 + eval chain mark -> 2 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.expected.json new file mode 100644 index 0000000000..67df31cf94 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.expected.json @@ -0,0 +1,35 @@ +{ + "type": "action", + "trace": true, + "admissible": "A feature reached through a part stands on the choice points its writers race at", + "outcomes": [ + { + "outputs": { + "cell.mark": { + "type": "Integer", + "value": 1, + "orderDependent": 2 + }, + "z": { + "type": "Integer", + "value": 1, + "orderDependent": 2 + } + } + }, + { + "outputs": { + "cell.mark": { + "type": "Integer", + "value": 2, + "orderDependent": 2 + }, + "z": { + "type": "Integer", + "value": 2, + "orderDependent": 2 + } + } + } + ] +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.seed-1.trace.golden new file mode 100644 index 0000000000..4753960b89 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.seed-1.trace.golden @@ -0,0 +1,19 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign cell.mark + eval literal 1 -> 1 +materialize: cell #1 +stmt assign twin.mark + eval literal 2 -> 2 + eval feature cell -> instance#1 + eval feature twin -> instance#1 +choice step 3: writes mark of object #1 := 1 by token 2, mark of object #1 := 2 by token 3 (unordered; mark of object #1 := 2 by token 3 stood; order-dependent: mark) +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: mark) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z + eval feature cell -> instance#1 + eval feature twin -> instance#1 + eval chain mark -> 2 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.sysml b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.sysml new file mode 100644 index 0000000000..58c1b91429 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.sysml @@ -0,0 +1,26 @@ +// Two features holding one object: `twin` references the cell `cell` names, so +// the branches writing through either chain race for that one object's mark, +// and both names stand on the order, as does what is read from either. +package test { + private import ScalarValues::*; + part def Cell { attribute mark : Integer = 0; } + action race { + part cell : Cell; + ref part twin : Cell = cell; + attribute z : Integer = 0; + first start; + fork split; + action a { assign cell.mark := 1; } + action b { assign twin.mark := 2; } + join sync; + action derive { assign z := twin.mark; } + done; + succession first start then split; + succession first split then a; + succession first split then b; + succession first a then sync; + succession first b then sync; + succession first sync then derive; + succession first derive then done; + } +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.trace.golden new file mode 100644 index 0000000000..b19509693d --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_alias_of_racing_writers.trace.golden @@ -0,0 +1,19 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign twin.mark + eval literal 2 -> 2 +materialize: cell #1 + eval feature cell -> instance#1 + eval feature twin -> instance#1 +stmt assign cell.mark + eval literal 1 -> 1 +choice step 3: writes mark of object #1 := 1 by token 2, mark of object #1 := 2 by token 3 (unordered; mark of object #1 := 1 by token 2 stood; order-dependent: mark) +choice step 3: tokens 2@a, 3@b (unordered; took 3@b first; order-dependent: mark) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z + eval feature cell -> instance#1 + eval feature twin -> instance#1 + eval chain mark -> 1 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.check.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.check.expected.json new file mode 100644 index 0000000000..26dc9d3e17 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.check.expected.json @@ -0,0 +1,4 @@ +{ + "verdict": "no violation, exhaustive", + "agreed": {"z": "0"} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.declared.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.declared.trace.golden new file mode 100644 index 0000000000..2e1afbf955 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.declared.trace.golden @@ -0,0 +1,16 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign left.raw + eval literal 1 -> 1 +materialize: left #1 +stmt assign left.raw + eval literal 2 -> 2 +choice step 3: writes raw of object #1 := 1 by token 2, raw of object #1 := 2 by token 3 (unordered; raw of object #1 := 2 by token 3 stood; order-dependent: raw) +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: raw) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z +materialize: right #2 + eval chain raw -> 0 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.expected.json new file mode 100644 index 0000000000..1aa0dafe17 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.expected.json @@ -0,0 +1,25 @@ +{ + "type": "action", + "trace": true, + "admissible": "A feature reached through a part stands on the choice points its writers race at", + "outcomes": [ + { + "outputs": { + "left.raw": {"type": "Integer", "value": 1, "orderDependent": 2}, + "left.scaled": {"type": "Integer", "value": 10, "orderDependent": 2}, + "right.raw": {"type": "Integer", "value": 0}, + "right.scaled": {"type": "Integer", "value": 0}, + "z": {"type": "Integer", "value": 0} + } + }, + { + "outputs": { + "left.raw": {"type": "Integer", "value": 2, "orderDependent": 2}, + "left.scaled": {"type": "Integer", "value": 20, "orderDependent": 2}, + "right.raw": {"type": "Integer", "value": 0}, + "right.scaled": {"type": "Integer", "value": 0}, + "z": {"type": "Integer", "value": 0} + } + } + ] +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.seed-1.trace.golden new file mode 100644 index 0000000000..2e1afbf955 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.seed-1.trace.golden @@ -0,0 +1,16 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign left.raw + eval literal 1 -> 1 +materialize: left #1 +stmt assign left.raw + eval literal 2 -> 2 +choice step 3: writes raw of object #1 := 1 by token 2, raw of object #1 := 2 by token 3 (unordered; raw of object #1 := 2 by token 3 stood; order-dependent: raw) +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: raw) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z +materialize: right #2 + eval chain raw -> 0 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.sysml b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.sysml new file mode 100644 index 0000000000..d30f079e0a --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.sysml @@ -0,0 +1,25 @@ +// Two parts of one definition: the race on left.raw leaves right.raw, what is +// computed from it, and the write read from it where they stand. +package test { + private import ScalarValues::*; + part def Sensor { attribute raw : Integer = 0; attribute scaled : Integer = raw * 10; } + action race { + part left : Sensor; + part right : Sensor; + attribute z : Integer = 0; + first start; + fork split; + action a { assign left.raw := 1; } + action b { assign left.raw := 2; } + join sync; + action derive { assign z := right.raw; } + done; + succession first start then split; + succession first split then a; + succession first split then b; + succession first a then sync; + succession first b then sync; + succession first sync then derive; + succession first derive then done; + } +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.trace.golden new file mode 100644 index 0000000000..520a8cf309 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_parts_apart.trace.golden @@ -0,0 +1,16 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign left.raw + eval literal 2 -> 2 +materialize: left #1 +stmt assign left.raw + eval literal 1 -> 1 +choice step 3: writes raw of object #1 := 1 by token 2, raw of object #1 := 2 by token 3 (unordered; raw of object #1 := 1 by token 2 stood; order-dependent: raw) +choice step 3: tokens 2@a, 3@b (unordered; took 3@b first; order-dependent: raw) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z +materialize: right #2 + eval chain raw -> 0 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.check.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.check.expected.json new file mode 100644 index 0000000000..ddde6cf1c8 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.check.expected.json @@ -0,0 +1,5 @@ +{ + "verdict": "divergent", + "divergent": {"w": ["1", "2"], "x": ["1", "2"]}, + "agreed": {"z": "7", "zz": "70"} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.declared.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.declared.trace.golden new file mode 100644 index 0000000000..7c15dd4eb0 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.declared.trace.golden @@ -0,0 +1,25 @@ +step 1: token 1@prime +stmt assign sensor.raw + eval literal 7 -> 7 +materialize: sensor #1 +step 2: token 1@split +step 3: token 2@a, token 3@b +stmt assign x + eval literal 1 -> 1 +stmt assign x + eval literal 2 -> 2 +choice step 4: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 2 by token 3 stood; order-dependent: x) +choice step 4: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: x) +step 4: token 2@sync, token 3@sync +step 5: token 4@derive +stmt assign z + eval chain raw -> 7 +stmt assign zz + eval feature raw -> 7 + eval literal 10 -> 10 + eval operator * -> 70 + eval chain scaled -> 70 +stmt assign w + eval feature x -> 2 +step 6: token 4@done +step 7: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.expected.json new file mode 100644 index 0000000000..8c9f14b9d8 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.expected.json @@ -0,0 +1,28 @@ +{ + "type": "action", + "trace": true, + "outcomes": [ + { + "outputs": { + "sensor.raw": {"type": "Integer", "value": 7}, + "sensor.scaled": {"type": "Integer", "value": 70}, + "w": {"type": "Integer", "value": 1}, + "x": {"type": "Integer", "value": 1}, + "z": {"type": "Integer", "value": 7}, + "zz": {"type": "Integer", "value": 70} + } + }, + { + "outputs": { + "sensor.raw": {"type": "Integer", "value": 7}, + "sensor.scaled": {"type": "Integer", "value": 70}, + "w": {"type": "Integer", "value": 2}, + "x": {"type": "Integer", "value": 2}, + "z": {"type": "Integer", "value": 7}, + "zz": {"type": "Integer", "value": 70} + } + } + ], + "admissible": "A feature reached through a part stands on the choice points its writers race at", + "orderDependent": {"x": 2, "w": 2} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.seed-1.trace.golden new file mode 100644 index 0000000000..7c15dd4eb0 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.seed-1.trace.golden @@ -0,0 +1,25 @@ +step 1: token 1@prime +stmt assign sensor.raw + eval literal 7 -> 7 +materialize: sensor #1 +step 2: token 1@split +step 3: token 2@a, token 3@b +stmt assign x + eval literal 1 -> 1 +stmt assign x + eval literal 2 -> 2 +choice step 4: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 2 by token 3 stood; order-dependent: x) +choice step 4: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: x) +step 4: token 2@sync, token 3@sync +step 5: token 4@derive +stmt assign z + eval chain raw -> 7 +stmt assign zz + eval feature raw -> 7 + eval literal 10 -> 10 + eval operator * -> 70 + eval chain scaled -> 70 +stmt assign w + eval feature x -> 2 +step 6: token 4@done +step 7: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.sysml b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.sysml new file mode 100644 index 0000000000..278099e71b --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.sysml @@ -0,0 +1,41 @@ +package test { + private import ScalarValues::*; + + // Two branches race on `x`, and `sensor.raw`, written once before the fork, + // is read after the join: the race is on another place, so what is read + // through the part stays bare while `x` and the read of `x` stand open. + part def Sensor { + attribute raw : Integer = 0; + attribute scaled : Integer = raw * 10; + } + + action race { + part sensor : Sensor; + attribute x : Integer = 0; + attribute z : Integer = 0; + attribute zz : Integer = 0; + attribute w : Integer = 0; + + first start; + action prime { assign sensor.raw := 7; } + fork split; + action a { assign x := 1; } + action b { assign x := 2; } + join sync; + action derive { + assign z := sensor.raw; + assign zz := sensor.scaled; + assign w := x; + } + done; + + succession first start then prime; + succession first prime then split; + succession first split then a; + succession first split then b; + succession first a then sync; + succession first b then sync; + succession first sync then derive; + succession first derive then done; + } +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.trace.golden new file mode 100644 index 0000000000..0ca3e881bf --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_read_of_unraced_stays_bare.trace.golden @@ -0,0 +1,25 @@ +step 1: token 1@prime +stmt assign sensor.raw + eval literal 7 -> 7 +materialize: sensor #1 +step 2: token 1@split +step 3: token 2@a, token 3@b +stmt assign x + eval literal 2 -> 2 +stmt assign x + eval literal 1 -> 1 +choice step 4: writes x := 1 by token 2, x := 2 by token 3 (unordered; x := 1 by token 2 stood; order-dependent: x) +choice step 4: tokens 2@a, 3@b (unordered; took 3@b first; order-dependent: x) +step 4: token 2@sync, token 3@sync +step 5: token 4@derive +stmt assign z + eval chain raw -> 7 +stmt assign zz + eval feature raw -> 7 + eval literal 10 -> 10 + eval operator * -> 70 + eval chain scaled -> 70 +stmt assign w + eval feature x -> 1 +step 6: token 4@done +step 7: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.check.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.check.expected.json new file mode 100644 index 0000000000..63e5315e75 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.check.expected.json @@ -0,0 +1,5 @@ +{ + "verdict": "divergent", + "divergent": {"z": ["1", "2"]}, + "agreed": {"m": "1200"} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.declared.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.declared.trace.golden new file mode 100644 index 0000000000..458a761382 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.declared.trace.golden @@ -0,0 +1,18 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign car.engine.rpm + eval literal 1 -> 1 +materialize: car #1 +materialize: Engine #2 +stmt assign car.engine.rpm + eval literal 2 -> 2 +choice step 3: writes rpm of object #2 := 1 by token 2, rpm of object #2 := 2 by token 3 (unordered; rpm of object #2 := 2 by token 3 stood; order-dependent: rpm) +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: rpm) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z + eval chain rpm -> 2 +stmt assign m + eval chain mass -> 1200 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.expected.json new file mode 100644 index 0000000000..5e80e6aceb --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.expected.json @@ -0,0 +1,22 @@ +{ + "type": "action", + "trace": true, + "outcomes": [ + { + "outputs": { + "car.mass": {"type": "Integer", "value": 1200}, + "m": {"type": "Integer", "value": 1200}, + "z": {"type": "Integer", "value": 1} + } + }, + { + "outputs": { + "car.mass": {"type": "Integer", "value": 1200}, + "m": {"type": "Integer", "value": 1200}, + "z": {"type": "Integer", "value": 2} + } + } + ], + "admissible": "A feature reached through a part stands on the choice points its writers race at", + "orderDependent": {"z": 2} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.seed-1.trace.golden new file mode 100644 index 0000000000..458a761382 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.seed-1.trace.golden @@ -0,0 +1,18 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign car.engine.rpm + eval literal 1 -> 1 +materialize: car #1 +materialize: Engine #2 +stmt assign car.engine.rpm + eval literal 2 -> 2 +choice step 3: writes rpm of object #2 := 1 by token 2, rpm of object #2 := 2 by token 3 (unordered; rpm of object #2 := 2 by token 3 stood; order-dependent: rpm) +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: rpm) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z + eval chain rpm -> 2 +stmt assign m + eval chain mass -> 1200 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.sysml b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.sysml new file mode 100644 index 0000000000..539c3795f1 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.sysml @@ -0,0 +1,37 @@ +package test { + private import ScalarValues::*; + + // Two branches each write `car.engine.rpm`, two parts deep: the race is on + // the place the whole chain reaches, and the value read from it after the + // join stands on it, while `car.mass`, which neither branch touches, stays bare. + part def Engine { attribute rpm : Integer = 0; } + part def Car { + attribute mass : Integer = 1200; + part engine : Engine; + } + + action race { + part car : Car; + attribute z : Integer = 0; + attribute m : Integer = 0; + + first start; + fork split; + action a { assign car.engine.rpm := 1; } + action b { assign car.engine.rpm := 2; } + join sync; + action derive { + assign z := car.engine.rpm; + assign m := car.mass; + } + done; + + succession first start then split; + succession first split then a; + succession first split then b; + succession first a then sync; + succession first b then sync; + succession first sync then derive; + succession first derive then done; + } +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.trace.golden new file mode 100644 index 0000000000..0d284a0e81 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_two_level_write.trace.golden @@ -0,0 +1,18 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign car.engine.rpm + eval literal 2 -> 2 +materialize: car #1 +materialize: Engine #2 +stmt assign car.engine.rpm + eval literal 1 -> 1 +choice step 3: writes rpm of object #2 := 1 by token 2, rpm of object #2 := 2 by token 3 (unordered; rpm of object #2 := 1 by token 2 stood; order-dependent: rpm) +choice step 3: tokens 2@a, 3@b (unordered; took 3@b first; order-dependent: rpm) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z + eval chain rpm -> 1 +stmt assign m + eval chain mass -> 1200 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.check.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.check.expected.json new file mode 100644 index 0000000000..1d4592b5d1 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.check.expected.json @@ -0,0 +1,5 @@ +{ + "verdict": "divergent", + "divergent": {"z": ["1", "2"], "zz": ["10", "20"]}, + "agreed": {} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.declared.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.declared.trace.golden new file mode 100644 index 0000000000..a0b38b8a78 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.declared.trace.golden @@ -0,0 +1,20 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign sensor.raw + eval literal 1 -> 1 +materialize: sensor #1 +stmt assign sensor.raw + eval literal 2 -> 2 +choice step 3: writes raw of object #1 := 1 by token 2, raw of object #1 := 2 by token 3 (unordered; raw of object #1 := 2 by token 3 stood; order-dependent: raw) +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: raw) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z + eval chain raw -> 2 +stmt assign zz + eval feature raw -> 2 + eval literal 10 -> 10 + eval operator * -> 20 + eval chain scaled -> 20 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.expected.json b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.expected.json new file mode 100644 index 0000000000..da8c697654 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.expected.json @@ -0,0 +1,24 @@ +{ + "type": "action", + "trace": true, + "outcomes": [ + { + "outputs": { + "sensor.raw": {"type": "Integer", "value": 1}, + "sensor.scaled": {"type": "Integer", "value": 10}, + "z": {"type": "Integer", "value": 1}, + "zz": {"type": "Integer", "value": 10} + } + }, + { + "outputs": { + "sensor.raw": {"type": "Integer", "value": 2}, + "sensor.scaled": {"type": "Integer", "value": 20}, + "z": {"type": "Integer", "value": 2}, + "zz": {"type": "Integer", "value": 20} + } + } + ], + "admissible": "A feature reached through a part stands on the choice points its writers race at", + "orderDependent": {"sensor.raw": 2, "sensor.scaled": 2, "z": 2, "zz": 2} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.seed-1.trace.golden new file mode 100644 index 0000000000..a0b38b8a78 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.seed-1.trace.golden @@ -0,0 +1,20 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign sensor.raw + eval literal 1 -> 1 +materialize: sensor #1 +stmt assign sensor.raw + eval literal 2 -> 2 +choice step 3: writes raw of object #1 := 1 by token 2, raw of object #1 := 2 by token 3 (unordered; raw of object #1 := 2 by token 3 stood; order-dependent: raw) +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: raw) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z + eval chain raw -> 2 +stmt assign zz + eval feature raw -> 2 + eval literal 10 -> 10 + eval operator * -> 20 + eval chain scaled -> 20 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.sysml b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.sysml new file mode 100644 index 0000000000..ec31a815a6 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.sysml @@ -0,0 +1,38 @@ +package test { + private import ScalarValues::*; + + // Two branches between one fork and one join each write `sensor.raw`, a + // feature reached through the action's part: the library orders neither + // write before the other, so the chained place stands open, as does + // `sensor.scaled`, valued by an expression over it, and the two values the + // read after the join writes from them. + part def Sensor { + attribute raw : Integer = 0; + attribute scaled : Integer = raw * 10; + } + + action race { + part sensor : Sensor; + attribute z : Integer = 0; + attribute zz : Integer = 0; + + first start; + fork split; + action a { assign sensor.raw := 1; } + action b { assign sensor.raw := 2; } + join sync; + action derive { + assign z := sensor.raw; + assign zz := sensor.scaled; + } + done; + + succession first start then split; + succession first split then a; + succession first split then b; + succession first a then sync; + succession first b then sync; + succession first sync then derive; + succession first derive then done; + } +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.trace.golden new file mode 100644 index 0000000000..8bcdae0173 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_chained_write_of_racing_writers.trace.golden @@ -0,0 +1,20 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign sensor.raw + eval literal 2 -> 2 +materialize: sensor #1 +stmt assign sensor.raw + eval literal 1 -> 1 +choice step 3: writes raw of object #1 := 1 by token 2, raw of object #1 := 2 by token 3 (unordered; raw of object #1 := 1 by token 2 stood; order-dependent: raw) +choice step 3: tokens 2@a, 3@b (unordered; took 3@b first; order-dependent: raw) +step 3: token 2@sync, token 3@sync +step 4: token 4@derive +stmt assign z + eval chain raw -> 1 +stmt assign zz + eval feature raw -> 1 + eval literal 10 -> 10 + eval operator * -> 10 + eval chain scaled -> 10 +step 5: token 4@done +step 6: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.check.expected.json b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.check.expected.json new file mode 100644 index 0000000000..f923fcb58a --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.check.expected.json @@ -0,0 +1,5 @@ +{ + "verdict": "divergent", + "divergent": {"z": ["0", "1"]}, + "agreed": {"x": "1"} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.declared.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.declared.trace.golden new file mode 100644 index 0000000000..2765214d42 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.declared.trace.golden @@ -0,0 +1,10 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign x + eval literal 1 -> 1 +stmt assign z + eval feature x -> 1 +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: z) +step 3: token 2@sync, token 3@sync +step 4: token 4@done +step 5: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.expected.json b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.expected.json new file mode 100644 index 0000000000..fbc9444920 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.expected.json @@ -0,0 +1,20 @@ +{ + "type": "action", + "trace": true, + "outcomes": [ + { + "outputs": { + "x": {"type": "Integer", "value": 1}, + "z": {"type": "Integer", "value": 0} + } + }, + { + "outputs": { + "x": {"type": "Integer", "value": 1}, + "z": {"type": "Integer", "value": 1} + } + } + ], + "admissible": "A read racing a write of the same feature stands on the choice point between them", + "orderDependent": {"z": 1} +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.seed-1.trace.golden new file mode 100644 index 0000000000..2765214d42 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.seed-1.trace.golden @@ -0,0 +1,10 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign x + eval literal 1 -> 1 +stmt assign z + eval feature x -> 1 +choice step 3: tokens 2@a, 3@b (unordered; took 2@a first; order-dependent: z) +step 3: token 2@sync, token 3@sync +step 4: token 4@done +step 5: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.sysml b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.sysml new file mode 100644 index 0000000000..02fad1b5c3 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.sysml @@ -0,0 +1,26 @@ +package test { + private import ScalarValues::*; + + // Between one fork and one join, one branch writes `x` while its sibling + // reads `x` into `z`: the library orders neither before the other, so the + // read may see either value and `z` stands open, while `x`, written once, + // holds `1` whichever order ran. + action race { + attribute x : Integer = 0; + attribute z : Integer = 0; + + first start; + fork split; + action a { assign x := 1; } + action b { assign z := x; } + join sync; + done; + + succession first start then split; + succession first split then a; + succession first split then b; + succession first a then sync; + succession first b then sync; + succession first sync then done; + } +} diff --git a/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.trace.golden b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.trace.golden new file mode 100644 index 0000000000..5350dcd07d --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_order_sibling_read_of_racing_write.trace.golden @@ -0,0 +1,10 @@ +step 1: token 1@split +step 2: token 2@a, token 3@b +stmt assign z + eval feature x -> 0 +stmt assign x + eval literal 1 -> 1 +choice step 3: tokens 2@a, 3@b (unordered; took 3@b first; order-dependent: z) +step 3: token 2@sync, token 3@sync +step 4: token 4@done +step 5: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.declared.trace.golden b/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.declared.trace.golden index 67086f9d90..0e9bd6bdc6 100644 --- a/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.declared.trace.golden @@ -13,7 +13,7 @@ run: exhibited state machine blinking of #1 step 2: token 1@wait eval literal 5 -> 5 eval index -> 5 [s] -choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran action watcher first; order-dependent: lit) +choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran action watcher first; order-dependent: sawLit) step 3: token 1@look stmt assign sawLit eval chain lit -> false diff --git a/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.seed-1.trace.golden index eca59af6fe..e1396550e9 100644 --- a/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.seed-1.trace.golden @@ -13,7 +13,7 @@ run: exhibited state machine blinking of #1 step 2: token 1@wait eval literal 5 -> 5 eval index -> 5 [s] -choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran state machine blinking of object #1 first; order-dependent: lit) +choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran state machine blinking of object #1 first; order-dependent: sawLit) run: exhibited state machine blinking of #1 exit: dark enter: shining (entry action) diff --git a/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.trace.golden b/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.trace.golden index eca59af6fe..e1396550e9 100644 --- a/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.trace.golden +++ b/internal/exec/runtime/testdata/conformance/clock_action_state_due_together.trace.golden @@ -13,7 +13,7 @@ run: exhibited state machine blinking of #1 step 2: token 1@wait eval literal 5 -> 5 eval index -> 5 [s] -choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran state machine blinking of object #1 first; order-dependent: lit) +choice at t=5.0: due action watcher, state machine blinking of object #1 (unordered; ran state machine blinking of object #1 first; order-dependent: sawLit) run: exhibited state machine blinking of #1 exit: dark enter: shining (entry action) diff --git a/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.declared.trace.golden index c44e63f7f1..dad11a565e 100644 --- a/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.declared.trace.golden @@ -1,7 +1,7 @@ exit: lstart enter: lwork transition: lstart -> lwork -choice at t=0.0: next do lwork, dispatch completion rstart 1->rwork (unordered; took do lwork first; order-dependent: seq) +choice at t=0.0: next do lwork, dispatch completion rstart 1->rwork (unordered; took do lwork first; order-dependent: i, seq) do: lwork stmt action body enter action node: state behavior @@ -19,7 +19,7 @@ enter action node: state behavior exit: rstart enter: rwork transition: rstart -> rwork -choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first; order-dependent: seq) +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first; order-dependent: i, seq) do: lwork iteration 2 stmt assign seq diff --git a/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.seed-1.trace.golden index a6cb7f301e..0b8abe20b6 100644 --- a/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.seed-1.trace.golden @@ -1,7 +1,7 @@ exit: rstart enter: rwork transition: rstart -> rwork -choice at t=0.0: next do rwork, dispatch completion lstart 1->lwork (unordered; took do rwork first; order-dependent: seq) +choice at t=0.0: next do rwork, dispatch completion lstart 1->lwork (unordered; took do rwork first; order-dependent: i, seq) do: rwork stmt action body enter action node: state behavior @@ -14,7 +14,7 @@ enter action node: state behavior exit: lstart enter: lwork transition: lstart -> lwork -choice do round at t=0.0: states rwork, lwork react (unordered; took rwork first; order-dependent: seq) +choice do round at t=0.0: states rwork, lwork react (unordered; took rwork first; order-dependent: i, seq) do: rwork stmt if eval feature seq -> 4 @@ -41,7 +41,7 @@ enter action node: state behavior eval operator * -> 450 eval feature i -> 1 eval operator + -> 451 -choice do round at t=0.0: states rwork, lwork react (unordered; took rwork first; order-dependent: seq) +choice do round at t=0.0: states rwork, lwork react (unordered; took rwork first; order-dependent: i, seq) do: rwork stmt assign seq eval feature seq -> 451 diff --git a/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.trace.golden b/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.trace.golden index c44e63f7f1..dad11a565e 100644 --- a/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_concurrent_inline_do_bodies.trace.golden @@ -1,7 +1,7 @@ exit: lstart enter: lwork transition: lstart -> lwork -choice at t=0.0: next do lwork, dispatch completion rstart 1->rwork (unordered; took do lwork first; order-dependent: seq) +choice at t=0.0: next do lwork, dispatch completion rstart 1->rwork (unordered; took do lwork first; order-dependent: i, seq) do: lwork stmt action body enter action node: state behavior @@ -19,7 +19,7 @@ enter action node: state behavior exit: rstart enter: rwork transition: rstart -> rwork -choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first; order-dependent: seq) +choice do round at t=0.0: states lwork, rwork react (unordered; took lwork first; order-dependent: i, seq) do: lwork iteration 2 stmt assign seq diff --git a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.declared.trace.golden index b6b4309838..d5be0653e3 100644 --- a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.declared.trace.golden @@ -1,4 +1,4 @@ -choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count) +choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count, n) do: top stmt action body enter action node: state behavior run diff --git a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.seed-1.trace.golden index b6b4309838..d5be0653e3 100644 --- a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.seed-1.trace.golden @@ -1,4 +1,4 @@ -choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count) +choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count, n) do: top stmt action body enter action node: state behavior run diff --git a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.trace.golden b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.trace.golden index b6b4309838..d5be0653e3 100644 --- a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_nested_perform.trace.golden @@ -1,4 +1,4 @@ -choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count) +choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count, n) do: top stmt action body enter action node: state behavior run diff --git a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.declared.trace.golden index 71b2276a34..d754cbfd42 100644 --- a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.declared.trace.golden @@ -1,4 +1,4 @@ -choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count) +choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count, n) do: top stmt action body stmt node work diff --git a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.seed-1.trace.golden index 71b2276a34..d754cbfd42 100644 --- a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.seed-1.trace.golden @@ -1,4 +1,4 @@ -choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count) +choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count, n) do: top stmt action body stmt node work diff --git a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.trace.golden b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.trace.golden index 71b2276a34..d754cbfd42 100644 --- a/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_do_step_cuts_typed_do.trace.golden @@ -1,4 +1,4 @@ -choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count) +choice at t=0.0: next do top, dispatch accept Stop (unordered; took do top first; order-dependent: count, n) do: top stmt action body stmt node work diff --git a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.declared.trace.golden index 6a2b190652..28f6b44ad8 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.declared.trace.golden @@ -8,7 +8,7 @@ eval operator > -> true eval operator / -> 2.0 eval literal 1 -> 1 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.seed-1.trace.golden index 6a2b190652..28f6b44ad8 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.seed-1.trace.golden @@ -8,7 +8,7 @@ eval operator > -> true eval operator / -> 2.0 eval literal 1 -> 1 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.trace.golden index 6a2b190652..28f6b44ad8 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once.trace.golden @@ -8,7 +8,7 @@ eval operator > -> true eval operator / -> 2.0 eval literal 1 -> 1 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.declared.trace.golden index 6a2b190652..28f6b44ad8 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.declared.trace.golden @@ -8,7 +8,7 @@ eval operator > -> true eval operator / -> 2.0 eval literal 1 -> 1 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.seed-1.trace.golden index 6a2b190652..28f6b44ad8 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.seed-1.trace.golden @@ -8,7 +8,7 @@ eval operator > -> true eval operator / -> 2.0 eval literal 1 -> 1 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.trace.golden index 6a2b190652..28f6b44ad8 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_beyond_a_draw_read_once_metadata.trace.golden @@ -8,7 +8,7 @@ eval operator > -> true eval operator / -> 2.0 eval literal 1 -> 1 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.declared.trace.golden index 1ffcac2f26..f366643e66 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.declared.trace.golden @@ -1,5 +1,5 @@ eval feature armed -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: armed) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign armed eval literal false -> false diff --git a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.seed-1.trace.golden index 1ffcac2f26..f366643e66 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.seed-1.trace.golden @@ -1,5 +1,5 @@ eval feature armed -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: armed) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign armed eval literal false -> false diff --git a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.trace.golden index 1ffcac2f26..f366643e66 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires.trace.golden @@ -1,5 +1,5 @@ eval feature armed -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: armed) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign armed eval literal false -> false diff --git a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.declared.trace.golden index 1ffcac2f26..f366643e66 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.declared.trace.golden @@ -1,5 +1,5 @@ eval feature armed -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: armed) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign armed eval literal false -> false diff --git a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.seed-1.trace.golden index 1ffcac2f26..f366643e66 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.seed-1.trace.golden @@ -1,5 +1,5 @@ eval feature armed -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: armed) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign armed eval literal false -> false diff --git a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.trace.golden index 1ffcac2f26..f366643e66 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_drawn_as_its_transition_fires_metadata.trace.golden @@ -1,5 +1,5 @@ eval feature armed -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: armed) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign armed eval literal false -> false diff --git a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.declared.trace.golden index 3ca5b2da97..786aece1dc 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.declared.trace.golden @@ -1,7 +1,7 @@ eval feature v -> 4 eval literal 0 -> 0 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.seed-1.trace.golden index 3ca5b2da97..786aece1dc 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.seed-1.trace.golden @@ -1,7 +1,7 @@ eval feature v -> 4 eval literal 0 -> 0 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.trace.golden index 3ca5b2da97..786aece1dc 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once.trace.golden @@ -1,7 +1,7 @@ eval feature v -> 4 eval literal 0 -> 0 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.declared.trace.golden index 3ca5b2da97..786aece1dc 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.declared.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.declared.trace.golden @@ -1,7 +1,7 @@ eval feature v -> 4 eval literal 0 -> 0 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.seed-1.trace.golden index 3ca5b2da97..786aece1dc 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.seed-1.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.seed-1.trace.golden @@ -1,7 +1,7 @@ eval feature v -> 4 eval literal 0 -> 0 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.trace.golden b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.trace.golden index 3ca5b2da97..786aece1dc 100644 --- a/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.trace.golden +++ b/internal/exec/runtime/testdata/conformance/state_junction_guards_read_once_metadata.trace.golden @@ -1,7 +1,7 @@ eval feature v -> 4 eval literal 0 -> 0 eval operator > -> true -choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: d) +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route) exit: a1 stmt assign d eval literal 0 -> 0 diff --git a/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.check.expected.json b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.check.expected.json new file mode 100644 index 0000000000..02422ea6fc --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.check.expected.json @@ -0,0 +1,5 @@ +{ + "verdict": "divergent", + "divergent": {"finalState": ["a2+b1", "a2+left", "a2+right"], "route": ["0", "1", "2"], "seen": ["false", "true"]}, + "agreed": {"armed": "false"} +} diff --git a/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.declared.trace.golden b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.declared.trace.golden new file mode 100644 index 0000000000..19f03e6999 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.declared.trace.golden @@ -0,0 +1,8 @@ +eval feature armed -> true +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route, seen) +exit: a1 +stmt assign armed + eval literal false -> false +enter: a2 +transition: a1 -> a2 (event: accept Go) +eval feature armed -> false diff --git a/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.expected.json b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.expected.json new file mode 100644 index 0000000000..74762ce70d --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.expected.json @@ -0,0 +1,166 @@ +{ + "type": "state", + "trace": true, + "events": [ + { + "signal": "Go" + } + ], + "admissible": "A read racing a write of the same feature stands on the choice point between them", + "outcomes": [ + { + "finalState": "a2+b1", + "stateVisits": [ + "work", + "a1", + "b1", + "a2" + ], + "outputs": { + "armed": { + "type": "Boolean", + "value": false + }, + "route": { + "type": "Integer", + "value": 0, + "orderDependent": 1 + }, + "seen": { + "type": "Boolean", + "value": false, + "orderDependent": 1 + } + } + }, + { + "finalState": "a2+b1", + "stateVisits": [ + "work", + "b1", + "a1", + "a2" + ], + "outputs": { + "armed": { + "type": "Boolean", + "value": false + }, + "route": { + "type": "Integer", + "value": 0, + "orderDependent": 1 + }, + "seen": { + "type": "Boolean", + "value": false, + "orderDependent": 1 + } + } + }, + { + "finalState": "a2+left", + "stateVisits": [ + "work", + "a1", + "b1", + "left", + "a2" + ], + "outputs": { + "armed": { + "type": "Boolean", + "value": false + }, + "route": { + "type": "Integer", + "value": 1, + "orderDependent": 1 + }, + "seen": { + "type": "Boolean", + "value": true, + "orderDependent": 1 + } + } + }, + { + "finalState": "a2+left", + "stateVisits": [ + "work", + "b1", + "a1", + "left", + "a2" + ], + "outputs": { + "armed": { + "type": "Boolean", + "value": false + }, + "route": { + "type": "Integer", + "value": 1, + "orderDependent": 1 + }, + "seen": { + "type": "Boolean", + "value": true, + "orderDependent": 1 + } + } + }, + { + "finalState": "a2+right", + "stateVisits": [ + "work", + "a1", + "b1", + "right", + "a2" + ], + "outputs": { + "armed": { + "type": "Boolean", + "value": false + }, + "route": { + "type": "Integer", + "value": 2, + "orderDependent": 1 + }, + "seen": { + "type": "Boolean", + "value": false, + "orderDependent": 1 + } + } + }, + { + "finalState": "a2+right", + "stateVisits": [ + "work", + "b1", + "a1", + "right", + "a2" + ], + "outputs": { + "armed": { + "type": "Boolean", + "value": false + }, + "route": { + "type": "Integer", + "value": 2, + "orderDependent": 1 + }, + "seen": { + "type": "Boolean", + "value": false, + "orderDependent": 1 + } + } + } + ] +} diff --git a/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.seed-1.trace.golden b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.seed-1.trace.golden new file mode 100644 index 0000000000..19f03e6999 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.seed-1.trace.golden @@ -0,0 +1,8 @@ +eval feature armed -> true +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route, seen) +exit: a1 +stmt assign armed + eval literal false -> false +enter: a2 +transition: a1 -> a2 (event: accept Go) +eval feature armed -> false diff --git a/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.sysml b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.sysml new file mode 100644 index 0000000000..e9fbc90299 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.sysml @@ -0,0 +1,32 @@ +// One Go enables a transition in each region of `work`. Region a's disarms the +// guard of region b's, whose target is a junction drawn once b's transition +// fires; the left branch writes route from nothing and seen from the guard's own +// feature. The guard, read as b's transition fires, races a's write: whether +// either branch effect ran stands on the order, so route stands on it as seen does. +package Test { + state Machine { + attribute armed : Boolean = true; + attribute route : Integer = 0; + attribute seen : Boolean = false; + + entry; then work; + state work parallel { + state a { + entry; then a1; + state a1; + state a2; + transition first a1 accept Go do assign armed := false then a2; + } + state b { + entry; then b1; + state b1; + junction split; + state left; + state right; + transition first b1 accept Go if armed then split; + transition first split do action both { assign route := 1; assign seen := armed; } then left; + transition first split do assign route := 2 then right; + } + } + } +} diff --git a/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.trace.golden b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.trace.golden new file mode 100644 index 0000000000..19f03e6999 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/state_order_guard_and_effect_read_racing_write.trace.golden @@ -0,0 +1,8 @@ +eval feature armed -> true +choice on accept Go: next a1(exit), b1(exit) (unordered; took a1(exit) first; order-dependent: route, seen) +exit: a1 +stmt assign armed + eval literal false -> false +enter: a2 +transition: a1 -> a2 (event: accept Go) +eval feature armed -> false diff --git a/internal/ir/lower/footprint.go b/internal/ir/lower/footprint.go index 63bd93984f..d72ac831be 100644 --- a/internal/ir/lower/footprint.go +++ b/internal/ir/lower/footprint.go @@ -20,12 +20,16 @@ import ( // (nil when unresolved) and the name; Local marks a pin, held per performance. // State marks the activity of a state, which a transition reads and writes. // Direct marks a name written alone, not reached through a chain or qualified. +// Via is the feature whose value holds the one a chain names (`left` in +// `left.raw`), nil for a name reached no such way; whether two such places hold +// one value is the run's to decide (features may alias), so Conflicts ignores it. type Place struct { Sym *symbols.Symbol Name string Local bool State *ast.StateNode Direct bool + Via *symbols.Symbol // Node is the node whose pin the place is, each performance of a node holding // its own; nil for a feature or a declaration's own value. Node ast.Node @@ -106,6 +110,46 @@ type Footprint struct { Dynamic bool Creates bool Routes bool + // Flows are the data flows of the move's statements, one each: what the + // statement writes stands on what it reads. None for a move described whole. + Flows []Flow +} + +// Flow is one statement's data flow: its writes stand on its reads. +type Flow struct { + Reads []Place + Writes []Place +} + +// WritesReading are the places the move writes standing on a read of a place +// among reads: the writes of the statements reading one, or every write of the +// move when a read outside its statements (a guard's) or a move described whole does. +func (f Footprint) WritesReading(reads func(Place) bool) []Place { + var out []Place + inFlow := false + for _, flow := range f.Flows { + if slices.ContainsFunc(flow.Reads, reads) { + inFlow = true + for _, p := range flow.Writes { + out = appendPlace(out, f.writeOf(p)) + } + } + } + if !inFlow { + return f.Writes + } + return out +} + +// writeOf is the move's write of the place a flow names, as the move holds it +// (a pin stamped with its performance), else the place as named. +func (f Footprint) writeOf(p Place) Place { + for _, w := range f.Writes { + if w.Sym == p.Sym && w.Name == p.Name { + return w + } + } + return p } // Dependent reports whether the two moves may not commute: a data race, both @@ -478,7 +522,11 @@ func (b *footprintBuilder) place(scope *symbols.Scope, segments []string, each f sym, _ := resolve.FeatureSymbolInScope(scope, segments) local := sym != nil && b.declaredByNode(sym) direct := len(segments) == 1 - each(Place{Sym: sym, Name: name, Local: local, Direct: direct}) + var via *symbols.Symbol + if !direct { + via, _ = resolve.FeatureSymbolInScope(scope, segments[:len(segments)-1]) + } + each(Place{Sym: sym, Name: name, Local: local, Direct: direct, Via: via}) if sym == nil { return nil } @@ -491,7 +539,7 @@ func (b *footprintBuilder) place(scope *symbols.Scope, segments []string, each f if usage, ok := sym.Decl.(*ast.Usage); ok { for _, redefined := range redefinedNames(usage) { if redefined != name { - each(Place{Sym: sym, Name: redefined, Local: local, Direct: direct}) + each(Place{Sym: sym, Name: redefined, Local: local, Direct: direct, Via: via}) } } b.calcUsage(sym, usage) @@ -795,9 +843,14 @@ func (b *footprintBuilder) invokesDeclaredBehavior(scope *symbols.Scope, qn *ast } // statements adds what a body's statements touch, blocks and their own flows included. +// statements adds a body's statements, each built apart so its own flow is kept. func (b *footprintBuilder) statements(stmts []Statement) { for _, stmt := range stmts { - b.statement(stmt) + sub := &footprintBuilder{resolver: b.resolver, graph: b.graph, node: b.node, scope: b.scope, + declared: b.declared, localDeclarations: b.localDeclarations} + sub.statement(stmt) + b.merge(sub.footprint) + b.footprint.Flows = append(b.footprint.Flows, Flow{Reads: sub.footprint.Reads, Writes: sub.footprint.Writes}) } } @@ -982,6 +1035,7 @@ func (b *footprintBuilder) merge(other Footprint) { b.footprint.Dynamic = b.footprint.Dynamic || other.Dynamic b.footprint.Creates = b.footprint.Creates || other.Creates b.footprint.Routes = b.footprint.Routes || other.Routes + b.footprint.Flows = append(b.footprint.Flows, other.Flows...) } // plainType reports whether constructing the named type creates an object that