PerSCiDO facilitates the exploration of research datasets.
Share your research datasets using PerSCiDO!
The VLTS benchmark suite is a collection of Labelled Transition Systems.
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 can be downloaded from http://cadp.inria.fr/resources/vlts/#section-3
Each benchmark is described in a Table with the following columns:
Column1: Benchmarck name, of the form "X_M_N.bcg.bz2", where X gives the origin of the benchmark (cwi or vasy), M is the number of states divided by 1000, and N is the number of transitions divided by 1000.
Column 2: Number of states
Column 3: Number of transitions
Column 4: Number of tau-transitions (a.k.a. invisible transitions or "i"-transitions).
Column 5: Number of distinct labels
Column 6: Branching factor (average [minimal - maximal])
Column 7: Presence of deadlocks: yes (X) or no (-)
Column 8: Presence of livelocks (i.e., cycles of one or more tau-transitions) : yes (X) or no (-)
Column 9: Deterministic graph (i.e., transitions going out of the same state have different labels): yes (X) or no (-)
Column 10: Version of the VLTS benchmark suite to which the benchmark belongs
Column 11: Size of the BCG file in kilobytes (1 kB = 1024 bytes)
Column 12: Size of the BCG file in kilobytes after compression by bzip2
All the graphs are encoded in the BCG (Binary-Coded Graphs) format, then compressed using the bzip2 tool. To our knowledge, this is up to now the most compact way for storing Very Large Transition Systems.
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:
This will produce a BCG graph named "graph.bcg".
You can read and process "graph.bcg" from a computer program in two different ways:
You can use the bcg_read API (Application Programming Interface), which provides a simple set of functions for handling BCG graphs. You will have to link your computer program against the BCG binary libraries.
You can use the bcg_io tool, which converts BCG graphs into a dozen of other formats (mostly textual formats). To avoid disk space overflow, it is recommended to use this tool in pipe mode, so that the converted graph is not written to disk. For instance:
bcg_io graph.bcg -aldebaran - | more
Keywords:concurrency theory, equivalence checking, graph, model checking
Corresponding tasks:factorial analysis, formal verification, model verification
Encoding data format:bcg -Binary-Coded Graphs-
VLTS Benchmark Suite. Jointly created by CWI/SEN2 and INRIA/VASY as a CADP resource.. Published 2018 via Perscido-Grenoble-Alpes;