6. Requirements: score, hunt, prove¶
The question: the fleet passes its requirements – how good is it really, and where does it break?
Passing is binary. Stakeholders also care how well the fleet performs.
One requirement matters more than another. The model states the answer:
ScoutMissions::scoring in missions.sysml declares weights, utility
shapes, and units on the requirement hierarchy itself. The scoreboard reads
those declarations and scores the fleet. Then the notebook turns
adversarial. longeron.analysis.verify hunts the configurations, event
sequences, and catalog mixes that break the requirements. Z3 decides
whether the requirement set can hold at all.
You will learn how to:
score the fleet’s MAUT hierarchy straight from the model, as a table and a treemap;
inject measured values and score the tutorial 4 winners through the trade-study bridge;
hunt violations to a shrunk catch, exact edges, and a minimal violating sortie;
measure a covering array’s violation recall against exhaustive ground truth;
prove a violation impossible and read the exact rational bound;
ask Z3 whether the requirement set is consistent.
Prerequisites: tutorial 2 for execution, tutorial 4 for the catalog and its winners, tutorial 5
for M0 individuals. Install the extras with
pip install "longeron[verify,trades,viz]". The widgets need JupyterLab.
On a static page each widget shows a placeholder.
import longeron
from longeron.analysis.scoreboard import architecture_values, scoreboard
model = longeron.load("../examples/deepscout")
scoring = model.find("ScoutMissions::scoring")
sb = scoreboard(scoring)
print(sb)
requirement weight share raw utility aggregate
scoring 1 100% - - 81.1%
effectiveness 3 43% - - 96.7%
isrStation 2 40% 275 min 100.0% 100.0%
logisticsWork 2 40% 187 kg km 100.0% 100.0%
interceptCatch 1 20% 66.8 m/s 83.6% 83.6%
affordability 2 29% - - 62.9%
fleetPrice 1 100% 9.71e+03 USD 62.9% 62.9%
operability 2 29% - - 75.9%
crewPortable 2 50% 6.89 kg 63.9% 63.9%
regulatory 1 25% pass 100.0% 100.0%
autonomyRoadmap 1 25% - - -
score (saw) 81.1%
The scoreboard, read off the fleet model¶
scoreboard(scoring) walks the requirement hierarchy and evaluates every
measure through the interpreter. It maps each raw value onto a utility
in [0, 1] and aggregates by weight. The root aggregate is the fleet’s
score: 81.1%.
Read the table top down. The three mission leaves score high, because the
Tutorial 4 winners beat their ramps by wide margins – the flying wings
of 0.12 saturate two of them. The board reads 275 minutes
on station, 187 kg km of delivery work, and a 66.8 m/s catchable crossing.
The other two branches hold the score down. The $9,706 fleet invoice sits
mid-ramp near 63%. The 6.89 kg loaded tip-prop courier holds crewPortable to
about 65%. regulatory is a hard pass/fail constraint, and it passes.
autonomyRoadmap declares no measure, so it is unmeasured: excluded from
its parent’s aggregate rather than counted as zero.
The widget below renders the same decomposition. Area is importance:
each cell’s area is its weight share, subdivided recursively. Color is
utility on a red-to-green ramp. The unmeasured autonomyRoadmap cell is
hatched grey. Hover a cell for its raw value with its declared unit.
(Widget cell: captured at landing.)
board = sb.widget()
board
How the model states it¶
The scoreboard needs no Python-side configuration. Four reserved attribute names on a requirement usage carry the whole vocabulary:
attribute |
meaning |
default |
|---|---|---|
|
importance among siblings |
|
|
utility shape name |
|
|
expression producing the raw value |
the requirement’s own |
|
display unit for the raw value |
|
Shapes anchor on further attributes. larger-is-better and
smaller-is-better ramp linearly between ramp0 (utility 0) and ramp1
(utility 1), clamped outside. step returns exactly 1 or 0. A requirement
with no measure and no constraint stays unmeasured.
The cell below prints the scoring package straight from the parsed model.
Three details deserve a close read. regulatory declares no shape and no
measure, only a require constraint: the 25 kg small-UAS certification
line scores as a hard step. interceptCatch puts ramp1 at 75 m/s – above even the dart,
now that its gust placard caps the catch at 66.8. The leaf measures reference package attributes that
default to the fleet’s reference design point. The trade bridge below
overrides them per candidate. The same file declares the mission floors tutorial 4
traded against, so the trades, the dashboard, and this board score one
truth.
print(longeron.to_sysml(scoring))
requirement scoring {
doc
/* The fleet-level MAUT hierarchy: mission effectiveness
* against affordability and operability, three levels deep.
* Weights are importance shares among siblings; each leaf
* declares its utility shape and ramp in mission units. */
requirement effectiveness {
attribute weight : Real = 3.0;
requirement isrStation {
attribute weight : Real = 2.0;
attribute utility : String = "larger-is-better";
attribute ramp0 : Real = 25.0;
attribute ramp1 : Real = 240.0;
attribute measure : Real = stationMinutes;
attribute unit : String = "min";
}
requirement logisticsWork {
attribute weight : Real = 2.0;
attribute utility : String = "larger-is-better";
attribute ramp0 : Real = 8.0;
attribute ramp1 : Real = 180.0;
attribute measure : Real = payloadRangeKgKm;
attribute unit : String = "kg km";
}
requirement interceptCatch {
attribute utility : String = "larger-is-better";
attribute ramp0 : Real = 25.0;
attribute ramp1 : Real = 75.0;
attribute measure : Real = maxTargetSpeed;
attribute unit : String = "m/s";
}
}
requirement affordability {
attribute weight : Real = 2.0;
requirement fleetPrice {
attribute utility : String = "smaller-is-better";
attribute ramp0 : Real = 16000.0;
attribute ramp1 : Real = 6000.0;
attribute measure : Real = fleetCost;
attribute unit : String = "USD";
}
}
requirement operability {
attribute weight : Real = 2.0;
requirement crewPortable {
attribute weight : Real = 2.0;
attribute utility : String = "smaller-is-better";
attribute ramp0 : Real = 12.0;
attribute ramp1 : Real = 4.0;
attribute measure : Real = heaviestBirdKg;
attribute unit : String = "kg";
}
requirement regulatory {
doc
/* Every fleet member stays under the 25 kg small-UAS
* certification line. */
require constraint {
heaviestBirdKg <= 25.0
}
}
requirement autonomyRoadmap;
}
}
Aggregation strategies¶
Simple additive weighting ("saw") is the MAUT default. It lets a strong
requirement offset a terrible one. "min" scores each group by its
weakest link. "geometric" punishes imbalance progressively. Any callable
over (weight, utility) pairs plugs in as a custom strategy.
The spread below makes the fleet’s imbalance visible. The same board
scores 68.8% additively and 32.5% by weakest link, because crewPortable
is the weakest measured leaf.
for strategy in ("saw", "min", "geometric"):
print(f"{strategy:>12}: {scoreboard(scoring, aggregation=strategy).score:.3f}")
def weakest_two(children):
"""A custom Aggregator: the mean of the two weakest utilities."""
worst = sorted(utility for _, utility in children)[:2]
return sum(worst) / len(worst)
print(f"{'weakest_two':>12}: {scoreboard(scoring, aggregation=weakest_two).score:.3f}")
additive = scoreboard(scoring, aggregation="saw").score
weakest = scoreboard(scoring, aggregation="min").score
geometric = scoreboard(scoring, aggregation="geometric").score
assert weakest <= geometric <= additive # the strategies order by severity
saw: 0.811
min: 0.629
geometric: 0.792
weakest_two: 0.724
Two more views of the same board¶
The Voronoi tessellation keeps the area and color semantics on organic cells. The layout is seeded and deterministic. Expanded groups draw a darker perimeter. Hovering a group’s twist spotlights its members.
The second cell scripts navigation. Double-click a group to zoom into it.
A breadcrumb bar tracks the zoom path, and Esc steps back out.
max_depth windows the render depth: deeper levels draw as aggregate
cells until you zoom in. Every navigation knob is a two-way trait, so the
kernel can drive the view. Navigation is view state only. It never changes
the score.
(Widget cells: captured at landing.)
sb.widget("voronoi")
zoomable = sb.widget(max_depth=1) # groups draw as aggregate cells
zoomable.zoom_root = "ScoutMissions::scoring::effectiveness" # zoom from the kernel
print("zoomed into:", zoomable.zoom_root)
print(f"score (zoom never changes it): {sb.score:.3f}")
zoomable
zoomed into: ScoutMissions::scoring::effectiveness
score (zoom never changes it): 0.811
What-if: injecting measured values¶
values= overrides raw measurements without touching the model. Keys
match requirement qualified names, requirement names, or the free
identifiers inside measure expressions and constraint bodies. This is
the seam every measurement source feeds. Tutorial 7 measures
occludedFraction and discOverlapVolume with a CAD engine and injects
them by name, like the bindings below. No CAD runs here.
Two scenarios move the verdict. First, a flight test measures the loiter
at 150 minutes instead of the promised 283. isrStation’s utility falls
from 100% to 58.1%. The score drops to 75.6%. Second, a heavier courier
busts the 25 kg certification line. regulatory flips to FAIL and
crewPortable bottoms out. The score falls to 60.6%.
flight_test = scoreboard(scoring, values={"stationMinutes": 150.0})
print(f"reference score : {sb.score:.3f}")
print(f"150 min measured : {flight_test.score:.3f}")
assert flight_test.score < sb.score # a shorter loiter can only cost utility
bust = scoreboard(scoring, values={"heaviestBirdKg": 26.0})
regulatory = next(row for row in bust.table() if row.name == "regulatory")
print(f"26 kg courier : {bust.score:.3f} (regulatory raw = {regulatory.raw})")
assert regulatory.raw is False # the hard certification line fails
assert regulatory.utility == 0.0
reference score : 0.811
150 min measured : 0.739
26 kg courier : 0.594 (regulatory raw = False)
The trade-study bridge: score the tutorial 4 winners¶
The scoring package’s default measures describe the fleet’s reference
design point: the three tutorial 4 mission winners and their combined invoice. The
bridge proves it. architecture_values turns a trade-study architecture’s
interpreter-exact metrics into values= bindings. The cell below rebuilds
the three winners, composes the fleet’s five measures from their metrics,
and rescores. The recomputed score matches the board’s default within one
part in a thousand, because the model’s defaults are the winners’ numbers,
rounded.
A cell click writes the requirement’s qualified name to the board’s
selected trait, the same linked-selection seam tutorial 3 teaches for
every widget.
A recorded sizing case crosses the same bridge. The second cell rebuilds
the ISR winner as an M0 case and runs it across the OpenMDAO bridge
(tutorials 5 and 4). It records the evaluated case and feeds the
snapshot to the scoreboard through case_values.
from longeron.analysis import trades
missions = {
"stationMinutes": ("ScoutMissions::IsrUav", "missionMass"),
"payloadRangeKgKm": ("ScoutMissions::LogisticsUav", "outboundMass"),
"maxTargetSpeed": ("ScoutMissions::InterceptUav", "missionMass"),
}
winners = {}
for metric, (qname, _mass) in missions.items():
study = trades.TradeStudy(model, qname)
winners[metric] = max(
(arch for arch in study.all_architectures() if arch.verified),
key=lambda arch, m=metric: arch.metrics[m],
)
fleet = {metric: architecture_values(arch)[metric] for metric, arch in winners.items()}
fleet["fleetCost"] = sum(arch.metrics["missionCost"] for arch in winners.values())
fleet["heaviestBirdKg"] = max(
winners[metric].metrics[mass] for metric, (_, mass) in missions.items()
)
for name, value in fleet.items():
print(f"{name:17s} {value:8.1f}")
bridged = scoreboard(scoring, values=fleet)
print(f"\nreference score: {sb.score:.4f}")
print(f"bridged score : {bridged.score:.4f}")
assert abs(bridged.score - sb.score) < 0.001 # the defaults ARE the winners, rounded
stationMinutes 274.6
payloadRangeKgKm 187.0
maxTargetSpeed 66.8
fleetCost 9706.5
heaviestBirdKg 6.9
reference score: 0.8112
bridged score : 0.8114
from longeron import m0
from longeron.analysis import mdao
isr_winner = winners["stationMinutes"]
case = m0.interpret(model, "ScoutMissions::IsrUav", selection=isr_winner.selection)
build = mdao.build_problem(model, "ScoutMissions::IsrUav", interpretation=case)
build.problem.run_model()
snapshot = mdao.record_case(build)
recorded = scoreboard(scoring, values=mdao.case_values(snapshot))
station = next(row for row in recorded.table() if row.name == "isrStation")
print(f"recorded case {snapshot.root.id}: stationMinutes = {station.raw:.1f} min")
assert abs(station.raw - isr_winner.metrics["stationMinutes"]) < 1e-6
recorded case ScoutMissions::IsrUav#0: stationMinutes = 274.6 min
The adversarial turn: verify¶
Everything above shows the model answering questions.
longeron.analysis.verify makes it fight back, from nothing but the
.sysml text. Four tiers share one oracle: hunt, sequences, cover,
and prove. Solvers only propose. Every verdict comes from the
interpreter.
Hunt: the shrunk catch and the exact edges¶
Free payloadMass on the quad and the domain ladder goes to work. No
constraint bounds the payload directly, so Z3 derives the window through
the same totalMass derivation chain the interpreter evaluates. The
window dips to -1.21 kg, because only the positive-mass assumption bounds
it from below. Hypothesis samples the window and shrinks each catch to the
simplest violator, deliberately not the tightest. The report pairs the
catch with interpreter-bisected edges, one per violated check.
The edges stack into the quad’s payload envelope:
the book takeoff limit at 0.29 kg;
the hover-margin floor at 0.68 kg;
canHoveritself at 2.18 kg;the current budgets past 6 kg.
The model states the first two edges in closed form as mtowPayload and
thrustLimitPayload. The cell asserts that the bisections agree with the
algebra.
A second hunt revisits tutorial 4’s redundancy catch. Against FailSafeHover, the
shrinker drives the quad’s motor-out violation to payload zero. The quad
fails motor-out hover even empty. The model agrees in closed form:
failsafePayload is negative.
from longeron.analysis import verify
quad_hunt = verify.hunt(
model,
"Rotorcraft::QuadCopter",
requirements=("DeepScout::FlightEnvelope",),
free=("payloadMass",),
seed=0,
)
dom = quad_hunt.domains["payloadMass"]
hi = dom.hi if dom.hi is not None else "unbounded (flagged)"
print(f"derived window: payloadMass in [{dom.lo}, {hi}] [{dom.unit}]")
catch = quad_hunt.counterexamples[0]
print(f"shrunk catch : {catch.bindings} violates {list(catch.violated)}")
for edge in sorted(quad_hunt.boundaries, key=lambda b: b.value):
print(f"exact edge : payloadMass = {edge.value:9.6f} kg flips {edge.violated}")
quad = longeron.Interpreter(model).instantiate("Rotorcraft::QuadCopter")
edges = {b.violated: b.value for b in quad_hunt.boundaries}
assert abs(edges["takeoffMassLimit [assert]"] - quad.slots["mtowPayload"]) < 1e-3
assert abs(edges["FlightEnvelope::hoverMargin"] - quad.slots["thrustLimitPayload"]) < 1e-3
motor_out = verify.hunt(
model,
"Rotorcraft::QuadCopter",
requirements=("DeepScout::FailSafeHover",),
free=("payloadMass",),
seed=0,
max_examples=30,
)
worst = motor_out.counterexamples[0]
print(f"\nmotor-out catch: {worst.bindings} violates {list(worst.violated)}")
assert quad.slots["failsafePayload"] < 0.0 # no payload survives a motor failure
derived window: payloadMass in [-1.21, unbounded (flagged)] [kg]
shrunk catch : {'payloadMass': 1.0} violates ['takeoffMassLimit [assert]', 'FlightEnvelope::hoverMargin']
exact edge : payloadMass = 0.290000 kg flips takeoffMassLimit [assert]
exact edge : payloadMass = 0.675603 kg flips FlightEnvelope::hoverMargin
exact edge : payloadMass = 2.184086 kg flips canHover [assert]
exact edge : payloadMass = 6.347924 kg flips escCurrentBudget [assert]
exact edge : payloadMass = 7.027836 kg flips hoverCurrentBudget [assert]
exact edge : payloadMass = 7.027836 kg flips cruiseCurrentBudget [assert]
motor-out catch: {'payloadMass': 0.0} violates ['FailSafeHover::motorOutHover']
Sequences: the minimal violating sortie¶
DeepScout::SortieStates guards launches behind a 30% battery floor.
Each climb-out to airborne burns 30%. The go-around path re-enters
airborne without repassing the guard. That is a sequence-sensitive trap:
no single state is unsafe, only a path. sequences reads the event
alphabet off the transitions, drives the live simulation against the
SafeSortie invariant, and shrinks away every irrelevant event. The
minimal sortie is four events long. One legal launch, then three
go-arounds drain the pack below zero.
interp = longeron.Interpreter(model)
print("event alphabet:", ", ".join(verify.events_of(interp, "DeepScout::SortieStates")))
seq = verify.sequences(
model, "DeepScout::SortieStates", requirements=("DeepScout::SafeSortie",), seed=0
)
sortie = seq.counterexamples[0]
print("minimal sortie:", " -> ".join(sortie.events))
print("violates :", list(sortie.violated))
assert seq.status == "violated"
event alphabet: goAround, land, launch, recharge
minimal sortie: launch -> goAround -> goAround -> goAround
violates : ['SafeSortie::noDeepDischarge']
Cover: t-way arrays, recall measured¶
The same variation points tutorial 4 enumerated become covering-array factors for the in-house IPOG generator. The interpreter settles every row exactly. The intercept catalog crosses 1,760 mixes, so pairwise needs only 55 rows. At this scale the exhaustive space is still enumerable. The report therefore measures violation recall against ground truth instead of promising it. Pairwise catches all five checks the exhaustive space violates: measured recall 100%.
pairwise = verify.cover(model, "ScoutMissions::InterceptUav", t=2)
cov = pairwise.coverage
print(f"array : {len(cov.rows)} pairwise rows vs {cov.exhaustive} exhaustive mixes")
print(f"violations : {pairwise.violations}")
print(f"measured recall: {cov.recall:.0%} of the checks any exhaustive mix violates")
assert cov.recall == 1.0
array : 60 pairwise rows vs 1920 exhaustive mixes
violations : ['canCatch', 'packPower', 'launchLift', 'propFit', 'cellMatch']
measured recall: 100% of the checks any exhaustive mix violates
The honest five of six: a genuine three-way interaction¶
Pairwise promises pair coverage, not violation coverage. The distinction stays invisible until a check needs three simultaneous choices. Requirements arrive throughout a program’s life, so graft one in with the programmatic authoring from tutorial 1. The flight-test campaign issues a thermal advisory against dash heat soak:
an enclosed wingless shell traps ESC heat;
a 2 kW-class motor produces that heat;
a pack that sustains the full-power draw for minutes lets the dash cook the ESC.
Any two of the three are fine. Exactly one catalog triple trips all three: the teardrop shell, the AT4120 motor, and the 16 Ah pack.
The pairwise array covers every pair inside that triple without ever seating all three together. Measured recall drops to five of six. The report says so instead of implying coverage it does not have. Raising the strength to t=3 seats every triple: 200 rows, recall back to 100%, and the offending mix caught and named.
from fractions import Fraction
from longeron import model as M
intercept = model.find("ScoutMissions::InterceptUav")
intercept.add(
M.Usage(
kind="constraint",
name="dashHeatSoak",
constraint_kind="assert",
result=longeron.parse_expression(
"not (airframe.wingSpan == 0.0 and airframe.fuselageLength > 0.5 "
"and motors.maxPowerW >= 2000.0 and battery.energyWh >= 350.0 "
"and battery.maxPowerW >= 5000.0)"
),
)
)
pairwise = verify.cover(model, "ScoutMissions::InterceptUav", t=2)
threeway = verify.cover(model, "ScoutMissions::InterceptUav", t=3)
t2_recall = Fraction(pairwise.coverage.recall).limit_denominator(12)
print(f"t=2: {len(pairwise.coverage.rows):3d} rows, measured recall {t2_recall}")
print(f"t=3: {len(threeway.coverage.rows):3d} rows, measured recall {threeway.coverage.recall:.0%}")
assert "dashHeatSoak" not in pairwise.violations # the miss pairwise cannot see
assert "dashHeatSoak" in threeway.violations
assert threeway.coverage.recall == 1.0
caught = next(c for c in threeway.counterexamples if "dashHeatSoak" in c.violated)
triple = {k: caught.selection[k] for k in ("airframe", "motors", "battery")}
print("the three-way interaction:", triple)
t=2: 60 rows, measured recall 5/6
t=3: 240 rows, measured recall 100%
the three-way interaction: {'airframe': 'teardropQuad', 'motors': 'at4120', 'battery': 'tattu16000'}
Prove: violation is impossible, and the exact ceiling¶
Sampling never proves absence. prove negates one check at a time under
the assumptions and all the other checks, and hands the negation to Z3.
UNSAT is a proof: no configuration that satisfies the rest can violate the
negated check. SAT witnesses go back through the interpreter before the
report believes them.
Tutorial 4 stated the X8’s redundancy claim. Here is its proof. Inside the
takeoff envelope, motorOutHover is UNSAT-safe, and so are canHover and
all three current budgets. The takeoff limit itself is the one breakable
check. Its witness survives the interpreter re-check. Optimize
attributes the exact payload envelope bound to it: 249/500 kg, an exact
rational, no float rounding. Where the algebra outruns the encoder (pow,
cos), the attribute pins at its interpreter-exact value. The refusal
lands in gaps, so the proof’s scope stays visible.
proofs = verify.prove(
model, "Rotorcraft::CoaxX8", requirements=("DeepScout::FailSafeHover",), free=("payloadMass",)
)
for proof in proofs.proofs:
print(f"{proof.requirement:42s} {proof.status}")
motor_out_proof = next(p for p in proofs.proofs if "motorOutHover" in p.requirement)
assert motor_out_proof.status == "proven-safe"
assert "takeoffMassLimit" in motor_out_proof.binding_constraint
ceiling = Fraction(motor_out_proof.bound)
print(f"\nexact envelope bound: {motor_out_proof.bound} kg = {float(ceiling):.3f} kg,")
print(f"attributed to {motor_out_proof.binding_constraint}")
print(f"encoder refusals recorded in gaps: {len(proofs.gaps)}")
assert sum(p.status == "proven-safe" for p in proofs.proofs) == len(proofs.proofs) - 1
CoaxX8::takeoffMassLimit violation
CoaxX8::canHover proven-safe
CoaxX8::hoverCurrentBudget proven-safe
CoaxX8::cruiseCurrentBudget proven-safe
CoaxX8::escCurrentBudget proven-safe
FailSafeHover::motorOutHover [require] proven-safe
exact envelope bound: 249/500 kg = 0.498 kg,
attributed to CoaxX8::takeoffMassLimit
encoder refusals recorded in gaps: 6
Every catch becomes an individual¶
A counterexample is more than numbers. materialize() turns the shrunk
bindings into an M0 interpretation: identified individuals with stable
ids, the population machinery from tutorial 5. The ordinary check
machinery re-checks the violator, so the catch is reproducible evidence,
not a solver anecdote. verify.counterexample_values feeds the same
individual to a scoreboard as values= bindings, which renders the
requirement it breaks as the red cell.
individual = catch.materialize()
root = individual.root
print(f"{root.id}: payloadMass = {root.slots['payloadMass']} kg,", end=" ")
print(f"totalMass = {root.slots['totalMass']} kg")
results = {check.name: check.passed for check in interp.check(root)}
for name, passed in results.items():
print(f" {name:20s} passed={passed}")
assert not results["takeoffMassLimit"] # the catch re-checks as a real violator
Rotorcraft::QuadCopter#0: payloadMass = 1.0 kg, totalMass = 2.21 kg
takeoffMassLimit passed=False
canHover passed=True
hoverCurrentBudget passed=True
cruiseCurrentBudget passed=True
escCurrentBudget passed=True
Can the requirements all hold? Z3 on consistency¶
verify asks whether a design breaks a requirement. Consistency is the
prior question: can the requirement set hold at all? analysis.smt
encodes the ISR sizing context symbolically and exactly, in rationals.
Three answers come back. First, the 90-minute station floor is
satisfiable. Z3 hands back a witness inside the legal loiter window.
Second, maximize prices the sharpest promises the requirement set
supports. The fastest legal loiter under the floor is exactly 177/8 m/s.
The longest station anywhere in the window is an exact rational just above
300 minutes. Third, a grafted 360-minute ask cannot hold. The UNSAT core
names the exact collision: longStation against the loiter-speed window
aboveStall and belowCruise. Only speeds outside the window could
stretch the battery that far. The requirement set forbids them.
from longeron.analysis import smt
system = smt.to_smt(model, "ScoutSizing::IsrPrime", requirements=("ScoutSizing::IsrStation",))
result = system.check()
witness = {
k: round(v, 2) for k, v in result.witness.items() if k in ("loiterSpeed", "stationMinutes")
}
print(f"IsrStation alone: {result.status}, witness {witness}")
assert result.status == "sat"
freed = smt.to_smt(
model, "ScoutSizing::IsrPrime", requirements=("ScoutSizing::IsrStation",), free=("loiterSpeed",)
)
fastest, _ = freed.maximize("loiterSpeed")
print(f"fastest legal loiter under the floor: {fastest} m/s = {float(Fraction(fastest))} m/s")
longest, _ = freed.maximize("stationMinutes")
best_minutes = Fraction(longest)
print(f"longest legal station: {float(best_minutes):.2f} min", end=" ")
print(f"(a {len(longest)}-character exact rational)")
deep = M.Definition(kind="requirement", name="DeepStare")
deep.add(M.Usage(kind="subject", name="uav", types=["IsrPrime"]))
deep.add(
M.Usage(
kind="constraint",
name="longStation",
constraint_kind="require",
result=longeron.parse_expression("uav.stationMinutes >= 360.0"),
)
)
model.find("ScoutSizing").add(deep)
conflicted = smt.to_smt(
model,
"ScoutSizing::IsrPrime",
requirements=("ScoutSizing::IsrStation", "ScoutSizing::DeepStare"),
free=("loiterSpeed",),
)
result = conflicted.check()
print(f"\nwith DeepStare's 360 min ask: {result.status}")
for label in result.core:
if not label.endswith(".value"):
print(" core:", label)
assert result.status == "unsat"
assert best_minutes < 360 # the exact ceiling already said no
IsrStation alone: sat, witness {'loiterSpeed': 15.0, 'stationMinutes': 200.35}
fastest legal loiter under the floor: 1409/64 m/s = 22.015625 m/s
longest legal station: 279.21 min (a 105-character exact rational)
with DeepStare's 360 min ask: unsat
core: DeepStare::longStation [require]
core: IsrPrime::aboveStall
core: IsrPrime::belowCruise
Verdicts are facts about interpretations¶
A verdict is a fact about an interpretation, never a free-standing number. Every number this notebook printed reads off an interpretation of the model:
the reference design point behind the 68.8% score;
the three winners behind the bridge;
the shrunk quad behind the catch;
the materialized mix behind the covering array’s miss.
The model states the requirements once. Every tier reads them there: the scoreboard’s utilities, the hunt’s windows, the prover’s negations, and the consistency core.
Where the thread continues:
Tutorial 7 measures the geometry claims with a CAD engine and injects
occludedFractionanddiscOverlapVolumeas thevalues=bindings this notebook practiced.Tutorial 9 assembles every perspective, this board included, into one dashboard and grafts a change through all of them.