-- CADP (CONSTRUCTION AND ANALYSIS OF DISTRIBUTED PROCESSES) -- http://cadp.inria.fr [Last updated: Thu Oct 6 11:24:20 CEST 2022] This directory contains an example for BCG_LABELS, BCG_MIN, BISIMULATOR, CAESAR, CAESAR.ADT, EVALUATOR4, EXP.OPEN, LNT2LOTOS, and SVL. This example is the specification of a distributed Eratosthenes sieve. It is based on a specification written in the XL language by Y.S. Ramakrishna and C.R. Ramakrishnan, which in turn is inspired from a Promela specification due to D. Peled. The LOTOS version was prepared by Frederic Lang in 2005, and the LNT version was prepared by Hubert Garavel and Gianluca Barbon in 2015. The sieve system consists of a pipeline of N+1 processes: - the first process, called generator, sends to the next process a bounded sequence of consecutive numbers starting at 2; - the next N processes, called units, are N instances of the same process; the first number received by a unit, which is prime by construction, is stored in a variable P and sent on the OUTPUT gate; then, each number received by the same unit is either sent forward if not divisible by P, or ignored otherwise. Processes in the pipeline communicate by asynchronous buffers. The system thus contains N buffers, each of which is an instance of a medium process. All buffer gates are eventually hidden, thus making invisible every internal communication between processes. In the end, OUTPUT is the only visible gate. The external behaviour of the system is thus a sequence of N transitions labelled respectively OUTPUT !M_1, ..., OUTPUT !M_N, where M_1, ..., M_N are the first N prime numbers (2, 3, 5, etc.). In this example, several compositional verification techniques are tried, possibly combined with partial order reduction. In all cases, the graphs of sequential processes are first generated, minimized, and then composed using the EXP.OPEN tool. The scenario is as follows: 1) The graph of an instance of the sieve involving 10 units is first generated with partial order reduction turned off and then reduced modulo branching bisimulation. 2) The graph of the same instance of the sieve is generated with partial order reduction (preserving branching bisimulation) turned on. 3) The graph of the same instance of the sieve is generated using incremental reduction: gates are hidden as early as possible in the expression and intermediate compositions reduced modulo branching bisimulation. 4) Finally, a value-passing mu-calculus formula is evaluated on the graph to check that the sieve effectively outputs the first N prime numbers, where the primality test is encoded in the formula. 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