Repository navigation
Conversation
Move verifier settings state onto the shared model and route every change through VerifierService, dropping the reactive FormGroup from the manager component. Settings inputs now bind one-way ([ngModel] + (ngModelChange)) and persist via the service, mirroring ConditionEditorComponent, so the side menu and bottom menu placements stay in sync. - Verifier.ts: VerifierSetting becomes a discriminated union with an `input` field; a Requiredness sub-union enforces required ⟹ default at compile time. - VerifierService: add load() (backend seam), updateSetting(), seedInputs() (input = default ?? ''), and a verifiersValid computed that gates only enabled verifiers, ready for a future "run verification" action. - verifier-manager: remove FormGroup/FormBuilder/Validators/ReactiveFormsModule and the TODO(backend); add onSettingChange(). - Add verifier.service.spec.ts covering seeding, updateSetting, and validity. Backend persistence is deferred until the endpoint exists: load() once at startup and hang the save off a blur event, not the per-keystroke path.
Let a numeric verifier setting declare its value type and constraints, validate
them inline, and gate the run on validity. The value stays a string end-to-end;
the number type exists only transiently in the UI, so seedInputs/updateSetting/
backend serialization are untouched and empty is always ''.
- Verifier.ts: add a `valueType: 'number'` text setting with optional `step` and
inclusive `range` ({min?, max?}). Omitted step means step=1 (integers) — documented.
Expanded into an explicit discriminated union so strict-template narrowing on
valueType is reliable.
- verifier-validation.ts: pure shared helpers (matchesStep, numberInputError,
isSettingValid) — single source of truth for the UI errors and the service gate.
- step-validator.directive.ts: [appStepValidator] template validator, since Angular
does not surface native stepMismatch into control.errors; reuses matchesStep.
- VerifierService: verifiersValid now gates on isSettingValid (range + step, not just
required). Made the demo max_threshold a number (step 0.5, range 0..100).
- verifier-manager: numeric branch with type=number + min/max/step/appStepValidator
and mat-error messages; onSettingChange coerces the accessor's number|null to the
canonical string. Invalid values are stored but flagged and blocked at the gate, so
the model never diverges from the view.
- Add tests for in-range/on-grid, out-of-range, non-integer, and empty-optional cases.
…inner arrows for numeric inputs.
…lean up `AppComponent` and refactor verifier manager paths.
…for validation and backend integration. Replace `value` with `id` for verifiers and settings across schema, frontend services, and components. Update global verify button functionality to respect active verifiers and ensure valid configurations.
…th `NumberInputValidatorDirective`, switch `type="number"` to `type="text"` with custom validation, and simplify input constraints for consistency between UI and service logic.
…ctive, add selected state styling, and replace `VerifyOption` with `MenuItem`.
…son` persistence, backend integration, and client-side state management
…styles to improve layout flexibility. Allow scrolling.
…ut, dynamic content templates, and AI synthesis integration.
# Conflicts: # frontend/package-lock.json # frontend/src/app/app.component.ts # frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.html # frontend/src/app/components/editor/condition/condition-editor/condition-editor.component.ts # frontend/src/app/components/editor/statements/composition-statement/composition-statement.component.html # frontend/src/app/components/editor/statements/simple-statement/simple-statement.component.html # frontend/src/app/components/editor/statements/statement/statement.component.html # frontend/src/app/components/editor/statements/statement/statement.component.ts # frontend/src/app/services/project/project.service.ts # frontend/src/app/services/tree/network/network-job.service.ts
… function for improved readability and alignment with modern practices.
…ate UI accordingly
…ation, frontend rendering, and UI enhancements
…oved clarity, set min width to reduce shifting
…or storage, update merging logic, UI adjustments, and backend integration.
…a model, persistence, parent/child sharing, and sequence intermediate conditions
- Popup: scrollable dialog, one accordion panel per enabled verifier
(catalog-driven, no hardcoding); `func` panel hosts the statement editor
and the node's own conditions and is open by default, other panels only
appear for verifiers with variables and edit verifier-specific conditions;
collapse state and content are independent per verifier
- Data model: sparse `verifierConditions` record on statements (formula-level
for the flattened root), round-tripped through mapper, file save/load, and
verify payloads; introduce `PRIMARY_VERIFIER_ID` as well-known verifier id;
old files without the records import unchanged
- Sharing: verifier condition subjects are keyed by the main condition
subject ("slot"), so parent/child sharing, conflict adoption, and
disconnect copying mirror the functional pre/post wiring automatically
- Sequences: per-verifier `verifierIntermediateConditions` on compositions,
edited via a per-panel "Intermediate" column and live-shared with the
children's conditions through the intermediate slot
- Serialization: explicit `toJSON` ordering keeps child statement trees last
in exported JSON; OpenAPI schemas extended with the new records
Booleans carry real JSON booleans instead of canonical strings and require a default, so no unset state exists. Schemas split the shared abstract into string-valued (text/select) and boolean value carriers; override merging rejects type-mismatched persisted values, falling back to the default.
…ment verify, refactor state handling and backend parameterization.
…er display logic - Introduce `status_placeholder` for verifiers to show status in static headers. - Update accordion panels to distinguish between expandable and non-expandable verifiers. - Adjust CSS for verifier status elements, ensuring proper alignment and display. - Extend unit tests to cover `status_placeholder` functionality, maintaining coverage.
…nhance `functionalOnly` logic, update node state transitions, and adjust UI for clarity
…djust UI for functional-only verification scenarios
Fan verification out to every enabled Verifier
Every done message now carries durationMs, measured by the backend with a monotonic clock: for a Verifier from the start of its run (scope check included) until its done is sent, on success and every failure path; for func from the start of the job's run. The complete message carries the job's total run time the same way. The console appends each Verifier's time to its "finished" line and, once the run completes, prints an overview below the closing line: "x/y verifiers successful", then how many failed and how many did not run, a note when functional verification failed, and the total time. y is every Catalog Verifier in the Root's verifier map; failed counts done messages with proven false; did not run covers disabled, unavailable and skipped Verifiers. The closing line's verdict still follows isProven. When the backend reports that the Verifier Catalog could not be read, the count lines are left out, since the Root then still holds the previous run's entries; the log line's prefix is a shared constant on both sides.
A repetition in the Verifier job now carries the loop's own invariant and variant next to its guard, the same for every Verifier and omitted where none was written, so a Verifier can reason about loops without re-deriving their specification.
…tings A Verifier's self-description declares its settings but no longer carries a current value: input is removed from the four setting kinds, and from VerifierSetting. The frontend still fills input on its merged view, from the saved override or the default; the values sent to a Verifier are unaffected. The mock Verifier now declares one example of every setting kind and variant, with labels and descriptions that name what each element is: text with and without a default, a bounded decimal number, a lower-bounded integer, a select, a boolean, and a variable with and without a description. Its result status echoes every resolved setting sorted by id, instead of two fixed ones.
Micronaut hyphenates camelCase keys when it rebuilds the Registry's settings map from flat properties (e.g. @Property), while a YAML Registry file keeps them exact. settingDefault and the unknown-setting-id check now compare ids in hyphenated form, so an override of boundedNumberSetting applies from either source. A Self-Description whose setting ids hyphenate to the same key is rejected, since a policy could not address them separately. The commented dev Registry example now overrides a setting the mock still declares.
Self-Descriptions now reject a non-positive step, a range whose min is not below its max, and duplicate select option ids. A default must follow the strict decimal grammar, lie within the range and on the step grid, or be one of the select's options. An empty default means no default, so a required Setting without one is rejected. Registry overrides go through the same checks.
Wrong-typed, unknown-option, out-of-range/off-step, or required-but-empty Override values no longer fall back to the Catalog default. ResolvedVerifier now reports why a Verifier's settings are unusable, and VerifierFanOut fails that Verifier the same way it fails a scope violation, before ever starting it.
The frontend validated number Settings by parsing with JS Number(), which accepts values the backend's NumberRule rejects (exponents, whitespace, a bare/trailing dot, a leading +, hex). Validate against the same -?\d+(\.\d+)? grammar instead, and treat only "" (not whitespace-only) as empty for a number Setting, so a value the UI shows as valid can no longer get the Verifier skipped by the backend.
A select with required: false could only be moved from one option to another, never back to unset, and even a raw "" override was treated as an invalid, unknown option on both stacks. Add a None entry to optional selects, keep "" as their legal empty value end to end, and add a matching mock Setting for trying it in the dev stack.
applyOverrides previously replaced a saved value with the Catalog default whenever the field couldn't represent it (wrong JSON type, unknown select option, or "" on a required select), so the UI looked valid and let a run start that the backend would then fail. A present value is no longer replaced by the default: one the field can't represent is marked with a savedValueError, which isSettingValid treats as invalid, and a required select's "" is caught by the required check. The four field templates show these as immediate errors instead of silently falling back.
The Variables section of the verifier manager now opens with a subtitle saying whether conditions for that verifier may use Java Variables alongside its own variables, or only its own.
…pdate related tests
…y conditions for 'verified-functional' and 'failed-non-functional' states
…tatement popup headers
Selection branches now share the selection's verifier preconditions, and repetitions pass their parent's verifier pre/postconditions through to the loop body, while functional conditions stay derived from guards and invariants. Links are also made on load via checkConditionSync, and a disconnected repetition keeps a copy of its verifier conditions.
If func fails, the verifiers enabled for the run never execute, but their entries were left as proven:false with no status. That made them look like real failures. They are now marked disabled on every statement and on the Root, the same way as verifiers that were not enabled.
Update from WebCorC to XCorC A Pluggable Framework for Non-Functional Properties in by-Construction Engineering
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
No description provided.