V-Matrix Queries and Diagnostics

Defines query functions: column, cell, allRecords, summary, etc.

def VerifiedMBSE.Matrix.VMatrix.column (m : VMatrix) (s : String) : Option VColumn

Get a column for a specific subsystem.

Equations

• m.column s = List.find? (fun (col : VerifiedMBSE.Matrix.VColumn) => col.subsystem == s) m.columns

def VerifiedMBSE.Matrix.VMatrix.cell (m : VMatrix) (l : VV.Layer) (s : String) : List VV.VVRecord

Get VVRecords for a specific cell.

Equations

• m.cell l s = match m.column s with | some col => col.atLayer l | none => []

def VerifiedMBSE.Matrix.VMatrix.allRecords (m : VMatrix) : List VV.VVRecord

Get all VVRecords flattened.

Equations

• m.allRecords = List.foldl (fun (acc : List VerifiedMBSE.VV.VVRecord) (col : VerifiedMBSE.Matrix.VColumn) => acc ++ col.records) [] m.columns

def VerifiedMBSE.Matrix.VMatrix.totalRecords (m : VMatrix) : Nat

Total VVRecord count.

Equations

• m.totalRecords = m.allRecords.length

def VerifiedMBSE.Matrix.VVRecord.summary (r : VV.VVRecord) : String

Summary string for a VVRecord.

Each of the eight Layer constructors is mapped to a three-letter abbreviation following ECSS-E-ST-10C conventions.

Equations

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

def VerifiedMBSE.Matrix.VColumn.summary (col : VColumn) : String

Summary string for a VColumn.

Equations

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

def VerifiedMBSE.Matrix.VMatrix.summary (m : VMatrix) : String

Summary string for a VMatrix.

Equations

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