LTS with a special "internal" transition τ.

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 τ.

@[reducible, inline]

abbrev Cslib.DecidableEqTau (α : Type u_1) [HasTau α] : Type u_1

Checking whether an element is τ is decidable.

Equations

• Cslib.DecidableEqTau α = ((a : α) → Decidable (a = Cslib.HasTau.τ))

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

• lts.τSTr = Relation.ReflTransGen (Cslib.LTS.Tr.toRelation lts Cslib.HasTau.τ)

theorem Cslib.LTS.τSTr.refl {Label : Type u_1} {State : Type u_2} {s : State} [HasTau Label] {lts : LTS State Label} : lts.τSTr s s

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

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

• lts.saturate = { Tr := lts.STr }

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

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.

theorem Cslib.LTS.tr_le_tr_saturate {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : lts.Tr ≤ lts.saturate.Tr

theorem Cslib.LTS.sTr_τSTr_iff {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.

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

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

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.

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.

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.

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.

theorem Cslib.LTS.subset_saturate_setImage_τ {Label : Type u_1} {State : Type u_2} {S : Set State} [HasTau Label] (lts : LTS State Label) : S ⊆ lts.saturate.setImage S HasTau.τ

Monotonicity of setImage on HasTau.τ.

theorem Cslib.LTS.empty_saturate_setImage_τ {Label : Type u_1} {State : Type u_2} {S : Set State} [HasTau Label] (lts : LTS State Label) : lts.saturate.setImage S HasTau.τ = ∅ ↔ S = ∅

setImage preserves (non-)emptyness.

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

• lts.τClosure S = lts.saturate.setImage S Cslib.HasTau.τ

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

Monotonicity of setImage on HasTau.τ.

inductive Cslib.LTS.SMTr {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : State → List Label → State → Prop

Saturated multistep transition relation.

• τ {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {s s' : State} : lts.STr s HasTau.τ s' → lts.SMTr s [] s'
• stepL {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {s1 : State} {μ : Label} {s2 : State} {μs : List Label} {s3 : State} : lts.STr s1 μ s2 → lts.SMTr s2 μs s3 → lts.SMTr s1 (μ :: μs) s3

theorem Cslib.LTS.SMTr.refl {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (s : State) : lts.SMTr s [] s

The saturated multistep transition relation is reflexive.

theorem Cslib.LTS.SMTr.comp {Label : Type u_1} {State : Type u_2} {s₁ : State} {μs₁ : List Label} {s₂ : State} {μs₂ : List Label} {s₃ : State} [HasTau Label] {lts : LTS State Label} (h₁ : lts.SMTr s₁ μs₁ s₂) (h₂ : lts.SMTr s₂ μs₂ s₃) : lts.SMTr s₁ (μs₁ ++ μs₂) s₃

The saturated multistep transition relation is transitive.

theorem Cslib.LTS.SMTr.fromMTr {Label : Type u_1} {State : Type u_2} {s : State} {μs : List Label} {s' : State} [HasTau Label] {lts : LTS State Label} (h : lts.MTr s μs s') : lts.SMTr s μs s'

A multistep transition implies a saturated multistep transition.

theorem Cslib.LTS.sMTr_τSTr_iff {Label : Type u_1} {State : Type u_2} {s s' : State} [HasTau Label] {lts : LTS State Label} : lts.τSTr s s' ↔ lts.SMTr s [] s'

theorem Cslib.LTS.saturate_mTr_sMTr_not_nil_iff {Label : Type u_1} {State : Type u_2} {μs : List Label} {s s' : State} [HasTau Label] {lts : LTS State Label} (hμs : μs ≠ []) : lts.saturate.MTr s μs s' ↔ lts.SMTr s μs s'

A saturated multistep transition with a nonempty label list implies a multistep transition.