IMPLEMENTATION
	TP3WinnieImp
REFINES
	TP3WinnieMachine
CONCRETE_VARIABLES
	C_NbPlaces
INVARIANT
	C_NbPlaces : 0..600 &
	C_NbPlaces = NbPlaces
INITIALISATION
	C_NbPlaces := 600
OPERATIONS

	/*------------------------------------------------------*/
	
	Ajout_Voiture =
		BEGIN
			C_NbPlaces := C_NbPlaces -1
		END;
	
	/*------------------------------------------------------*/
		
	Retire_Voiture =
		BEGIN
			C_NbPlaces := C_NbPlaces +1
		END;
	
	/*------------------------------------------------------*/
		
	NbLibre <-- Get_NbLibre =
		BEGIN
			NbLibre := C_NbPlaces
		END;
	
	/*------------------------------------------------------*/
		
	NbVoitures <-- Get_NbVoitures =
		BEGIN
			NbVoitures := 600-C_NbPlaces
		END
	
	/*------------------------------------------------------*/

END