MACHINE
        TP3WinnieMachine
ABSTRACT_VARIABLES
        TableParkings         /*Tableau des parkings*/
INVARIANT
        TableParkings : 0 .. 10 --> 0 .. 600
INITIALISATION
        TableParkings :: 0 .. 10 --> 0 .. 600
OPERATIONS



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

        Ajout_Voiture ( IdParking ) =
                PRE
                        IdParking : 0 .. 10 &
                        TableParkings ( IdParking ) > 0
                THEN
                        TableParkings ( IdParking ) := TableParkings ( IdParking ) - 1
                END ;

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

        Retire_Voiture ( IdParking ) =
                PRE
                        IdParking : 0 .. 10 &
                        TableParkings ( IdParking ) : 0 .. 599
                THEN
                        TableParkings ( IdParking ) := TableParkings ( IdParking ) + 1
                END ;

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

        NbLibre <-- Get_NbLibre ( IdParking ) =
                PRE
                        IdParking : 0 .. 10
                THEN
                        NbLibre := TableParkings ( IdParking )
                END ;

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

        NbVoitures <-- Get_NbVoitures ( IdParking ) =
                PRE
                        IdParking : 0 .. 10
                THEN
                        NbVoitures := 600 - TableParkings ( IdParking )
                END

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

END