MACHINE
	TestAgl
SETS
	STAGE;ENTREPRISE;EMPLOYE
VARIABLES
	stage,entreprise,employe,est_affecte,est_signataire,a_pour_responsable,est_propose
INVARIANT
	stage Í STAGE Ù
	entreprise Í ENTREPRISE Ù
	employe Í EMPLOYE Ù
	
	est_affecte Î employe ® entreprise Ù
	est_signataire Î employe  entreprise Ù
	est_signataire Í est_affecte Ù
	a_pour_responsable Î stage ® employe Ù
	est_propose Î stage ® entreprise Ù
	ran(a_pour_responsable) Ç dom(est_signataire) = Æ Ù
	(a_pour_responsable-1;est_propose) Í est_affecte
	
INITIALISATION
	stage,entreprise,employe,est_affecte,est_signataire,a_pour_responsable,est_propose := Æ,Æ,Æ,Æ,Æ,Æ,Æ

OPERATIONS

	Ajout_entreprise(ee) =
		PRE
			ee Î ENTREPRISE - entreprise
		THEN
			entreprise := entreprise È {ee}
		END;
		
	Supp_Employe(em) =
		PRE
			em Î employe
		THEN
			employe 				:= employe - {em} 				||
			est_affecte 		:= {em}  est_affecte 		||
			est_signataire 	:= {em}  est_signataire 	||
			a_pour_responsable:= a_pour_responsable  {em}		
		END;

	
	
	Affecte_Employe(em,en) =
		PRE
			em Î employe Ù
			em Ï dom(est_affecte) Ù
			en Î entreprise
		THEN
			est_affecte := est_affecte È {emaen}
		END;
		
	Desaffecte_Employe(em) =
		PRE
			em Î employe Ù
			em Î dom(est_affecte)
		THEN
			est_affecte 		:= {em}  est_affecte 		||
			est_signataire 	:= {em}  est_signataire 	||
			a_pour_responsable:= a_pour_responsable  {em}	
		END;

	
	Affecte_Signataire(em,en) =
		PRE
			em Î employe Ù
			em Î dom(est_affecte) Ù
			em Ï ran(a_pour_responsable) Ù
			en Î entreprise Ù
			{em a en} Í est_affecte Ù
			en Ï ran(est_signataire) 			
		THEN
			est_signataire := est_signataire È {emaen}
		END;

	Desaffecte_Signataire(em) =
		PRE
			em Î employe Ù
			em Î dom(est_affecte) Ù
			em Î dom(est_signataire)
		THEN
			est_signataire :={em}  est_signataire
		END;

	
	Ajout_Stage(en,em,st) =
		PRE
			en Î entreprise Ù 
			em Î employe Ù
			em Ïdom(est_signataire) Ù
			{em a en } Í est_affecte Ù
			st Î STAGE Ù
			st Ï dom(est_propose)
		THEN
			stage := stage È {st} ||
			a_pour_responsable := a_pour_responsable È {st a em} ||
			est_propose := est_propose È {st a en}
		END;	
		
	Supp_Stage(st) =
		PRE
			st Î stage
		THEN
			stage := stage - {st} ||
			a_pour_responsable := {st}  a_pour_responsable ||
			est_propose := {st}  est_propose
		END
END