Documentation

Cslib.Foundations.Semantics.LTS.OmegaExecution

Infinite executions of LTS #

source
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
Instances For
    source
    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.

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

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

    source
    theorem Cslib.LTS.OmegaExecution.prepend_execution_tr {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {μl : List Label} {t : State} {sl : List State} {ss : ωSequence State} {μs : ωSequence Label} {μ : Label} (he_head : lts.Execution s μl t sl) (he_tail : lts.OmegaExecution ss μs) (htr : lts.Tr t μ (ss 0)) :
    lts.OmegaExecution (sl ++ω ss) (μl ++ω ωSequence.cons μ μs)

    Prepend an infinite execution with a finite one, bridged with a transition.

    source
    theorem Cslib.LTS.OmegaExecution.prepend_execution {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} {s : State} {μl : List Label} {t : State} {sl : List State} {ss : ωSequence State} {μs : ωSequence Label} (he_head : lts.Execution s μl t sl) (he_tail : lts.OmegaExecution ss μs) (hm : ss 0 = t) :
    lts.OmegaExecution (sl ++ω ss.tail) (μl ++ω μs)

    Glue a finite execution and an infinite execution together on a common first and last state.

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

    source
    theorem Cslib.LTS.OmegaExecution.flatten_execution' {State : Type u_1} {Label : Type u_2} {lts : LTS State Label} [Inhabited Label] [Inhabited State] {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 : ℕ), 0 < (μls k).length) :
    lts.OmegaExecution (ωSequence.map List.dropLast sls).flatten μls.flatten

    Concatenating an infinite sequence of finite executions, with an explicit expression for the state sequence.

    source
    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 : ℕ), 0 < (μls k).length) :
    ∃ (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.

    source
    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 : ℕ), 0 < (μls k).length) :
    ∃ (ss : ωSequence State), lts.OmegaExecution ss μls.flatten ∧ ∀ (k : ℕ), ss (μls.cumLen k) = ts k

    Concatenating an infinite sequence of multistep transitions.