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

[Last updated: Thu Oct  6 11:17:18 CEST 2022]

This directory contains an example for BCG_CMP, BCG_MIN, CAESAR.ADT, CAESAR,
LNT2LOTOS, and SVL. Four systolic arrays computing the convolution product
are described (both in LNT and LOTOS). The four schemes B1, F, W1 and W2
proposed by Kung are tackled.

This example is presented in appendix D of:
   Hubert Garavel. Compilation et ve'rification de programmes LOTOS.
   These de Doctorat, Universite' Joseph-Fourier (Grenoble), Nov 89

See
   http://cadp.inria.fr/publications/Garavel-89-b-CD.html
and
   http://cadp.inria.fr/case-studies/89-b-systol.html

These examples are interesting, since an asynchronous language (LNT or
LOTOS) is used to descrive systolic arrays, which are typically synchronous.

Another interesting point is the use of symbolic expressions: the values
labelling the edges of the graphs are algebraic terms containg free variables.
This is achieved by providing appropriate "symbolic" implementations for
the data types (see file EXP.tnt for the LNT specifications, and files EXP.t
and EXP.f for the LOTOS specifications).

The file "demo.svl" implements the generation and reduction for branching
equivalence of the four graphs systol_B1, systol_F, systol_W1, and systol_W2.
It also checks that the graphs generated from LNT and LOTOS are pairwise
strongly bisimilar.

The whole verification scenario is described and commented in the file 
"demo.svl". It can be executed by typing:
$       svl demo
or even simply
$       svl

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

-------------------------------------------------------------------------------

Note about performance enhancements of CAESAR on this demo during the 1990s:

Benchmarks for CAESAR 3.2     for CAESAR 4.3	for CAESAR 5.2

   systol B1                  systol B1		systol B1
      cells: 3                (idem)		(idem)
      length: 8               (idem)		(idem)
      states: 37986           states: 133	states: 133
      edges: 54312            edges: 216	edges: 216
      time: 3:14              time: 0:25	time: 0:06

   systol F                   systol F		systol F
      cells: 7                (idem)		(idem)
      length: 19              (idem)		(idem)
      states: 438             states: 438	states: 438
      edges: 669              edges: 669	edges: 669
      time: 3:16              time: 0:42	time: 0:08

   systol W1                  systol W1		systol W1
      cells: 3                (idem)		(idem)
      length: 6               (idem)		(idem)
      states: 64004           states: 113	states: 113
      edges: 87596            edges: 181	edges: 181
      time: 5:01              time: 0:27	time: 0:06

   systol W2                  systol W2		systol W2
      cells: 7                (idem)		(idem)
      length: 26              (idem)		(idem)
      states: 447             states: 447	states: 447
      edges: 575              edges: 575	edges: 575
      time: 3:39              time: 0:46	time: 0:08