package lascar

  1. Overview
  2. Docs
package lascar
Legend:
Library
Module
Module type
Parameter
Class
Class type

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 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 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