V-Model Design Layers (ECSS-E-ST-10C Compliant, F5)

概要

ECSS-E-ST-10C の 7 階層 (mission/system/segment/subsystem/assembly/unit/part) に プロジェクト固有の component を加えた 8 階層。後方互換のため、旧 3 階層 .system / .subsystem / .component は同じ constructor 名を維持する。

順序付け: depth ベース

各 Layer に 0〜7 の整数 depth を割り当て、Ord instance と Layer.supports 関係を depth 比較で統一する。depth が大きいほど下層 （分解が進んだ側）。

Layer	depth	説明
mission	0	ミッション全体
system	1	宇宙機 1 機または地上局全体
segment	2	Space segment / Ground segment 等の大区分
subsystem	3	AOCS, EPS, TCS 等
assembly	4	組立体: アビオ箱、バルブ組
unit	5	ユニット: センサー単体、MCU 単体
component	6	コンポーネント: ADC IC、モーター（プロジェクト固有）
part	7	最終部品: 抵抗、ボルト等

後方互換

旧 3 階層 (.system, .subsystem, .component) を直接参照するコード （VColumn.allLayersCovered, SubSystemSpec.safetyRecord の .layer, Examples の .layer := .system 等）は、新版でも同じ constructor 名が そのまま使えるため 無変更でビルド通過 する。

Ord instance の変更点

旧 instance は pattern match で component < subsystem < system の順序を 与えていた（未使用だったが、記録のため）。新版は depth の自然順、すなわち mission < system < ... < part の順序になる。dead code 化していたため 影響範囲はない。

inductive VerifiedMBSE.VV.Layer : Type

V-model design layer (ECSS-E-ST-10C の 7 階層 + プロジェクト固有 component)。

• mission : Layer
• system : Layer
• segment : Layer
• subsystem : Layer
• assembly : Layer
• unit : Layer
• component : Layer
• part : Layer

@[implicit_reducible]

instance VerifiedMBSE.VV.instReprLayer : Repr Layer

Equations

• VerifiedMBSE.VV.instReprLayer = { reprPrec := VerifiedMBSE.VV.instReprLayer.repr }

def VerifiedMBSE.VV.instReprLayer.repr : Layer → Nat → Std.Format

Equations

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

def VerifiedMBSE.VV.instBEqLayer.beq : Layer → Layer → Bool

Equations

• VerifiedMBSE.VV.instBEqLayer.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

@[implicit_reducible]

instance VerifiedMBSE.VV.instBEqLayer : BEq Layer

Equations

• VerifiedMBSE.VV.instBEqLayer = { beq := VerifiedMBSE.VV.instBEqLayer.beq }

@[implicit_reducible]

instance VerifiedMBSE.VV.instDecidableEqLayer : DecidableEq Layer

Equations

• VerifiedMBSE.VV.instDecidableEqLayer x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def VerifiedMBSE.VV.Layer.depth : Layer → Nat

各層の深さ (0 = 最上位 mission、7 = 最下位 part)。

supports 関係と Ord instance はこの depth を通して定義される。

Equations

• VerifiedMBSE.VV.Layer.mission.depth = 0
• VerifiedMBSE.VV.Layer.system.depth = 1
• VerifiedMBSE.VV.Layer.segment.depth = 2
• VerifiedMBSE.VV.Layer.subsystem.depth = 3
• VerifiedMBSE.VV.Layer.assembly.depth = 4
• VerifiedMBSE.VV.Layer.unit.depth = 5
• VerifiedMBSE.VV.Layer.component.depth = 6
• VerifiedMBSE.VV.Layer.part.depth = 7

@[implicit_reducible]

instance VerifiedMBSE.VV.instOrdLayer : Ord Layer

Layer ordering via depth.

mission (0) < system (1) < ... < part (7) の自然順。 ECSS の階層構造図とも一致する（上位を小さい数値で示す）。

Equations

• VerifiedMBSE.VV.instOrdLayer = { compare := fun (a b : VerifiedMBSE.VV.Layer) => compare a.depth b.depth }