lunes, 29 de octubre de 2012

[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

1 comentario: