NEW
Font size
WorksheetsLearning Activity-5: The chameleons colony
Total questions: 24
Worksheet time: 12mins
¿Cuántos procedimientos tiene el modelo?
1
2
3
4
¿Cuántos procedimientos activos tiene el modelo?
1
2
3
4
¿Qué ocurre si se encuentran 2 camaleones rojos?
Se convierten en verdes
No ocurre nada
Se convierten en azules
Se dan un besito
¿Qué ocurre si se encuentran un camaleón verde y otro azul?
Se convierten en rojos
Tienen un camaleoncito
Se convierten en azules
Se convierten en verdes
Ejecuta la simulación (con paginación)
$ spin colony.pml | less
¿Se han convertido todos a un mismo color?
Si
No
Podemos asegurar que la extraña colonia de camaleones nunca podrá convertirse a un mismo color.
Si, seguro, libre de peligro
No, no lo podemos asegurar con rotundidad
No sé, dímelo tu
Depende del sexo de los camaleones
#define r !nRed
#define g !nGreen
#define b !nBlue
#define p ((g && b) || (r && g) || (r && b))
A partir del código, ¿cuál es el significado de la fórmula proposicional p?
Hay camaleones de 2 colores
Hay camaleones de 3 colores
Todos los camaleones son de un sólo color
Son de colores indeterminados
#define r !nRed
#define g !nGreen
#define b !nBlue
#define p ((g && b) || (r && g) || (r && b))
¿Cuál de las siguientes propiedades debe cumplirse para asegurar, siempre, el extraño comportamiento de la colonia de camaleones?
<>p
[]p
[]<>p
!<>p
#define r !nRed
#define g !nGreen
#define b !nBlue
#define p ((g && b) || (r && g) || (r && b))
¿Cuál de las siguientes propiedades será el contraejemplo que no debe cumplirse para asegurar, siempre, el extraño comportamiento de la colonia de camaleones?
<>p
[]p
[]<>p
!<>p
Vamos a generar la clausula never a partir de la fórmula proposicional:
$ spin -f '<>p' > ColorChange.ltl
Si, lo he hecho
No, no he podido
#define r !nRed
#define g !nGreen
#define b !nBlue
#define q (r && g && b)
A partir del código, ¿cuál es el significado de la fórmula proposicional q?
La colonia se ha convertido a un sólo color
La colonia se ha extinguido
La colonia se ha escapado
Hay camaleones de 3 colores
#define r !nRed
#define g !nGreen
#define b !nBlue
#define q (r && g && b)
¿Cuál de las siguientes propiedades debe cumplirse para asegurar, siempre, el extraño comportamiento de la colonia de camaleones?
<>q
[]q
[]<>q
!<>q
#define r !nRed
#define g !nGreen
#define b !nBlue
#define q (r && g && b)
¿Cuál de las siguientes propiedades será el contraejemplo que no debe cumplirse para asegurar la no extinción de la colonia?
<>q
[]q
[]<>q
!<>q
Vamos a generar la clausula never a partir de la fórmula proposicional:
$ spin -f '<>q' > Extinction.ltl
Si, lo he hecho
No, no he podido
Vamos a eliminar (dejar de ser activo) el Observer() en el modelo. Para ello, elimina la palabra active y graba.
Si, lo he hecho
No, no he podido
¿Qué método de búsqueda utiliza Spin?
En anchura (breath-first)
En profundidad
(depth-first)
En diagonal (diagonal-first)
Aleatoria (random)
¿Entendido?
Si
No
Vamos a analizar, mediante exploración de estados, la propiedad definida en ColorChange.ltl, para ello, hacemos:
$ spin -a -N ColorChange.ltl colony.pml
$ gcc -o pan pan.c
$ ./pan
¿Podemos asegurar que la colonia mantendrá siempre su extraño comportamiento?
Si, nunca se convertirán a un color
No, se convierten a un sólo color y pierden su atractivo
No se puede saber, hay muchas posibles combinaciones
No lo sabemos, porque depende de la época del año
Y ahora de forma intuitiva, crees que la colonia se puede extinguir alguna vez.
Si, es posible porque mueren alguna vez
No, nunca se extinguirán en este modelo
No se puede saber, hay muchas posibles combinaciones
No lo sabemos, porque depende de la época del año
Vamos a analizar, mediante exploración de estados, la propiedad definida en Extinction.ltl, para ello, hacemos:
$ spin -a -N Extinction.ltl colony.pml
$ gcc -o pan pan.c
$ ./pan
... y ahora, ¿podemos asegurar, con rotundidad, que la colonia nunca se extinguirá?
Efectivamente, nunca se extinguirá
Si que extingue. Todos muertos, una masacre
No se puede saber, hay muchas posibles combinaciones
No lo sabemos, porque depende de la época del año
La Señora Delfina La Fina nos informa que se ha escapado un camaleón verde. Ajusta el modelo.
¿Podemos seguir afirmando que la colonia nunca perderá su atractivo?
$ spin -a -N ColorChange.ltl colony.pml
$ gcc -o pan pan.c
$ ./pan
Si, nunca se convertirán a un color
No, se convierten a un sólo color y pierden su atractivo
No se puede saber, hay muchas posibles combinaciones
No lo sabemos, porque depende de la época del año
¿A qué color habría posibilidad de convertirse todos los camaleones?
Sugerencia: visualizar los últimos pasos de la traza
$ spin -t colony.pml
Rojo
Verde
Azul
Morado
Ajusta el modelo con las nuevas especificaciones (activa fight() y birth()) y vuelve a realizar un análisis de extinción de la colonia.
$ spin -a -N Extinction.ltl colony.pml
$ gcc -o pan pan.c
$ ./pan
... y ahora, ¿podemos asegurar, con rotundidad, que la colonia nunca se extinguirá?
Efectivamente, nunca se extinguirá
Si que extingue. Todos muertos, una masacre
No se puede saber, hemos alcanzado el límite de la profundidad de exploración
No lo sabemos, porque depende de la época del año
Aumenta la profundidad de búsqueda a 108.
$ ./pan -m100000000
... y ahora, ¿podemos asegurar, con rotundidad, que la colonia nunca se extinguirá?
Si, hemos un alcanzado un estado de extinción
Nunca se extingue
No se puede saber, hemos alcanzado el límite de la profundidad de exploración
Se extinguen la mitad
