|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
|
|
|
|
|
| Pictures courtesy of Jan Friso Groote and Frank van Ham (Technical University of Eindhoven) | ||||
The VLTS acronym stands for "Very Large Transition Systems".
The VLTS benchmark suite is a collection of Labelled Transition Systems (hereafter called benchmarks).
Each Labelled Transition System is a directed, connected graph, whose vertices are called states and whose edges are called transitions. There is one distinguished vertex called the initial state. Each transition is labelled by a character string called action or label. There is one distinguished label noted "i" that is used for so-called invisible transitions (also known as hidden transitions or tau-transitions).
The VLTS benchmarks have been obtained from various case studies about the modelling of communication protocols and concurrent systems. Many of these case studies correspond to real life, industrial systems.
The VLTS benchmark suite is designed to be a reference criterion for scientific assessment of algorithms and tools operating on large graphs.
In particular, this encompasses algorithms and tools for explicit state verification of concurrent systems, including:
Algorithms and tools operating on more general graphs than transition systems may also benefit from the VLTS benchmark suite by simply discarding label information attached to transitions.
The need for the VLTS benchmark suite was recognized in several places, e.g., by Agostino Dovier, Carla Piazza, and Alberto Policriti in their CAV'2001 paper ("A Fast Bisimulation Algorithm"):
The VLTS benchmark suite intends to fill this gap by providing a comprehensive set of benchmarks. We hope that it will be as useful as other standard benchmarks, such as those developed, e.g., to assess Binary Decision Diagrams packages.
First, you should make sure that you are working on a machine with enough free disk space available (at least 500 megabytes, 1 gigabyte to be safe).
If you do not have already the CADP tools installed on your machine, please registrate here.
After downloading a graph, say "graph.bcg.bz2", from the Table below, you must first uncompress it using the bunzip2 tool:
bunzip2 graph.bcg.bz2
This will produce a BCG graph named "graph.bcg".
You can read and process "graph.bcg" from a computer program in two different ways:
Note: In addition to the VLTS benchmarks, you might be interested by the various classes of `regular' benchmarks produced by the bcg_graph tool.
The VLTS benchmarks can be downloaded from the Table below. Each row of the Table corresponds to one benchmark. The columns of the Table contain the following data:
|
* Note: Benchmark "vasy_720_390" is not a connected graph: there are states and transitions that cannot be reached from the initial state. This fact is clear as the number of states is greater than the number of transitions, and is also confirmed by the bcg_info tool with option -unreachable: states 87,739...720,126 and 720,128...720,246 are unreachable (there are only 87,740 reachable states and 390,510 reachable transitions). This benchmark is included to make sure that tools operating on VLTSs handle disconnected graphs properly (i.e., that they do not crash nor loop indefinitely). There are two main reasons for this requirement: (1) the usual definition of Labelled Transition Systems given in most scientific papers and textbooks is not restricted to connected graphs, and (2) in practice, disconnected graphs are produced by distributed state space generation algorithms, which construct the global state space as a collection of several disconnected graph fragments (see, e.g., the definition of a partitioned LTS).
The diagram below summarizes facts about the dispersion of the VLTS-1 benchmarks. The average branching factor is equal to the number of transitions divided by the number of states. To obtain a diagram of reasonable size, the three benchmarks with the highest branching factor are represented with a lower ordinate (Y-axis) than actually.
|
|
For some of the above benchmarks, you can find here a fancy graphical visualization provided by Jan Friso Groote and Frank van Ham (Technical University of Eindhoven). |
|
We plan to extend the benchmark suite in the future. We are therefore interested in getting new benchmarks of various origins.
However, due to the limited capacity of our ftp site, a selection might be needed before including new benchmarks.
If you plan to donate new benchmarks, please keep in mind the following guidelines:
Please keep in mind that we will not update the benchmark suite every time a new benchmark is donated. We will wait to have a critical mass of new benchmarks before issuing a new version of the benchmark suite.
The bcg_labels tool with its -scramble option can be used to remove information contained in the labels of a BCG graph. This enables to donate a benchmark produced from an industrial case study without revealing intellectual property covered by non-disclosure agreements. Option -scramble is available since CADP BETA-VERSION 2008-g (December 2009). See the bcg_labels manual page for more information.
See also:
Back to the CADP Home Page