diff --git a/changes/unreleased/terminate-nested-flow-target.fixed.md b/changes/unreleased/terminate-nested-flow-target.fixed.md new file mode 100644 index 0000000000..a0d8fb74f4 --- /dev/null +++ b/changes/unreleased/terminate-nested-flow-target.fixed.md @@ -0,0 +1 @@ +- **A `terminate` inside a loop body names its own loop performance's node only.** `terminate slow;` in a loop body reached by several tokens ended the paused `slow` performances of the other loop performances too, and ran on as if it had ended its own. Each step of a statement node now owns what its body performs, so the terminate ends that body's `slow`; one that has already ended is reported as `performance already ended`, since `TerminateAction` ends an occurrence during its own performance. diff --git a/docs/project/spec-compliance.md b/docs/project/spec-compliance.md index 8b29ed3355..7e22dd41b8 100644 --- a/docs/project/spec-compliance.md +++ b/docs/project/spec-compliance.md @@ -785,7 +785,7 @@ checked after the result is bound is not a form the runtime offers, and none is | `then terminate;` as a node of an action's flow (SysML v2 §7.17.10 Terminate Actions; `Actions::TerminateAction :> Action` ends "the occurrence that is the performer" of it): the token reaching it ends the performance the flow belongs to — the action itself at top level, the nested node whose flow it is otherwise — with the outputs assigned so far; later nodes do not run, no data flow fires from a node that did not complete, and every other token of that performance is dropped, a forked sibling branch still running or parked at an `accept` included, in token-id order, each drop written to the trace. For the root the run ends `Completed` with the features as they are; for a nested node the parent's token takes the node's succession as after a normal completion, and no succession out of the node's inner nodes fires | `lower/action_nodes.go` (the node's body is one `Effect{EffectTerminate}` with `TerminateContaining`); `runtime/action_terminate.go` `performances.terminate` (a `terminated` unwinding caught by `ActionExecutor.stepToken` → `endTerminatedFor`), `endAround`, `leaveTerminated`, `dropTokensIn`; `runtime/trace.go` `RecordActionTerminate` | conformance `action_terminate_flow_node`, `action_terminate_fork_drops_sibling` + `.trace.golden` (the sibling parked at an accept is dropped before the action completes) | ✅ Faithful | | A named terminate action usage (`action stop terminate;`, SysML.xtext `TerminateActionUsage` with a declaration) reached by `then stop;` ends the performance whose flow it is a node of, as `then terminate;` does; the marker is kept on the usage, printed back and exported as `TerminateActionUsage` | `ast/defusage.go` `Usage.IsTerminate`; `parser/defusage.go` `parsePostModifiers`, `skipPastTerminateMarker` (`terminate` after an action's declaration is the marker, not a reference, and closes the declaration: a clause after it is reported); `lower/action_subflow.go` `lowerTerminateNode` (the statements its body declares run as a leaf's, then the terminate, `TerminateEnclosing`, which `runtime/action_terminate.go` `terminatedUsage` also reaches when a `terminate` of the body ends the usage's own performance first; the pins its body declares are its features, `lowerFeatures`; a body stating a flow of its own is `ErrInvalidActionFlow` at initialize), `lower/block_graph.go`; `export/rdf_out.go`/`rdf_in.go` | `parse/action_terminate.golden`, conformance `action_terminate_named_usage`, `action_terminate_joined_usage` (two successions synchronize at the usage; trace golden), `action_terminate_usage_with_pins` (a flow into a pin the usage's body declares), `action_terminate_usage_with_body` (its body's statements run before it ends the action), `action_terminate_usage_body_ends_itself` and `action_terminate_usage_in_block_names_itself` (a `terminate` in its own body ends the usage's performance there and the usage still ends the action or node it is a step of), robustness `terminate_usage_stating_a_flow_of_its_own`, `export/behavior_test.go` (terminate usage round trip); `parser/negative_test.go` (`terminate_repeated`, `terminate_then_typing`, `terminate_then_ordered`, `terminate_then_value`, `terminate_then_target`), `TestTerminateMarkerClosesTheDeclaration` | ✅ Faithful (a target written after the marker, `action stop terminate x;` — SysML.xtext `TerminateNode`'s `NodeParameterMember` — is reported rather than dropped; the target form is the statement `then terminate x;`. `examples/sysml-v2-training/19. Terminate Actions/Terminate Actions Example-1.sysml` parses with its marker and runs to completion: the nested node's body is two `perform`s with no `first` and no succession between them, and a `perform` is referential, not a composite subaction, so neither is performed and the `terminate` after `criticalActivity` is not reached) | | `terminate;` as a statement of a nested action node's body (`then action c1 { assign x := 1; terminate; }`) ends that node — "not any containing actions" — so the rest of the body does not run, the node's fork branches and paused work are dropped, and the parent continues along the node's succession and observes what the node assigned before it ended | `lower/action_graph.go` `lowerBody` (`*ast.TerminateStatement` lowered as `Effect{EffectTerminate}`, the target resolved at lowering time), `lowerStatement`; `runtime/action_statements.go` `actionStmtHost.effect` → `runtime/action_terminate.go` `performances.terminate`; `runtime/action_body_run.go` `usageWork.perform` and `runtime/action_statements.go` `performNode` (the unwinding of the node's own body ends it normally, dropping the tokens of a flow a node of an `if` branch or a loop body inside it owns) | conformance `action_terminate_nested_body`, `action_terminate_nested_fork` + `.trace.golden` (the node's sibling branch is dropped, the parent's other fork branch completes) | ✅ Faithful | -| `terminate ;` naming an action node of the flow the statement is in or of a flow enclosing it — the node itself (`action c1 { terminate c1; }`), the node whose body holds the statement's node, or a sibling node of an enclosing flow still running — ends every ongoing performance of that node, the earliest begun first, and every performance a token of that flow is parked at without having begun — a forked sibling the schedule has not reached yet (§7.17.10's `MonitoredActivity`, whose `waitForTimeOut` terminates `performCriticalActivity` whatever it has done), or an `accept` node waiting for a signal (an ongoing performance that has done nothing) — which end there, their body never run, the token going on along the node's succession (a merge can bring a second token to a node whose earlier performance is still paused): unwinding the body where the statement runs inside it, dropping the performance's tokens and abandoning its paused body in place where it runs beside it — the performance the token at the node holds, never another performance of the same node — after which the parent's token takes the node's succession. A name that resolves to no action node of an enclosing flow is reported (`ErrTerminateTarget`), as is a node whose every performance already ended (`ErrPerformanceEnded`) | `lower/action_graph.go` `lowerStatement` (`Effect.Terminates`/`Effect.Target`: `TerminateNode`, `TerminateUnknown`); `runtime/action_terminate.go` `terminateTargets` (up the frame chain through `subactions`), `performances.ongoingWith`, `ActionExecutor.ongoing`, `terminated.then`/`endAlongside` (the performances named after the one the statement runs within end once it has), `Token.performing`, `ActionExecutor.beginPending`/`endPending` (a parked token's performance, `actionFrame.heldAt`), `endOther`; `runtime/trace.go` `RecordActionTerminatePending`; `runtime/errors.go` `ErrTerminateTarget`, `ErrPerformanceEnded` | conformance `action_terminate_names_own_node`, `action_terminate_names_own_node_concurrently` + `.trace.golden` and `action_terminate_names_own_node_from_the_earlier` + `.trace.golden` (a performance naming its own node ends the other ongoing performances of it too, the order earliest-first kept across its own unwinding), `action_terminate_names_enclosing_node`, `action_terminate_names_sibling_flow` + `.trace.golden`, `action_terminate_names_concurrent_performances` + `.trace.golden`, `action_terminate_from_block_node_flow` + `.trace.golden` and `action_terminate_names_block_node` + `.trace.golden` (a `terminate` in the forked flow of a node an `if` branch declares names the node holding the branch, or the branch node around it: the forked waiter is dropped with the performance named); `action_terminate_names_sibling_before_it_begins` + `.trace.golden` (the `MonitoredActivity` shape: the terminated sibling had not begun, `terminate … ended before it began`) and `action_terminate_names_waiting_accept` + `.trace.golden` (`ended waiting`; the join after both branches still meets); `robustness_terminate_test.go` `terminate_of_an_ended_performance`, `terminate_of_an_unknown_name`, `terminate_of_a_node_of_a_sibling_flow` (a node nested inside a sibling branch is out of reach) | ✅ Faithful | +| `terminate ;` naming an action node of the flow the statement is in or of a flow enclosing it — the node itself (`action c1 { terminate c1; }`), the node whose body holds the statement's node, or a sibling node of an enclosing flow still running — ends every ongoing performance of that node held by the performances the statement runs within, the earliest begun first (a `terminate` inside a loop body names its own loop performance's node only: each performance of the body owns its own performances of the body's nodes, and another loop performance's are out of reach, whether paused or not), and every performance a token of that flow is parked at without having begun — a forked sibling the schedule has not reached yet (§7.17.10's `MonitoredActivity`, whose `waitForTimeOut` terminates `performCriticalActivity` whatever it has done), or an `accept` node waiting for a signal (an ongoing performance that has done nothing) — which end there, their body never run, the token going on along the node's succession (a merge can bring a second token to a node whose earlier performance is still paused): unwinding the body where the statement runs inside it, dropping the performance's tokens and abandoning its paused body in place where it runs beside it — the performance the token at the node holds, never another performance of the same node — after which the parent's token takes the node's succession. A name that resolves to no action node of an enclosing flow is reported (`ErrTerminateTarget`), as is a node whose every performance already ended (`ErrPerformanceEnded`) | `lower/action_graph.go` `lowerStatement` (`Effect.Terminates`/`Effect.Target`: `TerminateNode`, `TerminateUnknown`); `runtime/action_executor.go` `beginStatementStep` (a statement node's step is a performance owning what its body performs); `runtime/action_terminate.go` `terminateTargets` (up the frame chain through `subactions`), `performances.ongoingWith`, `ActionExecutor.ongoing`, `terminated.then`/`endAlongside` (the performances named after the one the statement runs within end once it has), `Token.performing`, `ActionExecutor.beginPending`/`endPending` (a parked token's performance, `actionFrame.heldAt`), `endOther`; `runtime/trace.go` `RecordActionTerminatePending`; `runtime/errors.go` `ErrTerminateTarget`, `ErrPerformanceEnded` | conformance `action_terminate_names_own_node`, `action_terminate_names_own_node_concurrently` + `.trace.golden` and `action_terminate_names_own_node_from_the_earlier` + `.trace.golden` (a performance naming its own node ends the other ongoing performances of it too, the order earliest-first kept across its own unwinding), `action_terminate_names_enclosing_node`, `action_terminate_names_sibling_flow` + `.trace.golden`, `action_terminate_names_concurrent_performances` + `.trace.golden`, `action_terminate_from_block_node_flow` + `.trace.golden` and `action_terminate_names_block_node` + `.trace.golden` (a `terminate` in the forked flow of a node an `if` branch declares names the node holding the branch, or the branch node around it: the forked waiter is dropped with the performance named); `action_terminate_names_sibling_before_it_begins` + `.trace.golden` (the `MonitoredActivity` shape: the terminated sibling had not begun, `terminate … ended before it began`) and `action_terminate_names_waiting_accept` + `.trace.golden` (`ended waiting`; the join after both branches still meets); `action_terminate_names_node_of_paused_bodies` + `.trace.golden` and `action_terminate_names_node_performing_action` + `.trace.golden` (each loop performance's slow, paused in its body or performing an action, is ended by a `terminate` inside it), `action_terminate_names_node_of_its_own_loop_performance` + `.trace.golden` (the other loop performances' paused slows nap on); `robustness_terminate_test.go` `terminate_of_an_ended_performance`, `terminate_of_an_unknown_name`, `terminate_of_a_node_of_a_sibling_flow` (a node nested inside a sibling branch is out of reach); `robustness_terminate_nested_test.go` `terminate_in_a_loop_body_of_its_own_ended_performance` (its own slow has ended, the other loop performances' paused ones are not reached: `ErrPerformanceEnded`, as `TerminateAction::terminateOccurrence : destroy` requires the occurrence's `endShot` to happen during the terminate), `terminate_in_a_loop_body_leaves_other_loop_performances`, `terminate_in_a_loop_body_before_its_node_began` | ✅ Faithful | | `terminate ;` whose target is an occurrence rather than an action node — `terminate this;` in an action a part performs (an exhibited or performed behavior is a performance the object owns, so `this` there is the object), a feature chain naming a part (`terminate sub.worker;`), or an expression evaluating to an object — ends that occurrence at the statement (SysML v2 §7.17.10 "forces the lifetime of the terminated occurrence to end"; `Actions::TerminateAction`'s `terminatedOccurrence`): its lifetime is recorded as ended, its owned portions with it — a part first read after the whole ended is reached as one that ended with it, its declared values readable and no behavior of it started — and every behavior it performs or exhibits ends where it stands — an action executor of it is `Terminated` with the writes made so far and its tokens dropped, a state machine it exhibits is terminated with no state exited and its do behaviors abandoned — while a behavior of another object stating the terminate runs on. A behavior whose performer ended between two steps ends the moment it is next run, before doing anything more | `lower/action_graph.go` `lowerStatement` (`TerminateOccurrence`, the target expression kept as `Effect.TargetExpr` with its scope); `runtime/occurrence_terminate.go` `performances.terminateOccurrence`, `terminateTargetOf` (the expression evaluated in the statement's frame to a `ValInstance`), `Context.endOccurrence`, `endBehaviorsWith`, `ActionExecutor.endTerminated`/`StateExecutor.endTerminated`, `performerEnded` (checked by `Context.beginExecutorRun` before every run of an executor); `runtime/lifetimes.go` `checkLiving` (a target that is destroyed, or a performance that already ended, is a typed error), `beginLife` (a part of an ended whole is born ended), `lifeEnded`, `checkPerformer`; `runtime/classifier_behavior.go` `startBehaviorsOfAll` (no behavior of an ended object starts); `runtime/trace.go` `RecordOccurrenceTerminate` | conformance `action_terminate_this_ends_part` + `.trace.golden` (the part's exhibited machine is terminated with its action), `action_terminate_names_exhibiting_part` + `.trace.golden` (a feature chain to another part: that part's machine ends, the terminating action runs on), `state_terminate_this_ends_performer` + `.trace.golden` (`terminate this;` in a do behavior ends the part exhibiting the machine), `action_terminate_owner_before_lazy_part` + `.trace.golden` (a part first read after its whole ended: the value read, its machine never started); `robustness_terminate_test.go` `terminate_of_a_non_action_feature` (`ErrTerminateOccurrence`: no occurrence), `terminate_of_a_literal_value`, `terminate_of_a_qualified_occurrence` (a chain that names no object), `terminate_of_a_destroyed_occurrence` (`ErrOccurrenceDestroyed`), `terminate_of_a_part_reached_after_its_whole_ended` (`ErrOccurrenceLifetime`: it ended with the whole), `terminate_of_an_occurrence_expression`, `terminate_of_an_ended_occurrence_in_a_state_body`, `behavior_of_an_ended_performer` (`ErrPerformerEnded`: a behavior of an occurrence that ended cannot be started) | ✅ Faithful | | `terminate` as a statement of a state's `entry`, `do` or `exit` body, or of a transition effect, ends that behavior at the statement — the containing action of the terminate is the behavior it is written in (`StatePerformance`'s `entry`/`do`/`exit` step, `Kernel Semantic Library/StatePerformances.kerml`), not the machine — so the rest of the body does not run, the state stays active and the machine keeps dispatching; the machine's exhibiting occurrence ends only when named (`terminate this;`, the row above). The unit ended is the action the `terminate` is written in: in the named shapes (`entry action a { … }`, `do action tick { … }`, `do eff;`) the named action; in the braced shapes (`entry { … }`, `do { … }`, `exit { … }`, a transition's `do { … }`, the machine's own `entry { … }`/`exit { … }`) the whole braced block, which is one anonymous `ActionUsage` with an `ActionBody` as SysML.xtext reads it — the `terminate` resolves to the block's own performance, so the statements after it do not run (a `do` block runs one statement a round, so an `accept` it would park at next never begins); the steps of a transition's own body (`then t { … }`) are the one shape lowered one behavior per statement, and a `terminate` in one ends the steps after it (`terminate …: ended before it began` trace lines); another member of the same kind beside the block (`entry action first;` next to `entry { … }`) and the state's other behaviors run as written — an `entry` block's `terminate` still lets the `do` start, an `exit` block's or an effect's still lets the transition complete | `lower/state_behavior.go` (a state behavior's `*ast.TerminateStatement` lowered as `Effect{EffectTerminate}` with its target, `TerminateContaining` for the bare form; `StateBehavior.Block` names the `TransitionMember` whose body's steps a behavior is one of, nil for every behavior that is a performance of its own), `lower/state_graph.go` `StateGraph.behaviorsIn`, `lowerBehaviorsFor`, `transitionEffects`, `lowerTransitionEdge`, `lower/state_inheritance.go` `addMember`, `cloneStateNode` (inherited bodies keep their terminate mappings); `runtime/state_statements.go` `stateStmtHost.effect` → `runtime/action_terminate.go` `performances.terminate` (the `terminated` unwinding ends the behavior's own performance, caught where the behavior was started), `stateStmtHost.ended` (`terminated`), `StateExecutor.executeBehaviors`, `endedBefore`; `runtime/state_executor.go` `stepDoAction`; `runtime/state_route.go` `runEffects`, `runBehaviors`; `runtime/state_region_entry.go` (fork branch effects) | conformance `state_terminate_entry_do_exit_behaviors` + `.trace.golden` (each of the three named bodies ends at its `terminate`; the assignments after it do not run, the state is still active for the next event); `state_terminate_braced_entry_do_exit_effect` + `.trace.golden` (braced `entry`, `do`, `exit` and transition `do` blocks each end at their `terminate`, the machine reaches the target), `state_terminate_braced_do_after_accept` + `.trace.golden` (the `accept` the block would park at next never begins; the state completes and the machine keeps dispatching), `state_terminate_braced_entry_among_named` (only the braced block is cut short; the named entry actions beside it run), `state_terminate_braced_inherited_by_two_usages` (the braced blocks of a definition, in two usages of it), `state_terminate_braced_do_in_one_region` + `.trace.golden` + `.check.expected.json` (a sibling region's `do` block is unaffected, on every schedule); `state_terminate_transition_body` + `.trace.golden` (a `terminate` among the steps of a transition's own body ends the steps after it, `ended before it began`, and the target is entered); `robustness_terminate_test.go` `terminate_of_an_unknown_name_in_a_state_body`, `terminate_of_a_value_in_a_transition_effect`; `robustness_terminate_block_test.go` `terminate_as_the_only_statement_of_a_block`, `second_terminate_of_an_ended_block_never_runs`, `terminate_in_a_loop_ends_the_block_once`, `terminate_of_a_state_name_in_a_block` | ✅ Faithful | | A transition whose target is a terminate action usage declared in the machine's body or in a composite state's (`transition busy accept Abort then stop; action stop terminate;`, SysML v2 §7.18.3: "to immediately terminate the containing state performance") ends the state-machine performance where it arrives: the transition's source is exited as any transition's is (its exit behavior runs, since the source *is* left) and the effect run, the states from the move's boundary down to the usage's owner are entered (their entry behaviors run; a composite's own entry transition never fires), then nothing else is exited, no other exit behavior runs, every do behavior under way — the sibling region's, the enclosing composite's, the machine's own — is abandoned where it stands, and no state is active. The run's `Outcome` is `Terminated` with `FinalState` empty (`StateTerminated`, distinct from `StateCompleted` at a final state); the REPL reports `State machine terminated (a \`terminate\` ended its performance short of a final state; no state is active)` and `%current` `Execution state: Terminated`; the LSP debugger state is `terminated`; the trace records `terminate : …` with the do behaviors abandoned. A route through a choice or junction whose taken branch reaches the usage, or out of a join once every source has arrived, ends the machine the same way once the compound transition completes — the sources, and the composite a segment leaves, are exited as for any transition out of it; a transition reaching the usage from another region, or from outside the composite that declares it, exits and enters what a move to a state beside the usage would. A fork branch may not lead into a terminate usage (`fork split: branch target must be a state`, at lowering): §7.18.3 gives the terminate as a transition's target, and a fork's branches enter one state per region. A machine inherited by a typed state usage owns copies of its terminate usages and pseudostates, nested ones too, so two usages of one definition each terminate through their own | `lower/state_graph.go` `StateGraph.Terminates`/`TerminateOwner` (every terminate action usage with the composite state that declares it; `lower.IsTerminateUsage`), `putCopiedVertex`/`copyInherited` (a transition naming the inherited declaration reaches the usage's own copy), `lower/state_inheritance.go` `cloneStateNode`; `resolve/transition.go` (a terminate usage is a valid transition endpoint); `runtime/state_route.go` `route.terminate`, `terminateBoundary`, `terminateExits`, `terminateEntries`, `terminateAlong`, `terminateAt`, `mayExit`; `runtime/state_executor.go` `terminateMachine`, `abandonMachine`; `runtime/executor_common.go` `StateTerminated`, `ExecutionState.Ended`; `runtime/outcome.go` `Outcome.Terminated`; `runtime/trace.go` `RecordStateTerminate`; `repl/meta.go` (the terminated wording); `lsp/debug.go` `debugTerminated` | conformance `state_terminate_transition_ends_machine` + `.trace.golden` (the source's exit and the effect run; the machine's do behavior is abandoned, `exits = 1`), `state_terminate_inside_composite` + `.trace.golden` (a terminate declared in a composite state, reached from its substate: the substate is exited, the composite is not), `state_terminate_inside_region` + `.trace.golden` (one region's transition ends the machine; the sibling region's state is not exited, its do behavior abandoned), `state_terminate_entering_composite` + `.trace.golden` (reached from outside the composite: the composite is entered on the way, its region never started), `state_terminate_through_choice` + `.trace.golden`, `state_terminate_through_junction` + `.trace.golden`, `state_terminate_through_join` + `.trace.golden` (both regions' states and the orthogonal state are exited before the join's effect; the run is terminated, at no final state), `state_terminate_inherited_by_two_usages` + `.trace.golden` (the second usage ends the machine through its own copy of a nested inherited terminate); `lower/state_inherited_test.go:TestToStateGraphTwoTypedUsagesOwnInheritedTerminateAndPseudostate`, `lower/fork_plan_test.go:TestToStateGraph_ForkShapeRejected` (`branch into a terminate action`); `repl/terminate_test.go` `TestStateDebuggerReportsATerminatedMachine`, `TestTerminatingThisEndsThePartsBehaviors`; the PSSM referee's *Terminate 003* (`pass`), *Terminate 001* and *002* (`fail` on the region-entry order of alignment finding 9; each reaches an admitted trace whose termination is complete) | ✅ Faithful | diff --git a/internal/exec/runtime/action_body_run.go b/internal/exec/runtime/action_body_run.go index 650460f023..5a6ede2502 100644 --- a/internal/exec/runtime/action_body_run.go +++ b/internal/exec/runtime/action_body_run.go @@ -484,7 +484,9 @@ type statementWork struct { token int64 frame *actionFrame node ast.Node - done bool + // step is the node's performance, owning the nodes its body performs. + step *actionFrame + done bool } func (w *statementWork) clone() bodyWork { c := *w; return &c } @@ -492,9 +494,10 @@ func (w *statementWork) clone() bodyWork { c := *w; return &c } func (w *statementWork) perform() error { e := w.exec if !w.done { - if err := e.executeBody(w.frame, w.frame.graph, w.node); err != nil { + if err := e.executeStatementBody(w.step, w.frame.graph); err != nil { return err } + w.step.ended = true w.done = true } idx, err := e.workToken(w.token) diff --git a/internal/exec/runtime/action_executor.go b/internal/exec/runtime/action_executor.go index 0f73a1c875..5755bdfd31 100644 --- a/internal/exec/runtime/action_executor.go +++ b/internal/exec/runtime/action_executor.go @@ -3065,7 +3065,32 @@ func performerSuffix(self *Instance) string { // runs the statements lowering recorded for it, then leaves for its successor. func (e *ActionExecutor) stepStatementNode(tokenIdx int) error { token := e.tokens[tokenIdx] - return e.runBody(tokenIdx, &statementWork{exec: e, token: token.ID, frame: token.frame, node: token.Location}) + step := e.beginStatementStep(token.frame, token.Location) + return e.runBody(tokenIdx, &statementWork{exec: e, token: token.ID, frame: token.frame, node: token.Location, step: step}) +} + +// beginStatementStep is a token's step of a statement node in frame: a transparent performance +// owning what the step's body performs, so a `terminate` there names the step's own. +func (e *ActionExecutor) beginStatementStep(frame *actionFrame, node ast.Node) *actionFrame { + scope := frame.graph.Scopes[node] + if scope == nil { + scope = frame.scope + } + return &actionFrame{ + node: node, + flow: frame.graph, + scope: scope, + parent: frame, + connections: frame.connections, + data: make(map[string]Value), + features: make(map[string]ast.FeatureDirection), + subactions: make(map[ast.Node]*actionFrame), + perfs: &e.performances, + run: frame.run, + began: e.ctx.newActivation(), + label: frame.describe(), + body: true, + } } // leaveStatementNode takes the token at tokenIdx on from node, retiring it where diff --git a/internal/exec/runtime/action_statements.go b/internal/exec/runtime/action_statements.go index 32fdb22773..33d42358a2 100644 --- a/internal/exec/runtime/action_statements.go +++ b/internal/exec/runtime/action_statements.go @@ -18,6 +18,8 @@ type actionStmtHost struct { perf *actionFrame // graph is the flow node is a node of. graph *lower.ActionGraph + // step is the performance of a statement node's step, owning what its body performs. + step *actionFrame } // executeBody runs the lowered statements graph records for node in perf, the @@ -31,6 +33,26 @@ func (e *performances) executeBody(perf *actionFrame, graph *lower.ActionGraph, return err } +// executeStatementBody runs the statements of the statement node step performs, in the +// performance around it, with what they perform owned by step. +func (e *performances) executeStatementBody(step *actionFrame, graph *lower.ActionGraph) error { + perf := step.parent + _, err := e.ctx.runStatements(func() *stmtEngine { + host := &actionStmtHost{exec: e, node: step.node, perf: perf, graph: graph, step: step} + lexical := perf.lexicalFrames() + return newStmtEngineIn(e.ctx, host, lexical[len(lexical)-1], lexical[:len(lexical)-1]) + }, graph.Bodies[step.node]) + return err +} + +// around is the performance the body's nodes are performed in and its terminates resolve from. +func (h *actionStmtHost) around() *actionFrame { + if h.step != nil { + return h.step + } + return h.perf +} + // runNodeBody runs the statements a control or initial node's body declares, // which the token passing through the node performs. func (e *ActionExecutor) runNodeBody(frame *actionFrame, node ast.Node) error { @@ -160,7 +182,7 @@ func (h *actionStmtHost) acceptReturn(Value, lower.Return) error { func (h *actionStmtHost) effect(engine *stmtEngine, s lower.Effect) error { env := engine.env if s.Kind == lower.EffectTerminate { - return h.exec.terminate(engine, h.perf, s) + return h.exec.terminate(engine, h.around(), s) } if s.Kind == lower.EffectStart { if err := h.exec.ctx.startEffect(engine.evalIn(s.Scope), s, h.exec.self); err != nil { @@ -204,7 +226,7 @@ func (h *actionStmtHost) effect(engine *stmtEngine, s lower.Effect) error { // performNode performs a nested action a block of the body declares as a // subperformance of the body's. func (h *actionStmtHost) performNode(engine *stmtEngine, graph *lower.ActionGraph, node *ast.Usage) (stmtFlow, error) { - return h.exec.performNode(h.perf, engine, graph, node) + return h.exec.performNode(h.around(), engine, graph, node) } // runFlow rejects a stated flow among statements: an action's own flow is the @@ -215,7 +237,7 @@ func (h *actionStmtHost) runFlow(lower.Block) (stmtFlow, error) { } func (h *actionStmtHost) runBlockFlow(engine *stmtEngine, block lower.Block) (stmtFlow, error) { - return h.exec.performBlockFlow(h.perf, engine, block) + return h.exec.performBlockFlow(h.around(), engine, block) } // performNode performs node, which a block of parent's body declares, as a subperformance diff --git a/internal/exec/runtime/robustness_terminate_nested_test.go b/internal/exec/runtime/robustness_terminate_nested_test.go new file mode 100644 index 0000000000..bfce1437c9 --- /dev/null +++ b/internal/exec/runtime/robustness_terminate_nested_test.go @@ -0,0 +1,134 @@ +package runtime + +import ( + "errors" + "strings" + "testing" + + "github.com/Open-MBEE/OpenSysML/internal/syntax/ast" +) + +// TestRuntimeRobustnessTerminateNestedFlowTarget pins which performances a `terminate` +// in a loop body names: those of its own loop body's performance, never another's. +func TestRuntimeRobustnessTerminateNestedFlowTarget(t *testing.T) { + t.Run("terminate_in_a_loop_body_of_its_own_ended_performance", testTerminateInALoopBodyOfItsOwnEndedPerformance) + t.Run("terminate_in_a_loop_body_leaves_other_loop_performances", testTerminateInALoopBodyLeavesOtherLoopPerformances) + t.Run("terminate_in_a_loop_body_before_its_node_began", testTerminateInALoopBodyBeforeItsNodeBegan) +} + +// executeLibraryActionSource executes the named action of src over the standard library. +func executeLibraryActionSource(t *testing.T, name, src string) (map[string]Value, error) { + t.Helper() + idx, _, ctx := buildRuntimeWithLibraries(t, "", parseAndBuild(t, src)) + sym := findSymbolByName(idx.DocumentRoot(""), name, ast.DefAction) + if sym == nil { + t.Fatalf("action %s not found", name) + } + return ctx.ExecuteAction(sym) +} + +// loopPerformancesHost reaches the loop node with three tokens a step apart, each +// performance of its body running slow (and the first two napping in it) before body. +func loopPerformancesHost(slow, body string) string { + return `package test { + private import ScalarValues::*; + private import ISQ::*; + private import SI::*; + action host { + out attribute entered : Integer = 0; + out attribute napped : Integer = 0; + out attribute later : Integer = 0; + fork split; + action pre; + action pre1; + action pre2; + succession first start then split; + succession first split then gate; + succession first split then pre; + succession first pre then gate; + succession first split then pre1; + succession first pre1 then pre2; + succession first pre2 then gate; + merge gate; + then loop { + action slow { + assign entered := entered + 1; + ` + slow + ` + } + ` + body + ` + } until true; + then done; + } + }` +} + +const nappingSlow = `if entered <= 2 { + action inner { + first start; + then action nap accept after 10 [s]; + then done; + } + assign napped := napped + 1; + }` + +// testTerminateInALoopBodyOfItsOwnEndedPerformance: the third loop performance's +// slow has ended when its body runs `terminate slow;`, while the other two loop +// performances' slows are still paused. Those are not its own, so it names an ended +// performance, which TerminateAction cannot end during its performance. +func testTerminateInALoopBodyOfItsOwnEndedPerformance(t *testing.T) { + _, err := executeLibraryActionSource(t, "host", loopPerformancesHost(nappingSlow, `if entered == 3 { + terminate slow; + } + assign later := later + 1;`)) + if !errors.Is(err, ErrPerformanceEnded) { + t.Fatalf("error = %v, want ErrPerformanceEnded", err) + } + if !strings.Contains(err.Error(), "slow") { + t.Fatalf("error = %v, want it to name slow", err) + } +} + +// testTerminateInALoopBodyLeavesOtherLoopPerformances: the third loop performance's +// slow ends itself from a watch due before the other two naps end; those two are +// another loop performance's and nap on to completion. +func testTerminateInALoopBodyLeavesOtherLoopPerformances(t *testing.T) { + values, err := executeLibraryActionSource(t, "host", loopPerformancesHost(nappingSlow+` else { + action guard { + first start; + then fork f; + succession first f then nap; + succession first f then watch; + action nap accept after 10 [s]; + action watch accept after 5 [s]; + succession first watch then stop; + action stop { terminate slow; } + } + assign napped := napped + 10; + }`, `assign later := later + 1;`)) + if err != nil { + t.Fatalf("execute: %v", err) + } + assertIntOutput(t, values, "entered", 3) + assertIntOutput(t, values, "napped", 2) + assertIntOutput(t, values, "later", 3) +} + +// testTerminateInALoopBodyBeforeItsNodeBegan: `terminate slow;` ordered before slow +// in a loop body has no performance of slow to end, its own or another's. +func testTerminateInALoopBodyBeforeItsNodeBegan(t *testing.T) { + _, err := executeActionSource(t, "host", `package test { + private import ScalarValues::*; + action host { + out attribute x : Integer = 0; + first start; + then loop { + terminate slow; + then action slow { assign x := 1; } + } until true; + then done; + } + }`) + if !errors.Is(err, ErrTerminateTarget) { + t.Fatalf("error = %v, want ErrTerminateTarget", err) + } +} diff --git a/internal/exec/runtime/snapshot.go b/internal/exec/runtime/snapshot.go index cfab20477d..2570f8897a 100644 --- a/internal/exec/runtime/snapshot.go +++ b/internal/exec/runtime/snapshot.go @@ -569,6 +569,11 @@ func (e *ActionExecutor) reachableFrames() []*actionFrame { visit(e.root) for _, token := range e.tokens { visit(token.frame) + if token.body != nil { + if w, ok := token.body.work.(*statementWork); ok { + visit(w.step) + } + } for _, perf := range token.performed() { visit(perf) } diff --git a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_its_own_loop_performance.expected.json b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_its_own_loop_performance.expected.json new file mode 100644 index 0000000000..d08c189895 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_its_own_loop_performance.expected.json @@ -0,0 +1,11 @@ +{ + "type": "action", + "libraries": true, + "trace": true, + "outputs": { + "entered": {"type": "Integer", "value": 3}, + "napped": {"type": "Integer", "value": 2}, + "passed": {"type": "Integer", "value": 3}, + "later": {"type": "Integer", "value": 3} + } +} diff --git a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_its_own_loop_performance.sysml b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_its_own_loop_performance.sysml new file mode 100644 index 0000000000..b8415a765f --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_its_own_loop_performance.sysml @@ -0,0 +1,55 @@ +package test { + private import ScalarValues::*; + private import ISQ::*; + private import SI::*; + + // The third loop performance's slow terminates itself while the first two nap: it names + // its own loop body's slow only, so the other two nap on and complete. + action host { + out attribute entered : Integer = 0; + out attribute napped : Integer = 0; + out attribute passed : Integer = 0; + out attribute later : Integer = 0; + + fork split; + action pre; + action pre1; + action pre2; + succession first start then split; + succession first split then gate; + succession first split then pre; + succession first pre then gate; + succession first split then pre1; + succession first pre1 then pre2; + succession first pre2 then gate; + merge gate; + then loop { + action slow { + assign entered := entered + 1; + if entered <= 2 { + action inner { + first start; + then action nap accept after 10 [s]; + then done; + } + assign napped := napped + 1; + } else { + action guard { + first start; + then fork f; + succession first f then nap; + succession first f then watch; + action nap accept after 10 [s]; + action watch accept after 5 [s]; + succession first watch then stop; + action stop { terminate slow; } + } + assign napped := napped + 1; + } + } + assign passed := passed + 1; + assign later := later + 1; + } until true; + then done; + } +} diff --git a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_its_own_loop_performance.trace.golden b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_its_own_loop_performance.trace.golden new file mode 100644 index 0000000000..60f2be2a50 --- /dev/null +++ b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_its_own_loop_performance.trace.golden @@ -0,0 +1,109 @@ +step 1: token 1@split +step 2: token 2@gate, token 3@pre, token 4@pre1 +choice step 3: tokens 2@gate, 3@pre, 4@pre1 (unordered; took 4@pre1 first) +step 3: token 2@loop until, token 3@gate, token 4@pre2 +stmt loop until + iteration 1 + stmt node slow + stmt assign entered + eval feature entered -> 0 + eval literal 1 -> 1 + eval operator + -> 1 + stmt if + eval feature entered -> 1 + eval literal 2 -> 2 + eval operator <= -> true + stmt node inner +enter action node: inner + eval literal 10 -> 10 + eval index -> 10 [s] +choice step 4: tokens 2@loop until, 3@gate, 4@pre2 (unordered; took 4@pre2 first) +step 4: token 2@loop until, token 3@loop until, token 4@gate, token 5@nap +stmt loop until + iteration 1 + stmt node slow + stmt assign entered + eval feature entered -> 1 + eval literal 1 -> 1 + eval operator + -> 2 + stmt if + eval feature entered -> 2 + eval literal 2 -> 2 + eval operator <= -> true + stmt node inner +enter action node: inner + eval literal 10 -> 10 + eval index -> 10 [s] +choice step 5: tokens 2@loop until, 3@loop until, 4@gate (unordered; took 4@gate first) +step 5: token 2@loop until, token 3@loop until, token 4@loop until, token 5@nap, token 6@nap +stmt loop until + iteration 1 + stmt node slow + stmt assign entered + eval feature entered -> 2 + eval literal 1 -> 1 + eval operator + -> 3 + stmt if + eval feature entered -> 3 + eval literal 2 -> 2 + eval operator <= -> false + stmt node guard +enter action node: guard + eval literal 5 -> 5 + eval index -> 5 [s] + eval literal 10 -> 10 + eval index -> 10 [s] +choice step 6: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) +step 6: token 2@loop until, token 3@loop until, token 4@loop until, token 5@nap, token 6@nap, token 8@nap, token 9@watch +choice step 7: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) + stmt terminate +terminate action node slow: dropped token 8@nap, token 9@stop + stmt assign passed + eval feature passed -> 0 + eval literal 1 -> 1 + eval operator + -> 1 + stmt assign later + eval feature later -> 0 + eval literal 1 -> 1 + eval operator + -> 1 + eval literal true -> true +choice step 7: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) +step 7: token 2@loop until, token 3@loop until, token 4@done, token 5@nap, token 6@nap +choice step 8: tokens 2@loop until, 3@loop until, 4@done (unordered; took 4@done first) +step 8: token 2@loop until, token 3@loop until, token 5@nap, token 6@nap +choice step 9: tokens 2@loop until, 3@loop until (unordered; took 3@loop until first) +leave action node: inner + stmt assign napped + eval feature napped -> 0 + eval literal 1 -> 1 + eval operator + -> 1 + stmt assign passed + eval feature passed -> 1 + eval literal 1 -> 1 + eval operator + -> 2 + stmt assign later + eval feature later -> 1 + eval literal 1 -> 1 + eval operator + -> 2 + eval literal true -> true +leave action node: inner + stmt assign napped + eval feature napped -> 1 + eval literal 1 -> 1 + eval operator + -> 2 + stmt assign passed + eval feature passed -> 2 + eval literal 1 -> 1 + eval operator + -> 3 + stmt assign later + eval feature later -> 2 + eval literal 1 -> 1 + eval operator + -> 3 + eval literal true -> true +choice step 9: writes napped := 2 by token 2, napped := 1 by token 3 (unordered; napped := 2 by token 2 stood) +choice step 9: writes passed := 3 by token 2, passed := 2 by token 3 (unordered; passed := 3 by token 2 stood) +choice step 9: writes later := 3 by token 2, later := 2 by token 3 (unordered; later := 3 by token 2 stood) +choice step 9: tokens 2@loop until, 3@loop until (unordered; took 3@loop until first) +step 9: token 2@done, token 3@done +choice step 10: tokens 2@done, 3@done (unordered; took 3@done first) +step 10: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_paused_bodies.sysml b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_paused_bodies.sysml index 1852771779..84160e7c86 100644 --- a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_paused_bodies.sysml +++ b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_paused_bodies.sysml @@ -3,11 +3,8 @@ package test { private import ISQ::*; private import SI::*; - // Three tokens reach the loop node through the merge a step apart, each running its - // body. The first two nap in a flow inside slow, so two performances of slow are - // paused at once, each held where its token's body paused, while the third skips - // the nap and its `terminate slow;` names the node: both paused performances end, - // their naps dropped and neither later assignment run, and both bodies go on past slow. + // Each loop body's slow naps while a watch inside it, due first, runs `terminate slow;`: + // that ends the paused slow of its own loop body's performance, its nap dropped. action host { out attribute entered : Integer = 0; out attribute napped : Integer = 0; @@ -29,19 +26,19 @@ package test { then loop { action slow { assign entered := entered + 1; - if entered <= 2 { - action inner { - first start; - then action nap accept after 10 [s]; - then done; - } - assign napped := napped + 1; + action inner { + first start; + then fork f; + succession first f then nap; + succession first f then watch; + action nap accept after 10 [s]; + action watch accept after 5 [s]; + succession first watch then stop; + action stop { terminate slow; } } + assign napped := napped + 1; } assign passed := passed + 1; - if passed == 1 { - terminate slow; - } assign later := later + 1; } until true; then done; diff --git a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_paused_bodies.trace.golden b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_paused_bodies.trace.golden index 6776254683..2be5aa4742 100644 --- a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_paused_bodies.trace.golden +++ b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_of_paused_bodies.trace.golden @@ -5,93 +5,88 @@ step 3: token 2@loop until, token 3@gate, token 4@pre2 stmt loop until iteration 1 stmt node slow - stmt assign entered - eval feature entered -> 0 - eval literal 1 -> 1 - eval operator + -> 1 - stmt if - eval feature entered -> 1 - eval literal 2 -> 2 - eval operator <= -> true + stmt action body + stmt assign entered + eval feature entered -> 0 + eval literal 1 -> 1 + eval operator + -> 1 stmt node inner enter action node: inner + eval literal 5 -> 5 + eval index -> 5 [s] eval literal 10 -> 10 eval index -> 10 [s] choice step 4: tokens 2@loop until, 3@gate, 4@pre2 (unordered; took 4@pre2 first) -step 4: token 2@loop until, token 3@loop until, token 4@gate, token 5@nap +step 4: token 2@loop until, token 3@loop until, token 4@gate, token 6@nap, token 7@watch stmt loop until iteration 1 stmt node slow - stmt assign entered - eval feature entered -> 1 - eval literal 1 -> 1 - eval operator + -> 2 - stmt if - eval feature entered -> 2 - eval literal 2 -> 2 - eval operator <= -> true + stmt action body + stmt assign entered + eval feature entered -> 1 + eval literal 1 -> 1 + eval operator + -> 2 stmt node inner enter action node: inner + eval literal 5 -> 5 + eval index -> 5 [s] eval literal 10 -> 10 eval index -> 10 [s] choice step 5: tokens 2@loop until, 3@loop until, 4@gate (unordered; took 4@gate first) -step 5: token 2@loop until, token 3@loop until, token 4@loop until, token 5@nap, token 6@nap +step 5: token 2@loop until, token 3@loop until, token 4@loop until, token 6@nap, token 7@watch, token 9@nap, token 10@watch stmt loop until iteration 1 stmt node slow - stmt assign entered - eval feature entered -> 2 - eval literal 1 -> 1 - eval operator + -> 3 - stmt if - eval feature entered -> 3 - eval literal 2 -> 2 - eval operator <= -> false + stmt action body + stmt assign entered + eval feature entered -> 2 + eval literal 1 -> 1 + eval operator + -> 3 + stmt node inner +enter action node: inner + eval literal 5 -> 5 + eval index -> 5 [s] + eval literal 10 -> 10 + eval index -> 10 [s] +choice step 6: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) +step 6: token 2@loop until, token 3@loop until, token 4@loop until, token 6@nap, token 7@watch, token 9@nap, token 10@watch, token 12@nap, token 13@watch +choice step 7: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) + stmt terminate +terminate action node slow: dropped token 12@nap, token 13@stop stmt assign passed eval feature passed -> 0 eval literal 1 -> 1 eval operator + -> 1 - stmt if - eval feature passed -> 1 - eval literal 1 -> 1 - eval operator == -> true - stmt terminate -terminate action node slow: dropped token 5@nap -terminate action node slow: dropped token 6@nap stmt assign later eval feature later -> 0 eval literal 1 -> 1 eval operator + -> 1 eval literal true -> true + stmt terminate +terminate action node slow: dropped token 9@nap, token 10@stop stmt assign passed eval feature passed -> 1 eval literal 1 -> 1 eval operator + -> 2 - stmt if - eval feature passed -> 2 - eval literal 1 -> 1 - eval operator == -> false stmt assign later eval feature later -> 1 eval literal 1 -> 1 eval operator + -> 2 eval literal true -> true + stmt terminate +terminate action node slow: dropped token 6@nap, token 7@stop stmt assign passed eval feature passed -> 2 eval literal 1 -> 1 eval operator + -> 3 - stmt if - eval feature passed -> 3 - eval literal 1 -> 1 - eval operator == -> false stmt assign later eval feature later -> 2 eval literal 1 -> 1 eval operator + -> 3 eval literal true -> true -choice step 6: writes passed := 3 by token 2, passed := 2 by token 3, passed := 1 by token 4 (unordered; passed := 3 by token 2 stood) -choice step 6: writes later := 3 by token 2, later := 2 by token 3, later := 1 by token 4 (unordered; later := 3 by token 2 stood) -choice step 6: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) -step 6: token 2@done, token 3@done, token 4@done -choice step 7: tokens 2@done, 3@done, 4@done (unordered; took 4@done first) -step 7: no active tokens +choice step 7: writes passed := 3 by token 2, passed := 2 by token 3, passed := 1 by token 4 (unordered; passed := 3 by token 2 stood) +choice step 7: writes later := 3 by token 2, later := 2 by token 3, later := 1 by token 4 (unordered; later := 3 by token 2 stood) +choice step 7: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) +step 7: token 2@done, token 3@done, token 4@done +choice step 8: tokens 2@done, 3@done, 4@done (unordered; took 4@done first) +step 8: no active tokens diff --git a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_performing_action.sysml b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_performing_action.sysml index 96e300bd15..20d13ce226 100644 --- a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_performing_action.sysml +++ b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_performing_action.sysml @@ -9,10 +9,8 @@ package test { then done; } - // As action_terminate_names_node_of_paused_bodies, but slow naps by performing an - // action of its own rather than running a flow: no token runs inside slow, so a - // paused performance of it is held only where its token's body paused. Both still - // end at `terminate slow;`, their naps abandoned, and both bodies go on past slow. + // As action_terminate_names_node_of_paused_bodies, but slow naps by performing Nap: + // each `terminate slow;` ends its own loop body's slow, abandoning that Nap. action host { out attribute entered : Integer = 0; out attribute napped : Integer = 0; @@ -34,15 +32,19 @@ package test { then loop { action slow { assign entered := entered + 1; - if entered <= 2 { - perform action nap : Nap; - assign napped := napped + 1; + action inner { + first start; + then fork f; + succession first f then nap; + succession first f then watch; + action nap : Nap; + action watch accept after 5 [s]; + succession first watch then stop; + action stop { terminate slow; } } + assign napped := napped + 1; } assign passed := passed + 1; - if passed == 1 { - terminate slow; - } assign later := later + 1; } until true; then done; diff --git a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_performing_action.trace.golden b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_performing_action.trace.golden index f9320211d0..a384a3900e 100644 --- a/internal/exec/runtime/testdata/conformance/action_terminate_names_node_performing_action.trace.golden +++ b/internal/exec/runtime/testdata/conformance/action_terminate_names_node_performing_action.trace.golden @@ -5,93 +5,94 @@ step 3: token 2@loop until, token 3@gate, token 4@pre2 stmt loop until iteration 1 stmt node slow - stmt assign entered - eval feature entered -> 0 - eval literal 1 -> 1 - eval operator + -> 1 - stmt if - eval feature entered -> 1 - eval literal 2 -> 2 - eval operator <= -> true - stmt node nap + stmt action body + stmt assign entered + eval feature entered -> 0 + eval literal 1 -> 1 + eval operator + -> 1 + stmt node inner +enter action node: inner + eval literal 5 -> 5 + eval index -> 5 [s] step 1: token 1@rest eval literal 10 -> 10 eval index -> 10 [s] -choice step 4: tokens 3@gate, 4@pre2 (unordered; took 4@pre2 first) -step 4: token 2@loop until, token 3@loop until, token 4@gate +choice step 4: tokens 2@loop until, 3@gate, 4@pre2 (unordered; took 4@pre2 first) +step 4: token 2@loop until, token 3@loop until, token 4@gate, token 6@nap, token 7@watch stmt loop until iteration 1 stmt node slow - stmt assign entered - eval feature entered -> 1 - eval literal 1 -> 1 - eval operator + -> 2 - stmt if - eval feature entered -> 2 - eval literal 2 -> 2 - eval operator <= -> true - stmt node nap + stmt action body + stmt assign entered + eval feature entered -> 1 + eval literal 1 -> 1 + eval operator + -> 2 + stmt node inner +enter action node: inner + eval literal 5 -> 5 + eval index -> 5 [s] step 1: token 1@rest eval literal 10 -> 10 eval index -> 10 [s] -choice step 5: tokens 2@loop until, 4@gate (unordered; took 4@gate first) -step 5: token 2@loop until, token 3@loop until, token 4@loop until +choice step 5: tokens 2@loop until, 3@loop until, 4@gate (unordered; took 4@gate first) +step 5: token 2@loop until, token 3@loop until, token 4@loop until, token 6@nap, token 7@watch, token 9@nap, token 10@watch stmt loop until iteration 1 stmt node slow - stmt assign entered - eval feature entered -> 2 - eval literal 1 -> 1 - eval operator + -> 3 - stmt if - eval feature entered -> 3 - eval literal 2 -> 2 - eval operator <= -> false + stmt action body + stmt assign entered + eval feature entered -> 2 + eval literal 1 -> 1 + eval operator + -> 3 + stmt node inner +enter action node: inner + eval literal 5 -> 5 + eval index -> 5 [s] +step 1: token 1@rest + eval literal 10 -> 10 + eval index -> 10 [s] +choice step 6: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) +step 6: token 2@loop until, token 3@loop until, token 4@loop until, token 6@nap, token 7@watch, token 9@nap, token 10@watch, token 12@nap, token 13@watch +choice step 7: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) +choice step 7: tokens 12@nap, 13@watch (unordered; took 13@watch first) + stmt terminate +terminate action node slow: dropped token 12@nap, token 13@stop stmt assign passed eval feature passed -> 0 eval literal 1 -> 1 eval operator + -> 1 - stmt if - eval feature passed -> 1 - eval literal 1 -> 1 - eval operator == -> true - stmt terminate -terminate action node slow: no token dropped -terminate action node slow: no token dropped stmt assign later eval feature later -> 0 eval literal 1 -> 1 eval operator + -> 1 eval literal true -> true +choice step 7: tokens 9@nap, 10@watch (unordered; took 10@watch first) + stmt terminate +terminate action node slow: dropped token 9@nap, token 10@stop stmt assign passed eval feature passed -> 1 eval literal 1 -> 1 eval operator + -> 2 - stmt if - eval feature passed -> 2 - eval literal 1 -> 1 - eval operator == -> false stmt assign later eval feature later -> 1 eval literal 1 -> 1 eval operator + -> 2 eval literal true -> true +choice step 7: tokens 6@nap, 7@watch (unordered; took 7@watch first) + stmt terminate +terminate action node slow: dropped token 6@nap, token 7@stop stmt assign passed eval feature passed -> 2 eval literal 1 -> 1 eval operator + -> 3 - stmt if - eval feature passed -> 3 - eval literal 1 -> 1 - eval operator == -> false stmt assign later eval feature later -> 2 eval literal 1 -> 1 eval operator + -> 3 eval literal true -> true -choice step 6: writes passed := 3 by token 2, passed := 2 by token 3, passed := 1 by token 4 (unordered; passed := 3 by token 2 stood) -choice step 6: writes later := 3 by token 2, later := 2 by token 3, later := 1 by token 4 (unordered; later := 3 by token 2 stood) -choice step 6: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) -step 6: token 2@done, token 3@done, token 4@done -choice step 7: tokens 2@done, 3@done, 4@done (unordered; took 4@done first) -step 7: no active tokens +choice step 7: writes passed := 3 by token 2, passed := 2 by token 3, passed := 1 by token 4 (unordered; passed := 3 by token 2 stood) +choice step 7: writes later := 3 by token 2, later := 2 by token 3, later := 1 by token 4 (unordered; later := 3 by token 2 stood) +choice step 7: tokens 2@loop until, 3@loop until, 4@loop until (unordered; took 4@loop until first) +step 7: token 2@done, token 3@done, token 4@done +choice step 8: tokens 2@done, 3@done, 4@done (unordered; took 4@done first) +step 8: no active tokens