Documentación y notas en Google Drive: https://docs.google.com/document/d/1s6xhIhSwTMZRl8EF4BMsqzO30vXrgwcxHdB_JVnJBms/edit?usp=sharing
- light.pml - Modelo para verificación formal, incluye especificación LTL
- light.c - Implementación en C del comportamiento de la luz
- button.c - Implementación en C del comportamiento de un pulsador