From b626ab824e74256f578b20ac5fead5ab7687beef Mon Sep 17 00:00:00 2001 From: Christian-Manuel Butzke Date: Wed, 1 Jul 2026 20:46:43 +0900 Subject: [PATCH] =?UTF-8?q?engine:=20choice=20pseudostate=20resolution=20+?= =?UTF-8?q?=20validation=20(SPEC=20=C2=A75.5.1)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Recognize choice nodes (a 'choice' branch list) as transient pseudostates, excluded from the active configuration. In run_transition, when a target resolves to a choice, run the triggering action, then resolve the branch chain in the source scope (first passing guard or the mandatory else; branch action runs; chained choices repeat) to a real target, then exit/enter as an external transition. Validate: exactly one else and last (collect_errors); branch targets resolve and the choice graph is acyclic (Machine build). Bundle the updated schema, bump to 0.0.2, add cases 23-25 to the harness, and add unit tests. Closes #34. --- README.md | 5 +- conformance/harness.py | 14 ++- conformance/test_conformance.py | 9 +- pyproject.toml | 2 +- src/harel/__init__.py | 2 +- src/harel/data/machine.schema.json | 14 ++- src/harel/instance.py | 34 +++++++ src/harel/model.py | 40 ++++++++ src/harel/validator.py | 21 ++++ tests/test_choice.py | 150 +++++++++++++++++++++++++++++ 10 files changed, 283 insertions(+), 8 deletions(-) create mode 100644 tests/test_choice.py diff --git a/README.md b/README.md index 1a19ba3..a698e19 100644 --- a/README.md +++ b/README.md @@ -11,9 +11,10 @@ Implements the **harel spec v0.0.1** (early alpha; all fruwehq harel repos share [synchronized version](https://github.com/fruwehq/harel)). Status: **passing the full conformance suite** — all 22 engine cases -(`conformance/01`–`22`) plus `conformance/cli/01`–`02`. Implements YAML 1.2 loading +(`conformance/01`–`25`) plus `conformance/cli/01`–`03`. Implements YAML 1.2 loading + validation, the full statechart semantics (RTC dispatch, hierarchy, orthogonal -regions + `done`, shallow/deep history, esvs, CEL guards, structured actions, +regions + `done`, shallow/deep history, choice pseudostates, esvs, CEL guards, +structured actions, active objects + bus, defer, timers, faults), static contracts, snapshot round-trip + safe-point migration, Mermaid `export`, and the §13 CLI. Built up the build order in [issue #3][issue]. diff --git a/conformance/harness.py b/conformance/harness.py index 0f3fd0e..6c2b3cb 100644 --- a/conformance/harness.py +++ b/conformance/harness.py @@ -60,6 +60,9 @@ def conformance_root() -> Path: "20-contract-fail", "21-snapshot-roundtrip", "22-migration", + "23-choice", + "24-choice-chain", + "25-choice-invalid", } ) @@ -156,7 +159,15 @@ def run_engine_case(case: EngineCase) -> None: assert case.machine_files, f"{case.name}: no machine files" if "static" in test: - root_raw = load_definitions(case.machine_files[0].read_text(encoding="utf-8"))[0].raw + from harel import ValidationError + + expected = bool(test["static"]["valid"]) + try: + root_raw = load_definitions(case.machine_files[0].read_text(encoding="utf-8"))[0].raw + except ValidationError: + # invalid at load time (schema / structural / choice rules) + assert expected is False, f"{case.name}: expected valid but load failed" + return errors = list(collect_errors(root_raw)) contracts: dict[str, dict[str, Any]] = {} cdir = case.path / "contracts" @@ -166,7 +177,6 @@ def run_engine_case(case: EngineCase) -> None: contracts[c["id"]] = c errors.extend(validate_contracts(root_raw, contracts)) valid = not errors - expected = bool(test["static"]["valid"]) assert valid is expected, ( f"{case.name}: static valid={valid} != {expected} ({errors})" ) diff --git a/conformance/test_conformance.py b/conformance/test_conformance.py index bf8ec37..34dad67 100644 --- a/conformance/test_conformance.py +++ b/conformance/test_conformance.py @@ -55,8 +55,15 @@ def _spec_schema() -> dict | None: def _each_machine_file() -> list[pytest.Param]: + import yaml + params: list[pytest.Param] = [] for case in engine_cases(): + # A `static: { valid: false }` case may hold a deliberately invalid machine + # (it must NOT load cleanly), so exclude it from the "loads and validates" gate. + test = yaml.safe_load(case.test_file.read_text(encoding="utf-8")) or {} + if test.get("static", {}).get("valid") is False: + continue for mf in case.machine_files: params.append(pytest.param(mf, id=f"{case.name}:{mf.name}")) for case in cli_cases(): @@ -85,7 +92,7 @@ def test_bundled_schema_matches_spec() -> None: def test_suite_present() -> None: if not CONFORMANCE_DIR.exists(): pytest.skip("conformance suite not fetched (offline; set HAREL_CONFORMANCE_DIR)") - assert len(engine_cases()) == 22, "expected 22 engine cases" + assert len(engine_cases()) == 25, "expected 25 engine cases" assert len(cli_cases()) == 3, "expected 3 CLI cases" diff --git a/pyproject.toml b/pyproject.toml index 62465cd..de5f173 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "harel-python" -version = "0.0.1" +version = "0.0.2" description = "Python reference implementation of the harel statechart engine" readme = "README.md" requires-python = ">=3.11" diff --git a/src/harel/__init__.py b/src/harel/__init__.py index 7869902..5d06197 100644 --- a/src/harel/__init__.py +++ b/src/harel/__init__.py @@ -43,7 +43,7 @@ "__version__", ] -__version__ = "0.0.1" +__version__ = "0.0.2" # Diagnostic logging under the ``harel`` logger; silent unless the host app # configures logging (e.g. ``logging.basicConfig(level=logging.DEBUG)``). diff --git a/src/harel/data/machine.schema.json b/src/harel/data/machine.schema.json index 48741d6..f83b948 100644 --- a/src/harel/data/machine.schema.json +++ b/src/harel/data/machine.schema.json @@ -136,6 +136,17 @@ } }, + "choiceBranch": { + "type": "object", + "required": ["transition_to"], + "additionalProperties": false, + "properties": { + "transition_to": { "$ref": "#/$defs/dottedRef" }, + "guard": { "$ref": "#/$defs/cel" }, + "action": { "$ref": "#/$defs/actionList" } + } + }, + "after": { "type": "object", "required": ["duration"], @@ -172,7 +183,8 @@ "on_events": { "type": "object", "additionalProperties": { "$ref": "#/$defs/transitionOrList" } }, "after": { "type": "array", "items": { "$ref": "#/$defs/after" } }, "defer": { "type": "array", "items": { "$ref": "#/$defs/identifier" } }, - "history": { "enum": ["none", "shallow", "deep"], "default": "none" } + "history": { "enum": ["none", "shallow", "deep"], "default": "none" }, + "choice": { "type": "array", "minItems": 2, "items": { "$ref": "#/$defs/choiceBranch" } } }, "allOf": [ { diff --git a/src/harel/instance.py b/src/harel/instance.py index d95eab5..61daa43 100644 --- a/src/harel/instance.py +++ b/src/harel/instance.py @@ -303,6 +303,17 @@ def run_transition( self.run_actions(actions, owner, event) return target = self.machine.resolve_target(owner, target_ref) + if target.type == "choice": + # Dynamic branching (§5.5.1): run the triggering action, then resolve the + # choice chain in the SOURCE scope (branch guards see the just-assigned + # esvs), then execute as an external transition to the real target. + self.run_actions(actions, owner, event) + target = self._resolve_choice(target, owner, event) + self._last_target = target.name + lca = self.machine.lca(owner, target) + self.exit_states(owner, lca, False) + self.enter_to(lca, target) + return self._last_target = target.name local = bool(transition.get("local")) if local: @@ -313,6 +324,29 @@ def run_transition( self.run_actions(actions, owner, event) self.enter_to(lca, target) + def _resolve_choice(self, node: State, owner: State, event: Event) -> State: + """Resolve a choice pseudostate chain to a real target state (SPEC §5.5.1). + + Branches are tried in order (first passing guard, or the unguarded default); + the chosen branch's action runs in the source scope; chained choices repeat. + """ + seen: set[str] = set() + while node.type == "choice": + if node.path in seen: + raise HarelError(f"cyclic choice '{node.name}'") + seen.add(node.path) + chosen: dict[str, Any] | None = None + for br in node.raw.get("choice") or []: + guard = br.get("guard") + if guard is None or cel.evaluate(guard, self.scope(owner, event)): + chosen = br + break + if chosen is None: + raise HarelError(f"choice '{node.name}' has no matching branch") + self.run_actions(chosen.get("action") or [], owner, event) + node = self.machine.resolve_target(node, chosen["transition_to"]) + return node + # --- completion --------------------------------------------------------- def _complete_composites(self) -> set[str]: """Active composite/orthogonal states whose region(s) all reached final.""" diff --git a/src/harel/model.py b/src/harel/model.py index 627294d..5f2c20e 100644 --- a/src/harel/model.py +++ b/src/harel/model.py @@ -38,6 +38,8 @@ def _infer_type(raw: dict[str, Any]) -> str: declared = raw.get("type") if isinstance(declared, str): return declared + if "choice" in raw: + return "choice" # a transient pseudostate (SPEC §5.5.1) if "regions" in raw: return "orthogonal" if "states" in raw: @@ -164,6 +166,9 @@ def _validate_references(self) -> None: for after in state.raw.get("after") or []: if "transition_to" in after: refs.append((after["transition_to"], f"{state.path}/after")) + for i, br in enumerate(state.raw.get("choice") or []): + if "transition_to" in br: + refs.append((br["transition_to"], f"{state.path}/choice/{i}")) for ref, where in refs: try: self.resolve_target(state, ref) @@ -174,9 +179,44 @@ def _validate_references(self) -> None: message=f"unresolved target '{ref}' from '{state.name}'", ) ) + errors.extend(self._choice_cycle_errors()) if errors: raise ValidationError(errors) + def _choice_cycle_errors(self) -> list[ErrorRecord]: + """Choices reachable via `transition_to` MUST be acyclic (§5.5.1).""" + errors: list[ErrorRecord] = [] + for state in self.by_path.values(): + if state.type != "choice": + continue + seen: set[str] = set() + node: State | None = state + while node is not None and node.type == "choice": + if node.path in seen: + errors.append( + ErrorRecord( + path=f"/top/{state.path}/choice", + message=f"cyclic choice reachable from '{state.name}'", + ) + ) + break + seen.add(node.path) + # follow the default (else) branch — a cycle on any branch shows here + # because every branch target is itself checked as a choice root. + branches = node.raw.get("choice") or [] + nxt = None + for br in branches: + if "transition_to" in br: + try: + cand = self.resolve_target(node, br["transition_to"]) + except KeyError: + continue + if cand.type == "choice": + nxt = cand + break + node = nxt + return errors + def _as_transition_list(spec: Any) -> list[dict[str, Any]]: if isinstance(spec, list): diff --git a/src/harel/validator.py b/src/harel/validator.py index 79f01ff..92ca5f3 100644 --- a/src/harel/validator.py +++ b/src/harel/validator.py @@ -94,6 +94,24 @@ def _reserved_name_errors(doc: dict[str, Any]) -> list[ErrorRecord]: return errors +def _check_choice(path: str, branches: list[Any], errors: list[ErrorRecord]) -> None: + """A choice MUST have exactly one default (unguarded) branch, and it MUST be last + (SPEC §5.5.1).""" + defaults = [i for i, br in enumerate(branches) if isinstance(br, dict) and "guard" not in br] + if not defaults: + errors.append( + ErrorRecord(path=f"{path}/choice", message="choice has no default (else) branch") + ) + elif len(defaults) > 1: + errors.append( + ErrorRecord(path=f"{path}/choice", message="choice has more than one default branch") + ) + elif defaults[0] != len(branches) - 1: + errors.append( + ErrorRecord(path=f"{path}/choice", message="the default (else) branch must be last") + ) + + def _forbid( name: object, reserved: frozenset[str], path: str, errors: list[ErrorRecord] ) -> None: @@ -112,6 +130,9 @@ def _walk_state(path: str, state: Any, errors: list[ErrorRecord]) -> None: """ if not isinstance(state, dict): return + choice = state.get("choice") + if isinstance(choice, list): + _check_choice(path, choice, errors) esvs = state.get("esvs") if isinstance(esvs, dict): for name in esvs: diff --git a/tests/test_choice.py b/tests/test_choice.py new file mode 100644 index 0000000..fe44581 --- /dev/null +++ b/tests/test_choice.py @@ -0,0 +1,150 @@ +"""Choice pseudostate — dynamic branching, chaining, and validation (SPEC §5.5.1).""" + +from __future__ import annotations + +import pytest + +from harel import Host, collect_errors, load_definitions +from harel.errors import ValidationError +from harel.model import Machine + +ATM = """\ +id: atm +events: + withdraw: { payload: { amount: { type: int, required: true } } } + reset: {} +top: + esvs: + balance: { type: int, init: 100 } + requested: { type: int, init: 0 } + initial: { transition_to: idle } + states: + idle: + on_events: + withdraw: + action: [ { assign: { requested: "event.payload.amount" } } ] + transition_to: check + check: + choice: + - { guard: "requested <= balance", transition_to: dispensing, + action: [ { assign: { balance: "balance - requested" } } ] } + - { transition_to: insufficient } + dispensing: + on_events: { reset: { transition_to: idle } } + insufficient: + on_events: { reset: { transition_to: idle } } +""" + + +def _atm() -> tuple[Host, object]: + host = Host() + host.register_all(load_definitions(ATM)) + inst = host.create_root(host.machines["atm"], "r") + host.run_to_quiescence() + return host, inst + + +def test_choice_branches_on_freshly_assigned_esv() -> None: + host, inst = _atm() + host.deliver("r", "withdraw", {"amount": 40}) # requested:=40; 40<=100 -> dispensing + host.run_to_quiescence() + assert inst.active_leaf_names() == ["dispensing"] + assert inst.resolved_esvs()["balance"] == 60 + assert inst.resolved_esvs()["requested"] == 40 + + +def test_choice_else_branch() -> None: + host, inst = _atm() + host.deliver("r", "withdraw", {"amount": 500}) # 500<=100 false -> else -> insufficient + host.run_to_quiescence() + assert inst.active_leaf_names() == ["insufficient"] + assert inst.resolved_esvs()["balance"] == 100 # unchanged + + +CHAIN = """\ +id: chain +events: + go: { payload: { n: { type: int, required: true } } } +top: + esvs: { n: { type: int, init: 0 } } + initial: { transition_to: start } + states: + start: + on_events: + go: { action: [ { assign: { n: "event.payload.n" } } ], transition_to: c1 } + c1: + choice: + - { guard: "n < 0", transition_to: negative } + - { transition_to: c2 } + c2: + choice: + - { guard: "n == 0", transition_to: zero } + - { transition_to: positive } + negative: {} + zero: {} + positive: {} +""" + + +@pytest.mark.parametrize("n,expected", [(-3, "negative"), (0, "zero"), (7, "positive")]) +def test_chained_choices(n: int, expected: str) -> None: + host = Host() + host.register_all(load_definitions(CHAIN)) + inst = host.create_root(host.machines["chain"], "r") + host.run_to_quiescence() + host.deliver("r", "go", {"n": n}) + host.run_to_quiescence() + assert inst.active_leaf_names() == [expected] + + +# --- validation ------------------------------------------------------------- +def _machine(pick_branches: str) -> str: + return f"""\ +id: m +events: {{ go: {{}} }} +top: + esvs: {{ x: {{ type: int, init: 1 }} }} + initial: {{ transition_to: a }} + states: + a: {{ on_events: {{ go: {{ transition_to: pick }} }} }} + pick: {{ choice: {pick_branches} }} + b: {{}} + c: {{}} +""" + + +def test_no_else_is_rejected() -> None: + import yaml + src = _machine('[ { guard: "x > 0", transition_to: b }, { guard: "x < 0", transition_to: c } ]') + errs = collect_errors(yaml.safe_load(src)) + assert any("default" in e["message"] for e in errs) + with pytest.raises(ValidationError): + load_definitions(src) + + +def test_else_must_be_last() -> None: + import yaml + src = _machine('[ { transition_to: b }, { guard: "x > 0", transition_to: c } ]') + errs = collect_errors(yaml.safe_load(src)) + assert any("last" in e["message"] for e in errs) + + +def test_cyclic_choice_rejected() -> None: + src = """\ +id: cyc +events: { go: {} } +top: + initial: { transition_to: a } + states: + a: { on_events: { go: { transition_to: c1 } } } + c1: { choice: [ { transition_to: c2 } ] } + c2: { choice: [ { transition_to: c1 } ] } +""" + with pytest.raises(ValidationError): + Machine(load_definitions(src)[0]) + + +def test_unresolved_branch_target_rejected() -> None: + src = _machine('[ { guard: "x > 0", transition_to: nowhere }, { transition_to: b } ]') + with pytest.raises(ValidationError): + Machine(load_definitions(src)[0])