3.3 Clausulas proporcionadas
Normalmente, la ejecución del proceso solo se guía por las reglas de sincronización capturadas en la semántica de las declaraciones de las especificaciones de proctype. Sin embargo, es posible definir restricciones globales adicionales en las ejecuciones de procesos. Esto se puede hacer con la ayuda de la palabra clave proporcionada que puede seguir la lista de parámetros de una declaración de proctype, como se ilustra en el siguiente ejemplo:
Esta es una traducción del libro SPIN model checker
Las cláusulas provistas utilizadas en este ejemplo fuerzan las ejecuciones del proceso para alternar, produciendo un flujo infinito de salida:
Un proceso no puede dar ningún paso a menos que su clausula proporcionada se evalúe como verdadera. Una cláusula proporcionada ausente se establece de manera predeterminada en la expresión verdadero, sin imponer restricciones adicionales en la ejecución del proceso. Las clausulas proporcionadas se pueden usar para implementar algoritmos de programación de procesos no estándar. Sin embargo, esta característica puede llevar una etiqueta de precio en la verificación del sistema. El uso de las clausulas provistas puede desactivar algunos de los algoritmos de optimización de búsqueda más potentes de SPIN (consulte el Capítulo 9).
3.4 Objetos de datos
Solo hay dos niveles de alcance en los modelos PROMELA: global y proceso local. Naturalmente, dentro de cada nivel de alcance, todos los objetos deben declararse antes de que puedan ser referenciados. Debido a que no hay niveles intermedios de alcance, el alcance de una variable global no se puede restringir a solo un subconjunto de procesos, y el alcance de una variable local de proceso no se puede restringir a bloques específicos de instrucciones. Se puede hacer referencia a una variable local desde su punto de declaración hasta el final del cuerpo de proctype en el que aparece, incluso cuando aparece en un bloque anidado (es decir, un fragmento de código encerrado en llaves). Esto se ilustra con el siguiente ejemplo:
Cuando se simula este modelo, produce la siguiente salida.
El tipo de datos sin signo, al igual que su contraparte en el lenguaje de programación C, se puede usar para declarar una cantidad que se almacena en un número definido por el usuario de bits n, con 1 ≤ n ≤ 32. Con solo dos excepciones, estos tipos de datos pueden almacenar solo valores sin signo. Las dos excepciones son short e int, que pueden contener valores positivos o negativos. Los rangos de valores precisos de los diversos tipos dependen de la implementación. Para abreviar, int y unsigned, el rango efectivo coincide con los del mismo tipo en los programas C cuando se compilan en el mismo hardware. Para byte, chan, mtype y pid, el rango coincide con el del tipo unsigned char en los programas C. Los rangos de valores para bit y bool siempre están restringidos a dos valores.
Las declaraciones típicas de variables de estos tipos básicos incluyen:
Solo se admiten matrices unidimensionales de variables, aunque existen formas indirectas de definir matrices multidimensionales mediante el uso de definiciones de estructura, como veremos en breve. Todas las variables, incluidas las matrices, se inicializan por defecto a cero, independientemente de si son globales o locales para un proceso. Las variables siempre tienen un rango estrictamente limitado de valores posibles. La variable w en el último ejemplo, por ejemplo, solo puede contener valores que pueden almacenarse en tres bits de memoria: de cero a siete. Una variable de tipo short, de manera similar solo puede contener valores que se pueden almacenar en dieciséis bits de memoria. En general, si se asigna un valor a una variable que se encuentra fuera de su dominio declarado, el valor asignado se trunca automáticamente. Por ejemplo, la asignación: byte a = 300; da como resultado la asignación del valor 44 (300 % 256). Cuando dicha asignación se realiza durante simulaciones aleatorias o guiadas, SPIN imprime un mensaje de error para alertar al usuario sobre el truncamiento. La advertencia no se genera durante las ejecuciones de verificación, para evitar la generación de grandes volúmenes de salida repetitiva. Como de costumbre, múltiples variables del mismo tipo se pueden agrupar detrás de un solo nombre de tipo, como en: byte a, b[3] = 1, c = 4;
En este caso, la variable llamada a es, por defecto, inicializada a cero; todos los elementos del conjunto b se inicializan en uno, y la variable c se inicializa en el valor cuatro. Las variables del tipo mtype pueden contener valores simbólicos que se deben introducir con una o más declaraciones mtype. Una declaración mtype generalmente se coloca al comienzo de la especificación, y simplemente enumera los nombres, por ejemplo de la siguiente manera:
Por supuesto, ninguno de los nombres especificados en una declaración mtype puede coincidir con palabras reservadas de PROMELA, como init o short. Como se muestra aquí, hay un printm de rutina de impresión especial predefinido que se puede usar para imprimir el nombre simbólico de un mtype variable. Puede haber múltiples declaraciones de tipo en un modelo, pero distintas declaraciones no declaran tipos distintos. El último modelo, por ejemplo, es indistinguible de SPIN de un modelo con una sola declaración de tipo, que contiene la concatenación (en orden inverso) de las dos listas, como en:
Debido al rango de valores restringidos del tipo subyacente, no se pueden declarar más de 255 nombres simbólicos en todas las declaraciones de tipo combinado. El analizador SPIN marca un error si se excede este límite.
3.5 Estructuras de datos
PROMELA tiene un mecanismo simple para introducir nuevos tipos de estructuras de registro de variables. El siguiente ejemplo declara dos de esas estructuras y las usa para pasar un conjunto de datos de un proceso a otro en una operación única e indivisible:
Hemos definido dos nuevos tipos de datos llamados Field y Record, respectivamente. La variable local goo en el proceso init se declara de tipo Record. Como antes, todos los campos en los nuevos tipos de datos que no se inicializan explícita mente (por ejemplo, todos los campos excepto f en las variables de tipo Field) se inicializan por defecto a cero. Las referencias a los elementos de una estructura se escriben en notación de puntos, como por ejemplo:
Una variable de un tipo definido por el usuario se puede pasar como un único argumento a un nuevo proceso en las instrucciones de ejecución, como se muestra en el ejemplo, siempre que no contenga arreglos. Entonces, en este caso, es válido pasar la variable llamada foo como parámetro al operador run, pero al usar goo se desencadenaría un mensaje de error de SPIN sobre los arreglos ocultos. En la siguiente sección veremos que estos nombres de tipo de estructura también se pueden usar como un declarador de campo en declaraciones de canales.
El mecanismo para introducir tipos definidos por el usuario permite una forma indirecta de declarar arrays multidimensionales, aunque PROMELA solo admite arreglos unidimensionales como objetos de primera clase. Se puede crear una matriz bidimensional, por ejemplo, de la siguiente manera:
Esto crea una estructura de datos de dieciséis elementos, que ahora puede ser referenciado como un a[i] .el [j]. Como en C, los índices de un arreglo de N elementos van desde cero hasta N-1.
Esta es una traducción del libro SPIN model checker
