MACHINE
        TP3WinnieMachine
ABSTRACT_VARIABLES
        NbPlaces /*Places libres */
INVARIANT
        NbPlaces : 0 .. 600
INITIALISATION
        NbPlaces := 600
OPERATIONS
        /*------------------------------------------------------*/

        Ajout_Voiture =
                PRE
                        NbPlaces > 0
                THEN
                        NbPlaces := NbPlaces - 1
                END ;

        /*------------------------------------------------------*/

        Retire_Voiture =
                PRE
                        NbPlaces : 0 .. 599
                THEN
                        NbPlaces := NbPlaces + 1
                END ;

        /*------------------------------------------------------*/

        NbLibre <-- Get_NbLibre =
                BEGIN
                        NbLibre := NbPlaces
                END ;

        /*------------------------------------------------------*/

        NbVoitures <-- Get_NbVoitures =
                BEGIN
                        NbVoitures := 600 - NbPlaces
                END

        /*------------------------------------------------------*/

END