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

[Last updated: Fri Apr 12 10:47:29 CEST 2024]

Introduction
============

  This directory contains an application of CADP to the verification
  of a distributed knowledge base system called Co4 and described in:

  [Pecheur-97] Charles Pecheur. Specification and Verification of the
  CO4 Distributed Knowledge System Using LOTOS. Proceedings of the
  12th IEEE International Conference on Automated Software Engineering
  ASE-97 (Incline Village, Nevada, USA), November 1997. Extended version
  available as INRIA Research Report RR-3259. 

  See
     http://cadp.inria.fr/publications/Pecheur-97.html
  and
     http://cadp.inria.fr/case-studies/97-a-co4.html

History of the LOTOS specification
==================================

  The LOTOS specification and the different verification stages were
  developed by Charles Pecheur in 1997. Several variants of the
  specification are provided and used to verify different properties.
  Verification is centered on the use of the EXHIBITOR tool.

  1) This specification has been written using Norman Ramsey's NOWEB
  literate programming system. The LOTOS files in this directory have
  been automatically extracted from a single source document, which
  also contains all commentaries. The source document is not provided
  but appears in typeset form as annex A of [Pecheur-97].

  2) The data types in this specification have been defined using
  Charles Pecheur's APERO concise syntax extensions. The LOTOS files 
  in this directory contain the translation of those definitions in
  standard LOTOS, tuned for the CADP data type compiler.

  In 2023, the LOTOS specification was revised and shortened by Hubert
  Garavel, who removed a number of useless definitions. The list of
  changes brought is documented in LOTOS/notes.txt.

History of the LNT specification
================================

  In 2022, the LOTOS specification was translated to LNT on the basis
  of a student project done by Vincent Ribot and Jolahn Vaudey (Univ.
  Grenoble Alpes). Their LNT specification was revised in November 2023
  by Hubert Garavel and modified to ensure strong equivalence with the
  LOTOS specification.

Contents of the present directory
=================================

=READ_ME.txt: the file you are presently reading.

co4_*_*.lnt: the different variants of the LNT specification, where the
  variable tags designate the chosen hierarchy and the chosen user input
  scenario, respectively. Refer to Annex A of [Pecheur-97] for details.

CO4_DATATYPES.lnt: the data type definitions, shared by all variants.

CO4_PROCESSES.lnt: the general process definitions, shared by all variants.

*.seq: filters on execution sequences, for use with EXHIBITOR.

short.rename: renaming file to shorten transition labels, in order to produce
  nicer-looking graph print-outs.

demo.svl: a script for SVL that automates all necessary tool invocations.

Contents of the LOTOS sub-directory
===================================

LOTOS/CO4_DATATYPES.lib: the data type definitions, shared by all variants.

LOTOS/CO4_PROCESSES.lib: the general process definitions, shared by all
  variants.

LOTOS/co4_*_*.lotos: the different variants of the LOTOS specification,
  where the variable tags designate the chosen hierarchy and the chosen
  user input scenario, respectively.

Execution using SVL
===================

The SVL script "demo.svl" allows to execute the entire verification. 
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