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

Calc tactic support for MTr

@[implicit_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 := ⋯ }

@[implicit_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 := ⋯ }

@[implicit_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 := ⋯ }

@[implicit_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 := ⋯ }