Parallel Composition of SubSystemSpec / FDIRBundle / BehavioralSpec

Binary composition operators for FDIRBundle, BehavioralSpec, and SubSystemSpec over the product Kripke structure ProductKripke x y. Each operator builds the composed value by composing the corresponding component of the two operands.

Contents

1. FDIRBundle.compose — parallel composition of two FDIRBundles.
2. BehavioralSpec.compose — parallel composition of two BehavioralSpecs.
3. SubSystemSpec.compose — parallel composition of two SubSystemSpecs.

All three are parameterized over arbitrary [ToKripke α S D] instances rather than specialized to StateMachine, so compositions of three or more operands nest directly:

let s₁₂ := SubSystemSpec.compose s₁ s₂ pk₁₂ hne₁ hne₂ [] ...
let s₁₂₃ := SubSystemSpec.compose s₁₂ s₃ pk₁₂₃ s₁₂.behavioral.nonEmpty hne₃ [] ...

The intermediate pk₁₂ : ProductKripke x₁ x₂ carries its own ToKripke instance, so the NonEmpty witness required at the next level is simply s₁₂.behavioral.nonEmpty.

FDIR composition semantics

• isFault := f₁.isFault p.1 ∨ f₂.isFault p.2 — either side fault
• isRecovery := f₁.isRecovery p.1 ∨ f₂.isRecovery p.2 — either side recovery
• isSafe := f₁.isSafe q.1 ∧ f₂.isSafe q.2 — both sides safe

Why isRecovery uses ∨

A natural first instinct is to define isRecovery := f₁.isRecovery p.1 ∧ f₂.isRecovery p.2 (both sides recovering simultaneously), but this condition is typically unreachable: if only one side experiences a fault, the other remains frozen at its nominal state, and a component-level FDIRBundle guarantees nothing about whether the non-faulting side ever enters its recovery predicate.

The ∨ semantics — "whichever side faulted must eventually recover" — matches the practical requirement and admits a straightforward proof via Leads_prod.of_left / .of_right. Use cases requiring stricter recovery (e.g. synchronized both-side recovery) can bypass this composition and construct FDIRBundle pk directly.

API granularity

Only binary compose is provided at this level. For variadic composition over a homogeneous list, see the anonymous-payload wrapper SubSystemPayload.composeMany in VV/VariadicCompose.lean, which threads compose through List.foldl.

def VerifiedMBSE.VV.FDIRBundle.compose {α β S₁ D₁ S₂ D₂ : Type} [Behavior.ToKripke α S₁ D₁] [Behavior.ToKripke β S₂ D₂] {x : α} {y : β} (f₁ : FDIRBundle x) (f₂ : FDIRBundle y) (pk : Behavior.ProductKripke x y) (hne₁ : (Behavior.ToKripke.toKripke x).NonEmpty) (hne₂ : (Behavior.ToKripke.toKripke y).NonEmpty) : FDIRBundle pk

Parallel composition of two FDIRBundles.

Because the type signature is parameterized over {α β} [ToKripke α S₁ D₁] [ToKripke β S₂ D₂] {x : α} {y : β}, the same API supports nested compositions such as FDIRBundle.compose f₁₂ f₃ pk₁₂₃ hne₁₂ hne₃.

The result is a unified FDIRBundle pk over the product Kripke structure pk : ProductKripke x y.

Construction:

• safety — Always_prod.of_and combines both safety properties into a conjunction over the product.
• detection — lift the left-side detection with Eventually_prod.of_left and wrap with Or.inl.
• recovery — use Leads_prod.of_left / .of_right on the side that faulted, then map through Or.inl / Or.inr into the composed isRecovery.

Equations

• One or more equations did not get rendered due to their size.

def VerifiedMBSE.VV.BehavioralSpec.compose {α β S₁ D₁ S₂ D₂ : Type} [Behavior.ToKripke α S₁ D₁] [Behavior.ToKripke β S₂ D₂] {x : α} {y : β} (_b₁ : BehavioralSpec x) (_b₂ : BehavioralSpec y) (pk : Behavior.ProductKripke x y) (hne₁ : (Behavior.ToKripke.toKripke x).NonEmpty) (hne₂ : (Behavior.ToKripke.toKripke y).NonEmpty) : BehavioralSpec pk

Parallel composition of two BehavioralSpecs.

The result is a BehavioralSpec pk over the product Kripke structure. Its nonEmpty field is built by ProductKripke.nonEmpty from the component NonEmpty witnesses.

Equations

• ⋯ = ⋯

def VerifiedMBSE.VV.SubSystemSpec.compose {α β S₁ D₁ S₂ D₂ : Type} [Behavior.ToKripke α S₁ D₁] [Behavior.ToKripke β S₂ D₂] {x : α} {y : β} (spec₁ : SubSystemSpec x) (spec₂ : SubSystemSpec y) (pk : Behavior.ProductKripke x y) (hne₁ : (Behavior.ToKripke.toKripke x).NonEmpty) (hne₂ : (Behavior.ToKripke.toKripke y).NonEmpty) (bridge : List Core.Connector) (hbridge : ∀ (c : Core.Connector), c ∈ bridge → c.source.part ∈ spec₁.structural.system.parts ++ spec₂.structural.system.parts ∧ c.target.part ∈ spec₁.structural.system.parts ++ spec₂.structural.system.parts) : SubSystemSpec pk

Parallel composition of two SubSystemSpecs.

Each field of the result is the component-level composition of the corresponding field of the operands. The result is a unified SubSystemSpec pk over the product Kripke structure pk.

• structural ← StructuralSpec.compose (with bridge connectors)
• behavioral ← BehavioralSpec.compose
• fdir ← FDIRBundle.compose

For N-ary composition, nest compose calls directly (see the module docstring). At the third step and beyond, the NonEmpty witness is available as s₁₂.behavioral.nonEmpty, since the intermediate ProductKripke carries its own ToKripke instance.

Equations

• spec₁.compose spec₂ pk hne₁ hne₂ bridge hbridge = { structural := spec₁.structural.compose spec₂.structural bridge hbridge, behavioral := ⋯, fdir := spec₁.fdir.compose spec₂.fdir pk hne₁ hne₂ }