Os FTSs no STeP

A tradução que o STeP faz entre os programas SPL e os FTSs segue essencialmente as regras definidas em [6], exceptuando alguns promenores de sintaxe relativos à forma como são escritos os FTSs e o mecanismo de representar a localização do controlo de execução.

A principal diferença entre o mecanismo usado pelo STeP para gerar os FTSs e o método apresentado em [6] consiste na forma como são tratadas as marcas existentes num programa. Enquanto que no método usado nas aulas teóricas o conjunto de marcas do programa é incorporado literalmente no conjunto V das variáveis do FTS, no STeP são geradas variáveis independentes para controlo do estado da execução dos programas. Para cada processo presente numa instrução de cooperação é gerada uma variável chamada pin, onde ndesigna a posição do processo nessa instrução. Por exemplo, para o programa da figura 1.9 seriam geradas as variáveis pi0 para indicar o estado de execução do processo P1 e pi1 para indicar o estado de execução do processo P2. Cada variável pin começa com o valor 0, sendo o seu valor incrementado de uma unidade sempre que o estado da execução avança sequencialmente através do processo. No caso do programa da figura 1.9 a correspondência entre as marcas colocadas pelo programador e o valor das variáveis pin gerado automaticamente pelo STeP é:

l0 $\Leftrightarrow$ pi0=0 $\land$ l1 $\Leftrightarrow$ pi0=1 $\land$ l2 $\Leftrightarrow$ pi0=2 $\land$

m0 $\Leftrightarrow$ pi1=0 $\land$ m1 $\Leftrightarrow$ pi1=1

Esta correspondência é normalmente visualisada na secção Control correspondence quando se importa um programa SPL para o STeP.

A principal razão pela qual o STeP faz esta geração automática de marcas deve-se ao facto de o programador por vezes não colocar marcas num programa ou então colocar marcas redundantes. Atente-se, por exemplo, no seguinte programa:

l1: [l2: skip; l3:]; l4:

Neste exemplo tanto as marcas l1 e l2, como as marcas l3 e l4, correspondem à mesma localização do programa. Quando o STeP gera os valores para pi0 esta redundância é eliminada, sendo gerada a seguinte equivalência:

l1 $\Leftrightarrow$ pi0=0 $\land$ l4 $\Leftrightarrow$ pi0=1

Daqui se poderia supôr que o STeP esqueceu as marcas l2 e l3. No entanto, tal não é verdade, pois se definirmos como objectivo de prova (opção Enter new goal do menu Properties) a propriedade <>l3 e depois simplificarmos (botão Simplify) obtemos a propriedade <>l4 que é equivalente. Assim, quando é gerada a equivalência

l4 $\Leftrightarrow$ pi0=1

deve-se entender que pi0=1 sempre que o programa se encontrar numa das marcas equivalentes a l4.

Se o programa não estiver etiquetado (ou faltarem etiquetas relevantes) aparecem, na secção Control correspondence, algumas marcas geradas automaticamente que o programador pode usar na especificação de propriedades temporais. Por exemplo, se o programa consistir apenas na instrução skip, a correspondência gerada é:

$1 $\Leftrightarrow$ pi0=0 $\land$ $2 $\Leftrightarrow$ pi0=1

Neste caso a mesma propriedade atrás referida poderia ser escrita como <>$2.

A sintaxe utilizada no STeP para descrever um FTS é muito simples:

• A descrição deve começar pela palavra reservada Transition System.
• Depois são declaradas as variáveis flexíveis do conjunto V. Esta secção tem a mesma sintaxe da secção de declarações de um programa SPL, à excepção dos seguintes factos:
  • normalmente não são utilizadas as cláusulas where para fixar restrições nos valores iniciais das variáveis (neste caso tal é feito através da condição inicial $\Phi$);
  • existem mais dois modos com que é possível classificar as variáveis - location quando a variável é uma marca (i.é, pertence ao conjunto M) ou control quando corresponde a uma variável pin gerada pelo STeP.
• A condição inicial $\Phi$ deve ser antecedida pela palavra reservada Initially.
• Depois de definidos V e $\Phi$ falta definir o conjunto J de transições. Cada transição começa por uma linha com a seguinte sintaxe:
  Transition nome requisito de justiça:
  O nome é um identificador qualquer. O requisito de justiça serve para qualificar cada transição quando à terminação, podendo tomar um dos seguintes valores:
  • Just, quando a transição deve obedecer ao requisito de justiça, que impede que uma transição que esteja continuamente activa (i.é, pronta a executar) nunca seja executada;
  • Compassionate, quando a transição deve obedecer a um requisito mais forte que o da Justiça, que indica que qualquer transição que esteja infinitas vezes activa deve também ter oportunidade de executar infinitas vezes;
  • NoFairness, quando não se impõe qualquer requisito de terminação para a transição.
  Depois aparecem separadas por ; as propriedades que correspondem às diversas sub-transições^3.1. Cada propriedade é especificada por uma fórmula de primeira ordem envolvendo variáveis declaradas na secção inicial do FTS e as respectivas versões "linha". Caso se pretenda utilizar estritamente a notação utilizada em [6] deve-se escrever essas propriedades antecedida da palavra reservada modrel. O predicado auxiliar $\overline{U}$ é aqui substituído pela palavra reservada modvar seguida de todas as variáveis contidas em U separadas por virgulas. Por exemplo as transições associadas à instrução while do programa da figura 1.9, descrivas anteriormente como J₀ e J₁ poderiam ser escritas no STeP como:
  
  

  Transition J0J1 Just:
      modrel l0 /\ x /\ !l0' /\  l1'
      modvar l0, l1
  ;
      modrel l0 /\ !x /\ !l0' /\  l2'
      modvar l0, l2
  

  
  
  
  Embora seja possível adoptar este método para descrever o FTS, em [3] aconselha-se o utilizador do STeP a "partir" a propriedade que caracteriza a transição na condição de activação e na condição que especifica a mudança nos valores das variáveis. A primeira deve ser antecedida da palavra reservada enable e a segunda da palavra reservada assign. No entanto a notação utilizada na secção antecedida por assign não é a da lógica de primeira ordem com variáveis "linha", mas sim a sintaxe usual das atribuições. Também não é necessário especificar quais são as únicas variáveis que mudam de valor, pois o STeP deduz esse conjunto automaticamente. Assim, seria preferivel escrever a transição anterior como:
  
  

  Transition J0J1 Just:
      enable     l0 /\ x
      assign     l0:=false, l1:=true
  
  ;
      enable     l0 /\ !x
      assign     l0:=false, l2:=true
  

  
  
  
  De notar que este é o método adoptado pelo STeP na tradução dos programas SPL para FTSs^3.2.

Como exemplo, apresenta-se na figura 3.1 o FTS gerado pelo STeP para o programa da figura 1.9. Note-se que STeP declara uma série de marcas que não são depois usadas na descrição do FTS, pois são utilizadas as equivalentes variáveis pin geradas automaticamente. Para se obter o FTS de um programa usa-se a opção Save transitions do menu File, sendo o FTS gravado num ficheiro à escolha. Também poderia ser usada a opção View transitions, mas esta usa uma sintaxe um pouco mais elaborada pois baseia-se na especificação modular de FTSs.

  

Figure 3.1: FTS do programa apresentado na figura 1.9

Transition System

out      y : int
local    x : bool
location $4 : bool
location $3 : bool
location m1 : bool
location m0 : bool
location $2 : bool
location l2 : bool
location l1 : bool
location l0 : bool
location $1 : bool
control  pi0 : [0..2]
control  pi1 : [0..1]
Initially (x = true /\ y = 0) /\ pi0 = 0 /\ pi1 = 0
Transition m0 Just:
    enable     pi1 = 0
    assign     pi1 := 1,x := false


Transition l0 Just:
    enable     pi0 = 0 /\ x
    assign     pi0 := 1

;
    enable     pi0 = 0 /\ ~x
    assign     pi0 := 2


Transition l1 Just:
    enable     pi0 = 1
    assign     pi0 := 0,y := y + 1

Note-se que, em vez de um programa escrito em SPL, é possível fornecer ao STeP o mesmo programa descrito como um FTS. Para tal, escreve-se num ficheiro de texto o FTS na notação acima apresentada, e depois usa-se a opção Load transitions do menu File para o "carregar" para o STeP.