MACHINE
	TP3WinnieMachine
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 /*Au moins 1 voiture dans le parking */
		THEN
			NbPlaces := NbPlaces +1
		END;
	
	/*------------------------------------------------------*/
		
	NbLibre <-- Get_NbLibre =
		BEGIN
			NbLibre := NbPlaces
		END;
	
	/*------------------------------------------------------*/
		
	NbVoitures <-- Get_NbVoitures =
		BEGIN
			NbVoitures := 600-NbPlaces
		END
	
	/*------------------------------------------------------*/
	
END