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

theorem Cslib.LTS.sTr_iff {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (a✝ : State) (a✝¹ : Label) (a✝² : State) : lts.STr a✝ a✝¹ a✝² ↔ a✝¹ = HasTau.τ ∧ a✝² = a✝ ∨ ∃ (s2 : State) (s3 : State), lts.τSTr a✝ s2 ∧ lts.Tr s2 a✝¹ s3 ∧ lts.τSTr s3 a✝²

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

Saturating an LTS does not change its saturated τ-transition relation.

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} {s : State} {μ : Label} [hHasTau : HasTau Label] (lts : LTS State Label) : lts.saturate.Tr s μ = lts.saturate.STr s μ

In a saturated LTS, transitions and saturated transitions agree for every label.

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

theorem Cslib.LTS.mem_τClosure_iff {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {S : Set State} {s' : State} : s' ∈ lts.τClosure S ↔ ∃ s ∈ S, lts.τSTr s s'

The τ-closure of S consists of the states reachable from S by τ-transitions.

@[simp]

theorem Cslib.LTS.τClosure_empty {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) : lts.τClosure ∅ = ∅

The τ-closure of the empty set is empty.

@[simp]

theorem Cslib.LTS.τClosure_union {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) (S T : Set State) : lts.τClosure (S ∪ T) = lts.τClosure S ∪ lts.τClosure T

The τ-closure distributes over binary unions.

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

Taking the τ-closure is monotone.

@[simp]

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

The τ-closure is idempotent.

theorem Cslib.LTS.saturate_setImage_of_ne_τ {Label : Type u_1} {State : Type u_2} [HasTau Label] (lts : LTS State Label) {S : Set State} {μ : Label} (hμ : μ ≠ HasTau.τ) : lts.saturate.setImage S μ = lts.τClosure (lts.setImage (lts.τClosure S) μ)

For a label other than τ, the saturated image of S is the τ-closure of the image of the τ-closure of S.

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.

theorem Cslib.LTS.τSTr_iff_exists_mTr_replicate {Label : Type u_1} {State : Type u_2} [HasTau Label] {lts : LTS State Label} {s t : State} : lts.τSTr s t ↔ ∃ (n : ℕ), lts.MTr s (List.replicate n HasTau.τ) t

A saturated τ-transition is a run along a list of τs.

theorem Cslib.LTS.sMTr_iff_exists_mTr_filter {Label : Type u_1} {State : Type u_2} [HasTau Label] [DecidableEqTau Label] {lts : LTS State Label} {s t : State} {μs : List Label} (hμs : ∀ μ ∈ μs, μ ≠ HasTau.τ) : lts.SMTr s μs t ↔ ∃ (νs : List Label), List.filter (fun (x : Label) => decide (x ≠ HasTau.τ)) νs = μs ∧ lts.MTr s νs t

A saturated run along a list of visible labels is a run whose labels, once the τs are dropped, are that list.