SysML v2 Textual Notation Generation

Functions to convert PartDef, Connector, System, VVRecord, and VColumn into SysML v2 textual notation.

def VerifiedMBSE.Output.portTypeToSysML (t : Core.KerMLType) : String

Convert a port type to a SysML v2 port def.

Equations

• VerifiedMBSE.Output.portTypeToSysML t = toString "port def " ++ toString (VerifiedMBSE.Output.baseTypeName t) ++ toString ";"

def VerifiedMBSE.Output.portDeclToSysML (p : Core.PortDef) (lvl : ℕ) : String

Convert a PortDef to a port declaration within a part.

Equations

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

def VerifiedMBSE.Output.partDefToSysML (pd : Core.PartDef) (lvl : ℕ) : String

Convert a PartDef to a SysML v2 part def.

Equations

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

def VerifiedMBSE.Output.PartDef.toSysML (pd : Core.PartDef) : String

PartDef.toSysML: top-level generation.

Equations

• VerifiedMBSE.Output.PartDef.toSysML pd = VerifiedMBSE.Output.partDefToSysML pd 0

def VerifiedMBSE.Output.portRefStr (pr : Core.PortRef) : String

Dot notation for PortRef.

Equations

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

def VerifiedMBSE.Output.connectorToSysML (c : Core.Connector) (name : String) (lvl : ℕ) : String

Convert a Connector to a SysML v2 connection def.

Equations

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

def VerifiedMBSE.Output.Connector.toSysML (c : Core.Connector) : String

Connector.toSysML: auto-generate name.

Equations

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

def VerifiedMBSE.Output.systemToSysML (sys : Core.System) (name : String) (lvl : ℕ) : String

Convert a System to a SysML v2 part def.

Equations

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

def VerifiedMBSE.Output.System.toSysML (sys : Core.System) (name : String) : String

System.toSysML: top-level generation.

Equations

• VerifiedMBSE.Output.System.toSysML sys name = VerifiedMBSE.Output.systemToSysML sys name 0

def VerifiedMBSE.Output.vvRecordToSysML (r : VV.VVRecord) (lvl : ℕ) : String

Convert a VVRecord to a SysML v2 requirement def.

Equations

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

def VerifiedMBSE.Output.VVRecord.toSysML (r : VV.VVRecord) : String

VVRecord.toSysML: top-level generation.

Equations

• VerifiedMBSE.Output.VVRecord.toSysML r = VerifiedMBSE.Output.vvRecordToSysML r 0

def VerifiedMBSE.Output.vColumnRequirementsToSysML (col : Matrix.VColumn) (lvl : ℕ) : String

Convert VColumn requirements to a SysML v2 package.

Equations

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

def VerifiedMBSE.Output.collectPortTypes (parts : List Core.PartDef) : List Core.KerMLType

Collect port type definitions (deduplicated).

Equations

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

def VerifiedMBSE.Output.portTypeSection (allParts : List Core.PartDef) (lvl : ℕ) : String

Generate port type definition section (excluding conjugated types).

Equations

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

def VerifiedMBSE.Output.partDefSection (allParts : List Core.PartDef) (lvl : ℕ) : String

Generate part definition section (deduplicated).

Equations

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