sig Id { }

sig Proyecto {
    idProyecto: Id,
    idSucursal: Id,
    equipo: set Empleado
}

abstract sig Empleado { }

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

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

/** ------------------------------------------------------------------------------------------------------------------------------------------------------ **/
/** ----No quitar ni comentar: fact destinado a obtener instancias con mas de dos colectivos y pasajeros--- **/
fact{#Proyecto > 2}
fact{#Empleado > 2}
/** --------------------------------------------------------------------------------------------------------------------------------------------------- **/

fact{  (Proyecto.idProyecto& Proyecto.idSucursal) = none}
fact{Permanente = Gerente+Desarrollador}

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


pred asignarEmpleado[p1,p2:Proyecto, e:Empleado]{
	(
		(
			e in Permanente and
			e !in p1.equipo and
			p2.equipo = p1.equipo + e
		) or
			(
			e in Contratista and
			e !in p1.equipo and
	 		e.supervisor !in p1.equipo and
			p2.equipo = p1.equipo + e 
		)
	) 	and
-- invariantes
	p2.idProyecto = p1.idProyecto
}


// exitos :)
// atte: Jorge