Converting from FLTS to LTS

def Cslib.FLTS.toLTS {State : Type u_1} {Label : Type u_2} (flts : FLTS State Label) : LTS State Label

FLTS is a special case of LTS.

Equations

• flts.toLTS = { Tr := fun (s1 : State) (μ : Label) (s2 : State) => flts.tr s1 μ = s2 }

@[instance_reducible]

instance Cslib.FLTS.instCoeLTS {State : Type u_1} {Label : Type u_2} : Coe (FLTS State Label) (LTS State Label)

Equations

• Cslib.FLTS.instCoeLTS = { coe := Cslib.FLTS.toLTS }

theorem Cslib.FLTS.toLTS_tr {State : Type u_1} {Label : Type u_2} {flts : FLTS State Label} {s1 : State} {μ : Label} {s2 : State} : flts.toLTS.Tr s1 μ s2 ↔ flts.tr s1 μ = s2

FLTS.toLTS correctly characterises transitions.

instance Cslib.FLTS.toLTS_deterministic {State : Type u_1} {Label : Type u_2} (flts : FLTS State Label) : flts.toLTS.Deterministic

The transition system of a FLTS is deterministic.

instance Cslib.FLTS.toLTS_imageFinite {State : Type u_1} {Label : Type u_2} (flts : FLTS State Label) : flts.toLTS.ImageFinite

The transition system of a FLTS is image-finite.

theorem Cslib.FLTS.toLTS_mtr {State : Type u_1} {Label : Type u_2} {flts : FLTS State Label} {s1 : State} {μs : List Label} {s2 : State} : flts.toLTS.MTr s1 μs s2 ↔ flts.mtr s1 μs = s2

Characterisation of multistep transitions.