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