package lascar

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

Module Lascar.LtsaSource

Labeled Transition Systems with State Attributes

A Labeled Transition System with Attributes on states (LTSA) is 6-uple (Q,L,A,I,a,R) where

  • Q is a set of state identifiers
  • L is a set of transition labels
  • A is a set of state attributes
  • I is a subset of Q giving the initial states
  • a is function from Q to A associating a state to its attribute
  • R is the transition relation, defined as a subset of QxLxQ
Sourcetype Utils.Dot.graph_style +=
  1. | Circular
    (*

    Circular layout (circo); default is layered

    *)
  2. | NoAttr
    (*

    Do not draw state attributes

    *)
  3. | NoLabel
    (*

    Do not draw transition label

    *)

Extension to the Dot.graph_style type for drawing LTSAs

Input signatures of the functor Ltsa.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 ATTR = sig ... end

Signature of the module describing state attributes

Sourcemodule type T = sig ... end

Output signature of the functor Ltsa.Make.

Functor building an implementation of the LTSA structure given an implementation of state identifiers, transition labels and state attributes

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

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

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

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

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

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

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 and type attr = S.attr) : sig ... end

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

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 and type attr = S.attr) : sig ... end

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