Conversions between LTS and Relation.

def Cslib.LTS.Tr.toRelation {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (μ : Label) : State → State → Prop

Returns the relation that relates all states s1 and s2 via a fixed transition label μ.

Equations

• Cslib.LTS.Tr.toRelation lts μ s1 s2 = lts.Tr s1 μ s2

def Cslib.LTS.Relation.toLTS {State : Type u_1} {Label : Type u_2} [DecidableEq Label] (r : State → State → Prop) (μ : Label) : LTS State Label

Any homogeneous relation can be seen as an LTS where all transitions have the same label.

Equations

• Cslib.LTS.Relation.toLTS r μ = { Tr := fun (s1 : State) (μ' : Label) (s2 : State) => if μ' = μ then r s1 s2 else False }

def Cslib.LTS.MTr.toRelation {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) (μs : List Label) : State → State → Prop

Returns the relation that relates all states s1 and s2 via a fixed list of transition labels μs.

Equations

• Cslib.LTS.MTr.toRelation lts μs s1 s2 = lts.MTr s1 μs s2

theorem Cslib.LTS.MTr.toReflTransGen {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) {s1 : State} {μs : List Label} {s2 : State} (h : lts.MTr s1 μs s2) : Relation.ReflTransGen lts.UnlabelledTr s1 s2

A multistep transition induces a reflexive-transitive path in the underlying unlabelled transition relation.

theorem Cslib.LTS.MTr.toTransGen {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) {s1 : State} {μs : List Label} {s2 : State} (h : lts.MTr s1 μs s2) (hne : μs ≠ []) : Relation.TransGen lts.UnlabelledTr s1 s2

A nonempty multistep transition induces a nonempty path in the underlying unlabelled transition relation.

theorem Cslib.LTS.reflTransGen_unlabelledTr_iff {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) {s1 s2 : State} : Relation.ReflTransGen lts.UnlabelledTr s1 s2 ↔ lts.CanReach s1 s2

The reflexive-transitive closure of the underlying unlabelled transition relation is exactly reachability in the LTS.

theorem Cslib.LTS.transGen_unlabelledTr_iff {State : Type u_1} {Label : Type u_2} (lts : LTS State Label) {s1 s2 : State} : Relation.TransGen lts.UnlabelledTr s1 s2 ↔ ∃ (μs : List Label), μs ≠ [] ∧ lts.MTr s1 μs s2

The transitive closure of the underlying unlabelled transition relation is exactly the nonempty multistep transitions of the LTS.

Calc tactic support for MTr

@[instance_reducible]

instance Cslib.LTS.instTransToRelationToRelationConsNil {State : Type u_1} {Label : Type u_2} {μ1 μ2 : Label} (lts : LTS State Label) : Trans (Tr.toRelation lts μ1) (Tr.toRelation lts μ2) (MTr.toRelation lts [μ1, μ2])

Transitions can be chained.

Equations

• lts.instTransToRelationToRelationConsNil = { trans := ⋯ }

@[instance_reducible]

instance Cslib.LTS.instTransToRelationToRelationCons {State : Type u_1} {Label : Type u_2} {μ : Label} {μs : List Label} (lts : LTS State Label) : Trans (Tr.toRelation lts μ) (MTr.toRelation lts μs) (MTr.toRelation lts (μ :: μs))

Transitions can be chained with multi-step transitions.

Equations

• lts.instTransToRelationToRelationCons = { trans := ⋯ }

@[instance_reducible]

instance Cslib.LTS.instTransToRelationToRelationHAppendListConsNil {State : Type u_1} {Label : Type u_2} {μs : List Label} {μ : Label} (lts : LTS State Label) : Trans (MTr.toRelation lts μs) (Tr.toRelation lts μ) (MTr.toRelation lts (μs ++ [μ]))

Multi-step transitions can be chained with transitions.

Equations

• lts.instTransToRelationToRelationHAppendListConsNil = { trans := ⋯ }

@[instance_reducible]

instance Cslib.LTS.instTransToRelationHAppendList {State : Type u_1} {Label : Type u_2} {μs1 μs2 : List Label} (lts : LTS State Label) : Trans (MTr.toRelation lts μs1) (MTr.toRelation lts μs2) (MTr.toRelation lts (μs1 ++ μs2))

Multi-step transitions can be chained.

Equations

• lts.instTransToRelationHAppendList = { trans := ⋯ }