Tarea 9 - Modelado de sistemas de transiciones

Para esta entrada se nos asignó analizar los ejemplos 2.29, 2.30 y 2.32 del libro Principles of model checking, para después modelar un ejemplo similar propio a manera de sistema de transiciones o de grafo de un programa (dependiendo cuál sea más conveniente).

Como sistema a modelar se me ocurrió una tortillería.

Los componentes que integran una tortillería son:

• Mano de obra, encargada de poner el maíz dentro del molino, de trasladar la masa resultante a la banda de cocción y finalmente de empaquetar el producto.
• Molino, encargado de moler el maíz para convertirlo en masa.
• Banda de cocción, una vez salida la masa del molino, ésta pasa a través de una banda donde es cortada en forma tradicional y posteriormente cocida.

Posteriormente realicé los siguientes diagramas de estado y de acción para cada componente.

En lo concerniente a la mano de obra.

• Estados:
• Inicio.
• Espera. 
• Traslado.
• Acciones:
• Llenado contenedor del molino.
• Recolección de masa una vez que haya salido del molino.
• Traslada masa a banda de cocción.

(Nota. Una vez que traslada la masa a la banda, regresa a esperar que salga más masa del molino o si éste ya está vacío lo vuelve a llenar)

En lo concerniente al molino.

• Estados:
• Ocupado.
• Libre.
• Acciones:
• Moliendo maíz.
• Esperando por más maíz o en estado de standby.

En lo concerniente a la banda de cocción.

• Estados:
• Procesando.
• Repetición.
• Finalización.
• Acciones:
• Moldeado y cocción.
• Repetición proceso de producción, volver al inicio del sistema.
• Fin proceso de producción.

Ya para el diagrama del sistema final abrevié tanto estados como acciones de la siguiente manera:

Mano de obra: (Inicio, Espera, Traslado) = (E0, E1, E2)

                         (Llenado, Recolección, Traslado)=(A0, A1, A2)

Molino: (Libre, Ocupado) = (0, 1)

              (Moliendo, Esperando) = (M,W)

Banda de cocción: (Procesar, Repetición, Finalización) = (P, R, T)

                              (Moldeado y cocción, Repetir proceso) = (C, Rp)

Y finalmente aquí está el esquema final:

Fuentes de Consulta

Principles of Model Checking