An OCaml library for manipulating Labeled Transition Systems
Switch branches/tags
Nothing to show
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.
Permalink
Failed to load latest commit information.
doc
etc
examples
src
.gitignore
CHANGELOG.md
KNOWNBUGS
LICENSE
META
Makefile
OPAM
README.md
TODO
VERSION
configure
descr
url

README.md

LASCAr

LASCAr is a library for manipulating Labeled Transition Systems (LTS) in OCaml. LASCAr provides functions for

  • building and inspecting models of such systems

  • generating graphical (.dot format) and text (.tex format) representations

  • computing execution trees and displaying them in graphical or text format

  • computing the product (in various flavors) of such systems

LASCAr provides implementations both for "generic" LTS (with or without state attributes) and for "specialized" versions :

  • deterministic and non-deterministic finite automata (DFA, NFA),

  • Mealy and Moore automata

  • Finite State Machines (FSMs)

The library makes a heavy use of functors to support genericity and to maximise code reuse.

Documentation

The library API is documented here.

Some annotated code snippets can be found here.

Other examples are provided in a dedicated directory.

Installation

The source code for the latest release is here. Compiling and installing requires GNU make and OCaml (version 4.03 or latter, with OCamlP4 support).

LASCAr is also available

  • via github (git clone https://github.com/jserot/lascar)

  • as an opam package

Usage

To use compile a program foo.ml making use of the library, simply execute

$ ocamlc -I <install_dir> -o foo utils.cma lascar.cma foo.ml

or, better, if the package has been installed with ocamlfind or opam

$ ocamlfind ocamlc -package lascar -linkpkg -o foo foo.ml

For displaying the generated .dot files, you will need to install the Graphviz suite of tools.