-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES)
-- http://cadp.inria.fr

[Last updated: Fri Apr 12 10:50:49 CEST 2024]

This directory contains an example for BCG_MIN, BCG_CMP, CAESAR, CAESAR.ADT,
EXP.OPEN, LNT2LOTOS, SVL, and XTL.

It describes the leader election protocol used in the HAVi (Home Audio-Video)
standard developed by eight consumer electronics companies (Grundig, Hitachi,
Matsushita, Philips, Sharp, Sony, Thomson, and Toshiba) in order to solve
interoperability problems for home audio/video networks.

The LOTOS and XTL source files for this example have been gracefully provided
by Judi Romijn (University of Nijmegen, The Netherlands). The case study is
fully described in the following document:

* Judi Romijn. "Model Checking a HAVi Leader Election Protocol".
* Technical Report SEN-R9915, CWI, June 1999.
* Available on-line from http://ir.cwi.nl/pub/4534/04534D.pdf

Two versions of the HAVi leader election protocol are contained in this demo:
an asynchronous and a synchronous one. The HAVi configuration considered here
involves two DCMs (Device Control Managers).

In 2022, the two LOTOS specifications were decomposed into libraries by
Hubert Garavel, who factored out common code between the synchronous and the
asynchronous versions. The LOTOS specifications were translated to LNT by
Hubert Garavel, on the basis of a student project done by Reyhane Falanji
and Florian Gallay (MOSIG, Univ. Grenoble Alpes, France). The LTSs generated
from the LNT and LOTOS specifications are pairwise strongly equivalent.
The LNT specifications are slightly more concise than the LOTOS ones (900
vs 980 lines). 

Files:
   doc/Romijn-99.pdf       original publication (1999)
   BUS.lnt                 LNT definitions of processes
   CHANNELS.lnt            LNT definitions of channels
   CMM.lnt                 LNT definitions of processes
   DCM_asyn.lnt            LNT definitions of processes
   DCM_sync.lnt            LNT definitions of processes
   HAVi_asyn.lnt           LNT definitions of the main process
   HAVi_sync.lnt           LNT definitions of the main process
   MS.lnt                  LNT definitions of types, functions, and processes
   TYPES.lnt               LNT definitions of types and functions
   demo.svl                compositional verification of the protocols
   LOTOS/HAVi_asyn.lotos   asynchronous protocol specification in LOTOS
   LOTOS/HAVi_sync.lotos   synchronous protocol specification in LOTOS
   LOTOS/*.lib             libraries of LOTOS data types and processes
   LOTOS/demo.svl          compositional state-space generation

This example makes use of the compositional verification features provided
by CADP, although the LTSs corresponding to the LNT and LOTOS specifications
can also be generated directly. As described in the "demo.svl" file, the HAVi
leader election protocol is divided into several processes, the corresponding
LTSs being automatically generated and reduced modulo strong equivalence.
These LTSs are then composed together (using LNT or LOTOS parallel composition
operators). The final LTSs are generated and stored in the files named
"HAVi_{asyn,sync}.bcg".

The desired temporal properties of the protocol are specified in XTL and
verified on the LTSs HAVi_{asyn,sync}.bcg using the XTL model-checker.

Typing the command
$	svl demo
or even simply
$	svl
will generate the LTSs automatically and then verify the temporal logic
properties, first for the asynchronous version, then for the synchronous
version.

After the verification you may type
$	svl -clean demo
or even simply
$	svl -clean
to remove all the generated files.

Note 1:

The translation to LNT simplified the LOTOS specifications in various ways:
- The projection functions firstn and secondn of type NodeTuple are defined
  but never used in the LOTOS code.
- Both processes ffDM and flDM are actually identical, since the 'leader'
  parameter of process ffDM is unused. These two processes have been merged
  and expanded in-line in process ifDM. 
- Both processes fliDM and ffiDM are similar, since calling fliDM [...] (...)
  is identical to calling ffiDM [...] (..., leader -> Id). These processes
  have been merged and expanded in-line in process DeclareLeader.
- Process DeclareCapability was expanded in-line in process ifDM.
- Both processes ilDM and Elect have been merged in a single process ilDM.
- In process downDM, stop [> B can be replaced by B.
- In processes BusReset and BusReset2, the gEvent parameter is useless.
- In processes CMMReady, CMMDeliver, CMMDeliver2, MSSuspend, and MSUp, the
  parameter gUpDown is useless.
- Similarly, useless variables and value parameters have been removed.
- The LNT specifications have been made more readable by reducing the nesting
  depth of parallel composition operators from 4 (in LOTOS) to 3 (in LNT).

Note 2:

The following tables summarize the sizes of individual processes obtained for
the LOTOS version of the asynchronous protocol, before and after minimization
modulo strong equivalence, using either CAESAR 6.0 (CADP 2001 "Ottawa") or
CAESAR 7.0 (CADP 2006 "Edinburgh"). The final LTS has 5,107 states and
18,725 transitions.

Using CAESAR 6.0:

+------------------+-----------------------++----------------------+
|                  | before  minimization  ||  after  minimization |
|    CAESAR 6.0    +---------+-------------++--------+-------------+
|                  | states  | transitions || states | transitions |
+------------------+---------+-------------++--------+-------------+
| BUSRESET         |      33 |          45 ||     16 |          24 |
+------------------+---------+-------------++--------+-------------+
| DCM (1)          | 404,477 |   3,025,842 ||     37 |         233 |
+------------------+---------+-------------++--------+-------------+
| DCM (2)          |   2,155 |      18,392 ||     27 |         170 |
+------------------+---------+-------------++--------+-------------+
| CMM (1), CMM (2) |   9,497 |      43,418 ||     12 |          49 |
+------------------+---------+-------------++--------+-------------+
| MS (1), MS (2)   |   2,279 |      17,931 ||     27 |         159 |
+------------------+---------+-------------++--------+-------------+

Using CAESAR 7.0:

+------------------+-----------------------++----------------------+
|                  | before  minimization  ||  after  minimization |
|    CAESAR 7.0    +---------+-------------++--------+-------------+
|                  | states  | transitions || states | transitions |
+------------------+---------+-------------++--------+-------------+
| BUSRESET         |      17 |          25 ||     16 |          24 |
+------------------+---------+-------------++--------+-------------+
| DCM (1)          |      92 |         977 ||     37 |         233 |
+------------------+---------+-------------++--------+-------------+
| DCM (2)          |      53 |         592 ||     27 |         170 |
+------------------+---------+-------------++--------+-------------+
| CMM (1), CMM (2) |      32 |         125 ||     12 |          49 |
+------------------+---------+-------------++--------+-------------+
| MS (1), MS (2)   |      69 |         504 ||     27 |         159 |
+------------------+---------+-------------++--------+-------------+