Module Ltsa

module Ltsa: sig .. end

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

`\|`	`NoLabel`
`\|`	`NoAttr`
`\|`	`Circular`	`(*`	Circular layout (circo); default is layered	`*)`

Extension to the Dot.graph_style type for drawing LTSAs

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.

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 building an implementation of the LTSA structure given an implementation of state identifiers, transition labels and state attributes

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

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