A notação usada nas aulas teóricas

Em [6] um FTS é descrito pelo triplo

$$<V, \Phi, J>$$

onde:

• V representa o conjunto de variáveis flexíveis, que inclui as variáveis usadas no programa e todas as marcas que servem para indicar onde se encontra o controlo de execução;
• $\Phi$ é uma proposição em lógica de primeira ordem que indica a condição que se deve verificar no início do programa; e
• J é um conjunto finito de transições, sendo cada transição descrita uma fórmula em lógica de primeira ordem que indica as condições em que a transição está activa e as alterações que se verificam em todas as variáveis quando a transição é executada.

Nas fórmulas que descrevem as transições, quando se pretende designar o valor duma variável no estado seguinte da execução utiliza-se uma variante "linha" dessa variável. Por exemplo, se pretendermos dizer que, após executada uma transição, o valor de uma variável x será igual ao seu valor actual mais um, escrevemos x'=x+1. A partir da proposição que descreve uma transição facilmente se obtem a condição que indica se a transição está ou não activa. Para isso basta substituir todas as variáveis linha da fórmula por uma variável rígida quantificada existencialmente. Para o caso de x'=x+1 teríamos $\exists a \cdot a = x+1$.

Depois de descrita a noção de FTS é apresentada em [6] a semântica do SPL utilizando este modelo computacional. O conjunto Vde variáveis é igual ao conjunto X de variáveis declaradas no programa mais o conjunto M de todas as marcas nele presentes. Para simplificar assume-se que todas as instruções estão etiquetadas com uma pré-localização e uma pós-localização. Assumindo que $\varphi$sintetiza, através de uma conjunção, todas as proposições presentes nas cláusulas where das declarações e que $I \subseteq M$ é o conjunto das marcas inicialmente activas no programa, então a condição inicial $\Phi$ é definida como:

$$\Phi \doteq \varphi \land \bigwedge_{l \in I} l \land \bigwedge_{m \in M \backslash I} \lnot m$$

Para cada instrução do SPL é apresentada em [6] a propriedade que corresponde à respectiva transição (ou transições) num FTS e a respectiva condição de activação. Devido à necessidade frequente de se indicar que apenas um pequeno conjunto de variáveis altera o seu valor, definiu-se o predicado auxiliar

$$\overline{U} \doteq \bigwedge_{y \in V \backslash U} (y'=y)$$

onde $U \subseteq V$ representa o conjunto de variáveis que altera o seu valor. As regras de tradução das instruções SPL para as respectivas propriedades e condições de activação são apresentadas na tabela 3.1. Nessa tabela $\alpha$ representa um canal assíncrono (sendo $L_\alpha$ o seu comprimento máximo) e $\beta$ um canal síncrono.

 

Table 3.1: Tradução das instruções SPL para transições nos FTSs

Instrução	Propriedade de transição	Activação
l: skip; m:	$l \land \lnot l' \land m' \land \overline{\{l,m\}}$	l
l: x:=e; m:	$(x'=e) \land l \land \lnot l' \land m' \land \overline{\{x,l,m\}}$	$\exists a \cdot (a=e) \land l$
l: $\alpha$<==e; m:	$(\alpha'=\alpha \cdot <e>) \land (\vert\alpha\vert < L_\alpha) \land l \land \lnot l' \land m' \land \overline{\{\alpha,l,m\}}$	$\exists a \cdot (a=e) \land l \land (\vert\alpha\vert < L_\alpha)$
l: $\alpha$==>u; m:	$(\alpha=<u'> \cdot \alpha') \land (\vert\alpha\vert > 0) \land l \land \lnot l' \land m' \land \overline{\{\alpha,l,m,u\}}$	$l \land (\vert\alpha\vert > 0)$
l: $\beta$<==e; m: e k: $\beta$==>u; n:	$(u'=e) \land l \land \lnot l' \land m' \land k \land \lnot k' \land n' \land \overline{\{u,l,m,k,n\}}$	$\exists a \cdot (a=e) \land l \land k$
...	...	...

 

Para exemplificar a tradução de um programa SPL num sistema de transição de acordo com estas regras, considere, mais uma vez, o programa apresentado na figura 1.9. Neste exemplo, o conjunto das variáveis do FTS é:

$$V = \{x,y,l0,l1,l2,m0,m1\}$$

A condição inicial é:

$$\Phi = x \land (y=0) \land l0 \land m0 \land \lnot l1 \land \lnot l2 \land \lnot m1$$

Finalmente, o conjunto de transições é definido como

$$J = \{J_0, J_1, J_2, J_3\}$$

onde

$$J_0 = l0 \land x \land \lnot l0' \land l1' \land \overline{\{l0,l1\}}$$

$$J_1 = l0 \land \lnot x \land \lnot l0' \land l2' \land \overline{\{l0,l2\}}$$

$$J_2 = l1 \land (y'=y+1) \land \lnot l1' \land l0' \land \overline{\{l1,l0,y\}}$$

$$J_3 = m0 \land \lnot x' \land \lnot m0' \land m1' \land \overline{\{m0,m1,x\}}$$