VMatrix: The Complete V-Matrix Structure

Defines the VMatrix structure, SubSystemComplete, and Complete (matrix completeness predicate).

structure VerifiedMBSE.Matrix.VMatrix : Type

VMatrix: two-dimensional V-model matrix.

• columns : List VColumn

def VerifiedMBSE.Matrix.VMatrix.SubSystemComplete (m : VMatrix) (subsystems : List String) : Prop

Subsystem completeness: a column exists for every specified subsystem.

Equations

• m.SubSystemComplete subsystems = ∀ (s : String), s ∈ subsystems → ∃ (col : VerifiedMBSE.Matrix.VColumn), col ∈ m.columns ∧ col.subsystem = s

def VerifiedMBSE.Matrix.VMatrix.Complete (m : VMatrix) (subsystems : List String) : Prop

Matrix completeness: all columns are layer-complete.

Equations

• m.Complete subsystems = (m.SubSystemComplete subsystems ∧ ∀ (col : VerifiedMBSE.Matrix.VColumn), col ∈ m.columns → col.Complete)

def VerifiedMBSE.Matrix.VMatrix.fromColumns (c1 c2 : VColumn) : VMatrix

Construct a VMatrix from two VColumns.

Equations

• VerifiedMBSE.Matrix.VMatrix.fromColumns c1 c2 = { columns := [c1, c2] }

theorem VerifiedMBSE.Matrix.VMatrix.fromColumns_contains_both (c1 c2 : VColumn) : c1 ∈ (fromColumns c1 c2).columns ∧ c2 ∈ (fromColumns c1 c2).columns

fromColumns contains both columns.

def VerifiedMBSE.Matrix.VMatrix.fullyTrusted (m : VMatrix) : Bool

Whether the V-matrix is fully trusted.

Equations

• m.fullyTrusted = m.columns.all fun (col : VerifiedMBSE.Matrix.VColumn) => col.fullyTrusted