Synchronising traces

This module defines synchronising traces for FLTS.

def Cslib.FLTS.IsSyncTrace {State : Type u_1} {Label : Type u_2} (flts : FLTS State Label) (μs : List Label) : Prop

A trace μs is synchronising if following it from any two states leads to the same state.

Equations

• flts.IsSyncTrace μs = ∀ (s₁ s₂ : State), flts.mtr s₁ μs = flts.mtr s₂ μs

def Cslib.FLTS.HasSyncTrace {State : Type u_1} {Label : Type u_2} (flts : FLTS State Label) : Prop

flts is synchronising, i.e., it has at least one synchronising trace.

Equations

• flts.HasSyncTrace = ∃ (μs : List Label), flts.IsSyncTrace μs