package lascar

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

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

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 ATTR = sig ... end

Signature of the module describing state attributes

module 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

module 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

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

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

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

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

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

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

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

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