Tarea 9: Grafo de programa

Para esta entrada de verificación voy a hacer un sistema en donde podamos modelar en base al reciclaje del papel, por lo que podemos decir que  el sistema consta de los siguientes procesos.

• Recolectar papel y Clasificar el papel(Recolección)
• Se moja y se bate para crear pasta (Creación_pasta)
• Se limpia la pasta de pegamento, tintes, etc. (Limpieza)
• Se moldea en superficia plana. (Molde_pasta)
• Secado y enrollado de hoja. (Generar_papel)

Entonces, podemos tener un sistema en donde por ejemplo, ya tenmos papel previamente limpiado, o ya tenemos la pasta, y se pueden automatizar los procesos ya que según el estado en el que tengamos el papel, vamos a utilizar las herramientas que tengamos, por lo que considero que estos serian los procesos fundamentales en donde los procesos tienen solamente dos estados llamados 0 y 1.

Ahora, en base a estos procedimiento, voy a crear el sistema en base al estado del papel en donde según el estado, vamos a crear las transiciones del sistema dado el siguiente diagrama.

En donde el sistema global inicial es 0000, pero para poder iniciar el ciclo necesitamos por lo menos tener papel, por lo que pongo como estado global el tener papel recolectado 1000.

Bibliografia.
Principles of Model Cheking, Baier & Katoen,