-- 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