Component Definitions

Defines PartDef (part definition with ports and an invariant), PortRef (port reference), Connector (port-to-port connection with compatibility proof), System (composition of parts and connectors), and WellFormed conditions.

structure VerifiedMBSE.Core.PartDef : Type

PartDef: part definition with ports and an invariant.

• baseType : KerMLType
• ports : List PortDef
• invariant : Prop

@[implicit_reducible]

instance VerifiedMBSE.Core.instReprPartDef : Repr PartDef

Equations

• VerifiedMBSE.Core.instReprPartDef = { reprPrec := VerifiedMBSE.Core.instReprPartDef.repr }

def VerifiedMBSE.Core.instReprPartDef.repr : PartDef → ℕ → Std.Format

Equations

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

def VerifiedMBSE.Core.PartDef.WellFormed (pd : PartDef) : Prop

Well-formedness of PartDef: every port's flowType has a specialization relation with baseType.

Equations

• pd.WellFormed = ∀ (p : VerifiedMBSE.Core.PortDef), p ∈ pd.ports → VerifiedMBSE.Core.specializes p.flowType pd.baseType ∨ VerifiedMBSE.Core.specializes pd.baseType p.flowType

structure VerifiedMBSE.Core.PortRef : Type

PortRef: reference to a port within a part (with membership proof).

• part : PartDef
• port : PortDef
• mem : self.port ∈ self.part.ports

structure VerifiedMBSE.Core.Connector : Type

Connector: connects two port references with a compatibility proof.

• source : PortRef
• target : PortRef
• compatible : Core.compatible self.source.port.flowType self.target.port.flowType

structure VerifiedMBSE.Core.System : Type

System: lists of parts and connectors.

• parts : List PartDef
• connectors : List Connector

def VerifiedMBSE.Core.System.WellFormed (sys : System) : Prop

Well-formedness of System: all connector sources/targets are in parts.

Equations

• sys.WellFormed = ∀ (c : VerifiedMBSE.Core.Connector), c ∈ sys.connectors → c.source.part ∈ sys.parts ∧ c.target.part ∈ sys.parts