Documentation

VerifiedMBSE.VV.VVBundle

SubSystemVVBundle: Automated VVRecord Construction #

Defines mkComponentRecord and SubSystemVVBundle, which batch-construct VVRecords from a SubSystemSpec.

B-7: Kripke 一般化 #

SubSystemSpec の Kripke 一般化に伴い、SubSystemVVBundle もその型引数を x : α ベースに一般化した。StateMachine 版も ProductStateMachine 版も同じ SubSystemVVBundle 型で扱える。

source
def VerifiedMBSE.VV.mkComponentRecord (subsysName : String) (idx : ℕ) (pd : Core.PartDef) (proof : pd.invariant) :
VVRecord

Helper to construct a component-level VVRecord.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    structure VerifiedMBSE.VV.SubSystemVVBundle {α S D : Type} [Behavior.ToKripke α S D] {x : α} (spec : SubSystemSpec x) :
    Type

    SubSystemVVBundle: bundle of VVRecords constructed from a SubSystemSpec.

    B-7 で SubSystemSpec が Kripke 一般化されたため、本構造の implicit 型引数も {α : Type} {S D : Type} [ToKripke α S D] {x : α} に変更された。 StateMachine 版・ProductStateMachine 版の両方に対応する。

    • componentRecords : List VVRecord

      List of component-level VVRecords

    • extraSystemRecords : List VVRecord

      Additional system-level VVRecords (e.g. power budget)

    Instances For
      source
      def VerifiedMBSE.VV.SubSystemVVBundle.allRecords {α S D : Type} [Behavior.ToKripke α S D] {x : α} {spec : SubSystemSpec x} (bundle : SubSystemVVBundle spec) :
      List VVRecord

      Get all VVRecords.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        theorem VerifiedMBSE.VV.SubSystemVVBundle.allRecords_length {α S D : Type} [Behavior.ToKripke α S D] {x : α} {spec : SubSystemSpec x} (bundle : SubSystemVVBundle spec) :
        bundle.allRecords.length = bundle.componentRecords.length + 3 + bundle.extraSystemRecords.length

        Theorem on VVRecord count.