package lascar

  1. Overview
  2. Docs

Module Lascar.LtsSource

Labeled Transition Systems

A Labeled Transition System is 4-uple (Q,L,I,R) where

  • Q is a set of state identifiers
  • L is a set of transition labels
  • I is a subset of Q giving the initial states
  • R is the transition relation, defined as a subset of QxLxQ

Input signatures of the functor Lts.Make.

Sourcemodule type STATE = Utils.OrderedTypeExt.T

Signature of the module describing state identifiers

Sourcemodule type LABEL = Utils.OrderedTypeExt.T

Signature of the module describing transition labels

Sourcemodule type T = sig ... end

Output signature of the functor Lts.Make.

Sourcemodule Make (S : STATE) (L : LABEL) : T with type state = S.t and type label = L.t

Functor building an implementation of the LTS structure given an implementation of state identifiers, transition labels

Sourcemodule Trans (S1 : T) (S2 : T) : sig ... end

Functor for converting a LTS, with a given implementation of state identifiers and transition labels into another one with different respective implementations

Sourcemodule Product (S1 : T) (S2 : T) : sig ... end

Functor for computing the external product, in different flavors, of two LTS

Sourcemodule Product3 (S1 : T) (S2 : T) (S3 : T) : sig ... end

Functor for computing the external product, in different flavors, of three LTS

Sourcemodule type Merge = sig ... end

Signature of the second argument for the IProduct functor

Sourcemodule IProduct (S : T) (M : Merge with type state = S.state and type label = S.label) : sig ... end

Functor for computing the internal product, in different flavors, of two LTS

Sourcemodule type Merge3 = sig ... end

Signature of the second argument for the IProduct3 functor

Sourcemodule IProduct3 (S : T) (M : Merge3 with type state = S.state and type label = S.label) : sig ... end

Functor for computing the "internal" product, in different flavors, of three LTS