Ideas para un proyecto TLA +

Question

Por favor, dame algunas sugerencias respecto a un tema en el proyecto TLA + idioma. Estoy tomando un curso sobre el lenguaje, que es el primer año que estoy aprendiendo sobre la especificación y verificación y no tengo ni idea de qué elegir para poner en práctica dentro de dos semanas. Algunas ideas?

Answer 1

proyectos juguete de costumbre con TLA + están en la línea de:

• Modelo un controlador de elevación: el ascensor tiene n puertas, y que tendrá que modelar tanto el comportamiento y las condiciones de seguridad, por ejemplo, que una vez en la parte superior, el ascensor no será más moverse hacia arriba, o que no hay que tener dos puertas abiertas a la vez, y ninguna puerta abierta cuando la cabina no se encuentra en frente de ella, y muchos más.
• tráfico Modelo controlador de luz: para el ejemplo de fácil, un cruce simple, con muchas limitaciones, tales como luces enfrentan están sincronizados, y si uno de los ejes tiene verde, aunque otra ha rojo. Puede refinar la cosa adición de detección del estado del tráfico, y el tiempo.
• Modelo una máquina de lavado: especialmente el armario puerta, y programas sencillos. Demostrar que no hay manera de cerrar la puerta, que es que siempre hay una solución para conseguir su ropa libre (incluso si está mojada) en un tiempo limitado (que tendrá que considerar una etapa de eliminación de agua), sin conseguir demasiada agua en su piso.

En general, los proyectos de juguetes interesantes para TLA + debe combinar un comportamiento relativamente simple, y las condiciones estructurales y de seguridad, de modo que usted será capaz de verificar el comportamiento que ha definido no invalidará las condiciones de seguridad.