Sistema de transiciones

Para esta semana en la clase de verificación nos fue encargada como tarea elegir o inventar un sistema y después modelarlo como un sistema de transiciones para crear un grafo del mismo. Sin mas el sistema de mi elección fue el siguiente:


Una partida de Póquer 
Bueno como todos sabemos el póquer es un juego muy conocido de apuestas, donde se juega con 52 cartas, donde al inició del juego a cada jugador se le asignan cinco cartas de las cuales durante el juego se le da la oportunidad de cambiar cualquier cantidad de ellas por otra del mazo de baraja y después se comparan las cartas de todos y se decide quien es el ganador.

En mi caso sera una partida entre dos jugadores y habrá un  tercer participante que servirá como juez a final del juego y sera quien reparta las cartas y haga cambios en las mismas, a este ente le llamaremos "Mazo" por que es el responsable del mazo de cartas.

Ahora mostrare las diferentes transiciones entre los componentes del sistema, de el lado izquierdo de el símbolo ":" pongo la transición y del lado derecho el estado al que lleva esta.

Jugadores:

• Recibir cartas : Pensando jugada, al cual llamaremos A.
• Cambiar cartas : Esperando oponente, al cual llamaremos B .
• Abrir mano o enseñar cartas : Esperando ganador, al cual llamaremos C.

Mazo:

1. Repartir cartas : Estado 2.
2. Cambiar cartas : Estado 3.
3. Elegir ganador : Estado 4.
4. Barajar cartas : Estado 1.

 El circulo denota el estado y la flecha la transición para llegar a dicho estado el primer estado es el cual tiene una flecha curvada que no tiene origen en ningún lugar.

 Una vez hecho esto no es posible mas fácilmente representar el sistema completo modelando las interacciones entre cada uno de los componentes. la notación "(A,A,1)" indica el estado actual y las flechas indican la transición para llegar a dicho estado.

Referencias:
http://is.ifmo.ru/books/_principles_of_model_checking.pdf