This directory contains the demo files of the Esterel bus arbiter
example. It contains the following files:

- arbiter4.strl:
  the Esterel source code for the arbiter with 4 cells.

- obs-arb4.strl:
  The Esterel source file where the program above is put in parallel
  with synchronous Esterel observers that define a set of safety
  properties plus a bounded liveness property. Each property is
  associated with a specific output signal defined within the
  corresponding observer. The goal is to check if these property
  signals can be emitted or not in some reachable state of the
  program.
  

- Makefile:
  This Makefile helps you to launch the verification sessions. You
  may edit the Makefile to set the variables CC to point to your
  preferred C compiler and ESTEREL to point the your Esterel
  compiler. The Makefile commands are:

  * make clean
      removes all the files generated by the verification session

  * make simple-verif
      launches a simple verification session (see below for details)

  * make obs-verif 
      launches a verification session for the verification of
      properties expressed with synchronous observers (see below for
      details).

Hereafter, we detail the steps of the different verification
sessions.

Generation of the blif files
----------------------------

To perform the verification under Xeve, the above Makefile commands
first generate the blif files of the Esterel programs using the Esterel
compiler as:

   esterel -causal -Lblif arbiter4.strl
   esterel -causal -Lblif obs-arb4.strl

These two commands generate the blif files arbiter4.blif and
obs-arb4.blif respectively. The option -causal is used to perform the
constructive analysis that is needed in the arbiter example, since the 
Esterel program is cyclic (see the Esterel documentation for more
details on this point).

Checking the properties
-----------------------

   1. Simple properties with "make simple-verif"
   ---------------------------------------------
   Type

      make simple-verif

   Both Xeve and Xes panels appear on the screen after an Esterel
   compilation of the program in the blif format and in C.
   Then you can check properties simply by fixing constant values to
   some input signals, forming an input condition, and check whether
   some output signals can be emitted or not under this input condition.
   Under Xeve, select the "CHECK OUTPUTS" verification function.

   Fix the input signals RequestIn2, RequestIn3, RequestIn4 to the
   constant value 0 by coloring them in blue using the underlying
   color palette. Fix the input signal RequestIn1 to value 1 by
   coloring the signal name in red. The input condition is "RequestIn1 
   is always present, the other input signals are always absent".

   Select the output signal AckOut1 and color the name in red. This
   means that we want to check if AckOut1 can be emitted under the
   input condition. Click on the "Apply" button. The output AckOut1
   is shown to be possibly emitted in a result window. A diagnostic
   path is saved in the file AckOut.esi in the input format of the
   graphical Esterel simulator Xes.

   Now color AckOut1 in blue. This time, we want to check if AckOut1
   can be not emitted under the input condition. Click on the "Apply"
   button again. A window showing that the output signal AckOut1 is
   always emitted.

   The .esi files Xeve generates (AckOut1.esi for example) can be
   played in the graphical Esterel simulator Xes in the Tape Recorder
   under the menu Commands of the Main Panel of Xes (*).

   2. Verifying Esterel observers with "make obs-verif"
   ----------------------------------------------------
   Type

      make obs-verif

   You can edit the file obs-arb4.strl to see the Esterel observers we 
   have written for this example. They define a set of safety
   properties. Notice that we have hidden the program output signals
   and let visible the observer output signals only. Color the output
   signals in red and click on the "Apply" button. A result window
   shows the status of each observer signal independently.

   The .esi files Xeve generates can be played in the graphical
   Esterel simulator Xes in the Tape Player/Recorder under the menu
   Commands of the Main Panel of Xes (*).

   (*) Remark: this make sens for pure programs only. For programs with
   values, Xeve enables verification on the control part, abstracting
   away the data-path. Hence, the diagnostic paths are not playable in 
   Xes as is. This will be made possible for valued programs in a later
   release.

Please send your comments, feedback and suggestions to
esterel-request@sophia.inria.fr and send your bug reports to
esterel-bugs@sophia.inria.fr.

Copyright CMA/INRIA 1996-2000.
