Generated values

Esdieff generates sample values for a selected effective data description, so firmware and app teams can test their code against a model without writing payloads by hand. Each Generated value aims at one Generation target, such as a minimum, a value just below it or a wrong type, and Sample-value checking settles it against the description it was generated for. Its admission, not its target, says whether the description admits it. The rules follow ADR 0041: Generated values settled by Sample-value checking, and the terms Generated value, Generation target, Representative value, Sample-value checking, Effective data description and Nullable come from the domain language.

#![allow(unused)]
fn main() {
use esdieff::{Admission, Catalogue, GenerationRequest, SampleKind, SourceInput};

let catalogue = Catalogue::take_inputs(vec![SourceInput::supplied(
    "model",
    br#"{"sdfProperty":{"level":{"type":"integer","minimum":10}}}"#,
)])?;
let request = GenerationRequest::new(catalogue.source_id("model").unwrap())
    .select(SampleKind::Property, "/sdfProperty/level");
let result = catalogue.generate(request)?;
let level = result.descriptions().next().unwrap();
let below = level.values().find(|value| value.target() == "below_minimum").unwrap();
assert_eq!((below.to_json(), below.admission()), ("9", Admission::Rejected));
Ok::<(), &'static str>(())
}

The generation contract identity is esdieff.generation/1. It binds the Generation targets, their order and the rules that build their values, so a release that changes any of them gets a new identity and a report keeps its meaning. Generation is deterministic, with no randomness or seed, so the same model and request give the same values in the same order.

Command line

esdieff generate --document MODEL [--kind KIND --pointer POINTER] [--format human|json|jsonl] MODEL_INPUT... generates values for descriptions of the model document MODEL, which must match one explicit MODEL_INPUT. Inputs are file paths, and - reads one document from standard input. --kind and --pointer select one description as esdieff sample does, with KIND one of property, data, action_input, action_output and event_output, and they come together or not at all. Without them every affordance description of the document is selected, as described under Selection. From the repository root, generate values for the rich thermostat model:

cargo run -- generate --document examples/thermostat-check/rich.sdf.json examples/thermostat-check/rich.sdf.json

--format human gives the human report, json the JSON report and jsonl the JSON Lines Trace entries. The shared color controls style the human report. Generation reports no model findings, so it exits 0 when generation completed for every selected description and 3 otherwise, including when any value stays undetermined. A missing --document, --kind without --pointer or the reverse, an unknown kind, format or option, a selector that selects nothing, a document that is not a supplied input and a second - are invocation errors that exit 2 with empty stdout. A report that cannot be written exits 4. The CLI contract states the shared rules.

Library operation

Catalogue::generate(request) performs one generation. GenerationRequest::new(document) selects every affordance description of a model document, and select(kind, pointer) narrows it to the one description that Sample selector selects. An unknown or non-model document, a malformed or oversized pointer, a selector whose definition is absent or has another kind, and a report allowance too small for the mandatory report envelope are request errors.

GenerationResult owns every value and borrows the Catalogue for its report. descriptions() yields each selected GeneratedDescription in selection order, and descriptions_omitted() counts selected descriptions beyond the ceiling or left out because their details did not fit the report byte limit. count(admission) counts the kept values Sample-value checking settled with that admission. selection_complete() is false when a grouping or affordance of the document could not be read, so some descriptions may be missing. complete() is true when the selection is complete, no description was omitted and every description is complete. disposition() is passed then and undetermined otherwise, never failed. document() and selector() echo the request. to_json(), to_json_lines(), to_human() and to_human_with_style(style) render the outputs below.

Each GeneratedDescription has its Sample selector kind() and pointer(), its state(), its kept values() in target order and values_omitted(), the distinct values left out beyond the ceiling, because they did not fit the report byte limit or because their Trace entry would be longer than a trace line. Its state is:

• Complete when every applicable target was generated and every kept value is admitted or rejected.
• Partial when generation ran out of the description’s allowance, values were omitted beyond the ceiling, for the report byte limit or for the trace line limit, or Sample-value checking left a value undetermined, including one whose check ran out of its own allowance.
• Unavailable when the description’s effective meaning could not be established, so no value was generated.

Each GeneratedValue has its target(), its to_json() text, in which each number keeps the spelling it was generated with, its admission() and its codes(), the distinct condition codes behind a rejection, at most 8, such as sample.bound.

Selection

With a selector, generation covers the one description that Sample-value checking would select for that kind and pointer, including an sdfData definition. Without one, it covers every Property, Action sdfInputData, Action sdfOutputData and Event sdfOutputData reachable from the document’s top-level groupings and affordances, including nested groupings. They are taken in document order, and an Action’s input comes before its output. sdfData definitions are generated only when selected explicitly, and Event input and groupings have no description to generate. A description whose effective meaning is unavailable is listed as unavailable, and a grouping, Action or Event that cannot be read leaves the selection partial.

Generation targets

Each description’s targets come in four groups, in this order. A target that does not apply produces no value, and so does one whose value would exceed the value capabilities, such as a string longer than a document may be or a value nested deeper than the depth limit. pattern has no target in this contract, since Esdieff does not synthesize strings that match a pattern.

The first group is the Representative values of ADR 0039, with their number, string, map and array rules:

The second group holds boundary values, which lie on an edge of the admitted range:

The third group holds values just outside the admitted range:

Array items

The items of an array value are copies of the first Representative value of its items description, or null without one. When the array requires unique items and holds two or more, its items are distinct instead: the Representative values of items in order, then further values that continue from the first of them. Numbers continue one unit at a time, strings vary their last character through a to z and then longer suffixes, and a boolean continues with the other boolean. Without an items description the items are the numbers from 0. When no such sequence has enough distinct items, such as for an items description with only a const, the target gives no value.

Nested targets

The fourth group holds the targets of each properties entry, in order, and then of items. Each is generated by these same rules for that nested description, including its own nested targets, and its value is placed where the nested description stands:

• inside the map its entry belongs to, beside the first Representative value of every other entry that map requires, so the enclosing constraints still apply
• among the items of its array, repeated as often as the array’s minItems requires and at least once, or beside other distinct items when the array requires unique items

A nested target is named after the path to it, as <entry>.<target> or items.<target>, so a minimum inside the level entry of settings data is level.minimum, and one inside the items of an array inside the readings entry is readings.items.minimum. With {"type":"object","required":["mode","level"],"properties":{"mode":{"enum":["off","heat"]},"level":{"type":"integer","minimum":5}}}, level.minimum is {"level":5,"mode":"off"} and level.below_minimum is {"level":4,"mode":"off"}. A nested value is often the same value as an earlier one, such as the map of Representative values, and is then kept once under the duplicate rules, which favor the nested boundary target. With {"type":"array","minItems":2,"uniqueItems":true,"items":{"type":"integer","minimum":3,"maximum":9}}, items.maximum is [9,3]. A Direct items description has no Nullable characteristic, so items never has a null target. Nested descriptions are followed only while their values can nest within the depth limit, and a value whose enclosing value cannot be built, such as one whose sibling entry has no Representative value, is not generated.

A unit follows the rules of the numeric bounds witnesses: it is 1 where the coefficient digit limit allows, and otherwise one of the bound’s last significant digit. So a maximum of 20.50 gives an above_maximum of 20.6, and a maximum of 1e600 gives 2e600, since adding 1 would need more digits than the limit allows. A count that is not an exact nonnegative integer within the value capabilities, and a step that is not a positive exact number, give no target.

Settlement and duplicates

Sample-value checking settles every kept value against the selected description, as it would a value supplied for that Property, sdfData definition, input or output. A target name never overrides admission. A below_minimum value that another constraint also rejects is just rejected, and a type value that a pattern rejects is rejected too. A value the checker cannot settle, such as one beside an unsupported pattern or one for map or array content without a type, is undetermined and leaves its description partial.

Each value is settled as soon as it is kept, so the admissions already settled stand when later generation runs out of the description’s allowance. Two targets can produce the same value, and it is then kept once. Values are the same when their JSON texts are, apart from the order of the entries in any map, so {"level":5,"mode":"off"} and {"mode":"off","level":5} are one value, while numbers compare by their exact spelling, so 10 and 1e1 are two. A duplicate is kept under the target with the highest precedence, so that a label names the constraint a value probes:

1. Boundary and outside targets, every target of the second and third groups apart from all_entries, rank above the Representative-value targets const, enum, default, type, alternative and null, and above all_entries.
2. Within each of these two classes, a nested target, <entry>.<target> or items.<target>, ranks above a top-level one.
3. Between targets of equal rank, the first in contract order keeps the value.

The value stands at the place of the target that keeps it and shows that target’s text. So a typed description with a minimum of 10 lists 10 as its minimum rather than as its type, a const of 3 beside a minimum of 3 lists 3 as the minimum, a const of 0 beside a type of integer lists 0 as the const, and an array of at least two unique integer items with a minimum of 0 lists [0,1] as items.minimum rather than as min_items. In a map that requires a mode enum starting with "off" and a level with a minimum of 5, the type map {"mode":"off","level":5}, the first mode.enum value and the level.minimum value are one value, listed once as level.minimum with the text {"level":5,"mode":"off"}.

Bounds

One description keeps at most 64 distinct values, and one request selects at most 1024 descriptions. Distinct values beyond the first ceiling are counted in values_omitted and leave their description partial. Descriptions beyond the second are counted in descriptions_omitted, have no values and leave the operation undetermined. These two ceilings keep a request finite under ADR 0009: Bounded processing and reporting and ADR 0013: Shared workflow and report guarantees.

Each piece of work has an allowance of its own, with the work, allocation, numeric and equality limits that one esdieff sample request receives against the same Catalogue, as ADR 0041: Generated values settled by Sample-value checking states. Composing the document and finding its descriptions spend the request’s allowance. Building one description’s values spends that description’s allowance, and running out of it stops generation of that description and leaves it partial. Each kept value is checked with an allowance of its own, and a check that runs out leaves that value undetermined and its description partial. So one heavy description or value never leaves the others unsettled.

Checking a value against an enum or a choice costs work roughly linear in its number of alternatives, so even an enum of thousands of values settles within one check’s allowance. Values whose checks are costlier, such as long unique arrays, can still run out of that allowance and stay undetermined.

The values a request keeps always fit the report byte limit, Limits::report_bytes. After the Catalogue’s mandatory report reserve and the generate envelope’s own, every description is charged the bytes its details need before its values are generated, and every kept value is charged the bytes its largest rendering needs, as a JSON report record, a JSON Lines Trace entry or a human report line, before it is kept. The charge assumes the longest target name the description can give, so when a target of higher precedence later takes the value under the duplicate rules, its name always fits. A description whose details do not fit is left out, counted in descriptions_omitted with a report_limit record, and leaves the operation undetermined. A distinct value that does not fit is left out, counted in values_omitted with a byte_limit record, and leaves its description partial. So every output format fits the limit, whatever the model asks for, such as many strings with a maxLength of millions. A value whose Trace entry would be longer than 1 MiB, the longest line a Recorded trace accepts, is left out the same way, also charged as if under the longest target name, so every JSON Lines entry replays through esdieff trace.

Report 1.5

The JSON report is schema:"esdieff.report", version:"1.5", operation:"generate", extending the shared report contract with these fields:

baseline.interpretations names the value interpretations that the checks relied on, as model reports name them. Every source stays in sources. Description details are written in selection order within the report byte limit, and any that do not fit are counted, never silently dropped. The human report shows the disposition, the value counts, then each description with its state and one line per value with its admission, its target padded to at most 40 characters, its value and its rejection codes. It is written one description at a time and gives the JSON report instead as soon as it would not fit the report byte limit.

JSON Lines

--format jsonl and to_json_lines() write one Trace entry per admitted or rejected value, each a JSON map on its own line ending in LF: {"kind":KIND,"pointer":POINTER,"value":VALUE,"expected":ADMISSION,"label":TARGET}, with the description’s Sample selector, the generated value, its settled admission as expected and its target as label. A target longer than 256 bytes, which only a long nested entry name gives, is left out as a label rather than shortened. Undetermined values are left out, and the exit code still reports them, as it does values left out for the report byte limit or the trace line limit. A run without settled values writes nothing at all.

The output is a Recorded trace, so esdieff trace replays it as regression vectors, as the trace contract describes. Replayed against the same model, every entry passes, because each expectation is the admission Sample-value checking settled. Replayed against a later revision, exactly the entries whose admission changed fail, such as a former maximum that a narrowed maximum now rejects. The output is byte-identical for the same model and request, so the vectors can be kept under version control.