IMPLEMENTATION
        TP3WinnieImp
REFINES
        TP3WinnieMachine
IMPORTS
        (C_TableParkings.BASIC_ARRAY_VAR) ( 0 .. 10 , 0 .. 600 )
INVARIANT
        (C_TableParkings.arr_vrb) = TableParkings
INITIALISATION
        (C_TableParkings.STR_ARRAY) ( 0 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 1 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 2 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 3 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 4 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 5 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 6 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 7 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 8 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 9 , 600 ) ;
        (C_TableParkings.STR_ARRAY) ( 10 , 600 )
OPERATIONS

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

        Ajout_Voiture ( IdParking ) =
                VAR xx IN
                        xx <-- (C_TableParkings.VAL_ARRAY) ( IdParking ) ;
                        xx := xx - 1 ;
                        (C_TableParkings.STR_ARRAY) ( IdParking , xx )
                END ;

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

        Retire_Voiture ( IdParking ) =
                VAR xx IN
                        xx <-- (C_TableParkings.VAL_ARRAY) ( IdParking ) ;
                        xx := xx + 1 ;
                        (C_TableParkings.STR_ARRAY) ( IdParking , xx )
                END ;

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

        NbLibre <-- Get_NbLibre ( IdParking ) =
                BEGIN
                        NbLibre <-- (C_TableParkings.VAL_ARRAY) ( IdParking )
                END ;

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

        NbVoitures <-- Get_NbVoitures ( IdParking ) =
                VAR xx IN
                        xx <-- (C_TableParkings.VAL_ARRAY) ( IdParking ) ;
                        NbVoitures := 600 - xx
                END

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

END