# ACLARACIÓN

parece que la web unsparciales renombra los archivos, asi que este es el codigo para que no se confundan.
El archivo AtomosProyecto y BasicoProyecto eran muy parecidos, así que los dejo plasmado acá en texto también.
Nota: El BasicoProyecto.als sí genera instancias, no es un bug. Recuerden ajustar el scope



AtomosProyecto.als

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
}

$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$

EstadosProyecto.als es esto:

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
	)
}


$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$$

Por ultimo, BasicoProyecto.als es esto


sig Id { }

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

abstract sig Empleado { }

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


/** ------------------------------------------------------------------------------------------------------------------------------------------------------ **/
/** ----No quitar ni comentar -----------------------------------------------------------------------------------------------------------------**/
-- facts destinado a obtener instancias con mas de dos proyectos y empleados
fact{#Proyecto > 2}
fact{#Empleado > 2}
-- facts destinados a establecer la capacidad del colectivo

fact{all p:Proyecto | #p.equipo < 12}

/** --------------------------------------------------------------------------------------------------------------------------------------------------- **/

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

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

fact{Permanente = Gerente+Desarrollador}



run {} for 4