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

[Last updated: Mon Nov  4 10:53:00 CET 2024]

This directory contains an example for BCG, BCG_MIN, BISIMULATOR, CAESAR, 
CAESAR.ADT, EVALUATOR, OPEN/CAESAR, PROJECTOR, and SVL. It describes a
reliable atomic multicast protocol written in full LOTOS (with values).

* This example originates from the HP Labs in Bristol.
* It is described in detail in:
*    Simon Bainbridge and Laurent Mounier
*    Specification and Verification of a Reliable Multicast Protocol
*    Hewlett-Packard Laboratories Bristol, U.K.
*    HPL-91-163, oct 1991
* It is summarized in:
*    Fernandez, Garavel, Mounier, Rasse, Rodriguez, and Sifakis
*    A Toolbox for the Verification of LOTOS Programs
*    Proceedings of the 14th International Conference on Software 
*    Engineering ICSE'14 (Melbourne, Australia), may 1992
*    Lori A. Clarke, editor, ACM.

Three versions of the rel/REL protocol are described:

- Version A (rel_rel_A.lnt) and Version B (rel_rel_B.lnt): they describe
  an architecture composed of 1 Transmitter and 2 Receiver nodes. These
  versions are verified using equivalence checking and model checking.

- Version C (rel_rel_C.lnt): it describes an architecture composed of
  1 Transmitter and 3 Receiver nodes. This version is verified compositionally
  with user-given interfaces.

The file "demo.svl" describes the verification of the protocol.
You can execute it by typing:
$	svl demo
or even simply 
$	svl

Detailed explanations on the verification scenario are given in "demo.svl".

After execution of the SVL scenario, all generated files can be removed 
by typing
$	svl -clean demo
or even simply
$	svl -clean


Note: The following tables summarize the sizes of the LTSs generated 
compositionally from the LOTOS specification of version C, before and
after minimization modulo strong equivalence, using either CAESAR 6.0
(CADP 2001 "Ottawa") or CAESAR 7.0 (CADP 2006 "Edinburgh").

Let Ri = (RECEIVER_NODE_i -||? "interface.lotos":INTERFACE [R_Ti, ...])
         where i = 1, 2, 3
     T = CRASH_TRANSMITTER
    A1 = (R2 |[R23, R32]| R3) -|[RT_2, RT_3]| T
    A2 = (R1 |[R12, R21, R13, R31]| A1) -|[RT_1, RT_2, RT_3]| T
and  F = hide ... in (A2 |[RT_1, RT_2, RT_3]| T)

Using CAESAR 6.0:

+----+-----------------------++-----------------------+
|    | before  minimization  ||  after  minimization  |
|6.0 +---------+-------------++---------+-------------+
|    | states  | transitions || states  | transitions |
+----+---------+-------------++---------+-------------+
| Ri |  16,674 |     108,047 ||   1,088 |      14,883 |
+----+---------+-------------++---------+-------------+
| T  |     187 |         264 ||      50 |         151 |
+----+---------+-------------++---------+-------------+
| A1 |  66,929 |     969,382 ||  31,475 |     431,072 |
+----+---------+-------------++---------+-------------+
| A2 | 311,775 |   2,672,613 ||  71,423 |     616,538 | 
+----+---------+-------------++---------+-------------+
| F  | 286,117 |   2,302,600 || 150,911 |   1,249,375 |
+----+---------+-------------++---------+-------------+

Using CAESAR 7.0:

+----+-----------------------++-----------------------+
|    | before  minimization  ||  after  minimization  |
|7.0 +---------+-------------++---------+-------------+
|    | states  | transitions || states  | transitions |
+----+---------+-------------++---------+-------------+
| Ri |   1,086 |       8,290 ||     369 |       7,313 |
+----+---------+-------------++---------+-------------+
| T  |     187 |         264 ||      50 |         151 |
+----+---------+-------------++---------+-------------+
| A1 |  22,557 |     481,830 ||  21,644 |     457,552 |
+----+---------+-------------++---------+-------------+
| A2 | 212,545 |   2,453,385 || 137,086 |   1,535,507 |
+----+---------+-------------++---------+-------------+
| F  | 692,429 |   6,737,959 || 150,911 |   1,249,375 |
+----+---------+-------------++---------+-------------+