##########################################################################
#                                                                        #
#  This file is part of GeneSyst.                                        #
#                                                                        #
#  Copyright (C) 2004-2009                                               #
#    CNRS (Centre National de la Recherche Scientifique)                 #
#    INSA (Institut National des Sciences Appliquees)                    #
#                                                                        #
#  you can redistribute it and/or modify it under the terms of the       #
#  CeCILL License (for Ce[a] C[nrs] I[nria] L[logiciel] L[ibre]),        #
#  version 2.                                                            #
#                                                                        #
#  It is distributed in the hope that it will be useful,                 #
#  but WITHOUT ANY WARRANTY; without even the implied warranty of        #
#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the          #
#  CeCILL License for more details. The license is provided in           #
#  french and in english in the Licences directory.                      #
##########################################################################

-------------------------------------------------------------------------
La classe "geneSyst.class" est le programme principal qui calcule
un système de transitions étiquetées associé à une machine (système) 
abstraite ou à un raffinement (si la machine qu'il raffine est founie).
Pour l'utilisation et l'appel du programme, voir le Manuel.ps.

La machine doit satisfaire les conditions suivantes :

1- La machine doit avoir des variables
2- Elle doit contenir une (et une seule) assertion de la forme :
   1.1 : si c'est une machine :
         P1 or P2 or P3 or ...
         C'est la décomposition disjonctive de l'invariant en états.
         
         
   1.2 : si c'est un raffinement :
         ((P1) <=> (R11 or R12)) and ((P2) <=> (R21 or R22)) and ...
         C'est la conjonction d'équivalences entre un état abstrait à gauche 
         et une décomposition disjonctive d'états du raffinement à droite. 
         
3- Elle doit avoir des opérations (Sous forme d'événements).

Remarque: il est important de valider les différentes obligations de preuve
          de la machine de départ pour etre certain que pour tout état qui 
          satisfait l'invariant, un au moins des Pi de la décomposition est 
          aussi satisfait (tous les états sont représentés).
-------------------------------------------------------------------------