$Id: README,v 1.1 1998/09/18 14:26:52 abel Exp $ 

Production Cell:

This examples was obtained from:

@InBook{Lindne94,
  author =       {Thomas Lindner},
  title =        {Case Study "Production Cell": A Comparative Study in Formal
                  Software Development},
  chapter =      2,
  publisher =    {FZI},
  year =         1994,
  pages =        {9,21}
}

It models the control of a plant in which a crane, two conveyor belts, a
rotating table, an articulated arm and a press are involved. The system is
closed, that is, there are no inputs.

The movement of all the pieces has been discretized and encoded. The number of
latches that the FSM will have is strongly dependent on the resolution chosen
for these encodings. That would be a possible way to obtain a more challenging
problem out of the same example. A parametric description, with one parameter
for each encoding would be ideal.

The formulas verified in the model refer to the limitation in the mobility of
the different parts (safety) as well as the continuous progress of the system.

See prodcell.ctl for the detailed set of formulas.

Author: Abelardo Pardo <abel@vlsi.colorado.edu>