Documentation

Cslib.Foundations.Semantics.LTS.HasTau

LTS with a special "internal" transition τ. #

source
class Cslib.HasTau (Label : Type v) :
Type v

A type of transition labels that includes a special 'internal' transition τ.

  • τ : Label

    The internal transition label, also known as τ.

Instances
    source
    def Cslib.LTS.τSTr {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) :
    State → State → Prop

    Saturated τ-transition relation.

    Equations
    Instances For
      source
      inductive Cslib.LTS.STr {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) :
      State → Label → State → Prop

      Saturated transition relation.

      • refl {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {s : State} : lts.STr s HasTau.τ s
      • tr {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {s1 s2 : State} {μ : Label} {s3 s4 : State} : lts.τSTr s1 s2 → lts.Tr s2 μ s3 → lts.τSTr s3 s4 → lts.STr s1 μ s4
      Instances For
        source
        def Cslib.LTS.saturate {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) :
        LTS State Label

        The LTS obtained by saturating the transition relation in lts.

        Equations
        Instances For
          source
          theorem Cslib.LTS.saturate_tr_sTr {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} :
          lts.saturate.Tr = lts.STr
          source
          theorem Cslib.LTS.STr.single {Label : Type u_1} {State : Type u_2} {s : State} {μ : Label} {s' : State} [HasTau Label] (lts : LTS State Label) :
          lts.Tr s μ s' → lts.STr s μ s'

          Any transition is also a saturated transition.

          source
          theorem Cslib.LTS.sTr_τSTr {Label : Type u_1} {State : Type u_2} {s s' : State} [HasTau Label] (lts : LTS State Label) :
          lts.STr s HasTau.τ s' ↔ lts.τSTr s s'

          STr transitions labeled by HasTau.τ are exactly the τSTr transitions.

          source
          theorem Cslib.LTS.saturate_τSTr_τSTr {Label : Type u_1} {State : Type u_2} {s : State} [hHasTau : HasTau Label] (lts : LTS State Label) :
          lts.saturate.τSTr s = lts.τSTr s

          In a saturated LTS, the transition and saturated transition relations are the same.

          source
          theorem Cslib.LTS.STr.trans_τ {Label : Type u_1} {State : Type u_2} {s1 s2 s3 : State} [HasTau Label] (lts : LTS State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 HasTau.τ s3) :
          lts.STr s1 HasTau.τ s3

          Saturated transitions labelled by τ can be composed.

          source
          theorem Cslib.LTS.STr.comp {Label : Type u_1} {State : Type u_2} {s1 s2 : State} {μ : Label} {s3 s4 : State} [HasTau Label] (lts : LTS State Label) (h1 : lts.STr s1 HasTau.τ s2) (h2 : lts.STr s2 μ s3) (h3 : lts.STr s3 HasTau.τ s4) :
          lts.STr s1 μ s4

          Saturated transitions can be composed.

          source
          theorem Cslib.LTS.saturate_tr_saturate_sTr {Label : Type u_1} {State : Type u_2} {μ : Label} {s : State} [hHasTau : HasTau Label] (lts : LTS State Label) (hμ : μ = HasTau.τ) :
          lts.saturate.Tr s μ = lts.saturate.STr s μ

          In a saturated LTS, the transition and saturated transition relations are the same.

          source
          theorem Cslib.LTS.mem_saturate_image_τ {Label : Type u_1} {State : Type u_2} {s : State} [HasTau Label] (lts : LTS State Label) :
          s ∈ lts.saturate.image s HasTau.τ

          In a saturated LTS, every state is in its τ-image.

          source
          def Cslib.LTS.τClosure {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (S : Set State) :
          Set State

          The τ-closure of a set of states S is the set of states reachable by any state in S by performing only τ-transitions.

          Equations
          Instances For