LASH is a toolset developed at the University of Liège 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.
The following features are under development and will soon become part
of the toolset:
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.