Artículo.
característica de retroceso del corrector de modelos garantiza que, finalmente, se prueben todos los valores posibles. La Figura 7 muestra el caso cuando la variable es de un tipo de enumeración, que se traduce a la declaración de selección de Promela. Concepto de asignación aleatoria. En muchos