Infinite executions of LTS

def Cslib.LTS.OmegaExecution {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (ss : ωSequence State) (μs : ωSequence Label) : Prop

An infinite execution is conceptually an infinite sequence of transitions. But it is technically more convenient to separate the states and the labels into two ω-sequences.

Equations

• lts.OmegaExecution ss μs = ∀ (i : ℕ), lts.Tr (ss i) (μs i) (ss (i + 1))

theorem Cslib.LTS.OmegaExecution.extract_execution {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {ss : ωSequence State} {μs : ωSequence Label} (h : lts.OmegaExecution ss μs) {n m : ℕ} (hnm : n ≤ m) : lts.Execution (ss n) (μs.extract n m) (ss m) (ss.extract n (m + 1))

Any finite execution extracted from an infinite execution is valid.

theorem Cslib.LTS.OmegaExecution.extract_mTr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {ss : ωSequence State} {μs : ωSequence Label} (h : lts.OmegaExecution ss μs) {n m : ℕ} (hnm : n ≤ m) : lts.MTr (ss n) (μs.extract n m) (ss m)

Any multistep transition extracted from an infinite execution is valid.

theorem Cslib.LTS.OmegaExecution.cons {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {μ : Label} {t : State} {ss : ωSequence State} {μs : ωSequence Label} (htr : lts.Tr s μ t) (hωtr : lts.OmegaExecution ss μs) (hm : ss 0 = t) : lts.OmegaExecution (ωSequence.cons s ss) (ωSequence.cons μ μs)

Prepends an infinite execution with a transition.

theorem Cslib.LTS.OmegaExecution.append {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {μl : List Label} {t : State} {ss : ωSequence State} {μs : ωSequence Label} (hmtr : lts.MTr s μl t) (hωtr : lts.OmegaExecution ss μs) (hm : ss 0 = t) : ∃ (ss' : ωSequence State), lts.OmegaExecution ss' (μl ++ω μs) ∧ ss' 0 = s ∧ ss' μl.length = t ∧ ωSequence.drop μl.length ss' = ss

Prepends an infinite execution with a finite execution.

theorem Cslib.LTS.OmegaExecution.flatten_execution {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} [Inhabited Label] {ts : ωSequence State} {μls : ωSequence (List Label)} {sls : ωSequence (List State)} (hexec : ∀ (k : ℕ), lts.Execution (ts k) (μls k) (ts (k + 1)) (sls k)) (hpos : ∀ (k : ℕ), (μls k).length > 0) : ∃ (ss : ωSequence State), lts.OmegaExecution ss μls.flatten ∧ ∀ (k : ℕ), ss.extract (μls.cumLen k) (μls.cumLen (k + 1)) = List.take (μls k).length (sls k)

Concatenating an infinite sequence of finite executions.

theorem Cslib.LTS.OmegaExecution.flatten_mTr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} [Inhabited Label] {ts : ωSequence State} {μls : ωSequence (List Label)} (hmtr : ∀ (k : ℕ), lts.MTr (ts k) (μls k) (ts (k + 1))) (hpos : ∀ (k : ℕ), (μls k).length > 0) : ∃ (ss : ωSequence State), lts.OmegaExecution ss μls.flatten ∧ ∀ (k : ℕ), ss (μls.cumLen k) = ts k

Concatenating an infinite sequence of multistep transitions.