Module Lts

module Lts: sig .. end

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.

module type STATE = Utils.OrderedTypeExt.T

Signature of the module describing state identifiers

module type LABEL = Utils.OrderedTypeExt.T

Signature of the module describing transition labels

module type T = sig .. end

Output signature of the functor Lts.Make.

module 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

module 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

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

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

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

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

module type Merge = sig .. end

Signature of the second argument for the Lts.IProduct functor

module 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

module type Merge3 = sig .. end

Signature of the second argument for the Lts.IProduct3 functor

module 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