What is it?
LASH is a toolset for representing infinite sets and exploring infinite state spaces. It is based on finite-state representations, which rely on finite-state automata for representing and manipulating infinite sets of values over various data domains.
The current version of LASH is beta version 0.92 and consists of- C libraries providing functions and datatypes for performing
the following tasks:
- Constructing and manipulating some types of finite-state automata (on finite and infinite words).
- Representing and manipulating finite and infinite sets of
values. The representation systems implemented by
LASH are
- The NDD (Number Decision Diagram), suited for sets of unbounded integer vectors. NDDs are slightly more expressive than Presburger arithmetic.
- The RVA (Real Vector Automaton), suited for sets of unbounded real and integer vectors. RVA can represent all the sets that can be defined in the first-order combined additive theory of the reals and integers.
- The QDD (Queue-content Decision Diagram), suited for sets of contents of unbounded FIFO queues.
- Exploring the state-space of systems composed of a finite control and of unbounded integer variables over which linear operations are performed.
-
Front-ends for
- Compiling program models expressed in the Simple-PROMELA and the Simple-IF languages, and exploring the state-space of these programs.
- Solving problems expressed in Presburger arithmetic.
- State-space exploration tools for timed systems and hybrid systems, based on the RVA package.
- A visualization tool for sets represented by NDDs and RVA.
Where can I find it?
The C sources of the LASH toolset are available free of charge for evaluation purposes and educational use. A copy of the most recent version can be downloaded here. After downloading, please consult the installation instructions.How can I use it?
Documentation and sample programs are available for some components of the package. Additional documentation is available in the source code.- Installation instructions
- Core package: [ Documentation | Examples ]
- NDD package: [ Documentation ]