diff --git a/README.md b/README.md index cd13982..376a5a4 100644 --- a/README.md +++ b/README.md @@ -45,6 +45,14 @@ The [synthetic tool-library example](examples/tool-library/README.md) includes a The [version-2 contract](docs/verifier-v2.md) and [synthetic fixture](examples/verifier/valid.json) specify the finite semantics. Use `--scenario S1 --view` to retrieve a context slice, while running checks against the full model. The [FHWA slice](docs/fhwa-merge-slice.md) is an unaccepted formalization proposal. [FRET reuse](docs/fret-spike.md), [context measurement](docs/context-measurement.md), and the separate [protected-runner boundary](docs/protected-runner.md) record limits and next work. +The optional [engineering view-quality checks](docs/engineering-view-quality.md) +validate declared function roots/levels/parent links and ordered participant +exchanges, with task-specific counts, coverage, timing, and justified exceptions. +The skills assess action meaning and engineering adequacy with the engineer; +structural acceptance does not establish either. Existing unannotated models +retain their current checks. Try the neutral fixture with +`python3 scripts/sysml.py examples/sysml/views/sample-handling.sysml --syntax-only --view-profile examples/sysml/views/task-profile.json`. + ## Use the skills The repository registers its three skills through symlinks under `.agents/skills/`, which Codex discovers when you open this project. They remain independently invocable and are scoped to this repository. Start a new project conversation if the skill selector has not refreshed. [Codex skill discovery](https://learn.chatgpt.com/docs/build-skills) documents repository scope and symlink support. diff --git a/docs/engineering-view-quality.md b/docs/engineering-view-quality.md new file mode 100644 index 0000000..fe5123a --- /dev/null +++ b/docs/engineering-view-quality.md @@ -0,0 +1,154 @@ +# Function and operational view quality + +Use rigor appropriate to the question, model maturity, and requested deliverable. +Identify the task brief's requested views, levels, scope, timing, and completeness +before drafting; carry these into an explicit task profile when computable. No +universal breadth, depth, number of functions, or timing requirement is implied. +Do not substitute an academic rubric for a general engineering rule. + +Functions describe actions or transformations. Prefer verb-object names such as +`CaptureSample`, with context, inputs, and outputs where useful. Parts/components +and actors name the entities that perform or participate in actions; a component +list is not a function decomposition. A dictionary of verbs or a naming regex +cannot determine whether a function has engineering meaning. The engineer must +assess that meaning, relevance, abstraction, coverage, and any naming exceptions. + +A **function tree** shows decomposition: one explicit level-0/root function, +numbered decomposition levels, and parent-child traceability. It does not specify +execution order. An **activity diagram** shows actions and control/object flow, +including decisions, concurrency, and loops as appropriate. A **sequence diagram** +shows participants and meaningful exchanges in order; it does not establish a +function hierarchy. Do not claim that a tree or an ordered narrative is an +executable activity/interaction model. Permitted behavior loops are distinct from +invalid cycles in a function decomposition. + +When a hierarchy is requested, record its root, each node's level, and its parent; +check requested levels and scope, including skipped levels, orphans, cycles, and +duplicate IDs. Establish breadth/depth/count constraints only from the actual task +or an engineer-directed profile. A shallow exploration may be sufficient. When +sequences are requested, establish the participants and ordered exchanges with +clear purpose and content. Include timing ranges when required by the brief or +rubric, or when useful and supported: numeric nonnegative min <= max, duration +units, and a timing reference/basis. Preserve unresolved timing instead of inventing +numbers. Review meaning and completeness with the engineer; machine structure +checks cannot settle either. + +## Opt-in documentary checks in the authoritative SysML model + +The existing three skill entry points support the same command: + +```sh +python3 skills/develop-system-concept/scripts/cse.py check \ + examples/sysml/views/sample-handling.sysml --syntax-only \ + --view-profile examples/sysml/views/task-profile.json --json +``` + +Use the actual skill/runtime path from another directory. `--kind` can still be +added for the requested skill's ordinary draft-shape check. Existing models with +no `cseViews` annotation and no profile retain their earlier checks. Legacy +version-1 JSON helpers keep their existing semantics; do not retrofit their prose +with executable logic or claim they perform these new checks. + +One package-owned `doc cseViews` block across the explicitly supplied model files +contains a `CSE-VIEWS/1.0` header followed by a JSON object with a `views` list. +Duplicate JSON keys, unknown fields in supported records, and malformed values +are errors. This is **documentary metadata**, not native SysML decomposition, +ownership, allocation, flow, or timing constraints. It stays within the model, +and binds uniquely by exact qualified name to extracted native elements. The +checker never manufactures missing elements or changes native model semantics. +Unsupported bindings require explicit modeling support rather than proxies. + +The [synthetic example](../examples/sysml/views/sample-handling.sysml) and +[task profile](../examples/sysml/views/task-profile.json) demonstrate both kinds: + +| Record | Fields and interpretation | +| --- | --- | +| Function tree | `id`, `kind: "function_tree"`, `nodes` list. Each node has `id`, `element` (native action definition or usage qualified name), `level` (nonnegative integer), and `parent` (node ID or null for root). One explicit level-0 root; each child is exactly one level below its parent. Native action bindings and IDs must be unique within this view. | +| Sequence | `id`, `kind: "sequence"`, `participants`, `exchanges`. Participants have `id` and `element` (native part **usage** qualified name). Participant bindings must be unique in the view. Exchanges are in list order, each with `id`, `from`, `to`, and nonempty `message`. Self exchanges are permitted. | +| Exchange timing | Optional `timing: {min, max, unit, basis}`. Both bounds are finite, nonnegative JSON numbers, min <= max. Units: singular/plural millisecond, second, minute, hour. `basis` states what elapsed interval is described. No conversion, timing execution, or cross-exchange arithmetic is performed. | + +View IDs are unique across the block. Node IDs are unique within a tree. +Participant and exchange IDs share a unique namespace within each sequence. +The same native element may appear in different views; refer to it by qualified +name rather than assuming identical local IDs imply a cross-view trace. +The current parser extracts only part usages outside part definitions for +participant binding. Other native structures remain outside this bounded checker. +An empty tree or sequence fails. An unrecognized kind, including `activity`, is +`unsupported`; existing activity models without this annotation remain unaffected. + +## Compatibility with maintained workflow metadata + +The unmerged `codex/cse-foundation-20261012` line already provides native role +bindings, acyclic `decomposes` relations, hierarchy parent checks, documentary +step precedence, and a source/geometry-qualified function diagram adapter. +This increment adds task-specific levels/counts/coverage and participant message +timing checks; it does not replace those features or change their renderer. + +If a supplied model also contains `cseWorkflow`, the new metadata supplements +that existing hierarchy. The checker reads its exact `CSE-WORKFLOW/1.0` header, +`workflow-1.0` version and identity/relation surface with strict JSON parsing. +Each tree node must use the unique existing **function ID** for its exact native +action binding. Its parent edges must match existing `decomposes` edges in the +selected scope, including any external parent of a nonroot selected node. +A scoped root may retain an outside parent as context. Omitted children outside +the selected scope are listed in `workflow_reconciliation.omitted_children`; +the task profile and engineer determine whether those omissions are appropriate. +Conflicting or ambiguous representations refuse the result. A documentary +`precedes`, information, or control relationship is never converted to hierarchy. + +This bounded comparison covers selected identities and decomposition edges; it +is not a full workflow, source, decision, or source-diagram validation. Run the +maintained workflow checks separately when using that runtime. The existing +workflow sequence view represents step precedence; the new participant/exchange +annotation is explicitly a distinct documentary sequence contract. Do not infer +cross-view order or native behavior from either. No unpublished branch dependency +is imported by this increment. + +## Task profile and justified tailoring + +`--view-profile PATH.json` supplies version 1 and a `views` list. Each entry +requires `id` and `kind`, identifying a required view. The profile is explicit +input, never discovered or derived from the draft to claim independent review. +The report binds it by a content digest. No profile is a protected acceptance +channel; the engineer retains authority over scope and exceptions. + +Optional profile fields: + +| Field | Meaning | +| --- | --- | +| `required_levels` | Function tree only: unique nonnegative integer levels that must be represented. | +| `level_counts` | Function tree only: map of decimal level strings to `{min, max}` count bounds (either bound may be omitted). Counts include only nodes in this view. | +| `child_counts` | Function tree only: map of parent node IDs to count bounds for direct children. The parent must exist, even for min 0. | +| `required_ids` | Required node IDs for a tree, or participant/exchange IDs for a sequence. This checks declared coverage, not engineering completeness. | +| `require_timing` | Sequence only: Boolean, default false. When true, each exchange needs timing. | +| `exceptions` | List of `{rule, target, rationale}` for actual task-profile gaps. Each rationale must be nonempty. Rules: `required_level`, `level_count`, `child_count`, `required_id`, or sequence `timing`. Targets are level strings, node IDs, or exchange IDs as applicable. | + +Counts have no default limits. To tailor a one-level study, request only its +needed levels; do not impose deeper decomposition. To retain a justified gap, +record the actual rationale in the task profile, for example: + +```json +{"rule": "timing", "target": "E2", "rationale": "Exploratory archive interface; timing deferred pending measurement."} +``` + +The report exposes every used exception; unused/duplicate exceptions are errors. +A rationale string does not authenticate engineer approval. Exceptions cannot +waive malformed structure, cycles, orphans, duplicate IDs, wrong native bindings, +or invalid timing values. Revise consequential scope or exceptions as a proposal +for the engineer; do not silently relax them to obtain success. + +## What the result means + +The nested `view_checks` report has claim scope `documentary_view_structure`. +Malformed contract/input gives `error`, structurally invalid declarations give +`fail`, missing requested views/levels/coverage/timing give `unknown`, and +unimplemented kinds give `unsupported`. These findings propagate into the parent +check status; none can yield an overall successful requested check. A pass with +exceptions means the declared structure and explicitly tailored profile passed. + +The report always identifies outstanding human assessments. Nonempty names, +messages, and rationale cannot prove action meaning, exchange usefulness, +adequate decomposition, task completeness, source truth, stakeholder acceptance, +realistic timing, or actual system behavior. Syntax, documentary structure, +controlled-clause compilation, synthetic tests, and supplied behavior evidence +remain separate claims. A local check is not protected execution. diff --git a/examples/sysml/views/sample-handling.sysml b/examples/sysml/views/sample-handling.sysml new file mode 100644 index 0000000..03dab63 --- /dev/null +++ b/examples/sysml/views/sample-handling.sysml @@ -0,0 +1,36 @@ +package SampleHandling { + doc /* Entirely synthetic view-check example. No engineering acceptance claimed. */ + part def Operator; + part def Station; + part def Archive; + part operator : Operator; + part station : Station; + part archive : Archive; + + action def ProcessSample; + action def CaptureSample; + action def StoreSample; + action def ValidateSample; + + doc cseViews /* + CSE-VIEWS/1.0 + {"views": [ + {"id": "FT", "kind": "function_tree", "nodes": [ + {"id": "F0", "element": "SampleHandling::ProcessSample", "level": 0, "parent": null}, + {"id": "F1", "element": "SampleHandling::CaptureSample", "level": 1, "parent": "F0"}, + {"id": "F2", "element": "SampleHandling::StoreSample", "level": 1, "parent": "F0"}, + {"id": "F3", "element": "SampleHandling::ValidateSample", "level": 2, "parent": "F1"} + ]}, + {"id": "SQ", "kind": "sequence", "participants": [ + {"id": "OP", "element": "SampleHandling::operator"}, + {"id": "ST", "element": "SampleHandling::station"}, + {"id": "AR", "element": "SampleHandling::archive"} + ], "exchanges": [ + {"id": "E1", "from": "OP", "to": "ST", "message": "Submit sample for capture", + "timing": {"min": 0, "max": 2, "unit": "seconds", "basis": "Elapsed after synthetic scenario trigger"}}, + {"id": "E2", "from": "ST", "to": "AR", "message": "Send validated sample record", + "timing": {"min": 1, "max": 4, "unit": "seconds", "basis": "Elapsed after E1 completes"}} + ]} + ]} + */ +} diff --git a/examples/sysml/views/task-profile.json b/examples/sysml/views/task-profile.json new file mode 100644 index 0000000..16114ca --- /dev/null +++ b/examples/sysml/views/task-profile.json @@ -0,0 +1,19 @@ +{ + "version": 1, + "views": [ + { + "id": "FT", + "kind": "function_tree", + "required_levels": [0, 1, 2], + "required_ids": ["F0", "F1", "F2", "F3"], + "level_counts": {"1": {"min": 2, "max": 4}}, + "child_counts": {"F0": {"min": 2, "max": 2}} + }, + { + "id": "SQ", + "kind": "sequence", + "required_ids": ["OP", "ST", "AR", "E1", "E2"], + "require_timing": true + } + ] +} diff --git a/scripts/check.py b/scripts/check.py index 49a26de..884b037 100644 --- a/scripts/check.py +++ b/scripts/check.py @@ -43,7 +43,7 @@ def main(): suites = ("test_develop_conops.py", "test_scenario_split.py", "test_concept.py", "test_verifier.py", "test_language.py", "test_language_oracle.py", "test_influence.py", "test_events.py", "test_public_language_cases.py", "test_sysml.py", "test_sysml_views.py", - "test_sysml_public.py", "test_skill_runtime.py") + "test_sysml_public.py", "test_skill_runtime.py", "test_engineering_views.py") for suite in suites: result = subprocess.run([sys.executable, "-B", str(ROOT / "tests" / suite)], cwd=ROOT, env=environment, text=True, diff --git a/scripts/sysml.py b/scripts/sysml.py index d36a895..f6708b2 100644 --- a/scripts/sysml.py +++ b/scripts/sysml.py @@ -20,16 +20,20 @@ def main(): parser.add_argument("--syntax-only", action="store_true", help="check SysML syntax and references without compiling CSE clauses") parser.add_argument("--kind", choices=("concept", "conops", "scenario"), help="also check the minimal model shape for this skill") + parser.add_argument("--view-profile", help="explicit task requirements for documentary function trees/sequences") parser.add_argument("--json", action="store_true") args = parser.parse_args() try: + view_profile = load_json(args.view_profile) if args.view_profile is not None else None + if args.view_profile is not None and not isinstance(view_profile, dict): + raise ValueError("View profile must be a JSON object, not null or another JSON value") manifest = load_json(args.manifest) if args.manifest else None evidence = load_json(args.evidence) if args.evidence else None except (OSError, ValueError) as exc: print(f"Cannot read input: {exc}", file=sys.stderr) return 2 report = check_sysml(args.model, manifest=manifest, evidence=evidence, review=args.review, - syntax_only=args.syntax_only, kind=args.kind) + syntax_only=args.syntax_only, kind=args.kind, view_profile=view_profile) if args.json: print(json.dumps(report, sort_keys=True, indent=2)) else: @@ -42,6 +46,10 @@ def main(): else: description = "supplied behavior evidence" print(f"{report['status']}: {description}, {len(report['results'])} compiled obligation(s)") + if "view_checks" in report: + print(f" documentary view structure: {report['view_checks']['status']}; action names, exchange meaning, and engineering adequacy need human review") + for exception in report['view_checks']['exceptions']: + print(f" exception {exception['view']}/{exception['rule']}/{exception['target']}: {exception['rationale']}") issues = report.get("parser_issues", []) for issue in issues[:8]: print(f" {issue.get('severity', 'ISSUE')} {issue.get('source')}:{issue.get('line')}: {issue.get('message')}") diff --git a/skills/develop-conops/SKILL.md b/skills/develop-conops/SKILL.md index 5e2398b..7d410d3 100644 --- a/skills/develop-conops/SKILL.md +++ b/skills/develop-conops/SKILL.md @@ -14,6 +14,8 @@ The engineer directs scope, interpretation, priorities, accepted assumptions, an 3. Integrate relevant scenarios, external responsibilities, and evaluation plans. Expose disagreement, coverage gaps, and reasons for deferral. Plan needed data and environments; distinguish improvement goals from accepted thresholds and test claims with suitable programs or evidence. 4. Incorporate feedback into affected work. Return the useful change, material findings, and any next engineer decision. Stop at the requested boundary; omit filler and repeated questionnaires. +Establish function and view quality proportionately to the requested task. Functions express actions or transformations; recommend verb-object names, distinguish them from component and actor names, and assess meaning with the engineer rather than a naive verb dictionary. A function tree expresses decomposition, an activity diagram control/object flow, and a sequence diagram ordered participant exchanges; none substitutes for another. For a requested hierarchy, establish an explicit level-0/root, numbered decomposition levels, and parent-child traceability. Check requested levels, orphans, cycles, and duplicate IDs. Tailor breadth, depth, counts, and completeness to the brief; no fixed counts apply universally. Sequences need identified participants and meaningful ordered exchanges; add numeric min <= max timing ranges with units and a timing basis when the task requires them. Keep unsupported timing unresolved. Preserve justified exceptions explicitly and consequential changes as proposals. Use the optional documentary view checks described in [the SysML record guidance](references/sysml.md); distinguish machine-verifiable structure from human assessment of action meaning, adequacy, and completeness. + For new recorded work, maintain a SysML v2 `.sysml` model as the authoritative CONOPS artifact; respect discussion-only requests. Read [the SysML record guidance](references/sysml.md) and use [the validated synthetic template](templates/default.sysml) when useful. Keep stakeholder concerns, operating modes, use cases, and qualitative uncertainties distinct. Run `python3 /scripts/cse.py check .sysml --syntax-only --kind conops` after edits; this launcher resolves the shared engine regardless of the current directory. Compile designated CSE clauses with its `check` command and run `--review` only when independent scope and supplied evidence exist. Narrative alone supplies no executable guard or effect. When a supported sampled requirement is present, run `python3 /scripts/cse.py testgen .sysml` as part of local draft evaluation and show the synthetic pass/fail variable-influence pairs. If none is present, say what remains qualitative or unsupported without inventing a threshold. Report uncovered variables and search limits; generated tests are not observed behavior evidence or FLIP coverage. diff --git a/skills/develop-conops/references/sysml.md b/skills/develop-conops/references/sysml.md index 02a39ea..a733f91 100644 --- a/skills/develop-conops/references/sysml.md +++ b/skills/develop-conops/references/sysml.md @@ -79,3 +79,42 @@ For an existing version-1 JSON record or an explicit legacy request, read `references/record.md` and use its original helper. Do not silently translate its prose into executable SysML constraints. Reconcile any migration with the engineer and record unsupported or lost meaning. + +## Requested function hierarchies and sequences + +Functions express actions (verb-object naming recommended), while components +and actors identify entities. Assess that distinction semantically with the +engineer; no verb dictionary establishes action meaning. A function tree records +decomposition with an explicit level-0 root, levels, and parent links. Activity +diagrams represent control/object flow; sequence diagrams represent participants +and ordered meaningful exchanges. Do not substitute these views for one another. +Tailor requested levels, breadth/depth counts, and coverage to the actual task; +there are no universal mandatory counts. Record justified exceptions explicitly. +Require timing only when the task calls for it; modeled ranges need finite +nonnegative numeric min <= max, duration units, and a timing reference/basis. + +The shared runtime's `docs/engineering-view-quality.md` defines optional +`doc cseViews` metadata (`CSE-VIEWS/1.0`) bound by exact qualified names to native +actions and part usages. It is a documentary view of the model, not native +ownership, decomposition, allocation, or executable behavior. For requested +levels/counts/coverage/timing, supply an explicit task profile: + +```text +python3 /scripts/cse.py check MODEL.sysml --syntax-only --view-profile PROFILE.json +``` + +Add the relevant `--kind` as before. The assistant maintains the model/profile, +runs these checks when those requested views are recorded, repairs ordinary +structural gaps, and reports remaining human judgments. A tree requires one +explicit level-0 root and consistent parent levels, without orphans, cycles, or +duplicate IDs. A sequence requires declared participants and ordered nonempty +exchanges; whether those messages are meaningful remains a human assessment. +Missing requested views/levels/coverage/timing cannot produce an overall pass. +A task profile may carry justified exceptions to its scope/count/timing gaps, +which are exposed in the report; rationale text does not authenticate approval. +Do not change accepted scope to make a check pass. Existing unannotated SysML and +legacy JSON checks preserve their prior semantics. State that those old checks +do not establish the new view-quality conditions; do not claim all existing +models were checked for them. See the shared runtime's +`examples/sysml/views/sample-handling.sysml` and `task-profile.json` for a neutral +synthetic example. Keep syntax, structure, semantic review, and behavior separate. diff --git a/skills/develop-operational-scenarios/SKILL.md b/skills/develop-operational-scenarios/SKILL.md index d0342e3..39a2047 100644 --- a/skills/develop-operational-scenarios/SKILL.md +++ b/skills/develop-operational-scenarios/SKILL.md @@ -16,6 +16,8 @@ The engineer directs scope, interpretation, accepted assumptions, and success cr 3. Run the available program checks. Investigate reported gaps, unclear intent, and unsupported assumptions. Prepare evaluation data, environments, and stakeholder feedback appropriate to the current question. Qualitative realism and stakeholder intent require evidence or engineer judgment. 4. Incorporate feedback. Return the useful change, material findings, and any next engineer decision. Stop at that work unit; additional scenarios and overall CONOPS integration are separate scope choices. Omit filler and repeated questionnaires. +Establish function and view quality proportionately to the requested task. Functions express actions or transformations; recommend verb-object names, distinguish them from component and actor names, and assess meaning with the engineer rather than a naive verb dictionary. A function tree expresses decomposition, an activity diagram control/object flow, and a sequence diagram ordered participant exchanges; none substitutes for another. For a requested hierarchy, establish an explicit level-0/root, numbered decomposition levels, and parent-child traceability. Check requested levels, orphans, cycles, and duplicate IDs. Tailor breadth, depth, counts, and completeness to the brief; no fixed counts apply universally. Sequences need identified participants and meaningful ordered exchanges; add numeric min <= max timing ranges with units and a timing basis when the task requires them. Keep unsupported timing unresolved. Preserve justified exceptions explicitly and consequential changes as proposals. Use the optional documentary view checks described in [the SysML record guidance](references/sysml.md); distinguish machine-verifiable structure from human assessment of action meaning, adequacy, and completeness. + For new recorded work, maintain a SysML v2 `.sysml` model as the authoritative scenario artifact; respect discussion-only requests. Read [the SysML record guidance](references/sysml.md) and use [the validated synthetic template](templates/default.sysml) when useful. Keep ordered interactions and unresolved outcomes explicit. Run `python3 /scripts/cse.py check .sysml --syntax-only --kind scenario` after edits; this launcher resolves the shared engine regardless of the current directory. Compile designated CSE clauses with its `check` command and run `--review` only when independent scope and supplied evidence exist. A narrative use case is not an executable step program. When a supported sampled requirement is present, run `python3 /scripts/cse.py testgen .sysml` as part of local draft evaluation and show the synthetic pass/fail variable-influence pairs. If none is present, say what remains qualitative or unsupported without inventing a threshold. Report uncovered variables and search limits; generated tests are not observed behavior evidence or FLIP coverage. diff --git a/skills/develop-operational-scenarios/references/sysml.md b/skills/develop-operational-scenarios/references/sysml.md index 02a39ea..a733f91 100644 --- a/skills/develop-operational-scenarios/references/sysml.md +++ b/skills/develop-operational-scenarios/references/sysml.md @@ -79,3 +79,42 @@ For an existing version-1 JSON record or an explicit legacy request, read `references/record.md` and use its original helper. Do not silently translate its prose into executable SysML constraints. Reconcile any migration with the engineer and record unsupported or lost meaning. + +## Requested function hierarchies and sequences + +Functions express actions (verb-object naming recommended), while components +and actors identify entities. Assess that distinction semantically with the +engineer; no verb dictionary establishes action meaning. A function tree records +decomposition with an explicit level-0 root, levels, and parent links. Activity +diagrams represent control/object flow; sequence diagrams represent participants +and ordered meaningful exchanges. Do not substitute these views for one another. +Tailor requested levels, breadth/depth counts, and coverage to the actual task; +there are no universal mandatory counts. Record justified exceptions explicitly. +Require timing only when the task calls for it; modeled ranges need finite +nonnegative numeric min <= max, duration units, and a timing reference/basis. + +The shared runtime's `docs/engineering-view-quality.md` defines optional +`doc cseViews` metadata (`CSE-VIEWS/1.0`) bound by exact qualified names to native +actions and part usages. It is a documentary view of the model, not native +ownership, decomposition, allocation, or executable behavior. For requested +levels/counts/coverage/timing, supply an explicit task profile: + +```text +python3 /scripts/cse.py check MODEL.sysml --syntax-only --view-profile PROFILE.json +``` + +Add the relevant `--kind` as before. The assistant maintains the model/profile, +runs these checks when those requested views are recorded, repairs ordinary +structural gaps, and reports remaining human judgments. A tree requires one +explicit level-0 root and consistent parent levels, without orphans, cycles, or +duplicate IDs. A sequence requires declared participants and ordered nonempty +exchanges; whether those messages are meaningful remains a human assessment. +Missing requested views/levels/coverage/timing cannot produce an overall pass. +A task profile may carry justified exceptions to its scope/count/timing gaps, +which are exposed in the report; rationale text does not authenticate approval. +Do not change accepted scope to make a check pass. Existing unannotated SysML and +legacy JSON checks preserve their prior semantics. State that those old checks +do not establish the new view-quality conditions; do not claim all existing +models were checked for them. See the shared runtime's +`examples/sysml/views/sample-handling.sysml` and `task-profile.json` for a neutral +synthetic example. Keep syntax, structure, semantic review, and behavior separate. diff --git a/skills/develop-system-concept/SKILL.md b/skills/develop-system-concept/SKILL.md index 28b0bd0..599b8dd 100644 --- a/skills/develop-system-concept/SKILL.md +++ b/skills/develop-system-concept/SKILL.md @@ -19,6 +19,8 @@ Reuse linked operational artifacts. Use available `$develop-operational-scenario Read supplied raw material in place. Keep raw source and private annotations out of Git and out of generated model/test reports; retain concise derived statements and source references needed for review. Keep user-specific models and reports in the repository's ignored `work/` directory or an approved private location on `/workspace`, and inspect Git status before any commit. If raw material is already tracked, surface that fact instead of silently copying or publishing it. +Establish function and view quality proportionately to the requested task. Functions express actions or transformations; recommend verb-object names, distinguish them from component and actor names, and assess meaning with the engineer rather than a naive verb dictionary. A function tree expresses decomposition, an activity diagram control/object flow, and a sequence diagram ordered participant exchanges; none substitutes for another. For a requested hierarchy, establish an explicit level-0/root, numbered decomposition levels, and parent-child traceability. Check requested levels, orphans, cycles, and duplicate IDs. Tailor breadth, depth, counts, and completeness to the brief; no fixed counts apply universally. Sequences need identified participants and meaningful ordered exchanges; add numeric min <= max timing ranges with units and a timing basis when the task requires them. Keep unsupported timing unresolved. Preserve justified exceptions explicitly and consequential changes as proposals. Use the optional documentary view checks described in [the SysML record guidance](references/sysml.md); distinguish machine-verifiable structure from human assessment of action meaning, adequacy, and completeness. + For new recorded work, maintain a SysML v2 `.sysml` model as the authoritative concept artifact; respect discussion-only requests. Read [the SysML record guidance](references/sysml.md) and use [the validated synthetic template](templates/default.sysml) when useful. Preserve qualitative unknowns and link operational elements rather than copying them. Run `python3 /scripts/cse.py check .sysml --syntax-only --kind concept` after edits; this launcher resolves the shared engine regardless of the current directory. Compile designated CSE clauses with its `check` command and run `--review` only when independent scope and supplied evidence exist. Ordinary documentation is not executable. When a supported sampled requirement is present, run `python3 /scripts/cse.py testgen .sysml` as part of local draft evaluation and show the synthetic pass/fail variable-influence pairs. If none is present, say what remains qualitative or unsupported without inventing a threshold. Report uncovered variables and search limits; generated tests are not observed behavior evidence or FLIP coverage. diff --git a/skills/develop-system-concept/references/sysml.md b/skills/develop-system-concept/references/sysml.md index 02a39ea..a733f91 100644 --- a/skills/develop-system-concept/references/sysml.md +++ b/skills/develop-system-concept/references/sysml.md @@ -79,3 +79,42 @@ For an existing version-1 JSON record or an explicit legacy request, read `references/record.md` and use its original helper. Do not silently translate its prose into executable SysML constraints. Reconcile any migration with the engineer and record unsupported or lost meaning. + +## Requested function hierarchies and sequences + +Functions express actions (verb-object naming recommended), while components +and actors identify entities. Assess that distinction semantically with the +engineer; no verb dictionary establishes action meaning. A function tree records +decomposition with an explicit level-0 root, levels, and parent links. Activity +diagrams represent control/object flow; sequence diagrams represent participants +and ordered meaningful exchanges. Do not substitute these views for one another. +Tailor requested levels, breadth/depth counts, and coverage to the actual task; +there are no universal mandatory counts. Record justified exceptions explicitly. +Require timing only when the task calls for it; modeled ranges need finite +nonnegative numeric min <= max, duration units, and a timing reference/basis. + +The shared runtime's `docs/engineering-view-quality.md` defines optional +`doc cseViews` metadata (`CSE-VIEWS/1.0`) bound by exact qualified names to native +actions and part usages. It is a documentary view of the model, not native +ownership, decomposition, allocation, or executable behavior. For requested +levels/counts/coverage/timing, supply an explicit task profile: + +```text +python3 /scripts/cse.py check MODEL.sysml --syntax-only --view-profile PROFILE.json +``` + +Add the relevant `--kind` as before. The assistant maintains the model/profile, +runs these checks when those requested views are recorded, repairs ordinary +structural gaps, and reports remaining human judgments. A tree requires one +explicit level-0 root and consistent parent levels, without orphans, cycles, or +duplicate IDs. A sequence requires declared participants and ordered nonempty +exchanges; whether those messages are meaningful remains a human assessment. +Missing requested views/levels/coverage/timing cannot produce an overall pass. +A task profile may carry justified exceptions to its scope/count/timing gaps, +which are exposed in the report; rationale text does not authenticate approval. +Do not change accepted scope to make a check pass. Existing unannotated SysML and +legacy JSON checks preserve their prior semantics. State that those old checks +do not establish the new view-quality conditions; do not claim all existing +models were checked for them. See the shared runtime's +`examples/sysml/views/sample-handling.sysml` and `task-profile.json` for a neutral +synthetic example. Keep syntax, structure, semantic review, and behavior separate. diff --git a/tests/test_engineering_views.py b/tests/test_engineering_views.py new file mode 100644 index 0000000..aec3a4c --- /dev/null +++ b/tests/test_engineering_views.py @@ -0,0 +1,388 @@ +"""Synthetic structural defects and valid tailoring, plus real native/CLI binding.""" + +from copy import deepcopy +import json +from pathlib import Path +import subprocess +import sys +import tempfile +import unittest +from unittest.mock import patch + +ROOT = Path(__file__).resolve().parents[1] +sys.path.insert(0, str(ROOT)) +from verifier.engineering_views import check_views +from verifier.sysml import CLASSES, JAR, check_sysml + +MODEL = ROOT / 'examples/sysml/views/sample-handling.sysml' +PROFILE = ROOT / 'examples/sysml/views/task-profile.json' + + +def fixture(): + # Unit tests exercise the view contract; only integration tests claim parsing. + body = MODEL.read_text().split('doc cseViews /*', 1)[1].split('*/', 1)[0].strip() + data = json.loads('\n'.join(body.splitlines()[1:])) + inventory = {group: [] for group in ('attributes', 'events', 'event_attributes', 'parts', + 'part_definitions', 'concerns', 'use_cases', 'actions', 'states', 'requirements', 'constraints', 'documents')} + inventory['actions'] = [{'qualified_name': node['element']} for node in data['views'][0]['nodes']] + inventory['parts'] = [{'qualified_name': item['element']} for item in data['views'][1]['participants']] + inventory['documents'] = [{'name': 'cseViews', 'owner_kind': 'Package', 'body': body}] + return data, inventory, json.loads(PROFILE.read_text()) + + +def run_case(data, inventory, profile=None): + inventory = deepcopy(inventory) + inventory['documents'][0]['body'] = 'CSE-VIEWS/1.0\n' + json.dumps(data) + return check_views(inventory, profile) + + +class ViewQualityTests(unittest.TestCase): + def setUp(self): + self.data, self.inventory, self.profile = fixture() + self.nodes = self.data['views'][0]['nodes'] + self.sequence = self.data['views'][1] + + def report(self, profile=True): + return run_case(self.data, self.inventory, self.profile if profile else None) + + def codes(self, report): + self.assertNotEqual(report['status'], 'pass', report) + return {f['code'] for f in report['findings']} + + def test_valid_structure_and_explicit_claim_limit(self): + original = deepcopy((self.inventory, self.profile)) + report = self.report() + self.assertEqual(report['status'], 'pass', report) + self.assertEqual(report['claim_scope'], 'documentary_view_structure') + self.assertTrue(report['human_review']) + self.assertEqual((self.inventory, self.profile), original) + self.assertEqual(len(report['profile_sha256']), 64) + + def test_unannotated_model_is_compatible_but_requested_view_cannot_pass(self): + self.inventory['documents'] = [] + self.assertEqual(check_views(self.inventory)['status'], 'pass') + self.assertIn('view_missing', self.codes(check_views(self.inventory, self.profile))) + + def test_missing_requested_level_and_coverage(self): + self.nodes.pop() + report = self.report() + self.assertEqual(report['status'], 'unknown') + self.assertTrue({'required_level', 'required_id'} <= self.codes(report)) + + def test_invalid_roots(self): + for mutation in ('missing', 'two', 'wrong_level', 'empty'): + data = deepcopy(self.data) + nodes = data['views'][0]['nodes'] + if mutation == 'missing': + nodes[0]['parent'] = 'F1' + elif mutation == 'two': + nodes[1].update(parent=None, level=0) + elif mutation == 'wrong_level': + nodes[0]['level'] = 1 + else: + nodes.clear() + with self.subTest(mutation=mutation): + self.assertIn('root', self.codes(run_case(data, self.inventory))) + + def test_orphan_and_skipped_levels(self): + self.nodes[1]['parent'] = 'Absent' + self.nodes[2]['level'] = 2 + self.assertTrue({'orphan', 'level'} <= self.codes(self.report())) + + def test_disconnected_cycle_and_self_cycle(self): + self.nodes[1]['parent'] = 'F3' + self.assertIn('cycle', self.codes(self.report())) + self.nodes[1]['parent'] = 'F1' + self.assertIn('cycle', self.codes(self.report())) + + def test_duplicate_ids_in_each_namespace(self): + for location in ('view', 'node', 'participant', 'exchange', 'participant_exchange'): + data = deepcopy(self.data) + seq = data['views'][1] + if location == 'view': + data['views'].append(deepcopy(data['views'][0])) + elif location == 'node': + data['views'][0]['nodes'].append(deepcopy(self.nodes[0])) + elif location == 'participant': + seq['participants'].append(deepcopy(seq['participants'][0])) + elif location == 'exchange': + seq['exchanges'].append(deepcopy(seq['exchanges'][0])) + else: + seq['exchanges'][0]['id'] = 'OP' + with self.subTest(location=location): + self.assertIn('duplicate_id', self.codes(run_case(data, self.inventory))) + + def test_binding_roles_missing_and_ambiguous_native(self): + self.nodes[1]['element'] = 'SampleHandling::station' + self.sequence['participants'][0]['element'] = 'SampleHandling::CaptureSample' + self.assertTrue({'function_binding', 'participant_binding'} <= self.codes(self.report())) + _, inv, _ = fixture() + inv['actions'].append(deepcopy(inv['actions'][0])) + inv['parts'].append(deepcopy(inv['parts'][0])) + data, _, _ = fixture() + self.assertTrue({'function_binding', 'participant_binding'} <= self.codes(run_case(data, inv))) + + def test_native_aliases_do_not_invent_functions_or_participants(self): + self.nodes[1]['element'] = self.nodes[0]['element'] + self.sequence['participants'][1]['element'] = self.sequence['participants'][0]['element'] + self.assertIn('duplicate_binding', self.codes(self.report())) + + def test_counts_are_task_specific_and_missing_parent_detected_even_min_zero(self): + for field, target, bounds in (('level_counts', '1', {'min': 5}), + ('level_counts', '1', {'max': 1}), ('child_counts', 'F0', {'min': 3}), + ('child_counts', 'Absent', {'min': 0})): + profile = deepcopy(self.profile) + profile['views'][0][field] = {target: bounds} + report = run_case(self.data, self.inventory, profile) + with self.subTest(field=field, bounds=bounds): + self.assertEqual(report['status'], 'unknown', report) + # A root-only exploration and no timing are valid without deeper task scope. + self.nodes[:] = self.nodes[:1] + for exchange in self.sequence['exchanges']: + exchange.pop('timing') + self.assertEqual(self.report(profile=False)['status'], 'pass') + + def test_sequence_requires_nonempty_exchanges_and_declared_endpoints(self): + self.sequence['exchanges'][0]['from'] = 'Absent' + self.sequence['exchanges'][0]['message'] = ' ' + self.assertTrue({'endpoint', 'exchange_text'} <= self.codes(self.report())) + self.sequence['exchanges'] = [] + self.assertIn('sequence_empty', self.codes(self.report(profile=False))) + + def test_self_exchange_and_documentary_order_are_permitted(self): + self.sequence['exchanges'][0]['to'] = 'OP' + self.sequence['exchanges'].reverse() + # List order is the declared order; not a claim about a real trace. + self.assertEqual(self.report()['status'], 'pass') + + def test_timing_required_only_by_profile(self): + self.sequence['exchanges'][0].pop('timing') + self.assertEqual(self.report(profile=False)['status'], 'pass') + self.assertIn('timing', self.codes(self.report())) + + def test_invalid_timing_never_passes_even_when_optional(self): + for values in ({'min': 3, 'max': 2}, {'min': -1}, {'max': float('inf')}, + {'max': float('nan')}, {'min': True}, {'max': '4'}, {'unit': ''}, + {'unit': 'meters'}, {'unit': []}, {'basis': ' '}): + data = deepcopy(self.data) + data['views'][1]['exchanges'][0]['timing'].update(values) + with self.subTest(values=values): + self.codes(run_case(data, self.inventory)) + self.sequence['exchanges'][0]['timing']['max'] = 0 + self.assertEqual(self.report()['status'], 'pass') + + def test_explicit_justified_exceptions_are_reported_without_semantic_acceptance(self): + self.sequence['exchanges'][0].pop('timing') + self.profile['views'][1]['exceptions'] = [{'rule': 'timing', 'target': 'E1', + 'rationale': 'Exploratory trigger; timing deferred pending measurement.'}] + report = self.report() + self.assertEqual(report['status'], 'pass', report) + self.assertEqual(report['exceptions'][0]['target'], 'E1') + self.nodes[1]['parent'] = 'Absent' + self.assertIn('orphan', self.codes(self.report())) + + def test_level_count_coverage_and_child_exceptions(self): + tree = self.profile['views'][0] + self.nodes.pop() + tree['level_counts'] = {'1': {'min': 4}} + tree['child_counts'] = {'F0': {'min': 4}} + tree['exceptions'] = [{'rule': rule, 'target': target, 'rationale': 'Synthetic deferred scope.'} + for rule, target in (('required_level', '2'), ('required_id', 'F3'), ('level_count', '1'), ('child_count', 'F0'))] + report = self.report() + self.assertEqual(report['status'], 'pass', report) + self.assertEqual(len(report['exceptions']), 4) + + def test_bad_or_unused_exceptions_are_errors_and_cannot_waive_structure(self): + for exception in ({'rule': 'cycle', 'target': 'F1', 'rationale': 'Do not waive structure'}, + {'rule': 'timing', 'target': 'E1', 'rationale': ''}, + {'rule': 'timing', 'target': 'E1', 'rationale': 'Not actually missing'}): + profile = deepcopy(self.profile) + profile['views'][1]['exceptions'] = [exception] + self.assertEqual(run_case(self.data, self.inventory, profile)['status'], 'error') + + def test_unknown_activity_does_not_substitute_for_tree(self): + self.data['views'][0]['kind'] = 'activity' + self.assertNotEqual(self.report()['status'], 'pass') + self.assertEqual(self.report(profile=False)['status'], 'unsupported') + + def test_strict_contract_rejects_typos_versions_and_invalid_counts(self): + for alteration in ('extra', 'version', 'bool_level', 'reverse_counts', 'bad_counts', 'wrong_kind', 'duplicate_profile', 'bad_list'): + data, inventory, profile = fixture() + if alteration == 'extra': + data['views'][0]['execute'] = 'not allowed' + elif alteration == 'version': + profile['version'] = True + elif alteration == 'bool_level': + data['views'][0]['nodes'][0]['level'] = False + elif alteration == 'reverse_counts': + profile['views'][0]['level_counts'] = {'1': {'min': 3, 'max': 1}} + elif alteration == 'bad_counts': + profile['views'][0]['level_counts'] = {'01': {'min': 2}} + elif alteration == 'wrong_kind': + profile['views'][1]['required_levels'] = [0] + elif alteration == 'duplicate_profile': + profile['views'].append(deepcopy(profile['views'][0])) + else: + data['views'][0]['nodes'] = 'wrong' + with self.subTest(alteration=alteration): + self.assertEqual(run_case(data, inventory, profile)['status'], 'error') + + def test_duplicate_json_keys_wrong_owner_and_multiple_blocks(self): + for body in ('CSE-VIEWS/9.0\n{}', 'CSE-VIEWS/1.0\n{"views":[],"views":[]}'): + inv = deepcopy(self.inventory) + inv['documents'][0]['body'] = body + self.assertEqual(check_views(inv)['status'], 'error') + self.inventory['documents'][0]['owner_kind'] = 'PartUsage' + self.assertEqual(check_views(self.inventory)['status'], 'error') + self.inventory['documents'] *= 2 + self.assertEqual(check_views(self.inventory)['status'], 'error') + + def test_requested_view_missing_and_wrong_kind(self): + self.data['views'].pop() + self.assertIn('view_missing', self.codes(self.report())) + self.profile['views'][0]['kind'] = 'sequence' + for field in ('required_levels', 'level_counts', 'child_counts'): + self.profile['views'][0].pop(field) + self.assertIn('view_kind', self.codes(self.report())) + + def workflow(self): + record = {field: {} for field in ("question", "sources", "elements", "relations", "workflows", "decisions", "questions", "trade_studies", "evidence")} + record["version"] = "workflow-1.0" + for node in self.nodes: + record["elements"][node["id"]] = {"kind": "function", "native_name": node["element"], + "label": node["id"], "description": "Synthetic function", "basis": None, "status": "proposed"} + if node["parent"] is not None: + record["relations"]["D" + node["id"]] = {"kind": "decomposes", "from": node["parent"], + "to": node["id"], "basis": None, "label": ""} + return record + + def with_workflow(self, record): + inventory = deepcopy(self.inventory) + inventory["documents"].append({"name": "cseWorkflow", "body": "CSE-WORKFLOW/1.0\n" + json.dumps(record)}) + return run_case(self.data, inventory, self.profile) + + def test_existing_workflow_hierarchy_must_match_without_duplicate_native_roles(self): + record = self.workflow() + report = self.with_workflow(record) + self.assertEqual(report["status"], "pass", report) + self.assertEqual(report["views"][0]["workflow_reconciliation"]["status"], "pass") + for mutation in ("reversed", "extra_parent", "alias", "missing_edge", "missing_function"): + changed = deepcopy(record) + if mutation == "reversed": + edge = changed["relations"]["DF1"] + edge["from"], edge["to"] = edge["to"], edge["from"] + elif mutation == "extra_parent": + changed["relations"]["EXTRA"] = {**changed["relations"]["DF1"], "from": "F2"} + elif mutation == "alias": + changed["elements"]["ALIAS"] = deepcopy(changed["elements"]["F1"]) + elif mutation == "missing_edge": + changed["relations"].pop("DF1") + else: + changed["elements"]["F1"]["kind"] = "step" + with self.subTest(mutation=mutation): + self.assertIn("workflow_conflict", self.codes(self.with_workflow(changed))) + + def test_workflow_external_parent_allowed_only_for_scoped_root_and_omissions_visible(self): + record = self.workflow() + record["elements"]["CONTEXT"] = {**record["elements"]["F0"], "native_name": "SampleHandling::Context"} + record["relations"]["CONTEXT_EDGE"] = {"kind": "decomposes", "from": "CONTEXT", "to": "F0", "basis": None, "label": ""} + self.assertEqual(self.with_workflow(record)["status"], "pass") + record["relations"]["CONTEXT_EDGE"]["to"] = "F1" + self.assertIn("workflow_conflict", self.codes(self.with_workflow(record))) + record["relations"].pop("CONTEXT_EDGE") + record["relations"]["OMITTED_EDGE"] = {"kind": "decomposes", "from": "F0", "to": "CONTEXT", "basis": None, "label": ""} + report = self.with_workflow(record) + self.assertEqual(report["status"], "pass") + self.assertEqual(report["views"][0]["workflow_reconciliation"]["omitted_children"], ["CONTEXT"]) + + def test_workflow_metadata_malformed_or_future_version_refuses_reconciliation(self): + for mutation in ("version", "containers", "relation", "extra"): + record = self.workflow() + if mutation == "version": + record["version"] = "workflow-9.0" + elif mutation == "containers": + record["elements"] = [] + elif mutation == "relation": + record["relations"]["DF1"]["to"] = "Absent" + else: + record["surprise"] = True + with self.subTest(mutation=mutation): + self.assertEqual(self.with_workflow(record)["status"], "error") + + def test_explicit_null_profile_cli_is_invalid_even_without_annotations(self): + # No parser is needed: invalid explicit input must fail before it runs. + (ROOT / '.tmp').mkdir(exist_ok=True) + with tempfile.TemporaryDirectory(dir=ROOT / '.tmp') as directory: + profile = Path(directory) / 'null.json' + for value in ('null', '[]', 'false', '"invalid"'): + profile.write_text(value) + result = subprocess.run([sys.executable, '-B', str(ROOT / 'scripts/sysml.py'), + str(ROOT / 'examples/sysml/concept.sysml'), '--syntax-only', '--view-profile', str(profile)], + text=True, capture_output=True) + self.assertEqual(result.returncode, 2, result.stderr + result.stdout) + self.assertIn('must be a JSON object', result.stderr) + + def test_structure_finding_propagates_to_parent_and_legacy_path_unchanged(self): + self.nodes[1]['parent'] = 'Absent' + inv = deepcopy(self.inventory) + inv['documents'][0]['body'] = 'CSE-VIEWS/1.0\n' + json.dumps(self.data) + with patch('verifier.sysml._parser_output', return_value=inv): + report = check_sysml(MODEL, syntax_only=True, view_profile=self.profile) + self.assertEqual(report['status'], 'fail', report) + self.assertIn('view_orphan', {f['code'] for f in report['findings']}) + inv['documents'] = [] + with patch('verifier.sysml._parser_output', return_value=inv): + report = check_sysml(MODEL, syntax_only=True) + self.assertEqual(report['status'], 'pass') + self.assertNotIn('view_checks', report) + + +@unittest.skipUnless(JAR.is_file() and (CLASSES / 'SysmlBridge.class').is_file(), 'Install pinned SysML parser') +class NativeViewIntegrationTests(unittest.TestCase): + def test_real_parser_binds_native_actions_parts_and_profile(self): + report = check_sysml(MODEL, syntax_only=True, view_profile=json.loads(PROFILE.read_text())) + self.assertEqual(report['status'], 'pass', report) + self.assertEqual(report['view_checks']['status'], 'pass') + self.assertEqual(len(report['inventory']['actions']), 4) + + def test_real_parser_reconciles_existing_workflow_and_rejects_conflicting_parent(self): + unit = ViewQualityTests() + unit.setUp() + record = unit.workflow() + record["question"] = {"text": "Synthetic sample-handling hierarchy", "basis": None} + (ROOT / '.tmp').mkdir(exist_ok=True) + with tempfile.TemporaryDirectory(dir=ROOT / '.tmp') as directory: + model = Path(directory) / 'joint-metadata.sysml' + source = MODEL.read_text().rsplit('}', 1)[0] + for conflict in (False, True): + if conflict: + record['relations']['DF1']['from'] = 'F2' + block = 'concern workflowContext { doc cseWorkflow /*CSE-WORKFLOW/1.0\n' + json.dumps(record) + '\n*/ }\n}' + model.write_text(source + block) + report = check_sysml(model, syntax_only=True, view_profile=json.loads(PROFILE.read_text())) + self.assertEqual(report['status'], 'fail' if conflict else 'pass', report) + if conflict: + self.assertIn('view_workflow_conflict', {f['code'] for f in report['findings']}) + + def test_all_three_entry_points_from_another_directory_and_nonzero_on_missing_level(self): + (ROOT / '.tmp').mkdir(exist_ok=True) + with tempfile.TemporaryDirectory(dir=ROOT / '.tmp') as directory: + for skill in ('develop-system-concept', 'develop-conops', 'develop-operational-scenarios'): + result = subprocess.run([sys.executable, '-B', str(ROOT / 'skills' / skill / 'scripts/cse.py'), + 'check', str(MODEL), '--syntax-only', '--view-profile', str(PROFILE), '--json'], + cwd=directory, text=True, capture_output=True) + self.assertEqual(result.returncode, 0, result.stderr + result.stdout) + self.assertEqual(json.loads(result.stdout)['view_checks']['status'], 'pass') + profile = json.loads(PROFILE.read_text()) + profile['views'][0]['required_levels'].append(3) + bad = Path(directory) / 'missing-level.json' + bad.write_text(json.dumps(profile)) + result = subprocess.run([sys.executable, '-B', str(ROOT / 'scripts/sysml.py'), str(MODEL), + '--syntax-only', '--view-profile', str(bad)], text=True, capture_output=True) + self.assertEqual(result.returncode, 1, result.stderr + result.stdout) + self.assertIn('view_required_level', result.stdout) + self.assertIn('no behavior evaluated', result.stdout) + + +if __name__ == '__main__': + unittest.main() diff --git a/verifier/engineering_views.py b/verifier/engineering_views.py new file mode 100644 index 0000000..fd48377 --- /dev/null +++ b/verifier/engineering_views.py @@ -0,0 +1,324 @@ +"""Documentary function-tree/sequence structure; never a behavioral or semantic proof.""" + +from collections import Counter +from hashlib import sha256 +import json +import math +import re + +VERSION = "cse-views-1.0" +ID = re.compile(r"[A-Za-z][A-Za-z0-9_-]{0,63}\Z") +UNITS = {"millisecond", "milliseconds", "second", "seconds", "minute", "minutes", "hour", "hours"} + + +def _object(value, required, optional=()): + if not isinstance(value, dict) or not set(required) <= set(value) or set(value) - set(required) - set(optional): + raise ValueError(f"Expected fields {sorted(required)}; optional {sorted(optional)}") + + +def _text(value): + return isinstance(value, str) and bool(value.strip()) + + +def _id(value): + return isinstance(value, str) and bool(ID.fullmatch(value)) + + +def _ids(value): + return isinstance(value, list) and all(_id(item) for item in value) and len(set(value)) == len(value) + + +def _integer(value): + return type(value) is int and value >= 0 + + +def _bounds(value): + _object(value, (), ("min", "max")) + if not value or any(not _integer(n) for n in value.values()) or value.get("min", 0) > value.get("max", math.inf): + raise ValueError("Counts need nonnegative integer min/max with min <= max") + + +def _unique_object(pairs): + result = {} + for key, value in pairs: + if key in result: + raise ValueError(f"Duplicate JSON key {key}") + result[key] = value + return result + + +def _profile(profile): + if profile is None: + return [] + _object(profile, ("version", "views")) + if type(profile["version"]) is not int or profile["version"] != 1 or not isinstance(profile["views"], list): + raise ValueError("View profile needs version 1 and views list") + seen = set() + for entry in profile["views"]: + _object(entry, ("id", "kind"), ("required_levels", "required_ids", "level_counts", "child_counts", "require_timing", "exceptions")) + if not _id(entry["id"]) or entry["id"] in seen or entry["kind"] not in ("function_tree", "sequence"): + raise ValueError("Profile views need unique IDs and supported kinds") + seen.add(entry["id"]) + if "required_ids" in entry and not _ids(entry["required_ids"]): + raise ValueError("required_ids must contain unique IDs") + if entry["kind"] == "function_tree": + if "require_timing" in entry: + raise ValueError("require_timing applies only to sequences") + levels = entry.get("required_levels", []) + if not isinstance(levels, list) or not all(_integer(n) for n in levels) or len(set(levels)) != len(levels): + raise ValueError("required_levels needs unique nonnegative integers") + for field in ("level_counts", "child_counts"): + values = entry.get(field, {}) + if not isinstance(values, dict): + raise ValueError(f"{field} must be an object") + for target, bounds in values.items(): + if not isinstance(target, str) or not (re.fullmatch(r"0|[1-9][0-9]*", target) if field == "level_counts" else _id(target)): + raise ValueError(f"Invalid {field} target") + _bounds(bounds) + else: + if set(entry) & {"required_levels", "level_counts", "child_counts"}: + raise ValueError("Hierarchy constraints apply only to function trees") + if "require_timing" in entry and type(entry["require_timing"]) is not bool: + raise ValueError("require_timing must be Boolean") + exceptions = entry.get("exceptions", []) + if not isinstance(exceptions, list): + raise ValueError("exceptions must be a list") + exception_keys = set() + for exception in exceptions: + _object(exception, ("rule", "target", "rationale")) + rule, target = exception["rule"], exception["target"] + allowed = {"required_level", "level_count", "child_count", "required_id"} if entry["kind"] == "function_tree" else {"timing", "required_id"} + if not isinstance(rule, str) or rule not in allowed or not _text(target) or not _text(exception["rationale"]): + raise ValueError("Exceptions need applicable rule, target, and nonempty rationale") + key = (rule, target) + if key in exception_keys: + raise ValueError("Duplicate exception") + exception_keys.add(key) + return profile["views"] + + +def _workflow(inventory): + """Read only the existing identity/hierarchy surface, not a workflow verdict.""" + docs = [doc for doc in inventory["documents"] if doc.get("name") == "cseWorkflow"] + if not docs: + return None + if len(docs) != 1: + raise ValueError("Reconciliation needs exactly one cseWorkflow block") + lines = docs[0]["body"].strip().splitlines() + if not lines or lines[0].strip() != "CSE-WORKFLOW/1.0": + raise ValueError("Unsupported workflow documentation header for reconciliation") + record = json.loads("\n".join(lines[1:]), object_pairs_hook=_unique_object, + parse_constant=lambda value: (_ for _ in ()).throw(ValueError(f"Nonfinite {value}"))) + _object(record, ("version", "question", "sources", "elements", "relations", "workflows", "decisions", "questions", "trade_studies", "evidence")) + if record["version"] != "workflow-1.0" or any(not isinstance(record[field], dict) for field in record if field != "version"): + raise ValueError("Unsupported workflow version or container shape for reconciliation") + for key, element in record["elements"].items(): + _object(element, ("kind", "native_name", "label", "description", "basis", "status")) + if not _id(key) or not _text(element["kind"]) or not _text(element["native_name"]): + raise ValueError("Malformed workflow element identity for reconciliation") + for key, relation in record["relations"].items(): + _object(relation, ("kind", "from", "to", "basis", "label")) + if not _id(key) or not _text(relation["kind"]) or any(not _id(relation[end]) or relation[end] not in record["elements"] for end in ("from", "to")): + raise ValueError("Malformed workflow relation identity for reconciliation") + return record + + +def _reconcile_tree(nodes, workflow): + """Compare selected native identities and directed edges; permit scoped context.""" + functions = {} + for key, element in workflow["elements"].items(): + if element["kind"] == "function": + functions.setdefault(element["native_name"], []).append(key) + for node in nodes.values(): + matches = functions.get(node["element"], []) + if len(matches) != 1 or matches[0] != node["id"]: + raise ValueError(f"{node['id']} must use the unique existing workflow function ID for {node['element']}") + expected = {(node["parent"], node["id"]) for node in nodes.values() if node["parent"] is not None} + edges = [(relation["from"], relation["to"]) for relation in workflow["relations"].values() + if relation["kind"] == "decomposes" and relation["to"] in nodes + and (nodes[relation["to"]]["parent"] is not None or relation["from"] in nodes)] + if set(edges) != expected or len(edges) != len(set(edges)): + raise ValueError("View parent links conflict with existing workflow decomposes edges in selected scope") + return {"claim_scope": "selected_workflow_function_identities_and_decomposition_edges", + "status": "pass", "omitted_children": sorted({relation["to"] for relation in workflow["relations"].values() + if relation["kind"] == "decomposes" and relation["from"] in nodes and relation["to"] not in nodes})} + + +def check_views(inventory, profile=None): + """Check package-owned cseViews docs against native bindings and optional task scope.""" + report = {"status": "pass", "checker_version": VERSION, + "claim_scope": "documentary_view_structure", "findings": [], "views": [], + "exceptions": [], "human_review": ["Functions express actions; verb-object names are recommended.", + "Assess decomposition adequacy and exchange meaning against the task and source.", + "Counts, text, bindings, and rationale do not establish completeness, approval, or behavior."]} + def issue(code, detail, view=None, status="fail"): + report["findings"].append({"code": code, "detail": detail, **({"view": view} if view else {})}) + rank = {"pass": 0, "unsupported": 1, "unknown": 2, "fail": 3, "error": 4} + if rank[status] > rank[report["status"]]: + report["status"] = status + try: + requirements = _profile(profile) + if profile is not None: + report["profile_sha256"] = sha256(json.dumps(profile, sort_keys=True, allow_nan=False).encode()).hexdigest() + docs = [doc for doc in inventory["documents"] if doc.get("name") == "cseViews"] + if not docs: + if requirements: + issue("view_missing", "No cseViews block for requested views", status="unknown") + return report + if len(docs) != 1 or docs[0].get("owner_kind") != "Package": + raise ValueError("Exactly one package-owned cseViews block is supported per supplied model set") + lines = docs[0]["body"].strip().splitlines() + if not lines or lines[0].strip() != "CSE-VIEWS/1.0": + raise ValueError("Expected CSE-VIEWS/1.0 header") + data = json.loads("\n".join(lines[1:]), object_pairs_hook=_unique_object, + parse_constant=lambda value: (_ for _ in ()).throw(ValueError(f"Nonfinite {value}"))) + _object(data, ("views",)) + if not isinstance(data["views"], list): + raise ValueError("views must be a list") + workflow = _workflow(inventory) + views = {} + for view in data["views"]: + if not isinstance(view, dict) or not _id(view.get("id")) or not _text(view.get("kind")): + raise ValueError("Each view needs an ID and kind") + key = view["id"] + if key in views: + issue("duplicate_id", f"Duplicate view ID {key}", key) + continue + views[key] = view + # Native bindings must be unique and of the declared role. No surrogate elements. + actions = Counter(item.get("qualified_name") for item in inventory["actions"]) + parts = Counter(item.get("qualified_name") for item in inventory["parts"]) + for key, view in views.items(): + kind = view["kind"] + report["views"].append({"id": key, "kind": kind}) + if kind == "function_tree": + _object(view, ("id", "kind", "nodes")) + if not isinstance(view["nodes"], list): + raise ValueError("nodes must be a list") + nodes, bindings = {}, set() + for node in view["nodes"]: + _object(node, ("id", "element", "level", "parent")) + if not _id(node["id"]) or not _text(node["element"]) or not _integer(node["level"]) or not (node["parent"] is None or _id(node["parent"])): + raise ValueError("Node needs ID, native action element, nonnegative level, and parent ID/null") + if node["id"] in nodes: + issue("duplicate_id", f"Duplicate node ID {node['id']}", key) + nodes[node["id"]] = node + if actions[node["element"]] != 1: + issue("function_binding", f"{node['id']} must bind uniquely to a native action", key) + if node["element"] in bindings: + issue("duplicate_binding", f"Repeated function element {node['element']}", key) + bindings.add(node["element"]) + roots = [node for node in nodes.values() if node["parent"] is None] + if len(roots) != 1 or roots[0]["level"] != 0: + issue("root", "Function tree needs exactly one explicit level-0 root", key) + for node in nodes.values(): + parent = nodes.get(node["parent"]) + if node["parent"] is not None: + if parent is None: + issue("orphan", f"{node['id']} has missing parent {node['parent']}", key) + elif node["level"] != parent["level"] + 1: + issue("level", f"{node['id']} must be one level below its parent", key) + # Iterative traversal also catches disconnected cycles without recursion limits. + completed = set() + for start in nodes: + path, current = set(), start + while current in nodes and current not in completed: + if current in path: + issue("cycle", f"Parent cycle includes {current}", key) + break + path.add(current) + current = nodes[current]["parent"] + completed.update(path) + if workflow is not None: + try: + reconciliation = _reconcile_tree(nodes, workflow) + report["views"][-1]["workflow_reconciliation"] = reconciliation + except ValueError as exc: + issue("workflow_conflict", str(exc), key) + elif kind == "sequence": + _object(view, ("id", "kind", "participants", "exchanges")) + if not isinstance(view["participants"], list) or not isinstance(view["exchanges"], list): + raise ValueError("participants and exchanges must be lists") + participants, bindings = set(), set() + for participant in view["participants"]: + _object(participant, ("id", "element")) + if not _id(participant["id"]) or not _text(participant["element"]): + raise ValueError("Participant needs ID and native part usage element") + if participant["id"] in participants: + issue("duplicate_id", f"Duplicate participant ID {participant['id']}", key) + participants.add(participant["id"]) + if parts[participant["element"]] != 1: + issue("participant_binding", f"{participant['id']} must bind uniquely to a native part usage", key) + if participant["element"] in bindings: + issue("duplicate_binding", f"Repeated participant element {participant['element']}", key) + bindings.add(participant["element"]) + if not participants or not view["exchanges"]: + issue("sequence_empty", "Sequence needs participants and ordered exchanges", key) + seen = set(participants) + for exchange in view["exchanges"]: + _object(exchange, ("id", "from", "to", "message"), ("timing",)) + if not _id(exchange["id"]): + raise ValueError("Exchange needs an ID") + if exchange["id"] in seen: + issue("duplicate_id", f"Duplicate sequence ID {exchange['id']}", key) + seen.add(exchange["id"]) + for endpoint in ("from", "to"): + if not _id(exchange[endpoint]) or exchange[endpoint] not in participants: + issue("endpoint", f"{exchange['id']} has undeclared {endpoint} participant", key) + if not _text(exchange["message"]): + issue("exchange_text", f"{exchange['id']} needs a nonempty message; meaning needs human review", key) + if "timing" in exchange: + timing = exchange["timing"] + _object(timing, ("min", "max", "unit", "basis")) + if (any(type(timing[n]) not in (int, float) or not math.isfinite(timing[n]) or timing[n] < 0 for n in ("min", "max")) + or timing["min"] > timing["max"] or not isinstance(timing["unit"], str) or timing["unit"] not in UNITS or not _text(timing["basis"])): + issue("timing_range", f"{exchange['id']} needs finite 0 <= min <= max, duration unit, and timing basis", key) + else: + issue("view_kind", f"Unsupported view kind {kind}; activity flow is distinct from decomposition and sequence", key, "unsupported") + for requirement in requirements: + key = requirement["id"] + view = views.get(key) + if view is None: + issue("view_missing", "Requested view is absent", key, "unknown") + continue + if view["kind"] != requirement["kind"]: + issue("view_kind", "View does not match requested kind", key) + continue + exceptions = {(e["rule"], e["target"]): e for e in requirement.get("exceptions", [])} + used = set() + def gap(rule, target, detail): + exception = exceptions.get((rule, str(target))) + if exception: + used.add((rule, str(target))) + report["exceptions"].append({"view": key, **exception}) + else: + issue(rule, detail, key, "unknown") + if view["kind"] == "function_tree": + nodes = view["nodes"] + ids = {node["id"] for node in nodes} + levels = Counter(node["level"] for node in nodes) + children = Counter(node["parent"] for node in nodes) + for level in requirement.get("required_levels", []): + if level not in levels: + gap("required_level", level, f"Requested level {level} is absent") + for field, counts, rule in (("level_counts", levels, "level_count"), ("child_counts", children, "child_count")): + for target, bounds in requirement.get(field, {}).items(): + count = counts[int(target) if field == "level_counts" else target] + if field == "child_counts" and target not in ids: + gap("child_count", target, f"Requested parent {target} is absent") + elif not bounds.get("min", 0) <= count <= bounds.get("max", math.inf): + gap(rule, target, f"{field} target {target}: count {count} outside {bounds}") + else: + ids = {item["id"] for group in ("participants", "exchanges") for item in view[group]} + if requirement.get("require_timing", False): + for exchange in view["exchanges"]: + if "timing" not in exchange: + gap("timing", exchange["id"], f"{exchange['id']} lacks requested timing") + for expected in requirement.get("required_ids", []): + if expected not in ids: + gap("required_id", expected, f"Requested ID {expected} is absent") + for unused in sorted(set(exceptions) - used): + issue("unused_exception", f"Exception {unused} did not justify an actual gap", key, "error") + except (ValueError, TypeError, KeyError, OverflowError, RecursionError) as exc: + issue("view_contract", str(exc), status="error") + return report diff --git a/verifier/sysml.py b/verifier/sysml.py index d3e50e2..0c09dae 100644 --- a/verifier/sysml.py +++ b/verifier/sysml.py @@ -16,6 +16,7 @@ from .language import LanguageError, _clock, check_document from .events import EventError, _quantity, check_event_trace, parse_event_clause from .influence import generate_influence_tests +from .engineering_views import check_views ROOT = Path(__file__).resolve().parents[1] CACHE = ROOT / ".cache" / "sysml" @@ -188,7 +189,7 @@ def _evidence(value, model_digest): def check_sysml(path, *, manifest=None, evidence=None, review=False, syntax_only=False, - kind=None, generate_tests=False, test_max_rows=16, test_evaluation_cap=2000, + kind=None, view_profile=None, generate_tests=False, test_max_rows=16, test_evaluation_cap=2000, parser_timeout=60, observation_cap=10000, work_cap=1000000): """Parse one SysML file with the pinned pilot, then check supported clauses.""" report = {"status": "pass", "checker_version": VERSION, "parser": PARSER, "claim_scope": "sysml_syntax_and_validation" if syntax_only else "supplied_behavior_evidence" if review else "sysml_and_controlled_text_compilation", @@ -264,6 +265,11 @@ def check_sysml(path, *, manifest=None, evidence=None, review=False, syntax_only _problem(report, "shape_gap", f"{kind} draft has no {category.replace('_', ' ')}", status="unknown") if syntax_only: report["claim_scope"] = f"sysml_syntax_and_{kind}_shape" + if view_profile is not None or any(doc.get("name") == "cseViews" for doc in parsed["documents"]): + report["view_checks"] = check_views(parsed, view_profile) + for finding in report["view_checks"]["findings"]: + _problem(report, "view_" + finding["code"], finding["detail"], + owner=finding.get("view"), status=report["view_checks"]["status"]) if syntax_only: report["inventory"] = {key: parsed[key] for key in ("part_definitions", "parts", "concerns", "use_cases", "actions", "states",