[VVS] 9. Modelado de Sistemas Concurrentes

La tarea consistió en elegir un sistema y modelarlo de 2 posibles maneras, ya sea mediante un sistema de transiciones o mediante un grafo de programa, elegí el sistema de transiciones.

El sistema que elegí fue una minimización de un restaurante de comida rápida.

Componentes:

• Cajero: Es el encargado de tomar las ordenes y pasarlas a la cocina para posteriormente cobrar el monto total del pedido.
• Cocina: Recibe las ordenes del cajero y se encarga de preparar el pedido, posteriormente sirve los platos para su posterior entrega.
• Ayudante: Se encarga de recibir los pedidos preparados por la cocina y los entrega al cliente, cerrando así el ciclo.

Siguiendo la nomenclatura del libro, el sistema completo queda definido por los componentes:

Modelado y descripción formal de los componentes:

Componente	Descripción	Modelado
Cajero	Estados {0} Espera {1} Orden recibida {2} Orden cobrada Acciones {Rec} Recibir la orden {Cob} Cobrar la orden {Pas} Pasar la orden a cocina
Cocina	Estados {0} Espera {1} Orden recibida {2} Orden preparada Acciones {Pas} Pasar orden (recibirla del cajero) {Pre} Preparar la orden {Ser} Servir la orden
Ayudante	Estados {0} Espera {1} Orden entregada Acciones {Ser} Servir la orden (Recibida de la cocina) {Ent} Entregar la orden al cliente

Diagrama de Transiciones

El sistema que elegí es altamente concurrente, es común que en un restaurante veamos a todo el equipo trabajando al mismo tiempo, por ejemplo, el cajero puede estar recibiendo ordenes constantemente y enviarlas a la cocina, no espera a que la cocina termine las ordenes, así mismo el ayudante quien constantemente entrega ordenes mientras el cajero y la cocina trabajan.

Es por ello que encontré múltiples caminos a diversos estados, pero se puede notar un miniloop con los estados {000} → {100} → {200} → {010} → {020} → {001} que indican el camino de la transición si el sistema no fuera concurrente

Referencias:

• [Libro] Principles of Model Checking - Christer Baier & Joost-Pieter Katoen