Ejemplos

Uno de los problemas clásicos que de prueban en este tipo de sistemas es el de los filósofos pensantes. En la figura 5.4

  

Figure 5.4: Modelado del problema de los filósofos pensantes en PetrA

Los filósofos se modelan con dos estados: pensando p_i y comiendo c_i. Los lugares etiquetados con t₁, t₂, t₃, t₄ y t₅ representan los tenedores que comparten. Cuando se cambia de estado pensando a comiendo, se verifica que se tengan ambos tenedores y se procede a hacer el cambio. Si la transición que va a realizar el cambio no cuenta con tokens en los lugares que representan a los tenedores, entonces no se puede cambiar de estado y el filósofo sigue pensando. Si un filósofo está en estado comiendo y va a pasar al estado pensando, debe regresar los tenedores (colocar tokens en los lugares que representan a los tenedores) y se pasa al estado pensando.