open util/ordering[Estado] as ord

sig Id { }

one sig Proyecto {
    idProyecto: Id,
    idSucursal: Id,
}

sig Empleado { }

sig Permanente extends Empleado { }
sig Gerente, Desarrollador extends Permanente { }
sig Contratista extends Empleado {    supervisor: Gerente }

sig Estado {
	equipo: set Empleado		
}

/** ----------------------- restricciones generales ---------------------------------- **/


fact{  (Proyecto.idProyecto& Proyecto.idSucursal) = none}

fact{no disj p1,p2: Proyecto | p1.idProyecto = p2.idProyecto}

fact{Permanente = Gerente+Desarrollador}


fact { all e:Estado | #(e.equipo&Contratista) <= #(e.equipo&Permanente)}



/** --------------------------- dinamica ----------------------------- **/


fact traces{ 
	inicializar[ord/first] and
	 all e: Estado-ord/last |
		let es= e.next |
			( some em:Empleado |
				asignarAlproy[e,es,em] or 
			  	quitarDelProy[e,es,em] 
			)
}

/** --------------------------- predicados de cambio ----------------------------- **/

pred inicializar[e:Estado] { e.equipo = none}

pred asignarAlproy[e1,e2:Estado, e:Empleado]{
	(
		e in Permanente and
		e !in e1.equipo and
		e2.equipo = e1.equipo + e 
	) or (
		e in Contratista and
		e !in e1.equipo and
		e.supervisor in e1.equipo and 
		e2.equipo = e1.equipo + e
	) 
}

pred quitarDelProy[e1,e2:Estado, e:Empleado]{
	(
		e in Permanente and
		e in e1.equipo and
		no (e1.equipo)&(supervisor.e) and 
		e2.equipo = e1.equipo - e 
	) or (
		e in Contratista and
		e in e1.equipo and
		e2.equipo = e1.equipo - e
	)
}