Este artículo presenta un método formal para cuantificar la rejugabilidad y variabilidad de los juegos digitales. El método combina el Modelo Formal Automatizado de Juego Espaciotemporal (FAST GM) – un lenguaje específico de dominio que representa entidades de juego mediante conjuntos finitos de estados, atributos espaciotemporales y transiciones probabilísticas- con un Transductor de Estado Finito de Diversidad de Juego basado en grafos (GD-FST) derivado automáticamente de esa descripción. El soporte de FAST-GM para la lógica lineal-temporal y probabilística permite una verificación rigurosa de los escenarios de juego. El GD-FST resultante se visualiza y edita en el entorno interactivo Tula, que ofrece descomposición jerárquica, simulación simbólica y Monte-Carlo, y cálculo automático de métricas de rejugabilidad. La parte dedicada a la aplicación muestra la aplicación del método a patrones comunes (ciclo roguelike, shooter generado procedimentalmente, película de acción en bucle temporal), lo que confirma la idoneidad del modelo para analizar tanto juegos completos como subsistemas individuales. El artículo también delimita el ámbito práctico de la técnica: el análisis exhaustivo es factible para subsistemas modulares o de un solo jugador en los que intervienen ≈10²-10³ entidades, mientras que los mundos emergentes a gran escala requieren aproximaciones y verificación simbólica. El conjunto de herramientas propuesto combina el rigor de los métodos formales con la claridad de la visualización gráfica, lo que proporciona a los diseñadores de juegos un mecanismo práctico para evaluar y mejorar la rejugabilidad en las primeras fases.