Finite executions of LTS #
A finite execution of lts : LTS State Label, a proposition lts.Execution s μs t ss, which says
that lts can transition from s to t through ss using the transition labels μ. That is,
the lists have the form μs = [μ₀, μ₁, ..., μₙ] and ss = [s, s₁, s₂, ..., sₙ, t], and there are
transitions lts.Tr s μ₀ s₁, lts.Tr s₁ μ₁ s₂, ..., lts.Tr sₙ μₙ t.
We define Cslib.LTS.Execution as an inductive proposition, which is equivalent to the definition
in terms of indicies: see Cslib.LTS.Execution.mk and Cslib.LTS.execution_iff_index.
Execution extends MTr by providing the intermediate states of a multistep transition:
lts.Execution s₁ μs s₂ ss means that lts can transition from s₁ to s₂ through ss using
the transition labels μ. This is equivalent to the proposition:
∃ _ : ss.length = μs.length + 1, ss[0] = s₁ ∧ ss[ss.length - 1] = s₂ ∧
∀ k < μs.length, lts.Tr ss[k] μ[k] ss[k + 1].
Access that formulation as a constructor using Cslib.LTS.Execution.mk, and its projections as
Cslib.LTS.Execution.length, Cslib.LTS.Execution.start, Cslib.LTS.Execution.last and
Cslib.LTS.Execution.trans.
- refl
{State : Type u_1}
{Label : Type u_2}
{lts : LTS State Label}
(s : State)
: lts.Execution s [] s [s]
Every state has an execution of zero steps terminating in itself.
- stepL
{State : Type u_1}
{Label : Type u_2}
{lts : LTS State Label}
{r s t : State}
{μ : Label}
{μs : List Label}
{ss : List State}
(htr : lts.Tr r μ s)
(hex : lts.Execution s μs t ss)
: lts.Execution r (μ :: μs) t (r :: ss)
Equivalent of
MTr.stepLfor executions.
Instances For
The lengths of μs and ss are constrained by the fact that each label μ ∈ μs represents
a transition between two states in ss.
Alias of Cslib.LTS.Execution.ss_ne_nil.
Every execution has at least one intermediate state.
lts transitions along the kth label in μs between the kth and (k + 1)th states in
ss.
Alternative constructor for Cslib.LTS.Execution, in terms of the indexed collections of
states and labels.
The inductive definition of Cslib.LTS.Execution is equivalent to that in terms of indices.
Deconstruct a positive-length execution, with a specific value for the second state in the sequence.
The states visited by an execution form a chain from the initial to the final state in the underlying unlabelled relation.
The states visited by an execution form a chain in the underlying unlabelled relation.