Dos asignaturas que se exigen entre sí
Alloy es un lenguaje para describir cosas y las relaciones entre ellas, y una herramienta que busca un ejemplo pequeño que rompa una afirmación. Cuando lo encuentra, ese ejemplo es el contraejemplo.
Una universidad guarda qué asignatura es previa de cuál. Nadie quiere un plan donde Álgebra exige Cálculo y Cálculo exige Álgebra: nadie podría matricularse. La regla "ninguna asignatura es previa de sí misma" no basta para evitarlo.
Al final de esta lección
Nota
Puedo leer un contraejemplo de Alloy y decir qué regla falta en el modelo.
Palabras clave
| Palabra | Qué significa | Ejemplo |
|---|---|---|
| Conjunto | un tipo de cosas del modelo | Course |
| Relación | los enlaces entre cosas, escritos como pares | prereq |
| Hecho | una regla que el modelo siempre cumple | |
| Afirmación | algo que Alloy comprueba sin imponerlo | |
| Instancia | un ejemplo concreto de cosas y enlaces que cumple las reglas | |
| Alcance | el tamaño máximo de cada conjunto que Alloy prueba | for 4 |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Un modelo son conjuntos y relaciones
En Alloy dices qué tipos de cosas hay, los conjuntos, y cómo se enlazan, las relaciones. Aquí hay asignaturas, y la relación prereq enlaza cada una con sus previas.
Una relación es una lista de pares. Que Algoritmos tenga como previa Programación es el par Algoritmos -> Programación.
Ejemplo: la relación prereq como pares
| Par | Se lee |
|---|---|
| Algoritmos -> Programación | Programación es previa de Algoritmos |
| Programación -> Matemáticas | Matemáticas es previa de Programación |
| Matemáticas -> Algoritmos | Algoritmos es previa de Matemáticas |
| c.prereq | las previas directas de c |
| c.^prereq | las previas directas e indirectas de c |
Las celdas que rellenan los estudiantes quedan en blanco en esta vista previa.
Un hecho se impone, una afirmación se comprueba
Un hecho es una regla que Alloy da por cierta en todos los ejemplos que busca. Una afirmación es algo que quieres saber si se sigue de los hechos.
Con check le pides un contraejemplo de la afirmación. Con run, un ejemplo cualquiera que cumpla las reglas. El alcance limita cuántas cosas prueba.
El modelo de las asignaturas previas
sig Course { prereq: set Course } // cada asignatura tiene un conjunto de previas
fact noSelfPrereq { no c: Course | c in c.prereq } // ninguna es previa de sí misma
assert NoCycles { no c: Course | c in c.^prereq } // ninguna lo es, ni de forma indirecta
check NoCycles for 4 // busca un contraejemplo de hasta 4 asignaturas
run HasPrereqs { some prereq } for 3 // pide un ejemplo con alguna previaCrea una carpeta para el modelo
mkdir -p ~/coursesSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Escribe el modelo en un archivo
printf '%s\n' 'sig Course { prereq: set Course }' '' 'fact noSelfPrereq { no c: Course | c in c.prereq }' '' 'assert NoCycles { no c: Course | c in c.^prereq }' 'check NoCycles for 4' '' 'run HasPrereqs { some prereq } for 3' > ~/courses/plan.alsSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Mira qué contestó Alloy a cada orden
alloy ~/courses/plan.als | grep -oE 'UNSAT|SAT'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Lee las dos instancias que encontró
alloy ~/courses/plan.als | grep -E 'instance|prereq='Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Cómo se lee un contraejemplo
Alloy llama Course$0 y Course$1 a las dos asignaturas del ejemplo. No tienen nombre propio: son cualquier par de asignaturas que se comporte así.
En el contraejemplo, cada una es previa de la otra. Como la regla del modelo solo prohíbe que una lo sea de sí misma, un ciclo de dos pasa. La herramienta de la máquina lo imprime como texto; la aplicación gráfica de Alloy lo dibuja con flechas.
Un error frecuente
Advertencia
Mucha gente cree que SAT en un check es una buena noticia. Es al revés. En un check, SAT significa que Alloy encontró un contraejemplo. Lo que quieres ver es UNSAT: no hay ninguno dentro del alcance.
Añade una regla que prohíba los ciclos
printf '%s\n' 'fact noCycles { no c: Course | c in c.^prereq }' >> ~/courses/plan.alsSe muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
Vuelve a comprobar el modelo
alloy ~/courses/plan.als | grep -oE 'UNSAT|SAT'Se muestra aquí y no se ejecuta. Crea una cuenta gratuita para pulsar Ejecutar y escribirlo en el terminal de tu propio laboratorio.
UNSAT vale dentro del alcance
Ahora el check da UNSAT, y el run sigue dando SAT. El run importa: si también diera UNSAT, el modelo sería tan estricto que no admitiría ningún plan.
Pero for 4 quiere decir que Alloy solo miró hasta cuatro asignaturas. Es muy buena señal, porque casi todos los fallos aparecen con pocas cosas, pero no es una demostración para cualquier tamaño.